mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.ComposableArrows.twoδ₁Toδ₀.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i j k : C} (f f_1 : i ⟶ j) (e_f : f = f_1) (g : j ⟶ k)
  (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg),
  CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h = CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f_1 g fg ⋯
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioo_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Ioo a b)), Subtype.val '' Set.Ici c = Set.Ico (↑c) b
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- An embedding into `ℂ` is real if it is fixed by complex conjugation.  -/
NumberField.ComplexEmbedding.IsReal : {K : Type u_1} → [inst : Field K] → (K →+* ℂ) → Prop
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.associator_eqToHom_inv_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y z t : B} (e₁ : x = y) (e₂ : y = z) (e₃ : z = t) {Z : x ⟶ t}
  (h :
    CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom e₁) (CategoryTheory.eqToHom e₂))
        (CategoryTheory.eqToHom e₃) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.eqToHom e₁) (CategoryTheory.eqToHom e₂)
          (CategoryTheory.eqToHom e₃)).inv
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.eqToHom e₁)
        (CategoryTheory.Bicategory.eqToHomTransIso e₂ e₃).inv)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.eqToHomTransIso e₁ ⋯).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.eqToHomTransIso ⋯ e₃).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.eqToHomTransIso e₁ e₂).hom
              (CategoryTheory.eqToHom e₃))
            h)))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_erase_eq_iff_not_compare_eq_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, (t.erase k).minKey he = t.minKey ⋯ ↔ ¬cmp k (t.minKey ⋯) = Ordering.eq
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_div : ∀ (a b : UInt16), (a / b).toUInt64 = a.toUInt64 / b.toUInt64
-- Mathlib.Topology.Maps.Basic
isOpenMap_iff_nhds_le : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f ↔ ∀ (x : X), nhds (f x) ≤ Filter.map f (nhds x)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppMatchState.info : Lean.PrettyPrinter.Delaborator.AppMatchState → Lean.Meta.MatcherInfo
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous₂.uniformContinuous : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {f : α → β → γ}, UniformContinuous₂ f → UniformContinuous (Function.uncurry f)
-- Init.Data.String.Lemmas.FindPos
String.Pos.toSlice_prevn : ∀ {n : ℕ} {s : String} {p : s.Pos}, (p.prevn n).toSlice = p.toSlice.prevn n
-- Mathlib.Data.DFinsupp.Lex
/-- The partial order on `DFinsupp`s obtained by the colexicographic ordering.
See `DFinsupp.Colex.linearOrder` for a proof that this partial order is in fact linear.  -/
DFinsupp.Colex.partialOrder : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] →
      [LinearOrder ι] → [(i : ι) → PartialOrder (α i)] → PartialOrder (Colex (Π₀ (i : ι), α i))
-- Mathlib.Data.Finset.Update
/-- If one replaces the variable indexed by `i`, then `f` no longer depends on
this variable.  -/
DependsOn.update : ∀ {ι : Type u_2} {π : ι → Type u_3} [inst : DecidableEq ι] {α : Type u_1} {f : ((i : ι) → π i) → α} {s : Finset ι},
  DependsOn f ↑s → ∀ (i : ι) (y : π i), DependsOn (fun x => f (Function.update x i y)) ↑(s.erase i)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- The definition of uniform integrable in mathlib is equivalent to the definition commonly
found in literature.  -/
MeasureTheory.uniformIntegrable_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β} [MeasureTheory.IsFiniteMeasure μ],
  1 ≤ p →
    p ≠ ⊤ →
      (MeasureTheory.UniformIntegrable f p μ ↔
        (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) ∧
          ∀ (ε : ℝ),
            0 < ε → ∃ C, ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε)
-- Mathlib.SetTheory.Ordinal.Notation
NONote.instWellFoundedRelation : WellFoundedRelation NONote
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rco.Internal.toArray_eq_toArray_iter : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rco α},
  r.toArray = (Std.Rco.Internal.iter r).toArray
-- Mathlib.Order.Cover
WCovBy.le_and_le_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {a b c : α}, a ⩿ b → (a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b)
-- Mathlib.Algebra.Module.SpanRank
Submodule.le_spanRank_restrictScalars : ∀ {R : Type u_1} {S : Type u_2} {M : Type u} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] (N : Submodule S M),
  N.spanRank ≤ (Submodule.restrictScalars R N).spanRank
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Data exhibiting that a given factorisation through a mono is initial.  -/
CategoryTheory.Limits.IsImage.lift_fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F : CategoryTheory.Limits.MonoFactorisation f} (self : CategoryTheory.Limits.IsImage F)
  (F' : CategoryTheory.Limits.MonoFactorisation f) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.lift F') (CategoryTheory.CategoryStruct.comp F'.m h) =
    CategoryTheory.CategoryStruct.comp F.m h
-- Mathlib.Tactic.Push
Mathlib.Tactic.Push.Config.mk.injEq : ∀ (distrib distrib_1 : Bool), ({ distrib := distrib } = { distrib := distrib_1 }) = (distrib = distrib_1)
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Get the `BinderInfo`s for the arguments of `mkAppN fn args`.  -/
Mathlib.Tactic.LibraryRewrite.getBinderInfos : Lean.Expr → Array Lean.Expr → Lean.MetaM (Array Lean.BinderInfo)
-- Mathlib.CategoryTheory.Functor.Trifunctor
/-- Given two bifunctors `F : C₁ ⥤ C₂₃ ⥤ C₄` and `G₂₃ : C₂ ⥤ C₃ ⥤ C₄`, this is
the trifunctor `C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄` obtained by composition.  -/
CategoryTheory.bifunctorComp₂₃ : {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₂₃] →
                    CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄) →
                      CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃) →
                        CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instPowNat : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → Pow (FractionalIdeal S P) ℕ
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPPrivateNames : Lean.Options → Bool
-- Mathlib.Topology.Order.LeftRightNhds
nhds_basis_Ioo_pos : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α] [IsOrderedAddMonoid α]
  [OrderTopology α] [NoMaxOrder α] (a : α), (nhds a).HasBasis (fun ε => 0 < ε) fun ε => Set.Ioo (a - ε) (a + ε)
-- Mathlib.Probability.Kernel.Composition.Comp
/-- Composition of two kernels.  -/
ProbabilityTheory.Kernel.comp : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mγ : MeasurableSpace γ} →
            ProbabilityTheory.Kernel β γ → ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel α γ
-- Lean.Meta.Sym.Simp.SimpM
/-- Maximum number of steps that can be performed by the simplifier.  -/
Lean.Meta.Sym.Simp.Config.maxSteps : Lean.Meta.Sym.Simp.Config → ℕ
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.mdifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} (Φ : PartialDiffeomorph I J M N n),
  n ≠ 0 → ∀ {x : M}, x ∈ Φ.source → MDiffAt ↑Φ.toPartialEquiv x
-- Mathlib.Topology.Separation.Basic
inseparable_eq_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X], Inseparable = Eq
-- Mathlib.Topology.Sheaves.Limits
TopCat.instHasLimitsOfSizeSheafOfHasLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] (X : TopCat),
  CategoryTheory.Limits.HasLimitsOfSize.{v, v, v, max v u} (TopCat.Sheaf C X)
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeries_def : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (k : ℕ),
  LieAlgebra.derivedSeries R L k = LieAlgebra.derivedSeriesOfIdeal R L k ⊤
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.modify.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α] (m : Std.DHashMap.Raw α β)
  (a : α) (f : β a → β a),
  m.modify a f = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.modify ⟨m, h⟩ a f) else ∅
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.cancelDen.inj : ∀ {c : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr} {val : ℤ} {x n : Lean.Grind.Linarith.Var}
  {c_1 : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr} {val_1 : ℤ} {x_1 n_1 : Lean.Grind.Linarith.Var},
  Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.cancelDen c val x n =
      Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.cancelDen c_1 val_1 x_1 n_1 →
    c = c_1 ∧ val = val_1 ∧ x = x_1 ∧ n = n_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α},
  t.WF → (k ∈ Std.TreeMap.Raw.filterMap f t ↔ ∃ (g : k ∈ t), (f (t.getKey k g) t[k]).isSome = true)
-- Mathlib.Data.Finsupp.Defs
Finsupp.instDecidableEq : {α : Type u_1} → {M : Type u_4} → [inst : Zero M] → [DecidableEq α] → [DecidableEq M] → DecidableEq (α →₀ M)
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.denote.eq_2 : ∀ (ctx : Int.Internal.Linear.Context) (a b : Int.Internal.Linear.Expr),
  Int.Internal.Linear.Expr.denote ctx (a.sub b) =
    Int.Internal.Linear.Expr.denote ctx a - Int.Internal.Linear.Expr.denote ctx b
-- Init.Data.Range.Polymorphic.UpwardEnumerable
_private.Init.Data.Range.Polymorphic.UpwardEnumerable.0.Std.PRange.UpwardEnumerable.least.eq_1 : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerableLeast? α] [hn : Nonempty α],
  Std.PRange.UpwardEnumerable.least = Std.PRange.least?.get ⋯
-- Mathlib.LinearAlgebra.RootSystem.RootPairingCat
/-- Objects in the category of root pairings.  -/
RootPairingCat : (R : Type u) → [CommRing R] → Type (max u (v + 1))
-- Mathlib.Algebra.Order.Group.End
RelEmbedding.coe_one : ∀ {α : Type u_1} {r : α → α → Prop}, ⇑1 = id
-- Mathlib.CategoryTheory.Join.Basic
/-- Composition in `C ⋆ D` is inherited from the compositions in `C` and `D`.  -/
CategoryTheory.Join.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → {x y z : CategoryTheory.Join C D} → x.Hom y → y.Hom z → x.Hom z
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find.congr_simp : ∀ {n : ℕ} (p p_1 : Fin n → Prop) (e_p : p = p_1) {inst : DecidablePred p} [inst_1 : DecidablePred p_1] (h : ∃ k, p k),
  Fin.find p h = Fin.find p_1 ⋯
-- Mathlib.Topology.Order.IsLUB
IsLUB.mem_closure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  IsLUB s a → s.Nonempty → a ∈ closure s
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_4} [inst_3 : NormedRing R] [inst_4 : Module R E] [IsBoundedSMul R E]
  {g : 𝕜 → E} [inst_6 : NormedAlgebra 𝕜 R] [IsScalarTower 𝕜 R E] {f : 𝕜 → R},
  Meromorphic f → Meromorphic g → Meromorphic (f • g)
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourierInv_congr_ae : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  {f₁ f₂ : V → E},
  f₁ =ᵐ[MeasureTheory.volume] f₂ → ∀ (x : V), FourierTransformInv.fourierInv f₁ x = FourierTransformInv.fourierInv f₂ x
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.mono_iff_cancel_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {Q R : C} (f : Q ⟶ R),
  CategoryTheory.Mono f ↔ ∀ (P : C) (g : P ⟶ Q), CategoryTheory.CategoryStruct.comp g f = 0 → g = 0
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is negative, then
`f` is a strictly antitone function.
Note that we don't require differentiability explicitly as it already implied by the derivative
being strictly negative.  -/
strictAnti_of_deriv_neg : ∀ {f : ℝ → ℝ}, (∀ (x : ℝ), deriv f x < 0) → StrictAnti f
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
TopCat.Sheaf.interUnionPullbackConeLift_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Sheaf C X)
  (U V : TopologicalSpace.Opens ↑X)
  (s :
    CategoryTheory.Limits.PullbackCone (F.obj.map (CategoryTheory.homOfLE ⋯).op)
      (F.obj.map (CategoryTheory.homOfLE ⋯).op)),
  CategoryTheory.CategoryStruct.comp (F.interUnionPullbackConeLift U V s) (F.obj.map (CategoryTheory.homOfLE ⋯).op) =
    s.fst
-- Mathlib.Logic.Nontrivial.Basic
/-- A pi type is nontrivial if it's nonempty everywhere and nontrivial somewhere.  -/
Pi.nontrivial_at : ∀ {I : Type u_3} {f : I → Type u_4} (i' : I) [inst : ∀ (i : I), Nonempty (f i)] [Nontrivial (f i')],
  Nontrivial ((i : I) → f i)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.restoreM_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α σ : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m (α × σ)),
  ⦃fun x_1 =>
    (Std.Do.wp x).apply
      (fun x =>
        match x with
        | (a, s) => Q.1 a s,
        Q.2)⦄
    MonadControl.restoreM x ⦃Q⦄
-- Init.Data.BitVec.Lemmas
BitVec.pow_succ : ∀ {w n : ℕ} {x : BitVec w}, x ^ (n + 1) = x ^ n * x
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterWithPostcondition.match_1.splitter : {β : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {f : β → Std.Iterators.PostconditionT n (ULift.{u_1, 0} Bool)} →
      (out : β) →
        (motive : Subtype (f out).Property → Sort u_3) →
          (__do_lift : Subtype (f out).Property) →
            ((h' : (f out).Property { down := false }) → motive ⟨{ down := false }, h'⟩) →
              ((h' : (f out).Property { down := true }) → motive ⟨{ down := true }, h'⟩) → motive __do_lift
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- The coefficients of `t` in a local frame at `x` only depend on `t` at `x`.  -/
IsLocalFrameOn.coeff_congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {n : WithTop ℕ∞} {x : M} {t t' : (x : M) → V x} (hs : IsLocalFrameOn I F n s u),
  t x = t' x → ∀ (i : ι), (hs.coeff i x) (t x) = (hs.coeff i x) (t' x)
-- Lean.Meta.Tactic.Grind.Types
/-- Key for the congruence table.
We need access to the `enodes` to be able to retrieve the equivalence class roots.
 -/
Lean.Meta.Grind.CongrKey : Lean.Meta.Grind.ENodeMap → Type
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.isColimit_precompose_iff : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes)
  {G : CategoryTheory.Functor J (Type w₀')} (e : (j : J) → G.obj j ≃ F.obj j)
  (naturality :
    ∀ {j j' : J} (f : j ⟶ j'),
      ⇑(e j') ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) =
        ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)),
  (c.precompose (fun {j'} => ⇑(e j')) ⋯).IsColimit ↔ c.IsColimit
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.mk.injEq : ∀ {X : SSet} {dim : ℕ} (simplex : X.obj (Opposite.op { len := dim })) (dim_1 : ℕ)
  (simplex_1 : X.obj (Opposite.op { len := dim_1 })),
  ({ dim := dim, simplex := simplex } = { dim := dim_1, simplex := simplex_1 }) = (dim = dim_1 ∧ simplex ≍ simplex_1)
-- Batteries.Tactic.Alias
/-- Forward direction of an iff alias  -/
Batteries.Tactic.Alias.AliasInfo.forward : Lean.Name → Batteries.Tactic.Alias.AliasInfo
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.not_bddAbove_of_tendsto_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {l : Filter α} [l.NeBot] {f : α → β} [NoMaxOrder β],
  Filter.Tendsto f l Filter.atTop → ¬BddAbove (Set.range f)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.addEntries.sizeOf_spec : ∀ (entries : Array Lean.Meta.SimpEntry),
  sizeOf (Lean.Elab.Tactic.ElabSimpArgResult.addEntries entries) = 1 + sizeOf entries
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.map_aroots_algebraMap : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDomain A]
  [inst_3 : Algebra R A] [inst_4 : CommRing B] [inst_5 : IsDomain B] [inst_6 : Algebra R B] [inst_7 : Algebra A B]
  [FaithfulSMul A B] [IsScalarTower R A B] {f : Polynomial R},
  (Polynomial.map (algebraMap R A) f).Splits → Multiset.map (⇑(algebraMap A B)) (f.aroots A) = f.aroots B
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.map_obj : ∀ {I : Type u_1} {J : Type u_2} (C : Type u_4) [inst : CategoryTheory.Category.{v_1, u_4} C] (p : I → J)
  [inst_1 : ∀ (j : J), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ↑(p ⁻¹' {j})) C]
  (X : CategoryTheory.GradedObject I C), (CategoryTheory.GradedObject.map C p).obj X = X.mapObj p
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.addCommMonoid.eq_1 : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  NonemptyInterval.addCommMonoid =
    { toAdd := instAddNonemptyInterval, add_assoc := ⋯, toZero := instZeroNonemptyInterval, zero_add := ⋯,
      add_zero := ⋯, toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯, add_comm := ⋯ }
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.mem_idealSet : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K}
  {J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))},
  x ∈ NumberField.mixedEmbedding.fundamentalCone.idealSet K J ↔
    x ∈ NumberField.mixedEmbedding.fundamentalCone K ∧ ∃ a ∈ ↑↑J, (NumberField.mixedEmbedding K) ↑a = x
-- Mathlib.Topology.ContinuousMap.LocallyConstant
/-- The inclusion of locally-constant functions into continuous
functions as an additive monoid hom.  -/
LocallyConstant.toContinuousMapAddMonoidHom : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        [inst_2 : AddMonoid Y] → [inst_3 : ContinuousAdd Y] → LocallyConstant X Y →+ C(X, Y)
-- Lean.Parser.Term
Lean.Parser.Term.optExprPrecedence.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.comap_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (J : CategoryTheory.Precoverage E),
  CategoryTheory.Precoverage.comap (F.comp G) J =
    CategoryTheory.Precoverage.comap F (CategoryTheory.Precoverage.comap G J)
-- Mathlib.Analysis.Normed.Group.Continuity
comap_norm_nhds_one : ∀ {E : Type u_4} [inst : SeminormedGroup E], Filter.comap norm (nhds 0) = nhds 1
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The angle between two vectors, with respect to an orientation given by `Orientation.map`
with a linear isometric equivalence, equals the angle between those two vectors, transformed by
the inverse of that equivalence, with respect to the original orientation.  -/
Orientation.oangle_map : ∀ {V : Type u_1} {V' : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedAddCommGroup V']
  [inst_2 : InnerProductSpace ℝ V] [inst_3 : InnerProductSpace ℝ V'] [inst_4 : Fact (Module.finrank ℝ V = 2)]
  [inst_5 : Fact (Module.finrank ℝ V' = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V') (f : V ≃ₗᵢ[ℝ] V'),
  ((Orientation.map (Fin 2) f.toLinearEquiv) o).oangle x y = o.oangle (f.symm x) (f.symm y)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.Proj.mul_apply : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ}
  (s t : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj V)) (x : ↥(Opposite.unop V)),
  ↑(s * t) x = ↑s x * ↑t x
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Zero is a left absorbing element for multiplication  -/
MonoidWithZero.zero_mul : ∀ {M₀ : Type u} [self : MonoidWithZero M₀] (a : M₀), 0 * a = 0
-- Mathlib.Tactic.NormNum.Inv
Mathlib.Meta.NormNum.isNNRat_inv_pos : ∀ {α : Type u_1} [inst : DivisionSemiring α] [CharZero α] {a : α} {n d : ℕ},
  Mathlib.Meta.NormNum.IsNNRat a n.succ d → Mathlib.Meta.NormNum.IsNNRat a⁻¹ d n.succ
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` preserves limits of shape `Jᵒᵖ`, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits of
shape `J`.  -/
CategoryTheory.Limits.preservesColimitsOfShape_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.PreservesColimitsOfShape J F.op
-- Mathlib.Data.Set.Lattice.Image
Set.iUnion_prod_const : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : Set β}, (⋃ i, s i) ×ˢ t = ⋃ i, s i ×ˢ t