mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableOn.smul_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {f : B → 𝕜}
  {s : (x : B) → E x} {u : Set B}, MDiff[u] f → MDiff[u] (T% s) → MDiff[u] fun x => ⟨x, (f • s) x⟩
-- Lean.Parser.Command
Lean.Parser.Command.assertNotImported.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.disjoint_span_singleton_of_notMem : ∀ {K : Type u_3} {V : Type u_6} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {s : Submodule K V} {x : V}, x ∉ s → Disjoint s (K ∙ x)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_biUnion_finset : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset ι} {f : ι → Set α},
  (↑s).PairwiseDisjoint f → (∀ b ∈ s, MeasurableSet (f b)) → μ (⋃ b ∈ s, f b) = ∑ p ∈ s, μ (f p)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coeFnAlgHom_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {N : Type u_6}
  [inst_4 : TopologicalSpace N] [inst_5 : ChartedSpace H N] {n : WithTop ℕ∞} {A : Type u_10} [inst_6 : NormedRing A]
  [inst_7 : NormedAlgebra 𝕜 A] [inst_8 : ContMDiffRing (modelWithCornersSelf 𝕜 A) n A]
  (a : ContMDiffMap I (modelWithCornersSelf 𝕜 A) N A n) (a_1 : N), ContMDiffMap.coeFnAlgHom a a_1 = a a_1
-- Init.Data.Range.Polymorphic.Iterators
/-- Internal function that constructs an iterator for a left-unbounded right-open range `*...hi`.
This is an internal function.
Use `Rio.iter` instead, which requires
importing `Std.Data.Iterators`.
 -/
Std.Rio.Internal.iter : {α : Type u} → [Std.PRange.UpwardEnumerable α] → [Std.PRange.Least? α] → Std.Rio α → Std.Iter α
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_add_of_nonempty : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s t : Set E},
  s.Nonempty →
    t.Nonempty → (Bornology.IsVonNBounded 𝕜 (s + t) ↔ Bornology.IsVonNBounded 𝕜 s ∧ Bornology.IsVonNBounded 𝕜 t)
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.stabilizerEquivStabilizer_symm : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g : G} {a b : α} (hg : b = g • a),
  (MulAction.stabilizerEquivStabilizer hg).symm = MulAction.stabilizerEquivStabilizer ⋯
-- Mathlib.RingTheory.Nilpotent.Basic
Prime.isRadical : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {y : R}, Prime y → IsRadical y
-- Lean.Meta.SynthInstance
/-- Return `LOption.some r` if succeeded, `LOption.none` if it failed, and `LOption.undef` if
instance cannot be synthesized right now because `type` contains metavariables.  -/
Lean.Meta.trySynthInstance : Lean.Expr → optParam (Option ℕ) none → Lean.MetaM (Lean.LOption Lean.Expr)
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.default_def : ∀ (V : Type u_3), default = ⊥
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.lift.isLift_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (X : C),
  (CategoryTheory.Quotient.lift.isLift r F H).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.Prod.toSigma : {α : Type u} → {β : Type v} → α × β → (_ : α) × β
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.eulerMascheroniSeq_zero : Real.eulerMascheroniSeq 0 = 0
-- Mathlib.Order.Max
IsBot.snd : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsBot x → IsBot x.2
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- If a linear map is surjective, then the map it induces on exterior powers is surjective.  -/
exteriorPower.map_surjective : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N},
  Function.Surjective ⇑f → Function.Surjective ⇑(exteriorPower.map n f)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.integral_abs_condExp_le : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E]
  [IsOrderedModule ℝ E] (f : α → E), ∫ (x : α), |μ[f | m] x| ∂μ ≤ ∫ (x : α), |f x| ∂μ
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.getElem?_toList_eq : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {r : Std.Rco α} {i : ℕ},
  r.toList[i]? = Option.filter (fun x => decide (x < r.upper)) (Std.PRange.succMany? i r.lower)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.Parallel.equivalence : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P], Equivalence AffineSubspace.Parallel
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.goto.sizeOf_spec : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : SizeOf K] [inst_1 : (a : K) → SizeOf (Γ a)]
  [inst_2 : SizeOf Λ] [inst_3 : SizeOf σ] (a : σ → Λ), sizeOf (Turing.TM2.Stmt.goto a) = 1
-- Mathlib.Order.RelClasses
/-- Set notation form of `ne_of_gt` -/
ne_of_ssuperset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, b ⊂ a → a ≠ b
-- Mathlib.Algebra.Group.Defs
SubNegZeroMonoid.toNegZeroClass : {G : Type u_2} → [self : SubNegZeroMonoid G] → NegZeroClass G
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
_private.Mathlib.Algebra.SkewMonoidAlgebra.Basic.0.SkewMonoidAlgebra.add : {k : Type u_1} →
  {G : Type u_2} → [inst : AddMonoid k] → SkewMonoidAlgebra k G → SkewMonoidAlgebra k G → SkewMonoidAlgebra k G
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_insertIfNew_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).size ≤ t.size + 1
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
_private.Mathlib.AlgebraicGeometry.Morphisms.FlatRank.0.AlgebraicGeometry.IsAffine.finrank.congr_simp : ∀ {X S : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine S] (f f_1 : X ⟶ S),
  f = f_1 →
    ∀ (s s_1 : ↥S), s = s_1 → AlgebraicGeometry.IsAffine.finrank✝ f s = AlgebraicGeometry.IsAffine.finrank✝ f_1 s_1
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.support_pow : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MonoidWithZero M₀] [IsReduced M₀] {n : ℕ} (f : ι → M₀),
  n ≠ 0 → (Function.support fun a => f a ^ n) = Function.support f
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.reorderPart : Lean.ParserDescr
-- Mathlib.Algebra.Ring.Basic
/-- The left multiplication map: `(a, b) ↦ a * b`. See also `AddMonoidHom.mulLeft`.  -/
AddMonoid.End.mulLeft : {R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → R →+ AddMonoid.End R
-- Init.Data.ByteArray.Basic
/-- An efficient implementation of `ForIn.forIn` for `ByteArray` that uses `USize`
rather than `Nat` for indices.

We claim this unsafe implementation is correct because an array cannot have more than
`USize.size` elements in our runtime. This is similar to the `Array` version.
 -/
ByteArray.forInUnsafe : {β : Type v} → {m : Type v → Type w} → [Monad m] → ByteArray → β → (UInt8 → β → m (ForInStep β)) → m β
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.pow : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.Splits → ∀ (n : ℕ), (f ^ n).Splits
-- Lean.MetavarContext
Lean.MetavarContext.addExprMVarDeclExp : Lean.MetavarContext →
  Lean.MVarId → Lean.Name → Lean.LocalContext → Lean.LocalInstances → Lean.Expr → Lean.MetavarKind → Lean.MetavarContext
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeLeftOpOfCone_ι_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F) (X : Jᵒᵖ),
  (CategoryTheory.Limits.coconeLeftOpOfCone c).ι.app X = (c.π.app (Opposite.unop X)).unop
-- Init.System.ST
instMonadExceptOfEST : (ε σ : Type) → MonadExceptOf ε (EST ε σ)
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
the common vertices will agree with those of the original path `f`. In particular,
a vertex `i` with `i < j` can be identified with the same vertex in `f`.  -/
SSet.StrictSegal.spine_δ_vertex_lt : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path (n + 1)) {i : Fin (n + 1)} {j : Fin (n + 2)},
  i.castSucc < j →
    (X.spine n
            ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X j))
              (sx.spineToSimplex f))).vertex
        i =
      f.vertex i.castSucc
-- Mathlib.Data.PNat.Interval
PNat.Icc_eq_finset_subtype : ∀ (a b : ℕ+), Finset.Icc a b = Finset.subtype (fun n => 0 < n) (Finset.Icc ↑a ↑b)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- `padicValRat p 1` is `0` for any `p`.  -/
padicValRat.one : ∀ {p : ℕ}, padicValRat p 1 = 0
-- Mathlib.Topology.Instances.CantorSet
/-- The ternary Cantor set satisfies the equation `C = C / 3 ∪ (2 / 3 + C / 3)`.  -/
cantorSet_eq_union_halves : cantorSet = (fun x => x / 3) '' cantorSet ∪ (fun x => (2 + x) / 3) '' cantorSet
-- Mathlib.Data.Set.Sups
Set.sups_infs_subset_right : ∀ {α : Type u_2} [inst : DistribLattice α] (s t u : Set α), t ⊼ u ⊻ s ⊆ (t ⊻ s) ⊼ (u ⊻ s)
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- An `EffectiveEpiFamily` consisting of a single `EffectiveEpi`
 -/
CategoryTheory.effectiveEpiFamilyStructSingletonOfEffectiveEpi : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {B X : C} →
      (f : X ⟶ B) → [CategoryTheory.EffectiveEpi f] → CategoryTheory.EffectiveEpiFamilyStruct (fun x => X) fun x => f
-- Mathlib.Analysis.Convex.Intrinsic
/-- The intrinsic closure of a set is its closure considered as a set in its affine span.  -/
intrinsicClosure : (𝕜 : Type u_1) →
  {V : Type u_2} →
    {P : Type u_5} →
      [inst : Ring 𝕜] →
        [inst_1 : AddCommGroup V] → [Module 𝕜 V] → [TopologicalSpace P] → [AddTorsor V P] → Set P → Set P
-- Init.ShareCommon
shareCommonM : {m : Type u_1 → Type u_2} → {α : Type u_1} → [MonadShareCommon m] → α → m α
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.instFintypeSubtypeEqNatSemilength : {n : ℕ} → Fintype { p // p.semilength = n }
-- Mathlib.Topology.ClusterPt
/-- **Alias** of the forward direction of `Filter.EventuallyEq.mapClusterPt_iff`. -/
MapClusterPt.congrFun : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} {v : α → X},
  u =ᶠ[F] v → MapClusterPt x F u → MapClusterPt x F v
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
NNRealRMK.le_rieszMeasure_of_isCompact_tsupport_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal)
  [inst_1 : T2Space X] [inst_2 : LocallyCompactSpace X] [inst_3 : MeasurableSpace X] [inst_4 : BorelSpace X]
  {f : CompactlySupportedContinuousMap X NNReal},
  (∀ (x : X), f x ≤ 1) → ∀ {K : Set X}, IsCompact K → tsupport ⇑f ⊆ K → ↑(Λ f) ≤ (NNRealRMK.rieszMeasure Λ) K
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Structure.mk : {L : FirstOrder.Language} →
  {M : Type w} →
    autoParam ({n : ℕ} → L.Functions n → (Fin n → M) → M) FirstOrder.Language.Structure.funMap._autoParam →
      autoParam ({n : ℕ} → L.Relations n → (Fin n → M) → Prop) FirstOrder.Language.Structure.RelMap._autoParam →
        L.Structure M
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_modify : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k k' : α} {fallback : β k'} {f : β k → β k},
      (m.modify k f).getD k' fallback =
        if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).getD fallback
        else m.getD k' fallback
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_X : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A),
  (Polynomial.aeval x) Polynomial.X = x
-- Mathlib.Analysis.Complex.Trigonometric
Real.tanh_sq_lt_one : ∀ (x : ℝ), Real.tanh x ^ 2 < 1
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instHasForget₂FiniteGrpMonoidHomCarrierToGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite : CategoryTheory.HasForget₂ FiniteGrp.{u_1} ProfiniteGrp.{u_1}
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.rightComm_def : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P],
  TensorProduct.rightComm R M N P =
    TensorProduct.assoc R M N P ≪≫ₗ TensorProduct.congr (LinearEquiv.refl R M) (TensorProduct.comm R N P) ≪≫ₗ
      (TensorProduct.assoc R M P N).symm
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (j k : ℕ)
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet (Opposite.op { len := j })),
  ¬A.EqId →
    CategoryTheory.CategoryStruct.comp ((s.cofan (Opposite.op { len := j })).inj A)
        (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.AlternatingFaceMapComplex.obj X).d j k)
          (s.πSummand (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := k })))) =
      0
-- Init.System.ST
ST.Out.val : {σ α : Type} → ST.Out σ α → α
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- Precomposition with a linear isometry preserves the operator norm.  -/
ContinuousLinearMap.opNNNorm_mul_linearIsometryEquiv : ∀ {𝕜 : Type u_1} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] (f : E →L[𝕜] E) (e : E ≃ₗᵢ[𝕜] E), ‖f * ↑↑e‖₊ = ‖f‖₊
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addXYZ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) (P Q : Fin 3 → R),
  W'.addXYZ P Q = ![W'.addX P Q, W'.addY P Q, W'.addZ P Q]
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesAt.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  (p : FormalMultilinearSeries 𝕜 E F) (x : E), HasFPowerSeriesAt f p x = ∃ r, HasFPowerSeriesOnBall f p x r
-- Mathlib.Analysis.Normed.Lp.WithLp
LinearMap.withLpMap_id : ∀ (p : ENNReal) {K : Type u_1} {V : Type u_4} [inst : Semiring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  LinearMap.withLpMap p LinearMap.id = LinearMap.id
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.IsSubDPIdeal.isDPMorphism : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A}
  [inst_1 : (x : A) → Decidable (x ∈ J)] (hJ : hI.IsSubDPIdeal J),
  (DividedPowers.IsSubDPIdeal.dividedPowers hI hJ).IsDPMorphism hI (RingHom.id A)
-- Mathlib.Logic.Equiv.Prod
Equiv.piEquivPiSubtypeProd_apply : ∀ {α : Type u_9} (p : α → Prop) (β : α → Type u_10) [inst : DecidablePred p] (f : (i : α) → β i),
  (Equiv.piEquivPiSubtypeProd p β) f = (fun x => f ↑x, fun x => f ↑x)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquiv_inverse : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C)
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)),
  (CategoryTheory.Over.ConstructProducts.conesEquiv B F).inverse =
    CategoryTheory.Over.ConstructProducts.conesEquivInverse B F
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.tautologicalCocone_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v₁))
  (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda P),
  (CategoryTheory.Presheaf.tautologicalCocone P).ι.app X = X.hom
-- Batteries.Data.Array.Pairwise
Array.instDecidablePairwiseOfDecidableRel : {α : Type u_1} → (R : α → α → Prop) → [DecidableRel R] → (as : Array α) → Decidable (Array.Pairwise R as)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- The `SlashInvariantForm` defined by an Eisenstein series of weight `k : ℤ`, level `Γ(N)`,
and congruence condition given by `a : Fin 2 → ZMod N`.  -/
EisensteinSeries.eisensteinSeriesSIF : {N : ℕ} →
  (Fin 2 → ZMod N) →
    (k : ℤ) → SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k
-- Mathlib.Analysis.Complex.Trigonometric
Real.inv_sqrt_one_add_tan_sq : ∀ {x : ℝ}, 0 < Real.cos x → (√(1 + Real.tan x ^ 2))⁻¹ = Real.cos x
-- Lean.Meta.Basic
/-- `withNewLocalInstances isClassExpensive fvars j k` updates the vector or local instances
using free variables `fvars[j] ... fvars.back`, and execute `k`.

- `isClassExpensive` is defined later.
- `isClassExpensive` uses `whnf` which depends (indirectly) on the set of local instances.  -/
_private.Lean.Meta.Basic.0.Lean.Meta.withNewLocalInstancesImp : {α : Type} → Array Lean.Expr → ℕ → Lean.MetaM α → Lean.MetaM α
-- Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
/-- The internal currying-uncurrying isomorphism `C(x ⊗ y, z) ≅ C(y, C(x, z))`.  -/
CategoryTheory.MonoidalClosed.ihomCurryIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (x y z : C) →
        [inst_2 : CategoryTheory.Closed x] →
          [inst_3 : CategoryTheory.Closed y] →
            [inst_4 : CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)] →
              CategoryTheory.MonoidalCategoryStruct.tensorObj x y ⟹ z ≅ y ⟹ x ⟹ z
-- Mathlib.Order.Partition.Finpartition
Finpartition.toSubtype.congr_simp : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {s : α} (P P_1 : Finpartition s) (e_P : P = P_1)
  {Pr : α → Prop} (Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)) (Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t))
  (Prbot : Pr ⊥) (hs : Pr s) (hP : ∀ p ∈ P.parts, Pr p),
  P.toSubtype Prsup Prinf Prbot hs hP = P_1.toSubtype Prsup Prinf Prbot hs ⋯
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
/-- If `k` is algebraically closed, this is the `k`-point of `X` associated to a closed point.  -/
AlgebraicGeometry.pointOfClosedPoint : {X : AlgebraicGeometry.Scheme} →
  {K : Type u} →
    [inst : Field K] →
      [IsAlgClosed K] →
        (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) →
          [AlgebraicGeometry.LocallyOfFiniteType f] →
            (x : ↥X) → IsClosed {x} → (AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X)
-- ProofWidgets.Util
/-- A copy of `Delaborator.withAnnotateTermInfo` for other syntactic categories.  -/
Lean.PrettyPrinter.Delaborator.withAnnotateTermLikeInfo : {n : Lean.SyntaxNodeKinds} →
  Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax n) → Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax n)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
/-- An upper estimate on the complex distance between two points in terms of the hyperbolic distance
and the imaginary part of one of the points.  -/
UpperHalfPlane.le_dist_coe : ∀ (z w : UpperHalfPlane), w.im * (1 - Real.exp (-dist z w)) ≤ dist ↑z ↑w
-- Mathlib.RingTheory.Int.Basic
Int.eq_pow_of_mul_eq_pow_odd_right : ∀ {a b c : ℤ}, IsCoprime a b → ∀ {k : ℕ}, Odd k → a * b = c ^ k → ∃ d, b = d ^ k
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The quotient map from the 1-cocycles of `A`, as a submodule of `G → A`, to `H¹(G, A)`.  -/
groupCohomology.H1π : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → ModuleCat.of k ↥(groupCohomology.cocycles₁ A) ⟶ groupCohomology.H1 A
-- Mathlib.CategoryTheory.Category.TwoP
pointedToTwoPSnd_obj_X : ∀ (X : Pointed), (pointedToTwoPSnd.obj X).X = Option X.X
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.addSubmonoid.eq_1 : ∀ (α : Type u_2) (β : Type u_4) [inst : TopologicalSpace α] [inst_1 : AddZeroClass β],
  HasCompactSupport.addSubmonoid α β = { carrier := {f | HasCompactSupport f}, add_mem' := ⋯, zero_mem' := ⋯ }
-- Lean.Elab.Level
Lean.Elab.Level.Context.mk.injEq : ∀ (options : Lean.Options) (ref : Lean.Syntax) (autoBoundImplicit : Bool) (options_1 : Lean.Options)
  (ref_1 : Lean.Syntax) (autoBoundImplicit_1 : Bool),
  ({ options := options, ref := ref, autoBoundImplicit := autoBoundImplicit } =
      { options := options_1, ref := ref_1, autoBoundImplicit := autoBoundImplicit_1 }) =
    (options = options_1 ∧ ref = ref_1 ∧ autoBoundImplicit = autoBoundImplicit_1)
-- Lean.Meta.AppBuilder
/-- Given `h : a = b`, returns a proof of `b = a`.  -/
Lean.Meta.mkEqSymm : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Tactic.DefEqTransformations
/-- This is `Lean.MVarId.changeLocalDecl` but makes sure to preserve local variable order.
 -/
Lean.MVarId.changeLocalDecl' : Lean.MVarId → Lean.FVarId → Lean.Expr → optParam Bool true → Lean.MetaM Lean.MVarId
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_right : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : WeierstrassCurve.Jacobian.PointClass F}
  {Q : Fin 3 → F}, W.NonsingularLift P → W.Nonsingular Q → Q 2 = 0 → W.addMap P ⟦Q⟧ = P
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.instT3Space : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (N : AddSubgroup G)
  [N.Normal] [hN : IsClosed ↑N], T3Space (G ⧸ N)
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.ae_of_ae_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β},
  AEMeasurable f μ → ∀ {p : β → Prop}, (∀ᵐ (y : β) ∂MeasureTheory.Measure.map f μ, p y) → ∀ᵐ (x : α) ∂μ, p (f x)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- The reversed version of `SimpleGraph.Walk.cons`, concatenating an edge to
the end of a walk.  -/
SimpleGraph.Walk.concat : {V : Type u} → {G : SimpleGraph V} → {u v w : V} → G.Walk u v → G.Adj v w → G.Walk u w
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.Equivalence.mapHomologicalComplex_inverse : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] (e : W₁ ≌ W₂) [inst_4 : e.functor.PreservesZeroMorphisms]
  (c : ComplexShape ι), (e.mapHomologicalComplex c).inverse = e.inverse.mapHomologicalComplex c
-- Init.Core
instBEqProd : {α : Type u_1} → {β : Type u_2} → [BEq α] → [BEq β] → BEq (α × β)