mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.VectorBundle.Hom
/-- Consider `C^n` maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a basemap
`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
One can apply `ψ  m` to `v m` and `w m`, and the resulting map is `C^n`.  -/
ContinuousOn.clm_bundle_apply₂ : ∀ {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {F₃ : Type u_12} {M : Type u_13}
  [inst : NontriviallyNormedField 𝕜] {E₁ : B → Type u_14} [inst_1 : (x : B) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B) → TopologicalSpace (E₁ x)]
  {E₂ : B → Type u_15} [inst_7 : (x : B) → AddCommGroup (E₂ x)] [inst_8 : (x : B) → Module 𝕜 (E₂ x)]
  [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_16} [inst_13 : (x : B) → AddCommGroup (E₃ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₃ x)] [inst_15 : NormedAddCommGroup F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [inst_18 : (x : B) → TopologicalSpace (E₃ x)]
  [inst_19 : TopologicalSpace B] [inst_20 : TopologicalSpace M] [inst_21 : FiberBundle F₁ E₁]
  [inst_22 : VectorBundle 𝕜 F₁ E₁] [inst_23 : FiberBundle F₂ E₂] [inst_24 : VectorBundle 𝕜 F₂ E₂]
  [inst_25 : FiberBundle F₃ E₃] [inst_26 : VectorBundle 𝕜 F₃ E₃] {b : M → B} {v : (x : M) → E₁ (b x)} {s : Set M}
  [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₃ x)] [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₃ x)]
  {ψ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x) →L[𝕜] E₃ (b x)} {w : (x : M) → E₂ (b x)},
  ContinuousOn (fun m => ⟨b m, ψ m⟩) s →
    ContinuousOn (fun m => ⟨b m, v m⟩) s →
      ContinuousOn (fun m => ⟨b m, w m⟩) s → ContinuousOn (fun m => ⟨b m, ((ψ m) (v m)) (w m)⟩) s
-- Mathlib.RingTheory.PowerBasis
PowerBasis.adjoin_gen_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (B : PowerBasis R S),
  R[B.gen] = ⊤
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_i : ∀ {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 l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex._auto_3),
  (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).i = X.iCycles f₁ f₂ n₁
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedInf_empty : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : DecidableLE α] [inst_2 : BoundedOrder α] (a : α),
  ∅.truncatedInf a = ⊥
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃MapObj_ext_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r}
  {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂}
  {X₃ : CategoryTheory.GradedObject I₃ C₃}
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] {j : J} {A : C₄}
  {f g :
    CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
        (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶
      A},
  f = g ↔
    ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) f =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) g
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_fun_sum' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {s : Finset ι} {X : ι → Ω → ℝ}
  [MeasureTheory.IsFiniteMeasure μ],
  (∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) →
    ProbabilityTheory.variance (fun ω => ∑ i ∈ s, X i ω) μ =
      ∑ i ∈ s, ∑ j ∈ s, ProbabilityTheory.covariance (X i) (X j) μ
-- Mathlib.Topology.Algebra.Group.Basic
Filter.neg_nhdsGT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [inst_2 : PartialOrder H] [IsOrderedAddMonoid H]
  [ContinuousNeg H] {a : H}, -nhdsWithin a (Set.Ioi a) = nhdsWithin (-a) (Set.Iio (-a))
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
IsZGroup.instOfIsCyclic : ∀ {G : Type u_1} [inst : Group G] [IsCyclic G], IsZGroup G
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageMap.factor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g)
  (m : CategoryTheory.Limits.ImageMap sq),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f.hom) m.map =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) (CategoryTheory.Limits.factorThruImage g.hom)
-- Init.Data.UInt.Lemmas
UInt64.toNat_mod : ∀ (a b : UInt64), (a % b).toNat = a.toNat % b.toNat
-- Mathlib.CategoryTheory.Category.Basic
/-- A variant of `aesop_cat` which does not fail when it is unable to solve the
goal. Use this only for exploration! Nonterminal `aesop` is even worse than
nonterminal `simp`.
 -/
CategoryTheory.aesop_cat_nonterminal : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate.eq_1 : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
  A.adjugate = Matrix.of fun i => A.transpose.cramer (Pi.single i 1)
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.toEquiv_reindexRingEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : Mul R]
  [inst_3 : AddCommMonoid R] (e : m ≃ n), ↑(Matrix.reindexRingEquiv R e) = Matrix.reindex e e
-- Lean.Meta.LazyDiscrTree
/-- Convert a pre-discrimination tree to a lazy discrimination tree.  -/
Lean.Meta.LazyDiscrTree.PreDiscrTree.toLazy : {α : Type} → Lean.Meta.LazyDiscrTree.PreDiscrTree α → Lean.Meta.LazyDiscrTree α
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- Integration by parts of Schwartz functions for directional derivatives.

Version for multiplication of scalar-valued Schwartz functions.  -/
SchwartzMap.integral_mul_lineDerivOp_right_eq_neg_left : ∀ {𝕜 : Type u_2} {D : Type u_4} [inst : NormedAddCommGroup D] [inst_1 : NormedSpace ℝ D] [inst_2 : MeasurableSpace D]
  {μ : MeasureTheory.Measure D} [BorelSpace D] [FiniteDimensional ℝ D] [μ.IsAddHaarMeasure] [inst_6 : NormedRing 𝕜]
  [inst_7 : NormedSpace ℝ 𝕜] [IsScalarTower ℝ 𝕜 𝕜] [SMulCommClass ℝ 𝕜 𝕜] (f g : SchwartzMap D 𝕜) (v : D),
  ∫ (x : D), f x * (LineDeriv.lineDerivOp v g) x ∂μ = -∫ (x : D), (LineDeriv.lineDerivOp v f) x * g x ∂μ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map from the short complex `(G × G →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A`
to `(H × H →₀ B) --d₂₁--> (H →₀ B) --d₁₀--> B`.  -/
groupHomology.mapShortComplexH1 : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u, u, u} k G} →
          {B : Rep.{u, u, u} k H} →
            (f : G →* H) → (A ⟶ Rep.res f B) → (groupHomology.shortComplexH1 A ⟶ groupHomology.shortComplexH1 B)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- Bundle the data of a parallel pair along with a common section as a functor out of the walking
reflexive pair  -/
CategoryTheory.Limits.reflexivePair : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A B : C} →
      (f g : A ⟶ B) →
        (s : B ⟶ A) →
          autoParam (CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B)
              CategoryTheory.Limits.reflexivePair._auto_1 →
            autoParam (CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B)
                CategoryTheory.Limits.reflexivePair._auto_3 →
              CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.isPrimitiveRoot_iff' : ∀ {R : Type u_4} [inst : CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ ξ : Rˣ},
  IsPrimitiveRoot ζ k → (IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ)
-- Mathlib.Algebra.MvPolynomial.Monad
/-- **Alias** of `MvPolynomial.eval₂Hom_C_eq_bind₁`. -/
MvPolynomial.eval₂Hom_C_left : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (f : σ → MvPolynomial τ R),
  MvPolynomial.eval₂Hom MvPolynomial.C f = ↑(MvPolynomial.bind₁ f)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cocone.ofCotrident_ι : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C}
  (t : CategoryTheory.Limits.Cotrident fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j))
  (j : CategoryTheory.Limits.WalkingParallelFamily J),
  (CategoryTheory.Limits.Cocone.ofCotrident t).ι.app j =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app j)
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.commShiftIso_hom_app_counit_app_shift : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) (A : Type u_3) [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] [adj.CommShift A] (a : A)
  (Y : D),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (G.comp F) a).hom.app Y)
      ((CategoryTheory.shiftFunctor D a).map (adj.counit.app Y)) =
    adj.counit.app ((CategoryTheory.shiftFunctor D a).obj Y)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.functorExt_inv_app : ∀ {J : CategoryTheory.Limits.MulticospanShape} {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Limits.WalkingMulticospan J) C}
  (left :
    (i : J.L) →
      F.obj (CategoryTheory.Limits.WalkingMulticospan.left i) ≅ G.obj (CategoryTheory.Limits.WalkingMulticospan.left i))
  (right :
    (i : J.R) →
      F.obj (CategoryTheory.Limits.WalkingMulticospan.right i) ≅
        G.obj (CategoryTheory.Limits.WalkingMulticospan.right i))
  (wl :
    autoParam
      (∀ (i : J.R),
        CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMulticospan.Hom.fst i)) (right i).hom =
          CategoryTheory.CategoryStruct.comp (left (J.fst i)).hom
            (G.map (CategoryTheory.Limits.WalkingMulticospan.Hom.fst i)))
      CategoryTheory.Limits.WalkingMulticospan.functorExt._auto_1)
  (wr :
    autoParam
      (∀ (i : J.R),
        CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMulticospan.Hom.snd i)) (right i).hom =
          CategoryTheory.CategoryStruct.comp (left (J.snd i)).hom
            (G.map (CategoryTheory.Limits.WalkingMulticospan.Hom.snd i)))
      CategoryTheory.Limits.WalkingMulticospan.functorExt._auto_3)
  (X : CategoryTheory.Limits.WalkingMulticospan J),
  (CategoryTheory.Limits.WalkingMulticospan.functorExt left right wl wr).inv.app X =
    (match X with
      | CategoryTheory.Limits.WalkingMulticospan.left i => left i
      | CategoryTheory.Limits.WalkingMulticospan.right i => right i).inv
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
/-- The vanishing ideal of a set `t` of points of the projective spectrum of a commutative ring `R`
is the intersection of all the relevant homogeneous prime ideals in the set `t`.

An element `f` of `A` can be thought of as a dependent function on the projective spectrum of `𝒜`.
At a point `x` (a homogeneous prime ideal) the function (i.e., element) `f` takes values in the
quotient ring `A` modulo the prime ideal `x`. In this manner, `vanishingIdeal t` is exactly the
ideal of `A` consisting of all "functions" that vanish on all of `t`.  -/
ProjectiveSpectrum.vanishingIdeal : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubmonoidClass σ A] →
          {𝒜 : ℕ → σ} → [inst_3 : GradedRing 𝒜] → Set (ProjectiveSpectrum 𝒜) → HomogeneousIdeal 𝒜
-- Lean.Server.Rpc.Basic
Lean.Lsp.instInhabitedRpcRef : Inhabited Lean.Lsp.RpcRef
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isLeftKanExtension_iff_postcompose : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor D D'}
  {F₀ : CategoryTheory.Functor C H} {F₁ : CategoryTheory.Functor D H} (α : F₀ ⟶ L.comp F₁) [F₁.IsLeftKanExtension α]
  {F₂ : CategoryTheory.Functor D' H} (L'' : CategoryTheory.Functor C D') (e : L.comp L' ≅ L'') (β : F₁ ⟶ L'.comp F₂)
  (γ : F₀ ⟶ L''.comp F₂),
  autoParam
      (CategoryTheory.CategoryStruct.comp α
          (CategoryTheory.CategoryStruct.comp (L.whiskerLeft β)
            (CategoryTheory.CategoryStruct.comp (L.associator L' F₂).inv
              (CategoryTheory.Functor.whiskerRight e.hom F₂))) =
        γ)
      CategoryTheory.Functor.isLeftKanExtension_iff_postcompose._auto_1 →
    (F₂.IsLeftKanExtension β ↔ F₂.IsLeftKanExtension γ)
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeries_baseChange : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {A : Type u_1}
  [inst_3 : CommRing A] [inst_4 : Algebra R A] (k : ℕ),
  LieAlgebra.derivedSeries A (TensorProduct R A L) k = LieSubmodule.baseChange A (LieAlgebra.derivedSeries R L k)
-- Mathlib.Data.Set.Subset
Set.preimage_val_sInter_eq_sInter : ∀ {α : Type u_2} {A : Set α} {S : Set (Set α)}, Subtype.val ⁻¹' ⋂₀ S = ⋂₀ ((fun x => Subtype.val ⁻¹' x) '' S)
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ioc_add_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ioc (a + n • b) (a + (n + 1) • b))
-- Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
/-- Quotients by submodules of full rank of free finite `ℤ`-modules are isomorphic
to a direct product of `ZMod`.
 -/
Submodule.quotientEquivPiZMod : {ι : Type u_1} →
  {M : Type u_3} →
    [inst : AddCommGroup M] →
      [inst_1 : Finite ι] →
        (N : Submodule ℤ M) →
          (b : Module.Basis ι ℤ M) →
            (h : Module.finrank ℤ ↥N = Module.finrank ℤ M) →
              M ⧸ N ≃+ ((i : ι) → ZMod (Submodule.smithNormalFormCoeffs b h i).natAbs)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.basisSet : {ι : Type u_3} → {s : Set (ι → ℕ)} → IsProperLinearSet s → [Finite ι] → Set (ι → ℕ)
-- Mathlib.Topology.Path
Path.refl_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X) (x_1 : ↑unitInterval), (Path.refl x) x_1 = x
-- Aesop.Frontend.Attribute
Aesop.Frontend.AttrConfig.rules : Aesop.Frontend.AttrConfig → Array Aesop.Frontend.RuleExpr
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Drop the keys corresponding to the next `n` expressions.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.matchTreeStars.drop : List Lean.Meta.RefinedDiscrTree.Key →
  List Lean.Meta.RefinedDiscrTree.Key → ℕ → List Lean.Meta.RefinedDiscrTree.Key × List Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.add_mul_div_right : ∀ {R : Type u} [inst : EuclideanDomain R] (x y z : R), y ≠ 0 → y ∣ x → (x + z * y) / y = x / y + z
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyData.map_cyclesMap' : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (hl₁ : S₁.LeftHomologyData) (hl₂ : S₂.LeftHomologyData) (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] [inst_5 : hl₁.IsPreservedBy F] [inst_6 : hl₂.IsPreservedBy F],
  F.map (CategoryTheory.ShortComplex.cyclesMap' φ hl₁ hl₂) =
    CategoryTheory.ShortComplex.cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_roo_eq_zero_iff : ∀ {m n i : ℕ}, (m<...n).toArray[i]! = 0 ↔ n ≤ i + (m + 1)
-- Mathlib.Topology.Connected.LocallyConnected
/-- A product of preconnected, locally connected spaces is locally connected. Note that an
arbitrary product of locally connected spaces need not be locally connected, so the
preconnectedness assumption cannot be dropped entirely (though it can be dropped for finitely
many factors, see `Pi.locallyConnectedSpace_of_finite_not_preconnectedSpace`).  -/
Pi.locallyConnectedSpace : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), LocallyConnectedSpace (X i)]
  [∀ (i : ι), PreconnectedSpace (X i)], LocallyConnectedSpace ((i : ι) → X i)
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_shiftLeft : ∀ {w k : ℕ} (x : BitVec w) (i : ℕ), (x <<< i).getMsbD k = x.getMsbD (k + i)
-- Mathlib.Analysis.Matrix.Order
/-- `Matrix.trace` as a positive linear map.  -/
Matrix.tracePositiveLinearMap : (n : Type u_3) →
  (α : Type u_4) →
    (𝕜 : Type u_5) →
      [Fintype n] → [inst : Semiring α] → [inst_1 : RCLike 𝕜] → [inst_2 : Module α 𝕜] → Matrix n n 𝕜 →ₚ[α] 𝕜
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.jdecl.sizeOf_spec : ∀ (j : Lean.IR.JoinPointId) (xs : Array Lean.IR.Param) (v b : Lean.IR.FnBody),
  sizeOf (Lean.IR.FnBody.jdecl j xs v b) = 1 + sizeOf j + sizeOf xs + sizeOf v + sizeOf b
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_subset_Iic_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : LocallyFiniteOrder α],
  Finset.Icc a b ⊆ Finset.Iic b
-- Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Conv.Path.body.sizeOf_spec : ∀ (name : Lean.Name) (next : Mathlib.Tactic.Conv.Path),
  sizeOf (Mathlib.Tactic.Conv.Path.body name next) = 1 + sizeOf name + sizeOf next
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_alter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k k' : α} {f : Option β → Option β},
  Std.DTreeMap.Internal.Impl.contains k' (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl =
    if compare k k' = Ordering.eq then (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome
    else Std.DTreeMap.Internal.Impl.contains k' t
-- Mathlib.Topology.Order.LeftRightNhds
/-- The filter of left neighborhoods has a basis of closed intervals.  -/
nhdsLE_basis_Icc : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMinOrder α]
  [DenselyOrdered α] {a : α}, (nhdsWithin a (Set.Iic a)).HasBasis (fun x => x < a) fun x => Set.Icc x a
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShiftCore.zero : ∀ {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] {F₁ F₂ : CategoryTheory.Functor C D} {τ : F₁ ⟶ F₂} (A : Type u_5)
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A], CategoryTheory.NatTrans.CommShiftCore τ 0
-- Mathlib.LinearAlgebra.Matrix.ToLin
Algebra.smulTower_leftMulMatrix_algebraMap_eq : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring T]
  [inst_3 : Algebra R S] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [inst_6 : IsScalarTower R S T] {m : Type u_4}
  {n : Type u_5} [inst_7 : Fintype m] [inst_8 : Fintype n] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n]
  (b : Module.Basis m R S) (c : Module.Basis n S T) (x : S) (i j : m) (k : n),
  (Algebra.leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k) = (Algebra.leftMulMatrix b) x i j
-- Std.Http.Data.Status
Std.Http.instInhabitedStatus.default : Std.Http.Status
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β] {f : β → β}, (m.modify k f)[k]! = (Option.map f m[k]?).get!
-- Init.Data.List.Impl
List.replace_eq_replaceTR : @List.replace = @List.replaceTR
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I],
  LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval C) ↔
    LinearIndependent ℤ fun (p : ↑(Profinite.NobelingProof.GoodProducts.range C)) => ↑p
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.triangle : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ f₃ : α → E'},
  (fun x => f₁ x - f₂ x) =o[l] g → (fun x => f₂ x - f₃ x) =o[l] g → (fun x => f₁ x - f₃ x) =o[l] g
-- Plausible.Gen
/-- Execute a `Gen` inside the `IO` monad using `size` as the example size  -/
Plausible.Gen.run : {α : Type} → Plausible.Gen α → ℕ → IO α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α}, (Std.TreeMap.Raw.unitOfList l cmp)[k]! = ()
-- Mathlib.Order.Fin.Basic
Fin.succAboveOrderEmb_apply : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p.succAboveOrderEmb i = p.succAbove i
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- A substructure satisfying `AddMemClass` is closed under addition.  -/
AddMemClass.add_mem : ∀ {S : Type u_3} {M : outParam (Type u_4)} {inst : Add M} {inst_1 : SetLike S M} [self : AddMemClass S M] {s : S}
  {a b : M}, a ∈ s → b ∈ s → a + b ∈ s
-- Mathlib.Computability.Language
Language.nil_mem_one : ∀ {α : Type u_1}, [] ∈ 1
-- Mathlib.Tactic.MkIffOfInductiveProp
Mathlib.Tactic.MkIff.Shape.mk.sizeOf_spec : ∀ (variablesKept : List Bool) (neqs : Option ℕ),
  sizeOf { variablesKept := variablesKept, neqs := neqs } = 1 + sizeOf variablesKept + sizeOf neqs
-- Lean.Util.Recognizers
Lean.Expr.iff? : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.then.eq_5 : ∀ (f : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont),
  (Turing.ToPartrec.Cont.fix f k).then = fun k' => Turing.ToPartrec.Cont.fix f (k.then k')
-- Mathlib.Algebra.Group.Basic
div_eq_inv_mul : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α), a / b = b⁻¹ * a