mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Lift a collection of morphisms to a morphism to the pullback.  -/
CategoryTheory.Limits.WidePullback.lift : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {B : C} →
        {objs : J → C} →
          {arrows : (j : J) → objs j ⟶ B} →
            [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] →
              {X : C} →
                (f : X ⟶ B) →
                  (fs : (j : J) → X ⟶ objs j) →
                    (∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) →
                      (X ⟶ CategoryTheory.Limits.widePullback B objs arrows)
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.Lex.wellFoundedLT_of_finite : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [Finite ι] [inst_2 : (i : ι) → Zero (α i)]
  [inst_3 : (i : ι) → LT (α i)] [hwf : ∀ (i : ι), WellFoundedLT (α i)], WellFoundedLT (Lex (Π₀ (i : ι), α i))
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeParams.capabilities : Lean.Lsp.InitializeParams → Lean.Lsp.ClientCapabilities
-- Lean.Parser.Term
Lean.Parser.Term.ident : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso_inv_naturality : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X₀ Y₀ : C₀}
  (f : X₀ ⟶ Y₀),
  CategoryTheory.CategoryStruct.comp (G₀.obj.map f.op)
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso data G₀ X₀).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso data G₀ Y₀).inv
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ (F.map f))
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.coveringNumber_two_mul_le_externalCoveringNumber : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal) (A : Set X),
  Metric.coveringNumber (2 * ε) A ≤ Metric.externalCoveringNumber ε A
-- Mathlib.Order.BoundedOrder.Basic
Pi.instTopForall.eq_1 : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Top (α' i)], Pi.instTopForall = { top := fun x => ⊤ }
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.models_formula_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : L.Formula α},
  T ⊨ᵇ φ ↔ ∀ (M : T.ModelType) (v : α → ↑M), φ.Realize v
-- Mathlib.Order.Interval.Set.Image
StrictMonoOn.image_Iio_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  StrictMonoOn f (Set.Iic b) → f '' Set.Iio b ⊆ Set.Iio (f b)
-- Lean.Meta.Instances
Lean.Meta.addInstanceEntry : Lean.Meta.Instances → Lean.Meta.InstanceEntry → Lean.Meta.Instances
-- Mathlib.Algebra.Order.Algebra
algebraMap_nonneg : ∀ {α : Type u_1} (β : Type u_2) [inst : CommSemiring α] [inst_1 : PartialOrder α] [inst_2 : Semiring β]
  [inst_3 : PartialOrder β] [inst_4 : Algebra α β] [ZeroLEOneClass β] [SMulPosMono α β] {a : α},
  0 ≤ a → 0 ≤ (algebraMap α β) a
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.lift_le_omega_natCast : ∀ {o : Ordinal.{u}} {n : ℕ}, Ordinal.lift.{v, u} o ≤ Ordinal.omega ↑n ↔ o ≤ Ordinal.omega ↑n
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mk.inj : ∀ {α : Type u_2} {inst : BooleanAlgebra α} {toSublattice : Sublattice α}
  {compl_mem' : ∀ {a : α}, a ∈ toSublattice.carrier → aᶜ ∈ toSublattice.carrier} {bot_mem' : ⊥ ∈ toSublattice.carrier}
  {toSublattice_1 : Sublattice α} {compl_mem'_1 : ∀ {a : α}, a ∈ toSublattice_1.carrier → aᶜ ∈ toSublattice_1.carrier}
  {bot_mem'_1 : ⊥ ∈ toSublattice_1.carrier},
  { toSublattice := toSublattice, compl_mem' := compl_mem', bot_mem' := bot_mem' } =
      { toSublattice := toSublattice_1, compl_mem' := compl_mem'_1, bot_mem' := bot_mem'_1 } →
    toSublattice = toSublattice_1
-- Init.Data.Slice.Array.Lemmas
Subarray.toList_mkSlice_roi : ∀ {α : Type u_1} {xs : Subarray α} {lo : ℕ},
  Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) = List.drop (lo + 1) (Std.Slice.toList xs)
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
/-- A finite-product-preserving presheaf is a sheaf for the extensive topology on a category which is
`FinitaryPreExtensive`.
 -/
CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.FinitaryPreExtensive C] {X : C}
  (S : CategoryTheory.Presieve X) [S.Extensive] (F : CategoryTheory.Functor Cᵒᵖ (Type w))
  [CategoryTheory.Limits.PreservesFiniteProducts F], CategoryTheory.Presieve.IsSheafFor F S
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.supSpanSingleton_apply_smul_self : ∀ {E : Type u_4} [inst : AddCommGroup E] {F : Type u_5} [inst_1 : AddCommGroup F] {K : Type u_7} {L : Type u_8}
  [inst_2 : DivisionRing K] [inst_3 : DivisionRing L] {σ : K →+* L} [inst_4 : Module K E] [inst_5 : Module L F]
  (f : E →ₛₗ.[σ] F) {x : E} (y : F) (hx : x ∉ f.domain) (c : K), ↑(f.supSpanSingleton x y hx) ⟨c • x, ⋯⟩ = σ c • y
-- Mathlib.Order.Filter.Germ.Basic
/-- **Alias** of the reverse direction of `Filter.Germ.coe_tendsto`. -/
Filter.Tendsto.germ_tendsto : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {lb : Filter β}, Filter.Tendsto f l lb → (↑f).Tendsto lb
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_eq_true : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr),
  (lhs.sub rhs).norm.isValidEq = true →
    (Int.Internal.Linear.Expr.denote ctx lhs = Int.Internal.Linear.Expr.denote ctx rhs) = True
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.isoOfEquivalence_hom_π_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasLimit F] {G : CategoryTheory.Functor K C}
  [inst_4 : CategoryTheory.Limits.HasLimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (k : K) {Z : C} (h : G.obj k ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfEquivalence e w).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G k) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F (e.inverse.obj k))
      (CategoryTheory.CategoryStruct.comp (w.inv.app (e.inverse.obj k))
        (CategoryTheory.CategoryStruct.comp (G.map (e.counit.app k)) h))
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic.0.ProbabilityTheory.HasIndepIncrements.indepFun_sub_sub.match_1_1.splitter : (motive : ℕ → Sort u_1) →
  (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((x : ℕ) → (x = 0 → False) → (x = 1 → False) → motive x) → motive x
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.image_rootSet_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 → ⇑(algebraMap A B) '' f.rootSet A = f.rootSet B
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.ext_iff : ∀ {X Y : TopCat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Lean.Environment
Lean.EffectiveImport.toImport : Lean.EffectiveImport → Lean.Import
-- Mathlib.Order.Hom.Basic
OrderIso.coe_symm_toEquiv : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), ⇑e.symm = ⇑e.symm
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.empty.nonempty_embedding_iff : ∀ {M : Type w} {N : Type w'} [inst : FirstOrder.Language.empty.Structure M]
  [inst_1 : FirstOrder.Language.empty.Structure N],
  Nonempty (FirstOrder.Language.empty.Embedding M N) ↔
    Cardinal.lift.{w', w} (Cardinal.mk M) ≤ Cardinal.lift.{w, w'} (Cardinal.mk N)
-- Mathlib.Dynamics.OmegaLimit
Flow.omegaLimit_image_subset : ∀ {τ : Type u_1} [inst : TopologicalSpace τ] [inst_1 : AddMonoid τ] {α : Type u_2} [inst_2 : TopologicalSpace α]
  (f : Filter τ) (ϕ : Flow τ α) (s : Set α) (t : τ),
  Filter.Tendsto (fun x => x + t) f f → omegaLimit f ϕ.toFun (ϕ.toFun t '' s) ⊆ omegaLimit f ϕ.toFun s
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- `AddMonoidAlgebra.map` of an injective function is injective.  -/
AddMonoidAlgebra.map_injective : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S),
  Function.Injective ⇑f → Function.Injective (AddMonoidAlgebra.map f)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffine_add : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Nonsingular P →
    W.Nonsingular Q →
      WeierstrassCurve.Jacobian.Point.toAffine W (W.add P Q) =
        WeierstrassCurve.Jacobian.Point.toAffine W P + WeierstrassCurve.Jacobian.Point.toAffine W Q
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.List.forIn'_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Mathlib.RingTheory.Algebraic.Defs
/-- An algebra is transcendental if some element is transcendental.  -/
Algebra.Transcendental : (R : Type u) → (A : Type v) → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → Prop
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.RightExactFunctor.whiskeringLeft_obj_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : C ⥤ᵣ D) {X Y : D ⥤ᵣ E} (f : X ⟶ Y),
  ((CategoryTheory.RightExactFunctor.whiskeringLeft C D E).obj F).map f =
    CategoryTheory.ObjectProperty.homMk (F.obj.whiskerLeft f.hom)
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_right_H : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ) (hpq : (c r).prev pq' = pq)
  (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq') [inst_3 : X.HasSpectralSequence data]
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData X data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀
          i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).right.H =
    X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedSymbolKind.default : Lean.Lsp.SymbolKind
-- Mathlib.Order.Minimal
OrderEmbedding.maximal_mem_image_iff : ∀ {α : Type u_2} {β : Type u_3} {a : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α ↪o β},
  a ∈ s → (Maximal (fun x => x ∈ ⇑f '' s) (f a) ↔ Maximal (fun x => x ∈ s) a)
-- Init.Data.Array.DecidableEq
_private.Init.Data.Array.DecidableEq.0.Array.isEqv.eq_1 : ∀ {α : Type u} (xs ys : Array α) (p : α → α → Bool),
  xs.isEqv ys p = if h : xs.size = ys.size then xs.isEqvAux ys h p xs.size ⋯ else false
-- Lean.Meta.Closure
Lean.Meta.Closure.mkNewLevelParam : Lean.Level → Lean.Meta.Closure.ClosureM Lean.Level
-- Mathlib.Control.Monad.Writer
/-- Capture the output produced by `f`, without intercepting.  -/
MonadWriter.listen : {ω : outParam (Type u)} → {M : Type u → Type v} → [self : MonadWriter ω M] → {α : Type u} → M α → M (α × ω)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ofBijective_apply_symm_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective ⇑f) (x : A₂),
  f ((AlgEquiv.ofBijective f hf).symm x) = x
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.of.eq_1 : ∀ {M : Type u_1}, MulArchimedeanOrder.of = Equiv.refl M
-- Mathlib.Analysis.Analytic.IsolatedZeros
HasFPowerSeriesAt.locally_zero_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜},
  HasFPowerSeriesAt f p z₀ → ((∀ᶠ (z : 𝕜) in nhds z₀, f z = 0) ↔ p = 0)
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.grind_ref.quot : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.instIsOverCompHomOfIsOver : ∀ {X Y Z S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] [inst_2 : Z.Over S] (f : X.PartialMap Y)
  (g : Y ⟶ Z) [AlgebraicGeometry.Scheme.PartialMap.IsOver S f] [AlgebraicGeometry.Scheme.Hom.IsOver g S],
  AlgebraicGeometry.Scheme.PartialMap.IsOver S (f.compHom g)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsCondKernelCDF.tendsto_atBot_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → StieltjesFunction ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsCondKernelCDF f κ ν → ∀ (p : α × β), Filter.Tendsto (↑(f p)) Filter.atBot (nhds 0)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.instIsIsoFunctorProdComparisonNatTransOfProdComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A : C)
  [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)],
  CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans F A)
-- Mathlib.Order.Monotone.Defs
/-- A function `f` is strictly monotone if `a < b` implies `f a < f b`.  -/
StrictMono : {α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → Prop
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.foldM : {α : Type u_1} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {β : Type v} → {m : Type v → Type w} → [Monad m] → (β → α → m β) → β → Lean.PersistentHashSet α → m β
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_eq_some_getD_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α} {fallback : β},
  t.contains a = true → Std.ExtDTreeMap.Const.get? t a = some (Std.ExtDTreeMap.Const.getD t a fallback)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.MorphismProperty.IsMonoidal.whiskerRight : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W : CategoryTheory.MorphismProperty C}
  {inst_1 : CategoryTheory.MonoidalCategory C} [self : W.IsMonoidal] {X₁ X₂ : C} (f : X₁ ⟶ X₂),
  W f → ∀ (Y : C), W (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y)
-- Init.Data.SInt.Lemmas
Int32.add_sub_cancel : ∀ (a b : Int32), a + b - b = a
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomMulAct.instMulActionAEEqFun.eq_1 : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : Monoid M] [inst_3 : MulAction M α] [inst_4 : MeasurableConstSMul M α]
  [inst_5 : MeasureTheory.SMulInvariantMeasure M α μ],
  DomMulAct.instMulActionAEEqFun = { toSMul := DomMulAct.instSMulAEEqFun, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Algebra.Order.Module.Field
inv_smul_lt_iff_of_neg : ∀ {𝕜 : Type u_1} {G : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup G] [inst_4 : PartialOrder G] [IsOrderedAddMonoid G] [inst_6 : Module 𝕜 G] {a : 𝕜} {b₁ b₂ : G}
  [PosSMulStrictMono 𝕜 G], a < 0 → (a⁻¹ • b₁ < b₂ ↔ a • b₂ < b₁)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqCompletionIdentifier : BEq Lean.Lsp.CompletionIdentifier
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.modPart_nonneg : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (r : ℚ), 0 ≤ PadicInt.modPart p r
-- Mathlib.GroupTheory.Focal
Subgroup.focalSubgroupOf.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.focalSubgroupOf = H.focalSubgroup.subgroupOf H
-- Init.Data.String.Decode
String.utf8EncodeCharFast.fun_cases_unfolding : ∀ (c : Char) (motive : List UInt8 → Prop),
  (have v := c.val;
    v ≤ 127 → motive [v.toUInt8]) →
    (have v := c.val;
      ¬v ≤ 127 → v ≤ 2047 → motive [(v >>> 6).toUInt8 &&& 31 ||| 192, v.toUInt8 &&& 63 ||| 128]) →
      (have v := c.val;
        ¬v ≤ 127 →
          ¬v ≤ 2047 →
            v ≤ 65535 →
              motive [(v >>> 12).toUInt8 &&& 15 ||| 224, (v >>> 6).toUInt8 &&& 63 ||| 128, v.toUInt8 &&& 63 ||| 128]) →
        (have v := c.val;
          ¬v ≤ 127 →
            ¬v ≤ 2047 →
              ¬v ≤ 65535 →
                motive
                  [(v >>> 18).toUInt8 &&& 7 ||| 240, (v >>> 12).toUInt8 &&& 63 ||| 128,
                    (v >>> 6).toUInt8 &&& 63 ||| 128, v.toUInt8 &&& 63 ||| 128]) →
          motive (String.utf8EncodeCharFast c)
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.startPos_matched : ∀ {s : String.Slice} {p q : s.Pos}, (String.Slice.Pattern.SearchStep.matched p q).startPos = p
-- Lean.Environment
Lean.instInhabitedAsyncConsts.default : Lean.AsyncConsts✝
-- Lean.Parser.Term
Lean.Parser.Term.bracketedBinderF : Lean.Parser.Parser
-- Aesop.Percent
Aesop.Percent.ofFloat : Float → Option Aesop.Percent
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.maxD_eq_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {km fallback : α}, t.maxD fallback = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.injective_iff_preservesEpimorphisms_yoneda_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : C),
  CategoryTheory.Injective J ↔ (CategoryTheory.yoneda.obj J).PreservesEpimorphisms
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.imp.injEq : ∀ (a a_1 a_2 a_3 : Mathlib.Tactic.ITauto.IProp), (a.imp a_1 = a_2.imp a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.quotDualCoannihilatorToDual_bijective : ∀ {K : Type u_4} {V : Type u_5} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (W : Subspace K (Module.Dual K V)) [FiniteDimensional K ↥W],
  Function.Bijective ⇑(Submodule.quotDualCoannihilatorToDual W)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- If `G` is a finite Galois group for `L/K`, then `L/K` is a Galois extension.  -/
IsGaloisGroup.isGalois : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [Finite G] [IsGaloisGroup G K L], IsGalois K L
-- Mathlib.Algebra.Group.Defs
AddCancelMonoid.toAddLeftCancelMonoid : {M : Type u} → [self : AddCancelMonoid M] → AddLeftCancelMonoid M
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.preimage_sup : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U V : Y.Opens},
  (TopologicalSpace.Opens.map f.base).obj (U ⊔ V) =
    (TopologicalSpace.Opens.map f.base).obj U ⊔ (TopologicalSpace.Opens.map f.base).obj V
-- Mathlib.Analysis.Complex.Basic
RCLike.map_nonneg_iff : ∀ {𝕜 : Type u_2} {𝕜' : Type u_3} [inst : RCLike 𝕜] [inst_1 : RCLike 𝕜'],
  RCLike.im RCLike.I = 1 → ∀ {a : 𝕜}, 0 ≤ (RCLike.map 𝕜 𝕜') a ↔ 0 ≤ a
-- Mathlib.Algebra.Order.Group.Abs
mabs_div_le_of_le_of_le : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b lb ub : G},
  lb ≤ a → a ≤ ub → lb ≤ b → b ≤ ub → |a / b|ₘ ≤ ub / lb
-- Init.Data.Order.Lemmas
Classical.Order.instMax : {α : Type u} → [LE α] → Max α
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.lintegral_comap : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {g : γ → α} (κ : ProbabilityTheory.Kernel α β) (hg : Measurable g) (c : γ)
  (g' : β → ENNReal), ∫⁻ (b : β), g' b ∂(κ.comap g hg) c = ∫⁻ (b : β), g' b ∂κ (g c)
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  (k : α) (f : β → β), m₁.Equiv m₂ → (m₁.modify k f).Equiv (m₂.modify k f)
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- An internal reflexive relation in the category of types gives rise to a standard reflexive
relation.  -/
TypeCat.refl_of_reflexiveRelation : ∀ {X R : Type w} {p₁ p₂ : R ⟶ X} (e : CategoryTheory.ReflexiveRelation p₁ p₂), Std.Refl (TypeCat.Rel.ofPair p₁ p₂)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `Bundle.Trivialization.localFrameCoeff`.

---

Coefficients of a section `s` of `V` w.r.t. the local frame `b.localFrame e i`.

If x is outside of `e.baseSet`, this returns the junk value 0.  -/
Bundle.Trivialization.localFrame_coeff : {𝕜 : 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] →
                                        [inst_13 : VectorBundle 𝕜 F V] →
                                          {ι : Type u_7} →
                                            (e : Bundle.Trivialization F Bundle.TotalSpace.proj) →
                                              [MemTrivializationAtlas e] →
                                                Module.Basis ι 𝕜 F →
                                                  [ContMDiffVectorBundle 1 F V I] → ι → (x : M) → V x →ₗ[𝕜] 𝕜