mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
SimpleGraph.ConnectedComponent.card_le_card_of_le : ∀ {V : Type u} [Finite V] {G G' : SimpleGraph V},
  G ≤ G' → Nat.card G'.ConnectedComponent ≤ Nat.card G.ConnectedComponent
-- Mathlib.Algebra.Star.LinearMap
/-- The intrinsic star convolutive ring on linear maps from `n → R` to `m → R`.  -/
Pi.convIntrinsicStarRingCommSemiring : {R : Type u_5} →
  [inst : CommSemiring R] →
    [StarRing R] →
      {n : Type u_8} →
        [inst_2 : DecidableEq n] → [inst_3 : Fintype n] → {m : Type u_10} → StarRing (WithConv ((n → R) →ₗ[R] m → R))
-- Init.Data.String.Basic
String.utf8PrevAux : List Char → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Data.Semiquot
Semiquot.instMonad : Monad Semiquot
-- Aesop.Forward.PremiseIndex
Aesop.instDecidableRelPremiseIndexLt : DecidableRel fun x1 x2 => x1 < x2
-- Mathlib.CategoryTheory.Limits.FunctorToTypes
CategoryTheory.FunctorToTypes.colimit.map_ι_apply : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K (Type w))) [inst_2 : CategoryTheory.Limits.HasColimit F]
  (j : J) {k k' : K} {f : k ⟶ k'} {x : (fun X => X) ((F.obj j).obj k)},
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.colimit F).map f))
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.colimit.ι F j).app k)) x) =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.colimit.ι F j).app k'))
      ((CategoryTheory.ConcreteCategory.hom ((F.obj j).map f)) x)
-- Mathlib.MeasureTheory.Measure.Complex
MeasureTheory.ComplexMeasure.equivSignedMeasure_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} (c : MeasureTheory.ComplexMeasure α),
  MeasureTheory.ComplexMeasure.equivSignedMeasure c =
    (MeasureTheory.ComplexMeasure.re c, MeasureTheory.ComplexMeasure.im c)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.hom_smul : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : TopologicalSpace S] {M₁ M₂ : TopModuleCat S} (s : S) (φ : M₁ ⟶ M₂),
  TopModuleCat.Hom.hom (s • φ) = s • TopModuleCat.Hom.hom φ
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.toNatIso_isoMk : ∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  {F G : CategoryTheory.Functor C D} (e : F ≅ G), CategoryTheory.Cat.Hom.toNatIso (CategoryTheory.Cat.Hom.isoMk e) = e
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_X_self : ∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] (i : σ), (MvPolynomial.pderiv i) (MvPolynomial.X i) = 1
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.trans_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P P' : HomotopicalAlgebra.Precylinder A)
  [inst_1 : CategoryTheory.Limits.HasPushout P.i₁ P'.i₀], (P.trans P').I = CategoryTheory.Limits.pushout P.i₁ P'.i₀
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_iff_forall_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m.isEmpty = true ↔ ∀ (a : α), m.contains a = false
-- Mathlib.Tactic.Linter.DocPrime
/-- The "docPrime" linter emits a warning on declarations that have no doc-string and whose
name ends with a `'`.

The file `scripts/nolints_prime_decls.txt` contains a list of temporary exceptions to this linter.
This list should not be appended to, and become emptied over time.
 -/
_private.Mathlib.Tactic.Linter.DocPrime.0.Mathlib.Linter.DocPrime.docPrimeLinter : Lean.Linter
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns `ULift.up true` if the pure predicate `p` returns `true` for
any element emitted by the iterator `it`.

`O(|it|)`. Short-circuits upon encountering the first match. The outputs of `it` are
examined in order of iteration.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.any`.
 -/
Std.IterM.Total.any : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → [Std.Iterators.Finite α m] → (β → Bool) → Std.IterM.Total m β → m (ULift.{w, 0} Bool)
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.surjInvRightHom.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  (S : GroupExtension N E G), S.surjInvRightHom = { toFun := Function.surjInv ⋯, rightInverse_rightHom := ⋯ }
-- Mathlib.MeasureTheory.Group.IntegralConvolution
MeasureTheory.integrable_mconv_iff : ∀ {M : Type u_1} {F : Type u_2} [inst : Monoid M] {mM : MeasurableSpace M} [MeasurableMul₂ M]
  [inst_2 : NormedAddCommGroup F] {μ ν : MeasureTheory.Measure M} {f : M → F} [MeasureTheory.SFinite ν],
  MeasureTheory.AEStronglyMeasurable f (μ.mconv ν) →
    (MeasureTheory.Integrable f (μ.mconv ν) ↔
      (∀ᵐ (x : M) ∂μ, MeasureTheory.Integrable (fun y => f (x * y)) ν) ∧
        MeasureTheory.Integrable (fun x => ∫ (y : M), ‖f (x * y)‖ ∂ν) μ)
-- Init.Data.Range.Polymorphic.Int
Std.PRange.instHasSizeInt : Std.Rxc.HasSize ℤ
-- Mathlib.Topology.Order.LiminfLimsup
Antitone.limsup_nhdsLT_eq_iInf₂_of_exists_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [DenselyOrdered α] [inst_4 : CompleteLattice β] {f : α → β},
  Antitone f → ∀ (a : α), (∃ b, b < a) → Filter.limsup f (nhdsWithin a (Set.Iio a)) = ⨅ r, ⨅ (_ : r < a), f r
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.map'_inv_eq_inv_map' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n m : ℕ} (h : n + 1 ≤ m)
  {f g : CategoryTheory.ComposableArrows C m} (app : f.obj' n ⋯ ≅ g.obj' n ⋯)
  (app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h),
  CategoryTheory.CategoryStruct.comp (f.map' n (n + 1) ⋯ h) app'.hom =
      CategoryTheory.CategoryStruct.comp app.hom (g.map' n (n + 1) ⋯ h) →
    CategoryTheory.CategoryStruct.comp (g.map' n (n + 1) ⋯ h) app'.inv =
      CategoryTheory.CategoryStruct.comp app.inv (f.map' n (n + 1) ⋯ h)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mult.inj : ∀ {p : Lean.Grind.CommRing.Power} {m : Lean.Grind.CommRing.Mon} {p_1 : Lean.Grind.CommRing.Power}
  {m_1 : Lean.Grind.CommRing.Mon},
  Lean.Grind.CommRing.Mon.mult p m = Lean.Grind.CommRing.Mon.mult p_1 m_1 → p = p_1 ∧ m = m_1
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.coeff_mapRingHom`. -/
MonoidAlgebra.mapRangeRingHom_apply : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (f : R →+* S) (x : MonoidAlgebra R M) (m : M), ((MonoidAlgebra.mapRingHom M f) x).coeff m = f (x.coeff m)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.out.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  (A : ArchimedeanClass M), A.out = ArchimedeanOrder.val (Quotient.out A)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.powerπ_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α : Type}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] (a : α) (i : (U.power α).I), (U.powerπ a).f i = i a
-- Mathlib.LinearAlgebra.AffineSpace.Basis
mem_finsuppAffineCoords_iff_linearCombination : ∀ {ι : Type u_1} {k : Type u_2} [inst : Ring k] {w : ι →₀ k},
  w ∈ finsuppAffineCoords ι k ↔ (Finsupp.linearCombination k 1) w = 1
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.instInhabitedState : Inhabited Lean.Meta.Grind.Arith.CommRing.State
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.comp.eq_1 : ∀ {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 : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F ⊣ G)
  (adj₂ : H ⊣ I),
  adj₁.comp adj₂ =
    CategoryTheory.Adjunction.mk'
      { homEquiv := fun x x_1 => (adj₂.homEquiv (F.obj x) x_1).trans (adj₁.homEquiv x (I.obj x_1)),
        unit :=
          CategoryTheory.CategoryStruct.comp adj₁.unit
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Functor.whiskerRight
                (CategoryTheory.CategoryStruct.comp F.rightUnitor.inv
                  (CategoryTheory.CategoryStruct.comp (F.whiskerLeft adj₂.unit) (F.associator H I).inv))
                G)
              ((F.comp H).associator I G).hom),
        counit :=
          CategoryTheory.CategoryStruct.comp ((I.comp G).associator F H).inv
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Functor.whiskerRight
                (CategoryTheory.CategoryStruct.comp (I.associator G F).hom
                  (CategoryTheory.CategoryStruct.comp (I.whiskerLeft adj₁.counit) I.rightUnitor.hom))
                H)
              adj₂.counit),
        homEquiv_unit := ⋯, homEquiv_counit := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_add' : ∀ {y z : ℝ}, y + z ≠ 0 → ∀ (x : NNReal), x ^ (y + z) = x ^ y * x ^ z
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.map.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S)
  [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂] (g₁ : Y ⟶ T) (g₂ : Z ⟶ T)
  [inst_2 : CategoryTheory.Limits.HasPullback g₁ g₂] (i₁ i₁_1 : W ⟶ Y) (e_i₁ : i₁ = i₁_1) (i₂ i₂_1 : X ⟶ Z)
  (e_i₂ : i₂ = i₂_1) (i₃ i₃_1 : S ⟶ T) (e_i₃ : i₃ = i₃_1)
  (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁)
  (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂),
  CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ =
    CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁_1 i₂_1 i₃_1 ⋯ ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) =
    (Std.Internal.List.containsKey k l || (List.map Sigma.fst toInsert).contains k)
-- Std.Http.Data.Headers.Value
/-- Creates a `Value` from a string, panicking with an error message if the string contains invalid
characters for HTTP header values.
 -/
Std.Http.Header.Value.ofString! : String → Std.Http.Header.Value
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.map_eq_of_equiv_equiv : ∀ {A : Type u_1} [inst : Field A] {R : Type u_3} {S : Type u_4} {T : Type u_5} [inst_1 : CommRing R] [IsDomain R]
  [inst_3 : Ring S] [inst_4 : Ring T] [IsDomain S] [IsDomain T] [inst_7 : Algebra R S] [inst_8 : Algebra A T]
  [Algebra.IsIntegral R S] {f : R ≃+* A} {g : S ≃+* T},
  (algebraMap A T).comp ↑f = (↑g).comp (algebraMap R S) → ∀ (x : S), Polynomial.map (↑f) (minpoly R x) = minpoly A (g x)
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.algHom_ext_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {F G : SymmetricAlgebra R M →ₐ[R] A},
  F = G ↔ ↑F ∘ₗ SymmetricAlgebra.ι R M = ↑G ∘ₗ SymmetricAlgebra.ι R M
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- The data that witnesses that a presheaf `A` is an ind-object. It consists of a small
filtered indexing category `I`, a diagram `F : I ⥤ C` and the data for a colimit cocone on
`F ⋙ yoneda : I ⥤ Cᵒᵖ ⥤ Type v` with cocone point `A`.  -/
CategoryTheory.Limits.IndObjectPresentation : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor Cᵒᵖ (Type v) → Type (max u (v + 1))
-- Mathlib.Algebra.Group.Commute.Hom
commute_map_iff : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [MulHomClass F M N] {f : F}, Function.Injective ⇑f → ∀ {x y : M}, Commute (f x) (f y) ↔ Commute x y
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_coe_neg_pi_div_two : (↑(-Real.pi / 2)).sign = -1
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.unsat_relabel_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Std.Sat.CNF α} {r : α → β},
  (∀ {v1 v2 : α}, Std.Sat.CNF.VarMem v1 f → Std.Sat.CNF.VarMem v2 f → r v1 = r v2 → v1 = v2) →
    ((Std.Sat.CNF.relabel r f).Unsat ↔ f.Unsat)
-- Mathlib.GroupTheory.Transfer
Subgroup.leftTransversals.diff_self : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ : ↥H →* A)
  (T : H.LeftTransversal) [inst_2 : H.FiniteIndex], Subgroup.leftTransversals.diff ϕ T T = 1
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns a list of all keys present in the tree map in ascending  order.  -/
Std.DTreeMap.Raw.keys : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → List α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic.0.tacticPderiv_simp : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.dirac_apply_ne_zero_iff_eq_one : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} {a : α},
  (MeasureTheory.Measure.dirac a) s ≠ 0 ↔ (MeasureTheory.Measure.dirac a) s = 1
-- Mathlib.Data.Nat.Init
Nat.not_two_dvd_bit1 : ∀ (n : ℕ), ¬2 ∣ 2 * n + 1
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- If the quotient by the center of a group is cyclic, then the group is commutative.  -/
isMulCommutative_of_isCyclic_quotient_center_self : ∀ (G : Type u_2) [inst : Group G] [IsCyclic (G ⧸ Subgroup.center G)], IsMulCommutative G
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {k a : α} {v : β}, (m.insertIfNew k v)[a]? = if (k == a) = true ∧ k ∉ m then some v else m[a]?
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.End_toOne_one : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A], 1 = CoalgHom.id R A
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabFunValues : Array Lean.Elab.DefViewElabHeader → Array Lean.Expr → Lean.Elab.Command.Scope → Lean.Elab.TermElabM (Array Lean.Expr)
-- Mathlib.Topology.Sheaves.CommRingCat
/-- The presheaf (of commutative rings), consisting of functions on an open set `U ⊆ X` with
values in some topological commutative ring `T`.

For example, we could construct the presheaf of continuous complex-valued functions of `X` as
```
presheafToTopCommRing X (TopCommRingCat.of ℂ)
```
(this requires `import Topology.Instances.Complex`).
 -/
TopCat.presheafToTopCommRing : (X : TopCat) → TopCommRingCat → TopCat.Presheaf CommRingCat X
-- Mathlib.Data.Finsupp.Single
Finsupp.erase_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a : α), Finsupp.erase a 0 = 0
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffOn_finsetProd' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {t : Finset ι}
  {f : ι → M → G}, (∀ i ∈ t, ContMDiffOn I' I n (f i) s) → ContMDiffOn I' I n (∏ i ∈ t, f i) s
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.Value : Type
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabel.name.sizeOf_spec : ∀ (n : String), sizeOf (Lean.Elab.InlayHintLabel.name n) = 1 + sizeOf n
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀'_map_F : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {K K' : ChainComplex C ℕ} (f : K ⟶ K'),
  (AlgebraicTopology.DoldKan.Γ₀'.map f).F = AlgebraicTopology.DoldKan.Γ₀.map f
-- Lean.Message
/-- Render `userName` as `MessageData`, attaching hover information for the local declaration with
that user-facing name if it is bound in the current `LocalContext`. The lookup uses `userName`
verbatim (so macro scopes are preserved for matching) and the rendered name uses
`userName.simpMacroScopes`. Falls back to plain text when the variable is not in scope.
 -/
Lean.MessageData.ofUserName : {m : Type → Type} → [Monad m] → [Lean.MonadLCtx m] → Lean.Name → m Lean.MessageData
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersion.isSubmersionOfComplement_complement : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  (h : Manifold.IsSubmersion I J n f), Manifold.IsSubmersionOfComplement h.complement I J n f
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.ofHom.eq_1 : ∀ {X Y : Type u} [inst : Semigroup X] [inst_1 : Semigroup Y] (f : X →ₙ* Y),
  Semigrp.ofHom f = CategoryTheory.ConcreteCategory.ofHom f
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.mk.sizeOf_spec : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} [inst_2 : SizeOf C₁]
  [inst_3 : SizeOf C₂] [inst_4 : ⦃X Y : C₁⦄ → (x : X ⟶ Y) → SizeOf (W₁ x)]
  [inst_5 : ⦃X Y : C₂⦄ → (x : X ⟶ Y) → SizeOf (W₂ x)] {X₁ : C₁} (w : X₂ ⟶ Φ.functor.obj X₁) (hw : W₂ w),
  sizeOf { X₁ := X₁, w := w, hw := hw } = 1 + sizeOf X₁ + sizeOf w + sizeOf hw
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelSectROfProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : α) [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  ProbabilityTheory.IsZeroOrMarkovKernel (κ.sectR a)
-- Mathlib.Topology.Algebra.ConstMulAction
ContinuousOn.const_vadd : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α]
  [inst_3 : TopologicalSpace β] {g : β → α} {s : Set β}, ContinuousOn g s → ∀ (c : M), ContinuousOn (c +ᵥ g) s
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedGE_iff_antitone_get`. -/
List.SortedGE.antitone_get : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGE → Antitone l.get
-- Mathlib.Data.ENNReal.Inv
ENNReal.top_div_of_ne_top : ∀ {a : ENNReal}, a ≠ ⊤ → ⊤ / a = ⊤
-- Mathlib.Algebra.Group.Defs
/-- The power operation: `a ^ n = a * ··· * a`; `a ^ (-n) = a⁻¹ * ··· a⁻¹` (`n` times)  -/
ZPow.zpow : {G : Type u} → [self : ZPow G] → ℤ → G → G
-- Mathlib.Data.Seq.Computation
Computation.exists_of_mem_map : ∀ {α : Type u} {β : Type v} {f : α → β} {b : β} {s : Computation α}, b ∈ Computation.map f s → ∃ a ∈ s, f a = b
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.lift_of : ∀ {α : Type u} {R : Type v} [inst : CommRing R] (f : α → R) (x : α), (FreeCommRing.lift f) (FreeCommRing.of x) = f x
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrpIdIso_inv_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : CategoryTheory.Grp C),
  (CategoryTheory.Functor.mapGrpIdIso.inv.app X).hom.hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular : ∀ {α : Type u_1} {inst : MeasurableSpace α} {inst_1 : TopologicalSpace α} {μ : MeasureTheory.Measure α}
  [self : μ.InnerRegularCompactLTTop], μ.InnerRegularWRT IsCompact fun s => MeasurableSet s ∧ μ s ≠ ⊤
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.isModule : Lean.ParseImports.State → Bool
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.measureEntries_eq_list_sum : ∀ {α : Type u_1} {β : Type u_2} (es : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)))
  (i : ℕ),
  Lean.PersistentHashMap.Node.measure.measureEntries✝ es i =
    (List.map Lean.PersistentHashMap.Entry.measure (List.drop i es.toList)).sum
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RoiSliceData : (α : Type u) → (α → Type v) → [Ord α] → Type (max u v)
-- Batteries.Tactic.Init
/-- Given a proof `h` of `p`, `absurd h` changes the goal to `⊢ ¬ p`.
If `p` is a negation `¬q` then the goal is changed to `⊢ q` instead.
 -/
Batteries.Tactic.tacticAbsurd_ : Lean.ParserDescr
-- Mathlib.Logic.Hydra
/-- A singleton `{a}` is accessible under `CutExpand r` if `a` is accessible under `r`,
assuming `r` is irreflexive.  -/
Acc.cutExpand : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Irrefl r] {a : α}, Acc r a → Acc (Relation.CutExpand r) {a}
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the smallest key in the tree map, returning `none` if the map is empty.
 -/
Std.TreeMap.Raw.minKey? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Option α
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.blockTriangular_reindex_iff : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} {R : Type v} {M : Matrix m m R} [inst : LT α] [inst_1 : Zero R]
  {b : n → α} {e : m ≃ n}, ((Matrix.reindex e e) M).BlockTriangular b ↔ M.BlockTriangular (b ∘ ⇑e)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.unbotD_ofNat : ∀ {α : Type u} [inst : NatCast α] (d : α) (n : ℕ) [inst_1 : n.AtLeastTwo],
  WithBot.unbotD d (OfNat.ofNat n) = OfNat.ofNat n
-- Lean.Parser.Level
Lean.Parser.Level.imax.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Stream.Init
Stream'.interleave_even_odd : ∀ {α : Type u} (s₁ : Stream' α), s₁.even ⋈ s₁.odd = s₁
-- Mathlib.Data.List.Forall2
List.forall₂_take : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (n : ℕ) {l₁ : List α} {l₂ : List β},
  List.Forall₂ R l₁ l₂ → List.Forall₂ R (List.take n l₁) (List.take n l₂)
-- Mathlib.Order.CompleteBooleanAlgebra
sSup_disjoint_iff : ∀ {α : Type u} [inst : Order.Frame α] {a : α} {s : Set α}, Disjoint (sSup s) a ↔ ∀ b ∈ s, Disjoint b a
-- Mathlib.RepresentationTheory.Intertwining
/-- The equiv between representations are symmetric.  -/
Representation.Equiv.symm : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    {ρ : Representation A G V} → {σ : Representation A G W} → ρ.Equiv σ → σ.Equiv ρ
-- Mathlib.Combinatorics.Hindman
/-- Constructor for `FS`. This is the preferred spelling over `FS.head'`.  -/
Hindman.FS.head : ∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M), a.head ∈ Hindman.FS a
-- Aesop.Tree.Tracing
Aesop.Rapp.traceTreeCore : Aesop.Rapp → Aesop.TraceOption → Lean.MetaM Unit
-- Mathlib.Data.Set.SymmDiff
Set.inter_symmDiff_distrib_left : ∀ {α : Type u} (s t u : Set α), s ∩ symmDiff t u = symmDiff (s ∩ t) (s ∩ u)