mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.minEntry?.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k : α) →
                (v : β) →
                  (r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r)) →
            ((size : ℕ) →
                (k : α) →
                  (v : β) →
                    (size_1 : ℕ) →
                      (k_1 : α) →
                        (v_1 : β) →
                          (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                            motive
                              (Std.DTreeMap.Internal.Impl.inner size k v
                                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)) →
              motive x
-- Mathlib.Data.Set.Subsingleton
Set.Nontrivial.eq_1 : ∀ {α : Type u} (s : Set α), s.Nontrivial = ∃ x ∈ s, ∃ y ∈ s, x ≠ y
-- Std.Async.Select
/-- A cleanup function that is called once any `Selector` has won the `Selectable.one` race.
 -/
Std.Async.Selector.unregisterFn : {α : Type} → Std.Async.Selector α → Std.Async.Async Unit
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
continuousOn_cfcₙ_setProd_nhdsSet : ∀ {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [ContinuousStar A]
  [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [CompleteSpace A] {s : Set 𝕜},
  ContinuousOn (fun fa => cfcₙ ((UniformOnFun.toFun {s}) fa.1) fa.2)
    ({f | ContinuousOn ((UniformOnFun.toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ
      {a | p a ∧ s ∈ nhdsSet (quasispectrum 𝕜 a)})
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
_private.Mathlib.CategoryTheory.Preadditive.OfBiproducts.0.CategoryTheory.SemiadditiveOfBinaryBiproducts.«term_+ᵣ_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.toGeneratedByTopCat_obj : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] (X_1 : ContinuousGeneratedByCat X),
  ContinuousGeneratedByCat.toGeneratedByTopCat.obj X_1 =
    { obj := TopCat.of (Topology.WithGeneratedByTopology X ↑X_1), property := ⋯ }
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.map_isLoop_iff : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {e : α} {f : α → β} {hf : Set.InjOn f M.E},
  autoParam (e ∈ M.E) Matroid.map_isLoop_iff._auto_1 → ((M.map f hf).IsLoop (f e) ↔ M.IsLoop e)
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
fst_integral : ∀ {X : Type u_1} {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F]
  [CompleteSpace F] {f : X → E × F}, MeasureTheory.Integrable f μ → (∫ (x : X), f x ∂μ).1 = ∫ (x : X), (f x).1 ∂μ
-- Mathlib.Order.Preorder.Finite
LinearOrder.strong_induction_of_finite : ∀ {α : Type u_4} [inst : LinearOrder α] [Finite α] {motive : α → Prop},
  (∀ (j : α), (∀ k < j, motive k) → motive j) → ∀ (i : α), motive i
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nnnorm_ofLp : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] (f : PiLp ⊤ β),
  ‖f.ofLp‖₊ = ‖f‖₊
-- Mathlib.Analysis.Complex.Trigonometric
Real.cosh_abs : ∀ (x : ℝ), Real.cosh |x| = Real.cosh x
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valued.toNormedField.norm_le_iff : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne] {x x' : L}, ‖x‖ ≤ ‖x'‖ ↔ Valued.v x ≤ Valued.v x'
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.natTransEquiv_symm_apply_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} (f : F ⟶ G) (x : C),
  (CategoryTheory.Functor.natTransEquiv.symm f).app x =
    TypeCat.ofHom fun x_1 => CategoryTheory.Functor.HomObj.ofNatTrans f
-- Mathlib.Order.Bounds.Basic
/-- An alternative constructor for `Lattice` using `IsLUB` and `IsGLB`.  -/
Lattice.ofIsLUBofIsGLB : {α : Type u_1} →
  [inst : PartialOrder α] →
    (sup inf : α → α → α) → (∀ (a b : α), IsLUB {a, b} (sup a b)) → (∀ (a b : α), IsGLB {a, b} (inf a b)) → Lattice α
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_dite_eq : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (a : ι)
  (b : (x : ι) → a = x → M), (∑ x ∈ s, if h : a = x then b x h else 0) = if a ∈ s then b a ⋯ else 0
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.Raw.Const.getEntryGED : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α → α × β → α × β
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (page : (r : ℤ) → autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_1 → HomologicalComplex C (c r))
  (iso :
    (r r' : ℤ) →
      (pq : κ) →
        (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence._auto_3) →
          (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_5) → (page r ⋯).homology pq ≅ (page r' ⋯).X pq)
  (page_1 : (r : ℤ) → autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_1 → HomologicalComplex C (c r))
  (iso_1 :
    (r r' : ℤ) →
      (pq : κ) →
        (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence._auto_3) →
          (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_5) →
            (page_1 r ⋯).homology pq ≅ (page_1 r' ⋯).X pq),
  ({ page := page, iso := iso } = { page := page_1, iso := iso_1 }) = (page = page_1 ∧ iso ≍ iso_1)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) binary products
preserves binary biproducts.  -/
CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F],
  CategoryTheory.Limits.PreservesBinaryBiproducts F
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_mul : ∀ (a b : UInt64), (a * b).toUInt16 = a.toUInt16 * b.toUInt16
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- `SemimoduleCat.Hom.hom` bundled as an additive equivalence.  -/
SemimoduleCat.homAddEquiv : {R : Type u} → [inst : Semiring R] → {M N : SemimoduleCat R} → (M ⟶ N) ≃+ (↑M →ₗ[R] ↑N)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticSeverity.warning : Lean.Lsp.DiagnosticSeverity
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.coeff_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f), 1 < f.natDegree → h.coeff h.root = Pi.single 1 1
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_add_eq_nnnorm_left : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (x : E) {y : E}, ‖y‖₊ = 0 → ‖x + y‖₊ = ‖x‖₊
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- The C-identity morphism
  `𝟙_ C ⟶ hom(x, x)`
used to equip `C` with the structure of a `C`-category  -/
CategoryTheory.MonoidalClosed.id : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (x : C) → [inst_2 : CategoryTheory.Closed x] → CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ x ⟹ x
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.add_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f g : M [⋀^ι]→L[R] N) [inst_7 : ContinuousAdd N] (v : ι → M), (f + g) v = f v + g v
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.toPiNat.sizeOf_spec : ∀ {ι : Type u_2} {X : Type u_5} {Y : ι → Type u_6} {f : (i : ι) → X → Y i} [inst : SizeOf ι] [inst_1 : SizeOf X]
  [inst_2 : (a : ι) → SizeOf (Y a)] (ofPiNat : X), sizeOf { ofPiNat := ofPiNat } = 1 + sizeOf ofPiNat
-- Lean.Declaration
Lean.QuotKind : Type
-- Lean.DocString.Types
Lean.Doc.instReprDescItem.repr : {α : Type u_1} → {β : Type u_2} → [Repr α] → [Repr β] → Lean.Doc.DescItem α β → ℕ → Std.Format
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Given a collection of isomorphisms between corresponding summands of a pair of biproducts
indexed by the same type, we obtain an isomorphism between the biproducts.  -/
CategoryTheory.Limits.biproduct.mapIso : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {f g : J → C} →
          [inst_2 : CategoryTheory.Limits.HasBiproduct f] →
            [inst_3 : CategoryTheory.Limits.HasBiproduct g] → ((b : J) → f b ≅ g b) → (⨁ f ≅ ⨁ g)
-- ProofWidgets.Component.MakeEditLink
ProofWidgets.instToJsonMakeEditLinkProps : Lean.ToJson ProofWidgets.MakeEditLinkProps
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocFrame.mk.inj : ∀ {content : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)}
  {priorParts : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)} {titleString : String}
  {title : Array (Lean.Doc.Inline Lean.ElabInline)} {content_1 : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)}
  {priorParts_1 : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)} {titleString_1 : String}
  {title_1 : Array (Lean.Doc.Inline Lean.ElabInline)},
  { content := content, priorParts := priorParts, titleString := titleString, title := title } =
      { content := content_1, priorParts := priorParts_1, titleString := titleString_1, title := title_1 } →
    content = content_1 ∧ priorParts = priorParts_1 ∧ titleString = titleString_1 ∧ title = title_1
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.cochainComplexXIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.ProjectiveResolution X) (n : ℤ) (k : ℕ)
  (h : -↑k = n), R.cochainComplexXIso n k h = HomologicalComplex.extendXIso R.complex ComplexShape.embeddingDownNat h
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.ιFree_freeMap_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {I J_1 : Type u} (f : I → J_1) (i : I) {Z : SheafOfModules R}
  (h : SheafOfModules.free J_1 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i)
      (CategoryTheory.CategoryStruct.comp (SheafOfModules.freeMap f) h) =
    CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree (f i)) h
-- Mathlib.Analysis.Calculus.VectorField
/-- The Lie bracket commutes with taking pullbacks. This requires the function to have symmetric
second derivative. Version in a complete space. One could also give a version avoiding
completeness but requiring that `f` is a local diffeomorphism.  -/
VectorField.pullback_lieBracket_of_isSymmSndFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace E]
  {f : E → F} {V W : F → F} {x : E},
  IsSymmSndFDerivAt 𝕜 f x →
    ContDiffAt 𝕜 2 f x →
      DifferentiableAt 𝕜 V (f x) →
        DifferentiableAt 𝕜 W (f x) →
          VectorField.pullback 𝕜 f (VectorField.lieBracket 𝕜 V W) x =
            VectorField.lieBracket 𝕜 (VectorField.pullback 𝕜 f V) (VectorField.pullback 𝕜 f W) x
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.not_rankFinite : ∀ {α : Type u_1} (M : Matroid α) [M.RankInfinite], ¬M.RankFinite
-- Aesop.Search.SearchM
Aesop.instInhabitedNormSimpContext : Inhabited Aesop.NormSimpContext
-- Mathlib.RingTheory.Discriminant
Algebra.discr_def : ∀ (A : Type u) {B : Type v} {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra A B] [inst_4 : Fintype ι] (b : ι → B), Algebra.discr A b = (Algebra.traceMatrix A b).det
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instGroup : {α : Type u_1} → [Group α] → Group (Colex α)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.derivative_T_eval_one : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ),
  Polynomial.eval 1 (Polynomial.derivative (Polynomial.Chebyshev.T R n)) = ↑n ^ 2
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.homologyMap'_sub : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData),
  CategoryTheory.ShortComplex.homologyMap' (φ - φ') h₁ h₂ =
    CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂ - CategoryTheory.ShortComplex.homologyMap' φ' h₁ h₂
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.abs_def : ∀ {α : Type u} {β : Type v} {φ : Ultrafilter α} [inst : AddCommGroup β] [inst_1 : LinearOrder β] (x : (↑φ).Germ β),
  |x| = Filter.Germ.map abs x
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.nle.sizeOf_spec : ∀ (lhs rhs : ℕ) (proof : Lean.Expr),
  sizeOf (Mathlib.Tactic.Order.AtomicFact.nle lhs rhs proof) = 1 + sizeOf lhs + sizeOf rhs + sizeOf proof
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.eq.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)}
  {k k' : ℕ} (hk : k < n) (hk' : k' < n) (j : (X k hk).fst) (j' : (X k' hk').fst)
  (a a_1 : (X k hk).snd j ⟶ (X k' hk').snd j') (k_1 k'_1 : ℕ) (hk_1 : k_1 < n) (hk'_1 : k'_1 < n)
  (j_1 : (X k_1 hk_1).fst) (j'_1 : (X k'_1 hk'_1).fst) (a_2 a_3 : (X k_1 hk_1).snd j_1 ⟶ (X k'_1 hk'_1).snd j'_1),
  (CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.eq✝ hk hk' j j' a a_1 =
      CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.eq✝ hk_1 hk'_1 j_1 j'_1 a_2 a_3) =
    (k = k_1 ∧ k' = k'_1 ∧ j ≍ j_1 ∧ j' ≍ j'_1 ∧ a ≍ a_2 ∧ a_1 ≍ a_3)
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
HasFDerivWithinAt.log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {f' : StrongDual ℝ E}
  {s : Set E}, HasFDerivWithinAt f f' s x → f x ≠ 0 → HasFDerivWithinAt (fun x => Real.log (f x)) ((f x)⁻¹ • f') s x
-- Init.Data.Int.Gcd
Int.pow_gcd_pow : ∀ {n m : ℤ} {k : ℕ}, (n ^ k).gcd (m ^ k) = n.gcd m ^ k
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.app_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Comonad C}
  (self : CategoryTheory.ComonadHom M N) (X : C),
  CategoryTheory.CategoryStruct.comp (self.app X) (N.ε.app X) = M.ε.app X
-- Mathlib.Algebra.Order.Interval.Basic
Interval.commMonoid : {α : Type u_2} → [inst : CommMonoid α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → CommMonoid (Interval α)
-- Mathlib.RingTheory.Multiplicity
multiplicity_self : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {a : α}, multiplicity a a = 1
-- Mathlib.MeasureTheory.Integral.Prod
/-- Change the order of integration, when one of the integrals is an interval integral.  -/
MeasureTheory.intervalIntegral_integral_swap : ∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] {a b : ℝ} {f : ℝ → α → E},
  MeasureTheory.Integrable (Function.uncurry f) ((MeasureTheory.volume.restrict (Set.uIoc a b)).prod μ) →
    ∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ = ∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Splitting.coe_addMonoidHom_mk : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} (s : G →+ E) (hs : Function.RightInverse ⇑s ⇑S.rightHom),
  ↑{ toAddMonoidHom := s, rightInverse_rightHom := hs } = s
-- Lean.Elab.Tactic.Grind.Basic
/-- Cache key for `Sym.simp` variant invocations.  -/
Lean.Elab.Tactic.Grind.SimpCacheKey : Type
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.continuous_fromLoop : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N),
  Continuous (GenLoop.fromLoop i)
-- Mathlib.Data.Finsupp.Basic
/-- `subtypeDomain p f` is the restriction of the finitely supported function `f` to subtype `p`.  -/
Finsupp.subtypeDomain : {α : Type u_1} → {M : Type u_5} → [inst : Zero M] → (p : α → Prop) → (α →₀ M) → Subtype p →₀ M
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for reverse monotonicity of addition on the right,
namely `a₁ + b ≤ a₂ + b → a₁ ≤ a₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedCancelAddMonoid`.  -/
AddRightReflectLE : (M : Type u_1) → [Add M] → [LE M] → Prop
-- Mathlib.Topology.Algebra.Support
locallyFinite_support_iff : ∀ {X : Type u_1} {M : Type u_7} {ι : Type u_9} [inst : TopologicalSpace X] [inst_1 : Zero M] {f : ι → X → M},
  (LocallyFinite fun i => Function.support (f i)) ↔ LocallyFinite fun i => tsupport (f i)
-- Lean.Environment
Lean.ModuleData.mk.inj : ∀ {isModule : Bool} {imports : Array Lean.Import} {constNames : Array Lean.Name} {constants : Array Lean.ConstantInfo}
  {extraConstNames : Array Lean.Name} {entries : Array (Lean.Name × Array Lean.EnvExtensionEntry)} {isModule_1 : Bool}
  {imports_1 : Array Lean.Import} {constNames_1 : Array Lean.Name} {constants_1 : Array Lean.ConstantInfo}
  {extraConstNames_1 : Array Lean.Name} {entries_1 : Array (Lean.Name × Array Lean.EnvExtensionEntry)},
  { isModule := isModule, imports := imports, constNames := constNames, constants := constants,
        extraConstNames := extraConstNames, entries := entries } =
      { isModule := isModule_1, imports := imports_1, constNames := constNames_1, constants := constants_1,
        extraConstNames := extraConstNames_1, entries := entries_1 } →
    isModule = isModule_1 ∧
      imports = imports_1 ∧
        constNames = constNames_1 ∧ constants = constants_1 ∧ extraConstNames = extraConstNames_1 ∧ entries = entries_1
-- Mathlib.Topology.Homeomorph.Lemmas
/-- The product over `S ⊕ T` of a family of topological spaces
is homeomorphic to the product of (the product over `S`) and (the product over `T`).

This is `Equiv.sumPiEquivProdPi` as a `Homeomorph`.
 -/
Homeomorph.sumPiEquivProdPi : (S : Type u_7) →
  (T : Type u_8) →
    (A : S ⊕ T → Type u_9) →
      [inst : (st : S ⊕ T) → TopologicalSpace (A st)] →
        ((st : S ⊕ T) → A st) ≃ₜ ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))
-- Mathlib.Analysis.Calculus.FDeriv.Star
fderiv_star : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : StarModule 𝕜 F] [inst_8 : ContinuousStar F] {f : E → F} {x : E}
  [inst_9 : TrivialStar 𝕜], fderiv 𝕜 (fun y => star (f y)) x = ↑(starL' 𝕜) ∘SL fderiv 𝕜 f x
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.toOneHom_injective : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N], Function.Injective MonoidHom.toOneHom
-- Mathlib.Order.Sublattice
Sublattice.map_map : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  {L : Sublattice α} (g : LatticeHom β γ) (f : LatticeHom α β),
  Sublattice.map g (Sublattice.map f L) = Sublattice.map (g.comp f) L
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.sub : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x₁ x₂ y₁ y₂ : M}, x₁ ≡ y₁ [SMOD U] → x₂ ≡ y₂ [SMOD U] → x₁ - x₂ ≡ y₁ - y₂ [SMOD U]
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} (h : t.WF),
  (Std.DTreeMap.Raw.filter f t).getKey? k = (t.getKey? k).pfilter fun x h' => f x (Std.DTreeMap.Raw.Const.get t x ⋯)
-- Lean.Util.FoldConsts
Lean.Expr.FoldConstsImpl.State.mk : Lean.PtrSet Lean.Expr → Lean.NameHashSet → Lean.Expr.FoldConstsImpl.State
-- Mathlib.GroupTheory.GroupAction.SubMulAction
coe_smul_fixedPoints_of_normal : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {H : Subgroup G} [hH : H.Normal] (g : G)
  (a : ↑(MulAction.fixedPoints (↥H) α)), ↑(g • a) = g • ↑a
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.WF.of_le : ∀ {n n' : ℕ} {α : Type u_1} {le : α → α → Bool} {s : Batteries.BinomialHeap.Imp.Heap α},
  n ≤ n' → Batteries.BinomialHeap.Imp.Heap.WF le n' s → Batteries.BinomialHeap.Imp.Heap.WF le n s
-- Mathlib.Combinatorics.SimpleGraph.LineGraph
/-- Lift an isomorphism between graphs to an isomorphism between their line graphs  -/
SimpleGraph.Iso.lineGraph : {V : Type u_1} → {V' : Type u_2} → {G : SimpleGraph V} → {G' : SimpleGraph V'} → G ≃g G' → G.lineGraph ≃g G'.lineGraph
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- Components of the unit of the adjunction `Cat.objects ⊣ Codiscrete.functorToCat`.  -/
CategoryTheory.Codiscrete.unitApp : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (CategoryTheory.Codiscrete C)
-- Mathlib.Order.Defs.PartialOrder
lt_of_le_of_ne' : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ≤ a → a ≠ b → b < a
-- Mathlib.Data.Int.ModEq
Int.add_modulus_mul_modEq_iff : ∀ {n a b c : ℤ}, a + n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.instFinalStructuredArrowCompPreOfRepresentablyFlat : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : E) [CategoryTheory.RepresentablyFlat F],
  (CategoryTheory.StructuredArrow.pre X F G).Final
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tensorRId_symm_apply : ∀ {R : Type uR} {M₁ : Type uM₁} [inst : CommRing R] [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
  [inst_3 : Invertible 2] (Q₁ : QuadraticForm R M₁) (x : M₁), Q₁.tensorRId.symm x = (TensorProduct.rid R M₁).symm x
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.dim_eq_of_mk_eq : ∀ {X : SSet} {n m : ℕ} {x : X.obj (Opposite.op { len := n })} {y : X.obj (Opposite.op { len := m })},
  { dim := n, simplex := x } = { dim := m, simplex := y } → n = m