mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.equivMapOfInjective.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup M) (f : M →ₙ+ N)
  (hf : Function.Injective ⇑f), S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
/-- In a `NonPreadditiveAbelian` category, a mono is the kernel of its cokernel. More precisely:
If `f` is a monomorphism and `s` is some colimit cokernel cocone on `f`, then `f` is a kernel
of `Cofork.π s`.  -/
CategoryTheory.NonPreadditiveAbelian.monoIsKernelOfCokernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.NonPreadditiveAbelian C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          [CategoryTheory.Mono f] →
            (s : CategoryTheory.Limits.Cofork f 0) →
              CategoryTheory.Limits.IsColimit s →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι f ⋯)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_subset_mul : ∀ {α : Type u_2} [inst : Mul α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ * s₂ ⊆ t₁ * t₂
-- Init.Data.UInt.Bitwise
UInt8.toUSize_shiftRight : ∀ (a b : UInt8), (a >>> b).toUSize = a.toUSize >>> (b.toUSize % 8)
-- Mathlib.Algebra.Category.ModuleCat.Products
/-- The categorical coproduct of a family of objects in `ModuleCat`
agrees with direct sum.
 -/
ModuleCat.coprodIsoDirectSum : {R : Type u} →
  [inst : Ring R] →
    {ι : Type v} →
      (Z : ι → ModuleCat R) →
        [DecidableEq ι] →
          [inst_2 : CategoryTheory.Limits.HasCoproduct Z] → ∐ Z ≅ ModuleCat.of R (DirectSum ι fun i => ↑(Z i))
-- Mathlib.Geometry.Manifold.Instances.Real
IccRightChart_apply : ∀ {x y : ℝ} [hxy : Fact (x < y)] (z : ↑(Set.Icc x y)), ↑(IccRightChart x y) z = ⟨WithLp.toLp 2 fun x_1 => y - ↑z, ⋯⟩
-- Mathlib.Analysis.Fourier.ZMod
Function.Even.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] (f : α → β), Function.Even f = ∀ (a : α), f (-a) = f a
-- Std.Data.HashSet.Lemmas
Std.HashSet.forIn_eq_forIn_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {δ : Type v} {m' : Type v → Type w} [inst : Monad m']
  [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ}, forIn m init f = forIn m.toList init f
-- Mathlib.Data.Sign.Defs
/-- The less-than-or-equal relation on signs.  -/
SignType.LE : SignType → SignType → Prop
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.ContextualizedCompletionInfo.ctx : Lean.Server.Completion.ContextualizedCompletionInfo → Lean.Elab.ContextInfo
-- Init.Data.List.Impl
/-- Removes the last element of the list, if one exists.

This is a tail-recursive version of `List.dropLast`, used at runtime.

Examples:
* `[].dropLastTR = []`
* `["tea"].dropLastTR = []`
* `["tea", "coffee", "juice"].dropLastTR = ["tea", "coffee"]`
 -/
List.dropLastTR : {α : Type u_1} → List α → List α
-- Lean.Meta.WHNF
Lean.Meta.reduceNatNativeUnsafe : Lean.Name → Lean.MetaM ℕ
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Reduction to diagonal form by elementary operations is invariant under reindexing.  -/
Matrix.Pivot.reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal : ∀ {n : Type u_1} {p : Type u_2} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : DecidableEq n] [inst_2 : DecidableEq p]
  [inst_3 : Fintype n] [inst_4 : Fintype p] (M : Matrix p p 𝕜) (e : p ≃ n),
  (∃ L L' D,
      (List.map Matrix.TransvectionStruct.toMatrix L).prod * (Matrix.reindexAlgEquiv 𝕜 𝕜 e) M *
          (List.map Matrix.TransvectionStruct.toMatrix L').prod =
        Matrix.diagonal D) →
    ∃ L L' D,
      (List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod =
        Matrix.diagonal D
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
/-- The discriminant of a matrix is defined to be the discriminant of its characteristic
polynomial.  -/
Matrix.discr : {R : Type u_1} → {n : Type u_2} → [CommRing R] → [Fintype n] → [DecidableEq n] → Matrix n n R → R
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b).hom =
    CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.id b)).inv
      (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom)
        (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.swap_bijective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Function.Bijective ⇑(Monoid.Coprod.swap M N)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranCounit_app_whiskerLeft_ranAdjunction_unit_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (G : CategoryTheory.Functor D H),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft ((L.ranAdjunction H).unit.app G)) (L.ranCounit.app (L.comp G)) =
    CategoryTheory.CategoryStruct.id (L.comp G)
-- Mathlib.Algebra.Group.Defs
IsLeftCancelMul.mk : ∀ {G : Type u} [inst : Mul G], (∀ (a : G), IsLeftRegular a) → IsLeftCancelMul G
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.inv_smul_set_distrib₀ : ∀ {α : Type u_1} [inst : GroupWithZero α] (a : α) (s : Set α), (a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.span_range_mk_kerGen : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b),
  Submodule.span (Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D)
      (Set.range fun i =>
        Algebra.Extension.Cotangent.mk (Algebra.Generators.PresentationOfFreeCotangent.Aux.kerGen✝ D i)) =
    ⊤
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialProd_succ' : ∀ {M : Type u_2} [inst : Monoid M] {n : ℕ} (f : Fin (n + 1) → M) (j : Fin (n + 1)),
  Fin.partialProd f j.succ = f 0 * Fin.partialProd (Fin.tail f) j
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddGroup.ofSeparation.eq_1 : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (h : ∀ (x : E), ‖x‖ = 0 → x = 0),
  NormedAddGroup.ofSeparation h =
    { toNorm := inst.toNorm, toAddGroup := inst.toAddGroup, toPseudoMetricSpace := inst.toPseudoMetricSpace,
      eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.RingTheory.PicardGroup
Module.Flat.top_mul_submoduleAlgebra : ∀ {R : Type u} {M : Type v} {A : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) [Module.Flat R M] [FaithfulSMul R A],
  ⊤ * Module.Flat.submoduleAlgebra e = ⊤
-- Init.Data.Vector.Lemmas
Vector.set_append : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} {i : ℕ} {x : α} (h : i < n + m),
  (xs ++ ys).set i x h = if h' : i < n then xs.set i x h' ++ ys else xs ++ ys.set (i - n) x ⋯
-- Std.Http.Data.Response
/-- Creates a new HTTP Response builder with the 200 status code.
 -/
Std.Http.Response.ok : Std.Http.Response.Builder
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.listR.eq_1 : ∀ {α : Type u_1}, RBTree.RBNode.Path.root.listR = []
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsVanKampenColimit.map_reflective : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasColimitsOfShape J C]
  {Gl : CategoryTheory.Functor C D} {Gr : CategoryTheory.Functor D C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful]
  {F : CategoryTheory.Functor J D} {c : CategoryTheory.Limits.Cocone (F.comp Gr)},
  CategoryTheory.IsVanKampenColimit c →
    ∀ [∀ (X : D) (f : X ⟶ Gl.obj c.pt), CategoryTheory.Limits.HasPullback (Gr.map f) (adj.unit.app c.pt)]
      [∀ (X : D) (f : X ⟶ Gl.obj c.pt),
          CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (Gr.map f) (adj.unit.app c.pt)) Gl]
      [∀ (X : C) (i : J) (f : X ⟶ c.pt),
          CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f (c.ι.app i)) Gl],
      CategoryTheory.IsVanKampenColimit (Gl.mapCocone c)
-- Mathlib.Topology.MetricSpace.Closeds
TopologicalSpace.Compacts.isometry_toCloseds : ∀ {α : Type u_1} [inst : EMetricSpace α], Isometry TopologicalSpace.Compacts.toCloseds
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.pos_of_isNNRat : ∀ {A : Type u_1} {e : A} {n d : ℕ} [inst : Semiring A] [inst_1 : LinearOrder A] [IsStrictOrderedRing A],
  Mathlib.Meta.NormNum.IsNNRat e n d → decide (0 < n) = true → 0 < e
-- Mathlib.GroupTheory.Torsion
AddCommGroup.freeRank_eq_zero : ∀ {G : Type u_1} [inst : AddCommGroup G], IsAddTorsion G → ∀ [inst_1 : AddGroup.FG G], AddCommGroup.freeRank G = 0
-- Std.Http.Internal.Char
/-- Checks if a character is valid after the first character of a URI scheme.
Valid characters are ASCII alphanumeric, `+`, `-`, and `.`.
 -/
Std.Http.Internal.Char.isValidSchemeChar : Char → Bool
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.Spec.uncons? : {m : Type u → Type u} →
  (self : MLList.Spec✝ m) → {α : Type u} → MLList.Spec.listM✝ self α → Option (Option (α × MLList.Spec.listM✝ self α))
-- Mathlib.MeasureTheory.Measure.TightNormed
MeasureTheory.isTightMeasureSet_of_forall_basis_tendsto : ∀ {E : Type u_1} {mE : MeasurableSpace E} {S : Set (MeasureTheory.Measure E)} [inst : NormedAddCommGroup E]
  {𝕜 : Type u_2} {ι : Type u_3} [inst_1 : RCLike 𝕜] [inst_2 : Fintype ι] [inst_3 : InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] (b : OrthonormalBasis ι 𝕜 E),
  (∀ (i : ι), Filter.Tendsto (fun r => ⨆ μ ∈ S, μ {x | r < ‖inner 𝕜 (b i) x‖}) Filter.atTop (nhds 0)) →
    MeasureTheory.IsTightMeasureSet S
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.coe_ofContinuousOpen : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap ↑e) (hs : IsOpen e.source),
  ↑(OpenPartialHomeomorph.ofContinuousOpen e hc ho hs) = ↑e
-- Mathlib.Data.Nat.Init
/-- **Alias** of `Nat.strongRec_eq`. -/
Nat.strongRecOn'_beta : ∀ {motive : ℕ → Sort u_1} (ind : (n : ℕ) → ((m : ℕ) → m < n → motive m) → motive n) (t : ℕ),
  Nat.strongRec ind t = ind t fun m x => Nat.strongRec ind m
-- Plausible.Gen
_private.Plausible.Gen.0.Plausible.test : ℕ → Plausible.Gen ℕ
-- Lean.Meta.CompletionName
Lean.Meta.addToCompletionBlackList : Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- a map `I₂ × I₃ → I₃`  -/
CategoryTheory.GradedObject.TriangleIndexData.p₂₃ : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₃ : Type u_3} →
      {J : Type u_4} →
        [inst : Zero I₂] →
          {r : I₁ × I₂ × I₃ → J} → {π : I₁ × I₃ → J} → CategoryTheory.GradedObject.TriangleIndexData r π → I₂ × I₃ → I₃
-- Mathlib.Algebra.Order.Module.Defs
neg_iff_neg_of_smul_pos : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : LinearOrder α] [inst_4 : LinearOrder β] [PosSMulMono α β] [SMulPosMono α β], 0 < a • b → (a < 0 ↔ b < 0)
-- Lean.Elab.DeclNameGen
/-- Generates an instance name for a declaration that has the given binders and type.
It tries to make these names relatively unique ecosystem-wide.

Note that this elaborates the binders and the type.
This means that when elaborating an instance declaration, we elaborate these twice.
 -/
Lean.Elab.Command.mkInstanceName : Array Lean.Syntax → Lean.Syntax → Lean.Elab.Command.CommandElabM Lean.Name
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- There is a walk between every pair of vertices in a connected component.  -/
SimpleGraph.ConnectedComponent.reachable_toSimpleGraph : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u ∈ C) (hv : v ∈ C),
  C.toSimpleGraph.Reachable ⟨u, hu⟩ ⟨v, hv⟩
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNonUnitalNonAssocCommSemiring : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonUnitalNonAssocCommSemiring R] →
      [IsTopologicalSemiring R] → NonUnitalNonAssocCommSemiring (SeparationQuotient R)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_X_add_C : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (r : R), (Polynomial.X + Polynomial.C r).roots = {-r}
-- Mathlib.FieldTheory.Galois.Basic
MulSemiringAction.toAlgEquiv.congr_simp : ∀ {G : Type u_2} (R : Type u_3) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G A] [inst_5 : SMulCommClass G R A] (g g_1 : G),
  g = g_1 → MulSemiringAction.toAlgEquiv R A g = MulSemiringAction.toAlgEquiv R A g_1
-- Mathlib.Algebra.Field.ULift
ULift.down_ratCast : ∀ {α : Type u} [inst : RatCast α] (q : ℚ), (↑q).down = ↑q
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.smulCommClass : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq γ] [inst_1 : SMul α γ] [inst_2 : SMul β γ]
  [SMulCommClass α β γ], SMulCommClass (Finset α) (Finset β) (Finset γ)
-- Init.Data.Nat.Lemmas
Nat.div_le_div_right : ∀ {a b c : ℕ}, a ≤ b → a / c ≤ b / c
-- Mathlib.Order.RelIso.Basic
RelIso.relEmbeddingCongr_symm_apply : ∀ {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop}
  {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₂ : r₂ ↪r s₂),
  (e₁.relEmbeddingCongr e₂).symm f₂ = (e₁.toRelEmbedding.trans f₂).trans e₂.symm.toRelEmbedding
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.instComonadicLeftAdjointCoalgebraForget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (G : CategoryTheory.Comonad C) → CategoryTheory.ComonadicLeftAdjoint G.forget
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.integral_theta_div_log_sq_isLittleO : (fun x => ∫ (t : ℝ) in 2..x, Chebyshev.theta t / (t * Real.log t ^ 2)) =o[Filter.atTop] fun x => x / Real.log x
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_one : Nat.factorial 1 = 1
-- Mathlib.MeasureTheory.Group.LIntegral
MeasureTheory.lintegral_sub_right_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : AddGroup G] [MeasurableAdd G]
  [μ.IsAddRightInvariant] (f : G → ENNReal) (g : G), ∫⁻ (x : G), f (x - g) ∂μ = ∫⁻ (x : G), f x ∂μ
-- Mathlib.LinearAlgebra.Basis.Fin
Module.Basis.finTwoProd.eq_1 : ∀ (R : Type u_7) [inst : Semiring R],
  Module.Basis.finTwoProd R = Module.Basis.ofEquivFun (LinearEquiv.finTwoArrow R R).symm
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- The sheaf condition
in terms of a limit diagram over all `{ V : Opens X // ∃ i, V ≤ U i }`
is equivalent to the reformulation
in terms of a limit diagram over `U i` and `U i ⊓ U j`.
 -/
TopCat.Presheaf.isSheafOpensLeCover_iff_isSheafPairwiseIntersections : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Presheaf C X),
  F.IsSheafOpensLeCover ↔ F.IsSheafPairwiseIntersections
-- Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
WithTop.measurable_of_measurable_comp_coe : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  [inst_3 : MeasurableSpace ι] [BorelSpace ι] {α : Type u_2} {mα : MeasurableSpace α} {f : WithTop ι → α},
  (Measurable fun p => f ↑p) → Measurable f
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Ordering.swap.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.eq) → (Unit → motive Ordering.gt) → motive x
-- Init.Data.Option.Lemmas
Option.pfilter_filter : ∀ {α : Type u_1} {o : Option α} {p : α → Bool} {q : (a : α) → Option.filter p o = some a → Bool},
  (Option.filter p o).pfilter q = o.pfilter fun a h => if h' : p a = true then q a ⋯ else false
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.comap_injective_isAddCommutative : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H : AddSubgroup G) {f : G' →+ G},
  Function.Injective ⇑f → ∀ [IsAddCommutative ↥H], IsAddCommutative ↥(AddSubgroup.comap f H)
-- Lean.Elab.Calc
Lean.Elab.Term.mkCalcFirstStepView : Lean.TSyntax `Lean.calcFirstStep → Lean.Elab.TermElabM Lean.Elab.Term.CalcStepView
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.inr_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc f g) h) =
    CategoryTheory.CategoryStruct.comp g h
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instEmptyCollectionTrie : {α : Type} → EmptyCollection (Lean.Meta.LazyDiscrTree.Trie α)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemTag.deprecated.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemTag.deprecated = 1
-- Mathlib.Dynamics.BirkhoffSum.NormedSpace
/-- If a function `g` is bounded,
then the difference between Birkhoff averages of `g`
along the orbit of `f x` and along the orbit of `x`
tends to zero.

See also `tendsto_birkhoffAverage_apply_sub_birkhoffAverage`.  -/
tendsto_birkhoffAverage_apply_sub_birkhoffAverage' : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] (𝕜 : Type u_3) [inst_1 : RCLike 𝕜]
  [inst_2 : NormedSpace 𝕜 E] {g : α → E},
  Bornology.IsBounded (Set.range g) →
    ∀ (f : α → α) (x : α),
      Filter.Tendsto (fun n => birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) Filter.atTop (nhds 0)
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.differentiableAt_LFunction : ∀ {N : ℕ} [inst : NeZero N] (Φ : ZMod N → ℂ) (s : ℂ), s ≠ 1 ∨ ∑ j, Φ j = 0 → DifferentiableAt ℂ (ZMod.LFunction Φ) s
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
/-- The Eisenstein series of weight `2` and level `1` defined as the conditional sum
of `m` in `[N,N]` of `e2Summand m`. This sum over symmetric intervals is handy in showing it is
Summable.  -/
EisensteinSeries.G2 : UpperHalfPlane → ℂ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.baseChange_polynomialX : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B), (W.baseChange B).polynomialX = Polynomial.map (Polynomial.mapRingHom ↑f) (W.baseChange A).polynomialX
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.comap_comap : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonAssocSemiring T] (s : Subsemiring T) (g : S →+* T) (f : R →+* S),
  Subsemiring.comap f (Subsemiring.comap g s) = Subsemiring.comap (g.comp f) s
-- Mathlib.Computability.Ackermann
_private.Mathlib.Computability.Ackermann.0.ack.match_1.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive 0 n) (h_2 : (m : ℕ) → motive m.succ 0)
  (h_3 : (m n : ℕ) → motive m.succ n.succ),
  (match 0, n with
    | 0, n => h_1 n
    | m.succ, 0 => h_2 m
    | m.succ, n.succ => h_3 m n) =
    h_1 n
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank : ∀ (K : Type u) (V : Type v) [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [Module.Free K V] [Module.Finite K V],
  Cardinal.lift.{u, v} (Cardinal.mk V) = Cardinal.lift.{v, u} (Cardinal.mk K) ^ Cardinal.lift.{u, v} (Module.rank K V)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrableOn_congr : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f g : X → ε} {μ : MeasureTheory.Measure X} {s : Set X},
  f =ᵐ[μ.restrict s] g → (MeasureTheory.LocallyIntegrableOn f s μ ↔ MeasureTheory.LocallyIntegrableOn g s μ)
-- Mathlib.RingTheory.PicardGroup
Submodule.unitsToPic_apply : ∀ (R : Type u) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] (I : (Submodule R A)ˣ), (Submodule.unitsToPic R A) I = CommRing.Pic.mk R ↥↑I
-- Init.Data.Nat.ToString
Nat.repr_of_ge : ∀ {n : ℕ}, 10 ≤ n → n.repr = (n / 10).repr ++ String.singleton (n % 10).digitChar
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_sup : ∀ {V : Type u} {G₁ G₂ : SimpleGraph V} (v : V), (G₁ ⊔ G₂).neighborSet v = G₁.neighborSet v ∪ G₂.neighborSet v
-- Init.Data.SInt.Lemmas
Int32.neg_mul_neg : ∀ (a b : Int32), -a * -b = a * b
-- Std.Do.WP.SimpLemmas
Std.Do.WP.withReader_MonadWithReader : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ρ α : Type u} {Q : Std.Do.PostCond α ps} [inst : MonadWithReaderOf ρ m]
  [inst_1 : Std.Do.WP m ps] (f : ρ → ρ) (x : m α),
  (Std.Do.wp (withReader f x)).apply Q = (Std.Do.wp (MonadWithReaderOf.withReader f x)).apply Q
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_zero : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)], ‖0‖ = 0
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- The map `H^n(f) ⟶ H^n(f ≫ g)` factors through `opZ^n(f, g)`.  -/
CategoryTheory.Abelian.SpectralObject.fromOpcycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (fg : i ⟶ k) →
                    CategoryTheory.CategoryStruct.comp f g = fg →
                      (n : ℤ) → X.opcycles f g n ⟶ (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.instAddCommMagma : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [AddCommMagma α] → AddCommMagma (Matrix m n α)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- Let `l'` be a measurably generated filter; let `l` be a of filter such that each `s ∈ l'`
eventually includes `Ioc u v` as both `u` and `v` tend to `l`. Let `μ` be a measure finite at `l'`.

Suppose that `f : ℝ → E` has a finite limit at `l' ⊓ ae μ`. Then `f` is interval integrable on
`u..v` provided that both `u` and `v` tend to `l`.

Typeclass instances allow Lean to find `l'` based on `l` but not vice versa, so
`apply Tendsto.eventually_intervalIntegrable_ae` will generate goals `Filter ℝ` and
`TendstoIxxClass Ioc ?m_1 l'`.  -/
Filter.Tendsto.eventually_intervalIntegrable_ae : ∀ {ι : Type u_1} {E : Type u_5} [inst : NormedAddCommGroup E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ}
  {l l' : Filter ℝ},
  StronglyMeasurableAtFilter f l' μ →
    ∀ [Filter.TendstoIxxClass Set.Ioc l l'] [l'.IsMeasurablyGenerated],
      μ.FiniteAtFilter l' →
        ∀ {c : E},
          Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (nhds c) →
            ∀ {u v : ι → ℝ} {lt : Filter ι},
              Filter.Tendsto u lt l → Filter.Tendsto v lt l → ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (u t) (v t)