mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.trans : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x y z : CommRingCat.Colimits.Prequotient F) (x_1 : CommRingCat.Colimits.Relation F x y)
  (x_2 : CommRingCat.Colimits.Relation F y z),
  CommRingCat.Colimits.Relation.below x_1 →
    motive x y x_1 → CommRingCat.Colimits.Relation.below x_2 → motive y z x_2 → CommRingCat.Colimits.Relation.below ⋯
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.alter.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Lean.DocString.Types
Lean.Doc.Inline.image.injEq : ∀ {i : Type u} (alt url alt_1 url_1 : String),
  (Lean.Doc.Inline.image alt url = Lean.Doc.Inline.image alt_1 url_1) = (alt = alt_1 ∧ url = url_1)
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.SublistForall₂.prod_le_prod' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulRightMono M] [MulLeftMono M] {l₁ l₂ : List M},
  List.SublistForall₂ (fun x1 x2 => x1 ≤ x2) l₁ l₂ → (∀ a ∈ l₂, 1 ≤ a) → l₁.prod ≤ l₂.prod
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- The gluing of two precylinders.  -/
HomotopicalAlgebra.Precylinder.trans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      (P P' : HomotopicalAlgebra.Precylinder A) →
        [CategoryTheory.Limits.HasPushout P.i₁ P'.i₀] → HomotopicalAlgebra.Precylinder A
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
/-- (Implementation) This is the bifunctor we will apply "filtered colimits commute with finite
limits" to.  -/
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange : {C : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    (A : CategoryTheory.Functor Cᵒᵖ (Type u)) →
      {J : Type} →
        [inst_1 : CategoryTheory.SmallCategory J] →
          CategoryTheory.Functor J Cᵒᵖ →
            CategoryTheory.Functor J
              (CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) (Type u))
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Path.congr_arrow : ∀ {X : SSet} {n : ℕ} {f g : X.Path n}, f = g → ∀ (i : Fin n), f.arrow i = g.arrow i
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.trW.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) {T : CategoryTheory.Pretriangulated.Triangle C},
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → P T.obj₃ → P.trW T.mor₁
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      k ∈ Std.DTreeMap.Raw.Const.alter t k f ↔ (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true
-- Mathlib.Algebra.Group.Irreducible.Lemmas
Irreducible.not_isSquare : ∀ {M : Type u_2} [inst : Monoid M] {x : M}, Irreducible x → ¬IsSquare x
-- Lean.Meta.Closure
Lean.Meta.Closure.Context.mk.sizeOf_spec : ∀ (zetaDelta : Bool), sizeOf { zetaDelta := zetaDelta } = 1 + sizeOf zetaDelta
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualLift_rightInverse : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (W : Subspace K V),
  Function.RightInverse ⇑W.dualLift ⇑(Submodule.dualRestrict W)
-- Batteries.Data.AssocList
Batteries.AssocList.foldl.eq_1 : ∀ {δ : Type u_1} {α : Type u_2} {β : Type u_3} (f : δ → α → β → δ) (init : δ) (as : Batteries.AssocList α β),
  Batteries.AssocList.foldl f init as = (Batteries.AssocList.foldlM (fun d a b => pure (f d a b)) init as).run
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
EulerSine.antideriv_sin_comp_const_mul : ∀ {z : ℂ}, z ≠ 0 → ∀ (x : ℝ), HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
-- Mathlib.Data.Finset.Insert
/-- **Alias** of the forward direction of `Finset.nonempty_iff_eq_singleton_default`. -/
Finset.Nonempty.eq_singleton_default : ∀ {α : Type u_1} [inst : Unique α] {s : Finset α}, s.Nonempty → s = {default}
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.eq_1 : ∀ {L : FirstOrder.Language} {α : Type w} {n : ℕ} (T : L.Theory) (φ ψ : L.BoundedFormula α n), T.Iff φ ψ = T ⊨ᵇ φ.iff ψ
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.reindexₐ_apply : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {A : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid A] [inst_4 : Mul A] [inst_5 : Star A] [inst_6 : Module R A] {e : m ≃ n}
  {M : CStarMatrix m m A} {i j : n}, (CStarMatrix.reindexₐ R A e) M i j = (Matrix.reindex e e) M i j
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- **Alias** of the reverse direction of `hasDerivWithinAt_add_const_iff`. -/
HasDerivWithinAt.add_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F),
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => f x + c) f' s x
-- Mathlib.Algebra.DirectSum.Ring
_private.Mathlib.Algebra.DirectSum.Ring.0.DirectSum.mul_assoc : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] (a b c : DirectSum ι fun i => A i), a * b * c = a * (b * c)
-- Init.Data.Nat.Lemmas
/-- See `forall_lt_succ_left'` for a variant where `p` takes the bound as an argument.  -/
Nat.forall_lt_succ_left : ∀ {n : ℕ} {p : ℕ → Prop}, (∀ m < n + 1, p m) ↔ p 0 ∧ ∀ m < n, p (m + 1)
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (P : CategoryTheory.Functor Cᵒᵖ A),
  (Φ.presheafFiberCocone P).pt = Φ.presheafFiber.obj P
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.mapComp'.eq_1 : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (h : CategoryTheory.CategoryStruct.comp f g = fg),
  F.mapComp' f g fg h = CategoryTheory.CategoryStruct.comp (F.mapComp f g) (F.map₂ (CategoryTheory.eqToHom ⋯))
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_obj₁ : ∀ {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) (a b : ℤ) (h : a + 1 = b) (j : C),
  ((t.triangleLEGE a b h).obj j).obj₁ = (t.truncLE a).obj j
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `LinearMap.ofIsCompl_apply_left`. -/
LinearMap.ofIsCompl_left_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (h : IsCompl p q) {φ : ↥p →ₗ[R] F}
  {ψ : ↥q →ₗ[R] F} (u : ↥p), (LinearMap.ofIsCompl h φ ψ) ↑u = φ u
-- Mathlib.Algebra.Group.Hom.Basic
/-- Given a zero-preserving morphism `f`,
`-f` is the zero-preserving morphism sending `x` to `-f x`.  -/
ZeroHom.instNeg : {M : Type u_2} → {N : Type u_3} → [inst : Zero M] → [inst_1 : NegZeroClass N] → Neg (ZeroHom M N)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.reverseAux.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) → ((r : List α) → motive [] r) → ((a : α) → (l r : List α) → motive (a :: l) r) → motive x x_1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.DelayedTheoremInstance.generation : Lean.Meta.Grind.DelayedTheoremInstance → ℕ
-- Mathlib.MeasureTheory.MeasurableSpace.Card
MeasurableSpace.compl_mem_generateMeasurableRec : ∀ {α : Type u} {s : Set (Set α)} {i j : Ordinal.{u_1}},
  j < i → ∀ {t : Set α}, t ∈ MeasurableSpace.generateMeasurableRec s j → tᶜ ∈ MeasurableSpace.generateMeasurableRec s i
-- Mathlib.Order.SuccPred.Limit
IsMin.not_isSuccLimit : ∀ {α : Type u_1} {a : α} [inst : Preorder α], IsMin a → ¬Order.IsSuccLimit a
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.single_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i i' : ι} {b : β i},
  (fun₀ | i => b) i' = if h : i = i' then Eq.recOn h b else 0
-- Mathlib.Geometry.Manifold.Instances.Sphere
OrthonormalBasis.fromOrthogonalSpanSingleton.congr_simp : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (n : ℕ) [inst_3 : Fact (Module.finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0),
  OrthonormalBasis.fromOrthogonalSpanSingleton n hv = OrthonormalBasis.fromOrthogonalSpanSingleton n hv
-- Batteries.Tactic.Lint.Frontend
Batteries.Tactic.Lint.instReprLintVerbosity.repr : Batteries.Tactic.Lint.LintVerbosity → ℕ → Std.Format
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_pair : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] (a b : α), sInf {a, b} = a ⊓ b
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Filter.EventuallyEq.iteratedDerivWithin_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} {f g : 𝕜 → F},
  f =ᶠ[nhdsWithin x s] g → f x = g x → iteratedDerivWithin n f s x = iteratedDerivWithin n g s x
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.restrictScalarsIsometry_toLinearMap : ∀ (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_6) [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ] (𝕜' : Type u_9)
  [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜' 𝕜] [inst_7 : NormedSpace 𝕜' E]
  [inst_8 : IsScalarTower 𝕜' 𝕜 E] [inst_9 : NormedSpace 𝕜' Fₗ] [inst_10 : IsScalarTower 𝕜' 𝕜 Fₗ] {𝕜'' : Type u_10}
  [inst_11 : Ring 𝕜''] [inst_12 : Module 𝕜'' Fₗ] [inst_13 : ContinuousConstSMul 𝕜'' Fₗ]
  [inst_14 : SMulCommClass 𝕜 𝕜'' Fₗ] [inst_15 : SMulCommClass 𝕜' 𝕜'' Fₗ],
  (ContinuousLinearMap.restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'').toLinearMap =
    ContinuousLinearMap.restrictScalarsₗ 𝕜 E Fₗ 𝕜' 𝕜''
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.leftComm_symm_tmul : ∀ (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] (m : M) (n : N) (p : P),
  (TensorProduct.leftComm R M N P).symm (n ⊗ₜ[R] (m ⊗ₜ[R] p)) = m ⊗ₜ[R] (n ⊗ₜ[R] p)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightKind.write.sizeOf_spec : sizeOf Lean.Lsp.DocumentHighlightKind.write = 1
-- Mathlib.Algebra.Homology.DerivedCategory.KInjective
CochainComplex.IsKInjective.Qh_map_bijective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (K : HomotopyCategory C (ComplexShape.up ℤ)) (L : CochainComplex C ℤ)
  [L.IsKInjective], Function.Bijective DerivedCategory.Qh.map
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.ofBijective_apply_symm_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {n : N} (f : M →+ N)
  (hf : Function.Bijective ⇑f), f ((AddEquiv.ofBijective f hf).symm n) = n
-- Mathlib.Order.Filter.Cofinite
/-- The pullback of the `Filter.cofinite` under an injective function is equal to `Filter.cofinite`.
See also `Filter.comap_cofinite_le` and `Function.Injective.tendsto_cofinite`.  -/
Function.Injective.comap_cofinite_eq : ∀ {α : Type u_2} {β : Type u_3} {f : α → β}, Function.Injective f → Filter.comap f Filter.cofinite = Filter.cofinite
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
MvPowerSeries.gaussNorm_nonneg : ∀ {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) (f : MvPowerSeries σ R) [inst : Semiring R],
  (∀ (a : R), v a ≥ 0) → 0 ≤ MvPowerSeries.gaussNorm v c f
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.mapToSubgraph.eq_2 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (v_3 : V) (h : G.Adj u v_3) (p : G.Walk v_3 v),
  (SimpleGraph.Walk.cons h p).mapToSubgraph =
    SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.map (SimpleGraph.Subgraph.inclusion ⋯) p.mapToSubgraph)
-- Mathlib.Topology.DenseEmbedding
Dense.isDenseEmbedding_val : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, Dense s → IsDenseEmbedding Subtype.val
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Standard formula, computing the Laplacian from the standard orthonormal basis of a real inner
product space.
 -/
InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] (f : E → F),
  Laplacian.laplacian f = fun x =>
    ∑ i, (iteratedFDeriv ℝ 2 f x) ![(stdOrthonormalBasis ℝ E) i, (stdOrthonormalBasis ℝ E) i]
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.isBoundedUnder_le_iff : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α},
  f' =Θ[l] g' →
    (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f') ↔
      Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ g'))
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.ssubset_indep : ∀ {α : Type u_1} {M : Matroid α} {C X : Set α}, M.IsCircuit C → X ⊂ C → M.Indep X
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- If `P` is separated for `R` and every family has an amalgamation, then `P` is a sheaf for `R`.
 -/
CategoryTheory.Presieve.IsSeparatedFor.isSheafFor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X},
  CategoryTheory.Presieve.IsSeparatedFor P R →
    (∀ (x : CategoryTheory.Presieve.FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) →
      CategoryTheory.Presieve.IsSheafFor P R
-- Std.Data.HashMap.Lemmas
Std.HashMap.equiv_empty_iff_isEmpty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.Equiv ∅ ↔ m.isEmpty = true
-- Mathlib.Topology.VectorBundle.Hom
hom_trivializationAt_source : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] [inst_13 : (x : B) → TopologicalSpace (E₁ x)] [inst_14 : FiberBundle F₁ E₁]
  [inst_15 : VectorBundle 𝕜₁ F₁ E₁] [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂]
  [inst_18 : VectorBundle 𝕜₂ F₂ E₂] [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [inst_21 : RingHomIsometric σ] (x₀ : B),
  (trivializationAt (F₁ →SL[σ] F₂) (fun x => E₁ x →SL[σ] E₂ x) x₀).source =
    Bundle.TotalSpace.proj ⁻¹' ((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.one_le_coe : ∀ {α : Type u} [inst : One α] {a : α} [inst_1 : LE α], 1 ≤ ↑a ↔ 1 ≤ a
-- Mathlib.Topology.JacobsonSpace
JacobsonSpace.closure_inter_closedPoints_eq_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [JacobsonSpace X] {S : Set X},
  IsLocallyClosed S → closure (S ∩ closedPoints X) = closure S
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_comm : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β)
  (t : Finset γ) (f : β → γ → α), (s.sup fun b => t.sup (f b)) = t.sup fun c => s.sup fun b => f b c
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `lipschitzOnWith_neg_iff`. -/
LipschitzOnWith.of_neg : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal}
  {f : α → E} {s : Set α}, LipschitzOnWith K (-f) s → LipschitzOnWith K f s
-- Lean.Expr
/-- Return the function (name) and arguments of an application.  -/
Lean.Expr.getAppFnArgs : Lean.Expr → Lean.Name × Array Lean.Expr
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.comap_nhds_le : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ (x : α), Filter.comap f (nhds (f x)) ≤ nhds x
-- Lean.Parser.Term
Lean.Parser.Term.matchAlts : optParam Lean.Parser.Parser Lean.Parser.termParser → Lean.Parser.Parser
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.equiv_iff_toListModel_perm : ∀ {α : Type u} {β : α → Type v} {t t' : Std.DTreeMap.Internal.Impl α β}, t.Equiv t' ↔ t.toListModel.Perm t'.toListModel
-- Mathlib.Order.Defs.PartialOrder
Preorder.toLT : {α : Type u_2} → [self : Preorder α] → LT α
-- Init.Data.String.Lemmas.Iterate
String.Slice.forIn_eq_forIn_chars : ∀ {β : Type u} {m : Type u → Type v} [inst : Monad m] {s : String.Slice} {b : β} {f : Char → β → m (ForInStep β)},
  forIn s b f = forIn s.chars b f
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abv_mul : ∀ {S : Type u_5} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_6} [inst_2 : Semiring R] (abv : R → S)
  [IsAbsoluteValue abv] (x y : R), abv (x * y) = abv x * abv y
-- Mathlib.Tactic.Ring.RingNF
_private.Mathlib.Tactic.Ring.RingNF.0.Mathlib.Tactic.RingNF.instEvalExprConfig_1 : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.RingNF.Config
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.toMonoidHom_apply : ∀ (R : Type u_1) (G : Type u_2) (V : Type u_3) [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V] (π : ContRepresentation R G V)
  (g : G), π.toMonoidHom g = π g
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.shortExact_shortComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C), Φ.shortComplex.ShortExact
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.prime : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m)
  (q :
    ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
            (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace),
  (AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal f_deg hm q).IsPrime
-- Mathlib.AlgebraicTopology.SingularHomology.Basic
AlgebraicTopology.singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (n : ℕ) (R : C) (X : TopCat) [TotallyDisconnectedSpace ↑X],
  n ≠ 0 → HomologicalComplex.ExactAt (((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj X) n
-- Mathlib.RingTheory.RootsOfUnity.Basic
instSubsingletonSubtypeUnitsMemSubgroupRootsOfUnityOfNatNat : ∀ {M : Type u_1} [inst : CommMonoid M], Subsingleton ↥(rootsOfUnity 1 M)
-- Mathlib.Algebra.Order.Floor.Defs
Int.floorRing_ceil_eq : @FloorRing.ceil = @Int.ceil
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `BitVec.toNat`.  -/
BitVec.reduceToNat : Lean.Meta.Simp.DSimproc
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_monadLift_StateT_apply : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α σ : Type u}
  {epost : EPred} (x : m α) (post : α → σ → Pred),
  Lean.Order.PartialOrder.rel (fun s => Std.Internal.Do.wp x (fun a => post a s) epost)
    (Std.Internal.Do.wp (MonadLift.monadLift x) post epost)
-- Mathlib.CategoryTheory.Category.ULift
/-- The functorial version of `ULift.down`.  -/
CategoryTheory.ULift.downFunctor : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor (ULift.{u₂, u₁} C) C
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.symmetryEquiv_symm_apply_coe : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂)
  (c₁₂ : ComplexShape I₁₂) [inst : TotalComplexShape c₁ c₂ c₁₂] [inst_1 : TotalComplexShape c₂ c₁ c₁₂]
  [inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂] (j : I₁₂) (x : ↑(c₁.π c₂ c₁₂ ⁻¹' {j})),
  ↑((c₁.symmetryEquiv c₂ c₁₂ j).symm x) = (x.1.2, x.1.1)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.image_eq_target_inter_inv_preimage : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {s : Set α}, s ⊆ e.source → ↑e '' s = e.target ∩ ↑e.symm ⁻¹' s
-- Mathlib.Order.Category.Lat
Lat.hasForgetToPartOrd : CategoryTheory.HasForget₂ Lat PartOrd
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        {d e : CategoryTheory.Factorisation f} →
          (h : d.mid ⟶ e.mid) →
            autoParam (CategoryTheory.CategoryStruct.comp d.ι h = e.ι) CategoryTheory.Factorisation.Hom.ι_h._autoParam →
              autoParam (CategoryTheory.CategoryStruct.comp h e.π = d.π)
                  CategoryTheory.Factorisation.Hom.h_π._autoParam →
                d.Hom e
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.CallHierarchy.mk.inj : ∀ {item : Lean.Lsp.CallHierarchyItem} {fromRanges : Array Lean.Lsp.Range} {children : Array Lean.Lsp.Ipc.CallHierarchy}
  {item_1 : Lean.Lsp.CallHierarchyItem} {fromRanges_1 : Array Lean.Lsp.Range}
  {children_1 : Array Lean.Lsp.Ipc.CallHierarchy},
  { item := item, fromRanges := fromRanges, children := children } =
      { item := item_1, fromRanges := fromRanges_1, children := children_1 } →
    item = item_1 ∧ fromRanges = fromRanges_1 ∧ children = children_1
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
Filter.EventuallyEq.iteratedFDerivWithin' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E}
  {f f₁ : E → F} {x : E},
  f₁ =ᶠ[nhdsWithin x s] f →
    t ⊆ s → ∀ (n : ℕ), iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[nhdsWithin x s] iteratedFDerivWithin 𝕜 n f t
-- Mathlib.Algebra.Group.Action.Units
AddUnits.instVAdd.eq_1 : ∀ {M : Type u_3} {α : Type u_5} [inst : AddMonoid M] [inst_1 : VAdd M α],
  AddUnits.instVAdd = { vadd := fun m a => ↑m +ᵥ a }