mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasurableEmbedding.exists_stronglyMeasurable_extend : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {x : MeasurableSpace α} {x_1 : MeasurableSpace γ}
  [inst : TopologicalSpace β],
  MeasurableEmbedding g →
    MeasureTheory.StronglyMeasurable f →
      (∀ (a : γ), Nonempty β) → ∃ f', MeasureTheory.StronglyMeasurable f' ∧ f' ∘ g = f
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.isSome.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (val : α) (h_1 : (val : α) → motive (some val))
  (h_2 : Unit → motive none),
  (match some val with
    | some val => h_1 val
    | none => h_2 ()) =
    h_1 val
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- An equivalence of categories involving monoidal functors is monoidal if the underlying
adjunction satisfies certain compatibilities with respect to the monoidal functor data.  -/
CategoryTheory.Equivalence.IsMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (e : C ≌ D) → [e.functor.Monoidal] → [e.inverse.Monoidal] → Prop
-- Mathlib.Data.Set.Restrict
Set.domRestrict_ite : ∀ {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [inst : (x : α) → Decidable (x ∈ s)],
  (s.domRestrict fun a => if a ∈ s then f a else g a) = s.domRestrict f
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A countably compact set has a finite subcover for any countable open cover.  -/
IsCountablyCompact.elim_finite_subcover : ∀ {ι : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] {A : Set E},
  IsCountablyCompact A →
    ∀ [Countable ι] {U : ι → Set E}, (∀ (i : ι), IsOpen (U i)) → A ⊆ ⋃ i, U i → ∃ t, A ⊆ ⋃ i ∈ t, U i
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_le_maxKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false →
    ∀ {k : α} {v : β k} {fallback : α}, (cmp (t.maxKeyD fallback) ((t.insertIfNew k v).maxKeyD fallback)).isLE = true
-- Mathlib.Tactic.Simps.Basic
/-- Generated lemmas that are fully applied, i.e. generates equalities between applied functions.
Set this to `false` to generate equalities between functions.  -/
Simps.Config.fullyApplied : Simps.Config → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Path.arrow_interval : ∀ {X : SSet} {n : ℕ} (f : X.Path n) (j l : ℕ) (k' : Fin l) (k : Fin n)
  (h : autoParam (j + l ≤ n) SSet.Path.arrow_interval._auto_1),
  autoParam (j + ↑k' = ↑k) SSet.Path.arrow_interval._auto_3 → (f.interval j l h).arrow k' = f.arrow k
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement'_def : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.IsComplement' K ↔ AddSubgroup.IsComplement ↑H ↑K
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_filterMap : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.getD k fallback = ((t.get? k).bind (f k)).getD fallback
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.completedLFunction_zero : ∀ {N : ℕ} [inst : NeZero N] (s : ℂ), ZMod.completedLFunction 0 s = 0
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instInsertProd : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Insert (α × β) (Std.TreeMap.Raw α β cmp)
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.div_tendsto_atTop_zero_iff_degree_lt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Q ≠ 0 →
    (Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop (nhds 0) ↔ P.degree < Q.degree)
-- Init.Data.SInt.Basic
instReprISize : Repr ISize
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
/-- The induced map of the left projection map X × Y → X  -/
FundamentalGroupoidFunctor.projLeft : (A : TopCat) →
  (B : TopCat) →
    CategoryTheory.Functor ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B)))
      ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A)
-- Init.Prelude
/-- Function used for determining whether a syntax pattern `` `(id) `` is matched.
There are various conceivable notions of when two syntactic identifiers should be regarded as identical,
but semantic definitions like whether they refer to the same global name cannot be implemented without
context information (i.e. `MonadResolveName`). Thus in patterns we default to the structural solution
of comparing the identifiers' `Name` values, though we at least do so modulo macro scopes so that
identifiers that "look" the same match. This is particularly useful when dealing with identifiers that
do not actually refer to Lean bindings, e.g. in the `stx` pattern `` `(many($p)) ``.  -/
Lean.Syntax.matchesIdent : Lean.Syntax → Lean.Name → Bool
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_mul_right_one' : ∀ {α : Type u_2} [inst : Group α] {b : α}, (fun x => x * b⁻¹) ⁻¹' 1 = {b}
-- Mathlib.Data.Multiset.MapFold
Multiset.rel_map_left : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} {r : α → β → Prop} {s : Multiset γ} {f : γ → α} {t : Multiset β},
  Multiset.Rel r (Multiset.map f s) t ↔ Multiset.Rel (fun a b => r (f a) b) s t
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- If two measures coincide locally, then a set is everywhere positive for the former iff it is
everywhere positive for the latter.  -/
MeasureTheory.Measure.isEverywherePos_iff_of_forall_exists_nhds_eq : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ ν : MeasureTheory.Measure α} {s : Set α},
  (∀ x ∈ s, ∃ t ∈ nhds x, ∀ u ⊆ t, ν u = μ u) → (ν.IsEverywherePos s ↔ μ.IsEverywherePos s)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_natCast_mul : ∀ {x : ℝ}, 0 ≤ x → ∀ (n : ℕ) (z : ℝ), x ^ (↑n * z) = (x ^ n) ^ z
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Any.eq_1 : ∀ {α : Type u_1} (p : α → Prop), RBTree.RBNode.Any p RBTree.RBNode.nil = False
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.localTrivAt_apply_mk : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (b : B) (a : F), ↑(Z.localTrivAt b) ⟨b, a⟩ = (b, a)
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.instIsIsoPost : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesLimit F G]
  [inst_4 : CategoryTheory.Limits.HasLimit F], CategoryTheory.IsIso (CategoryTheory.Limits.limit.post F G)
-- Init.Data.UInt.Lemmas
USize.sub_zero : ∀ (a : USize), a - 0 = a
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The coefficient of a monomial in `(uniqueAlgEquiv R σ).symm P` is the coefficient of the
corresponding univariate monomial in `P`.  -/
MvPolynomial.coeff_uniqueAlgEquiv_symm : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] [inst_1 : Unique σ] (P : Polynomial R) (d : σ →₀ ℕ),
  MvPolynomial.coeff d ((MvPolynomial.uniqueAlgEquiv R σ).symm P) = P.coeff (d default)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  [inst_2 : CategoryTheory.IsSplitEpi f] {c : CategoryTheory.Limits.KernelFork f} (i : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel i).pt = X
-- Init.Data.Option.Basic
/-- Returns `true` on `some x` and `false` on `none`.  -/
Option.isSome : {α : Type u_1} → Option α → Bool
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) [inst_2 : S.HasRightHomology] {Z : C} (h_1 : h.Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.pOpcycles (CategoryTheory.CategoryStruct.comp h.opcyclesIso.hom h_1) =
    CategoryTheory.CategoryStruct.comp h.p h_1
-- Init.Data.Array.Zip
Array.zipWithAll_map_right : ∀ {α : Type u_1} {β β' : Type u_2} {γ : Type u_3} {as : Array α} {bs : Array β} {f : β → β'}
  {g : Option α → Option β' → γ},
  Array.zipWithAll g as (Array.map f bs) = Array.zipWithAll (fun a b => g a (f <$> b)) as bs
-- Mathlib.Algebra.Ring.ULift
/-- `ULift` is functorial for ring homomorphisms.  -/
RingHom.ulift : {R : Type u_1} →
  {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → ULift.{u₁, u_1} R →+* ULift.{u₂, u_2} S
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.distribSMul.eq_1 : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : DistribSMul N R],
  AddMonoidAlgebra.distribSMul = { toSMulZeroClass := AddMonoidAlgebra.smulZeroClass, smul_add := ⋯ }
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `monotone_dual_iff`. -/
Monotone.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Monotone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- An isomorphism of multilinear maps given an isomorphism between their codomains.

This is `Linear.compAlternatingMap` as an isomorphism,
and the alternating version of `LinearEquiv.multilinearMapCongrRight`.  -/
LinearEquiv.alternatingMapCongrRight : {ι : Type u_7} →
  {R' : Type u_10} →
    {M'' : Type u_11} →
      {N'' : Type u_13} →
        {N₂'' : Type u_14} →
          [inst : CommSemiring R'] →
            [inst_1 : AddCommMonoid M''] →
              [inst_2 : AddCommMonoid N''] →
                [inst_3 : AddCommMonoid N₂''] →
                  [inst_4 : Module R' M''] →
                    [inst_5 : Module R' N''] →
                      [inst_6 : Module R' N₂''] → (N'' ≃ₗ[R'] N₂'') → M'' [⋀^ι]→ₗ[R'] N'' ≃ₗ[R'] M'' [⋀^ι]→ₗ[R'] N₂''
-- Mathlib.Data.List.Rotate
/-- A version of `List.getElem_rotate` that represents `l[k]` in terms of
`(List.rotate l n)[⋯]`, not vice versa. Can be used instead of rewriting `List.getElem_rotate`
from right to left.  -/
List.getElem_eq_getElem_rotate : ∀ {α : Type u} (l : List α) (n k : ℕ) (hk : k < l.length), l[k] = (l.rotate n)[(l.length - n % l.length + k) % l.length]
-- Batteries.Data.String.Lemmas
String.Pos.Raw.extract.go₂.eq_2 : ∀ (a a_1 : String.Pos.Raw) (c : Char) (cs : List Char),
  String.Pos.Raw.extract.go₂ (c :: cs) a a_1 = if a = a_1 then [] else c :: String.Pos.Raw.extract.go₂ cs (a + c) a_1
-- Mathlib.LinearAlgebra.Matrix.Echelon.Basic
Matrix.IsLeadingEntry.row_ne_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type v} {A : Matrix m n R} [inst : Zero R] [inst_1 : LT n] {i : m} {c : n},
  A.IsLeadingEntry i c → A i ≠ 0
-- Mathlib.Algebra.Regular.Basic
IsAddRightRegular.left_of_addCommute : ∀ {R : Type u_1} [inst : Add R] {a : R}, (∀ (b : R), AddCommute a b) → IsAddRightRegular a → IsAddLeftRegular a
-- Mathlib.Logic.Basic
dite_ne_left_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {a : α} {B : ¬P → α}, dite P (fun x => a) B ≠ a ↔ ∃ (h : ¬P), a ≠ B h
-- Mathlib.Algebra.Group.Defs
IsCancelAdd.toIsRightCancelAdd : ∀ {G : Type u} {inst : Add G} [self : IsCancelAdd G], IsRightCancelAdd G
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.valueMonoid_eq_valueGroup' : ∀ {A : Type u_1} {B : Type u_2} [inst : GroupWithZero A] [inst_1 : GroupWithZero B] (f : A →*₀ B),
  ↑f.valueMonoid = ↑f.valueGroup
-- Init.Data.UInt.Bitwise
instAssociativeUInt8HOr : Std.Associative fun x1 x2 => x1 ||| x2
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.withMCtxImp : {α : Type} → Lean.MetavarContext → Lean.MetaM α → Lean.MetaM α
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] [ProperSpace 𝕜] {a : A}, (spectrum 𝕜 a).Nonempty → ∃ k ∈ spectrum 𝕜 a, ↑‖k‖₊ = spectralRadius 𝕜 a
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Cylinder.IsVeryGood.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P P_1 : HomotopicalAlgebra.Cylinder A),
  P = P_1 →
    ∀ [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A A] [inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C]
      [inst_4 : HomotopicalAlgebra.CategoryWithFibrations C], P.IsVeryGood = P_1.IsVeryGood
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.postcomp.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {Y Z : C} {n : ℕ} (β β_1 : CategoryTheory.Abelian.Ext Y Z n),
  β = β_1 → ∀ (X : C) {a b : ℕ} (h : a + n = b), β.postcomp X h = β_1.postcomp X h
-- Mathlib.Topology.Filter
Filter.nhds_atTop : ∀ {α : Type u_2} [inst : Preorder α], nhds Filter.atTop = ⨅ x, Filter.principal (Set.Iic (Filter.principal (Set.Ici x)))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α} {h : k ∈ Std.ExtDHashMap.Const.insertManyIfNewUnit m l},
  Std.ExtDHashMap.Const.get (Std.ExtDHashMap.Const.insertManyIfNewUnit m l) k h = ()
-- Std.Http.Data.URI.Basic
/-- HTTP request target forms as defined in RFC 9112 Section 3.3.

Reference: https://www.rfc-editor.org/rfc/rfc9112.html#section-3.3
 -/
Std.Http.RequestTarget : Type
-- Mathlib.Computability.TuringMachine.Computable
/-- A Turing machine + a time function +
a proof it outputs `f` in at most `time(input.length)` steps.  -/
Turing.TM2ComputableInTime : {α β αΓ βΓ : Type} → (α → List αΓ) → (β → List βΓ) → (α → β) → Type 1
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.instInhabitedEntry : {α : Type u_1} → {β : Type u_2} → {σ : Type u_3} → Inhabited (Lean.PersistentHashMap.Entry α β σ)
-- Init.Prelude
/-- Zero, the smallest natural number.

Using `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the
[simp normal form](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).
 -/
Nat.zero : ℕ
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.symm_mk_zpow : ∀ {M : Type u_1} [inst : DivInvMonoid M] (a : Mᵈᵐᵃ) (n : ℤ), DomMulAct.mk.symm (a ^ n) = DomMulAct.mk.symm a ^ n
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv Y)
      (CategoryTheory.MonoidalCategoryStruct.associator X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv
-- Mathlib.AlgebraicTopology.SingularHomology.Basic
AlgebraicTopology.ι_singularChainComplexFunctorAdjunction_counit_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (n : ℕ) (F : CategoryTheory.Functor TopCat C) (X : TopCat)
  (i : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Sigma.ι
        (fun x => ((CategoryTheory.evaluation TopCat C).obj (SimplexCategory.toTop.{w}.obj { len := n })).obj F) i)
      (((AlgebraicTopology.singularChainComplexFunctorAdjunction C n).counit.app F).app X) =
    F.map i.down
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.instTypeNameRealizeConstKey : TypeName Lean.Environment.RealizeConstKey✝
-- Mathlib.Algebra.Group.Graph
AddMonoidHom.mgraph_eq_mrange_prod : ∀ {G : Type u_1} {H : Type u_2} [inst : AddMonoid G] [inst_1 : AddMonoid H] (f : G →+ H),
  f.mgraph = AddMonoidHom.mrange ((AddMonoidHom.id G).prod f)
-- Mathlib.Data.Vector.Basic
List.Vector.pmap_cons : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) (a : α) (v : List.Vector α n)
  (hp : ∀ x ∈ (a ::ᵥ v).toList, p x), List.Vector.pmap f (a ::ᵥ v) hp = f a ⋯ ::ᵥ List.Vector.pmap f v ⋯
-- Init.Sym.DSimp.DSimprocDSL
/-- Try `a`, if no progress try `b`.  -/
Lean.Parser.Sym.DSimp.orElse : Lean.TrailingParserDescr
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.Scheme.isSeparated_iff : ∀ (X : AlgebraicGeometry.Scheme), X.IsSeparated ↔ AlgebraicGeometry.IsSeparated (CategoryTheory.Limits.terminal.from X)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
instAddGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (G : Type u)
  [inst_9 : TopologicalSpace G] [inst_10 : ChartedSpace H G] [inst_11 : AddGroup G] [inst_12 : LieAddGroup I (↑⊤) G]
  (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ),
  instAddGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf IM I M G U =
    { add := instAddGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf._aux_1 IM I M G U, add_assoc := ⋯,
      zero := instAddGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf._aux_4 IM I M G U, zero_add := ⋯, add_zero := ⋯,
      nsmul := instAddGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf._aux_8 IM I M G U, nsmul_zero := ⋯,
      nsmul_succ := ⋯, neg := instAddGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf._aux_12 IM I M G U,
      sub := instAddGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf._aux_14 IM I M G U,
      zsmul := instAddGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf._aux_16 IM I M G U, sub_eq_add_neg := ⋯,
      zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- If `e : M ≃* N` is a multiplicative equivalence between two monoids, then
`MonoidAlgebra.domCongr e` is an algebra equivalence between their monoid algebras.  -/
MonoidAlgebra.domCongr : (R : Type u_1) →
  (A : Type u_4) →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Monoid M] → [inst_4 : Monoid N] → M ≃* N → MonoidAlgebra A M ≃ₐ[R] MonoidAlgebra A N
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.Const.alterₘ.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.continuousAt_setToFun_of_dominated : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {X : Type u_7} [inst_4 : TopologicalSpace X] [FirstCountableTopology X]
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {fs : X → α → E} {x₀ : X} {bound : α → ℝ},
  (∀ᶠ (x : X) in nhds x₀, MeasureTheory.AEStronglyMeasurable (fs x) μ) →
    (∀ᶠ (x : X) in nhds x₀, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ →
        (∀ᵐ (a : α) ∂μ, ContinuousAt (fun x => fs x a) x₀) →
          ContinuousAt (fun x => MeasureTheory.setToFun μ T hT (fs x)) x₀
-- Mathlib.Topology.VectorBundle.Hom
/-- Assume `eᵢ` and `eᵢ'` are trivializations of the bundles `Eᵢ` over base `B` with fiber `Fᵢ`
(`i ∈ {1,2}`), then `Pretrivialization.continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂'` is the
coordinate change function between the two induced (pre)trivializations
`Pretrivialization.continuousLinearMap σ e₁ e₂` and
`Pretrivialization.continuousLinearMap σ e₁' e₂'` of the bundle of continuous linear maps.  -/
Bundle.Pretrivialization.continuousLinearMapCoordChange : {𝕜₁ : 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] →
                                          (e₁ e₁' : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) →
                                            (e₂ e₂' : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) →
                                              [Bundle.Trivialization.IsLinear 𝕜₁ e₁] →
                                                [Bundle.Trivialization.IsLinear 𝕜₁ e₁'] →
                                                  [Bundle.Trivialization.IsLinear 𝕜₂ e₂] →
                                                    [Bundle.Trivialization.IsLinear 𝕜₂ e₂'] →
                                                      B → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoo_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a < b → Set.uIoo a b = Set.Ioo a b
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.natMul.inj : ∀ {k : ℕ} {a : Lean.Grind.Linarith.Expr} {k_1 : ℕ} {a_1 : Lean.Grind.Linarith.Expr},
  Lean.Grind.Linarith.Expr.natMul k a = Lean.Grind.Linarith.Expr.natMul k_1 a_1 → k = k_1 ∧ a = a_1
-- Init.System.Promise
IO.instNonemptyPromise : ∀ {α : Type} [s : Nonempty α], Nonempty (IO.Promise α)
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.addUnit_of_mem_ofAddUnits_spec_mem : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} {h : x ∈ S.ofAddUnits},
  S.addUnit_of_mem_ofAddUnits h ∈ S
-- Mathlib.CategoryTheory.Bicategory.Opposites
/-- The functor from the hom-category `a ⟶ b` in `Bᵒᵖ` to its bicategorical opposite
`unop b ⟶ unop a`.  -/
Bicategory.Opposite.unopFunctor : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (a b : Bᵒᵖ) → CategoryTheory.Functor (a ⟶ b) (Opposite.unop b ⟶ Opposite.unop a)
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.isOpen_iff_of_isColimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat}
  (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c) (X : Set ↑c.pt),
  IsOpen X ↔ ∀ (j : J), IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)
-- Mathlib.Algebra.Free
/-- The unique semigroup homomorphism that sends `of x` to `of (f x)`.  -/
FreeSemigroup.map : {α : Type u} → {β : Type v} → (α → β) → FreeSemigroup α →ₙ* FreeSemigroup β