mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Sym.SymM
/-- Registers a new `SymM` state extension. Extensions can only be registered during initialization.
Returns a handle for typed access to the extension's state.
 -/
Lean.Meta.Sym.registerSymExtension : {σ : Type} → IO σ → IO (Lean.Meta.Sym.SymExtension σ)
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.isLocallyArtinian_iff_of_isOpenCover : ∀ {X : AlgebraicGeometry.Scheme} {ι : Type u_1} {U : ι → X.Opens},
  TopologicalSpace.IsOpenCover U →
    (∀ (i : ι), AlgebraicGeometry.IsAffineOpen (U i)) →
      (AlgebraicGeometry.IsLocallyArtinian X ↔ ∀ (i : ι), IsArtinianRing ↑(X.presheaf.obj (Opposite.op (U i))))
-- Mathlib.Data.Set.Lattice
Set.iUnion_ge_eq_iUnion_nat_add : ∀ {α : Type u_1} (u : ℕ → Set α) (n : ℕ), ⋃ i, ⋃ (_ : i ≥ n), u i = ⋃ i, u (i + n)
-- Mathlib.Analysis.Convex.Hull
convex_convexHull : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s : Set E), Convex 𝕜 ((convexHull 𝕜) s)
-- Init.Data.Range.Polymorphic.PRange
/-- The upper bound of the range. `upper` is not included in the range.
   -/
Std.Rio.upper : {α : Type u} → Std.Rio α → α
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivAtFilter_finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] (i : Fin n.succ) → F' i} {l : Filter (E × E)},
  HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x)) φ' l ↔
    HasFDerivAtFilter φ (ContinuousLinearMap.proj 0 ∘SL φ') l ∧
      HasFDerivAtFilter φs (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') l
-- Std.Data.TreeSet.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise `fallback`.
If they key is contained the result is guaranteed to be pointer equal to the key in the set.
 -/
Std.TreeSet.getD : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → α → α
-- Mathlib.Tactic.NormNum.Prime
Mathlib.Meta.NormNum.isNat_minFac_4 : ∀ {n n' k : ℕ},
  Mathlib.Meta.NormNum.IsNat n n' →
    Mathlib.Meta.NormNum.MinFacHelper n' k → (k * k).ble n' = false → Mathlib.Meta.NormNum.IsNat n.minFac n'
-- Mathlib.NumberTheory.AbelSummation
_private.Mathlib.NumberTheory.AbelSummation.0.abelSummationProof.ineqofmemIco : ∀ {a b : ℝ} {k : ℕ}, k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊ → a ≤ ↑k ∧ ↑k + 1 ≤ b
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.comp_aeval : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {a : σ → S} [inst_4 : IsTopologicalSemiring R] [inst_5 : IsUniformAddGroup R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : CompleteSpace S] [inst_8 : T2Space S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S] (ha : MvPowerSeries.HasEval a)
  {T : Type u_4} [inst_13 : CommRing T] [inst_14 : UniformSpace T] [inst_15 : IsUniformAddGroup T]
  [inst_16 : IsTopologicalRing T] [inst_17 : IsLinearTopology T T] [inst_18 : T2Space T] [inst_19 : Algebra R T]
  [inst_20 : ContinuousSMul R T] [inst_21 : CompleteSpace T] {ε : S →ₐ[R] T} (hε : Continuous ⇑ε),
  ε.comp (MvPowerSeries.aeval ha) = MvPowerSeries.aeval ⋯
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsTwoSided.instHMul : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} [J.IsTwoSided], (I * J).IsTwoSided
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `ContinuousLinearMap.toLinearMap_pow`. -/
ContinuousLinearMap.coe_pow : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] (f : M₁ →L[R₁] M₁) (n : ℕ), ↑(f ^ n) = ↑f ^ n
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
AddGroup.isAddCyclic_of_coprime_card_ker : ∀ {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddGroup N] (f : M →+ N),
  (Nat.card ↥f.ker).Coprime (Nat.card N) →
    ∀ [IsAddCyclic ↥f.ker] [hN : IsAddCyclic N], Function.Surjective ⇑f → IsAddCyclic M
-- Batteries.Data.AssocList
List.toAssocList.eq_def : ∀ {α : Type u_1} {β : Type u_2} (x : List (α × β)),
  x.toAssocList =
    match x with
    | [] => Batteries.AssocList.nil
    | (a, b) :: es => Batteries.AssocList.cons a b es.toAssocList
-- Lean.DocString.Types
Lean.Doc.instInhabitedBlock.default : {i : Type u} → {b : Type v} → Lean.Doc.Block i b
-- Mathlib.Topology.Instances.Matrix
Summable.matrix_blockDiag : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [inst : AddCommMonoid R]
  [inst_1 : TopologicalSpace R] {L : SummationFilter X} {f : X → Matrix (m × p) (n × p) R},
  Summable f L → Summable (fun x => (f x).blockDiag) L
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.mem_span_latticeBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.mixedEmbedding.latticeBasis K)) ↔
    x ∈ NumberField.mixedEmbedding.integerLattice K
-- Mathlib.Order.TypeTags
WithBot.recBotCoe_coe : ∀ {α : Type u_1} {C : WithBot α → Sort u_2} (d : C ⊥) (f : (a : α) → C ↑a) (x : α), WithBot.recBotCoe d f ↑x = f x
-- Mathlib.Topology.Sets.VietorisTopology
/-- The topology of `Compacts α` has a basis consisting of sets of the form
`{K | K ⊆ U₁ ∪ … ∪ Uₙ, K ∩ U₁ ≠ ∅, …, K ∩ Uₙ ≠ ∅}`, where `U₁, …, Uₙ` are open sets.

See also `TopologicalSpace.IsTopologicalBasis.compacts` for a variant where the sets `Uᵢ`
are chosen from some basis.  -/
TopologicalSpace.Compacts.isTopologicalBasis : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  TopologicalSpace.IsTopologicalBasis
    ((fun u => {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ ∀ U ∈ u, IsOpen U})
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
add_le_of_le_tsub_left_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, a ≤ c → b ≤ c - a → a + b ≤ c
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInlayHintOptions : Lean.ToJson Lean.Lsp.InlayHintOptions
-- Mathlib.Algebra.Polynomial.Basic
_private.Mathlib.Algebra.Polynomial.Basic.0.Polynomial.support.match_1.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (motive : Polynomial R → Sort u_2) (p : AddMonoidAlgebra R ℕ)
  (h_1 : (p : AddMonoidAlgebra R ℕ) → motive { toFinsupp := p }),
  (match { toFinsupp := p } with
    | { toFinsupp := p } => h_1 p) =
    h_1 p
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Quiver.FreeGroupoid.instCategory : {V : Type u} → [inst : Quiver V] → CategoryTheory.Category.{max u v, u} (Quiver.FreeGroupoid V)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isUnsatEq_k.eq_1 : ∀ (p : Int.Internal.Linear.Poly),
  p.isUnsatEq_k = Int.Internal.Linear.Poly.rec (fun k => (k.beq' 0).not') (fun x x_1 x_2 x_3 => false) p
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.comp_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) (X : C) {Z : D} (h : H.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp α β).app X) h =
    CategoryTheory.CategoryStruct.comp (α.app X) (CategoryTheory.CategoryStruct.comp (β.app X) h)
-- Mathlib.Tactic.NormNum.Result
/-- Given `Mathlib.Meta.NormNum.Result.isBool p b`, this is the type of `p`.
Note that `BoolResult p b` is definitionally equal to `Expr`, and if you write `match b with ...`,
then in the `true` branch `BoolResult p true` is reducibly equal to `Q($p)` and
in the `false` branch it is reducibly equal to `Q(¬ $p)`.  -/
Mathlib.Meta.NormNum.BoolResult : Q(Prop) → Bool → Type
-- Mathlib.Combinatorics.Hindman
/-- We could have taken this as the definition of `U + V`, but then we would have to
prove that it defines an ultrafilter.  -/
Ultrafilter.eventually_add : ∀ {M : Type u_1} [inst : Add M] (U V : Ultrafilter M) (p : M → Prop),
  (∀ᶠ (m : M) in ↑(U + V), p m) ↔ ∀ᶠ (m : M) in ↑U, ∀ᶠ (m' : M) in ↑V, p (m + m')
-- Mathlib.Algebra.Notation.Defs
dite_mul_dite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Mul α] (a : P → α) (b : ¬P → α) (c : P → α) (d : ¬P → α),
  ((if h : P then a h else b h) * if h : P then c h else d h) = if h : P then a h * c h else b h * d h
-- Lean.Message
Lean.MessageData.formatAux : Lean.NamingContext → Option Lean.MessageDataContext → Lean.MessageData → BaseIO Std.Format
-- Mathlib.Order.TypeTags
_private.Mathlib.Order.TypeTags.0.WithBot.instRepr.match_1.splitter : {α : Type u_1} →
  (motive : WithBot α → Sort u_2) → (o : WithBot α) → (Unit → motive none) → ((a : α) → motive (some a)) → motive o
-- Mathlib.Combinatorics.Derangements.Basic
derangements.eq_1 : ∀ (α : Type u_1), derangements α = {f | ∀ (x : α), f x ≠ x}
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.injective : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] [T0Space α] {f : α → β},
  IsUniformInducing f → Function.Injective f
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonWorkspaceEdit.fromJson : Lean.Json → Except String Lean.Lsp.WorkspaceEdit
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.normalizeIsoApp'.match_1.eq_3 : ∀ (C : Type u_1)
  (motive :
    CategoryTheory.FreeMonoidalCategory C → CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C → Sort u_2)
  (X Y : CategoryTheory.FreeMonoidalCategory C) (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C)
  (h_1 :
    (a : C) →
      (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) →
        motive (CategoryTheory.FreeMonoidalCategory.of a) x)
  (h_2 :
    (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) →
      motive CategoryTheory.FreeMonoidalCategory.unit x)
  (h_3 :
    (X Y : CategoryTheory.FreeMonoidalCategory C) →
      (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) → motive (X.tensor Y) n),
  (match X.tensor Y, n with
    | CategoryTheory.FreeMonoidalCategory.of a, x => h_1 a x
    | CategoryTheory.FreeMonoidalCategory.unit, x => h_2 x
    | X.tensor Y, n => h_3 X Y n) =
    h_3 X Y n
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.dual_ordConnectedSection : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α),
  (⇑OrderDual.ofDual ⁻¹' s).ordConnectedSection = ⇑OrderDual.ofDual ⁻¹' s.ordConnectedSection
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- If `f` has a local max on `s` at `a` and both `y` and `-y` belong to the positive tangent cone
of `s` at `a`, then `f' y = 0`.  -/
IsLocalMaxOn.fderivWithin_eq_zero : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a y : E},
  IsLocalMaxOn f s a → y ∈ posTangentConeAt s a → -y ∈ posTangentConeAt s a → (fderivWithin ℝ f s a) y = 0
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.monoLM_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n₁ n₂ : ℕ∞} {K₁ K₂ : TopologicalSpace.Compacts E}
  (f : ContDiffMapSupportedIn E F n₁ K₁), ⇑((ContDiffMapSupportedIn.monoLM 𝕜) f) = ⇑(if n₂ ≤ n₁ ∧ K₁ ≤ K₂ then f else 0)
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_symm_none : ∀ {n : ℕ} (i : Fin (n + 1)), (finSuccEquiv' i).symm none = i
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
/-- A map `f` is said to be $C^{k+(α)}$ at `a`, where `k` is a natural number and `0 ≤ α ≤ 1`,
if it is $C^k$ at this point and $D^kf(x)-D^kf(a) = O(‖x - a‖ ^ α)$ as `x → a`.

When naming lemmas about this predicate, `k` is called "order", and `α` is called "exponent".  -/
ContDiffPointwiseHolderAt : {E : Type u_1} →
  {F : Type u_2} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → ℕ → ↑unitInterval → (E → F) → E → Prop
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_union_lt_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α},
  μ s < ⊤ → μ t < ⊤ → μ (s ∪ t) < ⊤
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry?.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.leaf.minEntry? = none
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.fvar.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (args : Array (Lean.Compiler.LCNF.Arg pu)),
  sizeOf (Lean.Compiler.LCNF.LetValue.fvar fvarId args) = 1 + sizeOf fvarId + sizeOf args
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.equivCostructuredArrow_inverse : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C),
  (CategoryTheory.Limits.Cone.equivCostructuredArrow F).inverse = CategoryTheory.Limits.Cone.fromCostructuredArrow F
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- See note [partially-applied ext lemmas].  -/
ExteriorAlgebra.hom_ext : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] {f g : ExteriorAlgebra R M →ₐ[R] A},
  f.toLinearMap ∘ₗ ExteriorAlgebra.ι R = g.toLinearMap ∘ₗ ExteriorAlgebra.ι R → f = g
-- Lean.Elab.DefView
/-- Elaboration results.  -/
Lean.Elab.HeaderProcessedSnapshot.view : Lean.Elab.HeaderProcessedSnapshot → Lean.Elab.DefViewElabHeaderData
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.op_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A),
  P.op.I = Opposite.op P.P
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ιMulti_family_mul_of_disjoint : ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m n : ℕ}
  {I : Type u_1} [inst_3 : LinearOrder I] (v : I → M) (s : ↑(Set.powersetCard I m)) (t : ↑(Set.powersetCard I n))
  (h : Disjoint ↑s ↑t),
  ExteriorAlgebra.ιMulti_family R m v s * ExteriorAlgebra.ιMulti_family R n v t =
    Equiv.Perm.sign (Set.powersetCard.permOfDisjoint h) •
      ExteriorAlgebra.ιMulti_family R (m + n) v (Set.powersetCard.disjUnion h)
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.natCast_eq_ofNat : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (n : ℕ), ↑n = OfNat.ofNat n
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_add_iff_of_ge : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α]
  {a₁ a₂ b₁ b₂ : α}, a₁ ≤ a₂ → b₁ ≤ b₂ → (a₂ + b₂ ≤ a₁ + b₁ ↔ a₁ = a₂ ∧ b₁ = b₂)
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
AlgebraicGeometry.ext_of_apply_closedPoint_eq : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [IsAlgClosed K]
  {f g : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X} (h : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K))
  [AlgebraicGeometry.LocallyOfFiniteType h],
  CategoryTheory.CategoryStruct.comp f h =
      CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K)) →
    CategoryTheory.CategoryStruct.comp g h =
        CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K)) →
      f (IsLocalRing.closedPoint K) = g (IsLocalRing.closedPoint K) → f = g
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.single.eq_1 : ∀ (n : ℕ) (h : 0 < n), Composition.single n h = { blocks := [n], blocks_pos := ⋯, blocks_sum := ⋯ }
-- Lean.Util.ForEachExprWhere
/-- Implements caching trick similar to the one used at `FindExpr` and `ReplaceExpr`.
 -/
Lean.ForEachExprWhere.State.visited : Lean.ForEachExprWhere.State → Array Lean.Expr
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_int_eq : ∀ {M : Type u_9} [inst : AddCommGroup M] (s : AddSubgroup M), (Submodule.span ℤ ↑s).toAddSubgroup = s
-- Mathlib.Geometry.Manifold.Immersion
/-- A choice of chart on the co-domain `N` of an immersion `f` at `x`:
w.r.t. this chart and the data `h.domChart` and `h.equiv`,
`f` will look like an inclusion `u ↦ (u, 0)` in these extended charts.
The particular chart is arbitrary, but this choice matches the witnesses given by
`h.equiv` and `h.domChart`.  -/
Manifold.IsImmersionAt.codChart : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup E''] →
              [inst_4 : NormedSpace 𝕜 E''] →
                {H : Type u_7} →
                  [inst_5 : TopologicalSpace H] →
                    {G : Type u_9} →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {N : Type u_13} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} → Manifold.IsImmersionAt I J n f x → OpenPartialHomeomorph N G
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.epi_of_epi_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.ReflectsEpimorphisms] {X Y : C} {f : X ⟶ Y},
  CategoryTheory.Epi (F.map f) → CategoryTheory.Epi f
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.setLike : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : AddMonoid ι] →
        [inst_1 : Semiring A] →
          [inst_2 : SetLike σ A] →
            [inst_3 : AddSubmonoidClass σ A] →
              {𝒜 : ι → σ} → [inst_4 : DecidableEq ι] → [inst_5 : GradedRing 𝒜] → SetLike (HomogeneousSubsemiring 𝒜) A
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.coe_of : ∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : AlexandrovDiscrete α], ↑(AlexDisc.of α).toTopCat = α
-- Mathlib.Data.List.Nodup
List.nodup_flatten : ∀ {α : Type u} {L : List (List α)}, L.flatten.Nodup ↔ (∀ l ∈ L, l.Nodup) ∧ List.Pairwise List.Disjoint L
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.instIsCorepresentableCompUliftFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v))
  [F.IsCorepresentable], (F.comp CategoryTheory.uliftFunctor.{w, v}).IsCorepresentable
-- Mathlib.Topology.Category.DeltaGenerated
/-- `deltaGeneratedToTop` is fully faithful.  -/
DeltaGenerated.fullyFaithfulDeltaGeneratedToTop : DeltaGenerated.deltaGeneratedToTop.FullyFaithful
-- Std.Data.ExtDHashMap.Basic
/-- Creates a hash map from a list of keys, associating the value `()` with each key.

This is mainly useful to implement `HashSet.ofList`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.  -/
Std.ExtDHashMap.Const.unitOfList : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → List α → Std.ExtDHashMap α fun x => Unit
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetDecl.binderName : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetDecl pu → Lean.Name
-- Std.Data.TreeMap.Slice
Std.TreeMap.instSliceableRcoSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.instSliceableRcoSlice._auto_1) →
      Std.Rco.Sliceable (Std.TreeMap α β cmp) α (Std.DTreeMap.Internal.Const.RcoSlice α β)
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.dist_inequality : ∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α},
  ContractingWith K f → ∀ (x y : α), dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - ↑K)
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.localEpi.of_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Epi f], P.localEpi f
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
/-- A version of `Complex.cpow_int_mul` with RHS that matches `Complex.cpow_mul`.

The assumptions on the arguments are needed
because the equality fails, e.g., for `x = -I`, `n = 2`, `y = 1/2`.  -/
Complex.cpow_int_mul' : ∀ {x : ℂ} {n : ℤ}, -Real.pi < ↑n * x.arg → ↑n * x.arg ≤ Real.pi → ∀ (y : ℂ), x ^ (↑n * y) = (x ^ n) ^ y
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.ofπ'_var : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (π : (relations.G →₀ A) →ₗ[A] M) (hπ : π ∘ₗ relations.map = 0) (g : relations.G),
  (Module.Relations.Solution.ofπ' π hπ).var g = π fun₀ | g => 1
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The trivial `AddSubgroup` `{0}` of an `AddGroup` `G`.  -/
AddSubgroup.instBot : {G : Type u_1} → [inst : AddGroup G] → Bot (AddSubgroup G)
-- Init.Data.Vector.Lemmas
Vector.mem_singleton_self : ∀ {α : Type u_1} (a : α), a ∈ #v[a]
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.ins.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (y : α)
  (parent : RBTree.RBNode.Path α) (b : RBTree.RBNode α) (h_1 : (t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t)
  (h_2 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.red parent y b) a)
  (h_3 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.red a y parent) b)
  (h_4 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.black parent y b) a)
  (h_5 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.black a y parent) b),
  (match RBTree.RBNode.Path.right RBTree.RBColor.red a y parent, b with
    | RBTree.RBNode.Path.root, t => h_1 t
    | RBTree.RBNode.Path.left RBTree.RBColor.red parent y b, a => h_2 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.red a y parent, b => h_3 a y parent b
    | RBTree.RBNode.Path.left RBTree.RBColor.black parent y b, a => h_4 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.black a y parent, b => h_5 a y parent b) =
    h_3 a y parent b
-- Mathlib.Algebra.Homology.QuasiIso
quasiIsoAt_of_comp_right : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L)
  (φ' : L ⟶ M) (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : M.HasHomology i]
  [hφ' : QuasiIsoAt φ' i] [hφφ' : QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i], QuasiIsoAt φ i
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.norm_toLp : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E] [inst_5 : OpensMeasurableSpace E]
  [inst_6 : SecondCountableTopologyEither E F] {f : SchwartzMap E F} {p : ENNReal} {μ : MeasureTheory.Measure E}
  [hμ : μ.HasTemperateGrowth], ‖f.toLp p μ‖ = (MeasureTheory.eLpNorm (⇑f) p μ).toReal
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Command.declareSyntaxCatQuotParser : Lean.Name → Lean.Elab.Command.CommandElabM Unit