mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Hom.Bounded
TopHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Top α] [inst_1 : Top β] [inst_2 : Top γ] {g₁ g₂ : TopHom β γ}
  {f : TopHom α β}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.add_neg`.  -/
Left.add_neg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a b : α},
  a < 0 → b < 0 → a + b < 0
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.sphere_zero_subset : ∀ {n d : ℕ}, Behrend.sphere n d 0 ⊆ 0
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonCond : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplit.mk.injEq : ∀ (pred : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred) (k : ℕ) (h : Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof)
  (pred_1 : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred) (k_1 : ℕ)
  (h_1 : Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof),
  ({ pred := pred, k := k, h := h } = { pred := pred_1, k := k_1, h := h_1 }) = (pred = pred_1 ∧ k = k_1 ∧ h = h_1)
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.supportLocallyFiniteWithinDomain : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y]
  (D : Function.locallyFinsuppWithin U Y), ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ D.support).Finite
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.singleton_injective : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α], Function.Injective fun x => {x}
-- Mathlib.Geometry.Manifold.PartitionOfUnity
BumpCovering.coe_toSmoothPartitionOfUnity : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (f : BumpCovering ι M s)
  (hf : ∀ (i : ι), ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ ⇑(f i)) (i : ι),
  ⇑((f.toSmoothPartitionOfUnity hf) i) = ⇑(f.toPartitionOfUnity i)
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A local diffeomorphism on `s` is differentiable on `s`.  -/
IsLocalDiffeomorphOn.mdifferentiableOn : ∀ {𝕜 : 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] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {s : Set M},
  IsLocalDiffeomorphOn I J n f s → n ≠ 0 → MDiff[s] f
-- Mathlib.Data.Seq.Defs
Stream'.Seq.val_eq_get : ∀ {α : Type u} (s : Stream'.Seq α) (n : ℕ), ↑s n = s.get? n
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- Additive semigroup homomorphism between the function spaces
`I → α` and `I → β`, induced by an additive semigroup homomorphism `f` between `α` and `β`  -/
AddHom.compLeft : {α : Type u_5} → {β : Type u_6} → [inst : Add α] → [inst_1 : Add β] → (α →ₙ+ β) → (I : Type u_7) → (I → α) →ₙ+ I → β
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformlyOn.congr : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] {f' : ι → β → α},
  HasSumUniformlyOn f g s →
    (∀ᶠ (n : Finset ι) in Filter.atTop, Set.EqOn (fun x => ∑ i ∈ n, f i x) (fun x => ∑ i ∈ n, f' i x) s) →
      HasSumUniformlyOn f' g s
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ (Y : C) {n : ℕ} (x₂ : CategoryTheory.Abelian.Ext S.X₂ Y n),
      (CategoryTheory.Abelian.Ext.mk₀ S.f).comp x₂ ⋯ = 0 → ∃ x₁, (CategoryTheory.Abelian.Ext.mk₀ S.g).comp x₁ ⋯ = x₂
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
/-- A *Hilbert C⋆-module* is a complex module `E` endowed with a right `A`-module structure
(where `A` is typically a C⋆-algebra) and an inner product `⟪x, y⟫_A` which satisfies the
following properties.  -/
CStarModule : (A : Type u_1) →
  (E : Type u_2) →
    [inst : NonUnitalSemiring A] →
      [StarRing A] →
        [Module ℂ A] →
          [inst : AddCommGroup E] →
            [Module ℂ E] → [PartialOrder A] → [SMul A E] → [Norm A] → [Norm E] → Type (max u_1 u_2)
-- Mathlib.Topology.Algebra.Group.Basic
add_mem_connectedComponent_zero : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddZeroClass G] [ContinuousAdd G] {g h : G},
  g ∈ connectedComponent 0 → h ∈ connectedComponent 0 → g + h ∈ connectedComponent 0
-- Mathlib.NumberTheory.FactorisationProperties
Nat.abundant_iff_not_perfect_and_not_deficient : ∀ {n : ℕ}, 0 ≠ n → (n.Abundant ↔ ¬n.Perfect ∧ ¬n.Deficient)
-- Mathlib.Topology.Sion
/-- From lower semicontinuity of `f(·, y)` and compactness  of `X`,
deduce that `sublevelLeft` sets are nonempty  -/
_private.Mathlib.Topology.Sion.0.Sion.nonempty_sublevelLeft : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β}
  [inst_1 : TopologicalSpace E],
  X.Nonempty →
    IsCompact X →
      (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
        ∀ (y : ↑Y) {b : β}, (∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b) → (Sion.sublevelLeft✝ X f b ↑y).Nonempty
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_zero : ∀ (f : (a : Ordinal.{u_3}) → a < 0 → Ordinal.{max u_3 u_4}), Ordinal.blsub 0 f = 0
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Reinterpret an equivariant monoid homomorphism as a monoid homomorphism.  -/
MulDistribMulActionHom.toMonoidHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {A : Type u_4} →
            [inst_2 : Monoid A] →
              [inst_3 : MulDistribMulAction M A] →
                {B : Type u_5} → [inst_4 : Monoid B] → [inst_5 : MulDistribMulAction N B] → (A →ₑ*[φ] B) → A →* B
-- Lean.Elab.InfoTree.Main
_private.Lean.Elab.InfoTree.Main.0.Lean.Elab.modifyInfoTrees : {m : Type → Type} →
  [Lean.Elab.MonadInfoTree m] →
    (Lean.PersistentArray Lean.Elab.InfoTree → Lean.PersistentArray Lean.Elab.InfoTree) → m Unit
-- Mathlib.Algebra.Field.Basic
div_sub_div : ∀ {K : Type u_1} [inst : Field K] (a : K) {b : K} (c : K) {d : K},
  b ≠ 0 → d ≠ 0 → a / b - c / d = (a * d - b * c) / (b * d)
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.instFiniteDimensionalOfIsReflexive : ∀ (K : Type u_4) (V : Type u_5) [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.IsReflexive K V], FiniteDimensional K V
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mk.injEq : ∀ {G : Type u_3} [inst : Group G] (toSubmonoid : Submonoid G)
  (inv_mem' : ∀ {x : G}, x ∈ toSubmonoid.carrier → x⁻¹ ∈ toSubmonoid.carrier) (toSubmonoid_1 : Submonoid G)
  (inv_mem'_1 : ∀ {x : G}, x ∈ toSubmonoid_1.carrier → x⁻¹ ∈ toSubmonoid_1.carrier),
  ({ toSubmonoid := toSubmonoid, inv_mem' := inv_mem' } = { toSubmonoid := toSubmonoid_1, inv_mem' := inv_mem'_1 }) =
    (toSubmonoid = toSubmonoid_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.keys_insertIfNew_perm : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : BEq α] [Std.TransOrd α]
  [Std.LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.keys.Perm
    (if Std.DTreeMap.Internal.Impl.contains k t = true then t.keys else k :: t.keys)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.affineBasicOpen_coe : ∀ (X : AlgebraicGeometry.Scheme) {U : ↑X.affineOpens} (f : ↑(X.presheaf.obj (Opposite.op ↑U))),
  ↑(X.affineBasicOpen f) = X.basicOpen f
-- Mathlib.Logic.Function.OfArity
Function.OfArity.const_zero : ∀ (α : Type u) {β : Type u} (b : β), Function.OfArity.const α b 0 = b
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.antitone_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], Antitone CategoryTheory.MorphismProperty.rlp
-- Mathlib.Analysis.BoxIntegral.Basic
/-- The integral of a function `f` over a box `I` along a filter `l` w.r.t. a volume `vol`.
Returns zero on non-integrable functions.  -/
BoxIntegral.integral : {ι : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              [Fintype ι] →
                BoxIntegral.Box ι →
                  BoxIntegral.IntegrationParams → ((ι → ℝ) → E) → BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤ → F
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      cmp k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
          k ∈ List.map Prod.fst l → (t.insertMany l).getKey? k' = some k
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.one_apply_zero : ∀ {M₀ : Type u_7} {N₀ : Type u_8} [inst : MulZeroOneClass M₀] [inst_1 : MulZeroOneClass N₀]
  [inst_2 : DecidablePred fun x => x = 0] [inst_3 : Nontrivial M₀] [inst_4 : NoZeroDivisors M₀], 1 0 = 0
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.Pi.containsIdentities : ∀ {J : Type w} {C : J → Type u} [inst : (j : J) → CategoryTheory.Category.{v, u} (C j)]
  (W : (j : J) → CategoryTheory.MorphismProperty (C j)) [∀ (j : J), (W j).ContainsIdentities],
  (CategoryTheory.MorphismProperty.pi W).ContainsIdentities
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.length_le_of_isSubwalk : ∀ {V : Type u_1} {G : SimpleGraph V} {u₁ v₁ u₂ v₂ : V} {q : G.Walk u₁ v₁} {p : G.Walk u₂ v₂},
  p.IsSubwalk q → p.length ≤ q.length
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Given `A : AddCommGrpCat` and a ring morphism `R →+* End A`, this is an object in
`ModuleCat R`, whose underlying abelian group is `A` and whose scalar multiplication is
given by `R`.  -/
ModuleCat.mkOfSMul : {R : Type u} → [inst : Ring R] → {A : AddCommGrpCat} → (R →+* CategoryTheory.End A) → ModuleCat R
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.ext_iff : ∀ {V : Type u} {x y : SimpleGraph V}, x = y ↔ x.Adj = y.Adj
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.isCompl_span_singleton_of_isCoatom_of_notMem : ∀ {K : Type u_3} {V : Type u_6} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {s : Submodule K V} {x : V}, IsCoatom s → x ∉ s → IsCompl s (K ∙ x)
-- Mathlib.Data.Num.ZNum
Num.mod_zero : ∀ (n : Num), n % 0 = n
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp ((F.mapComp g h).inv.toNatTrans.app ((F.map f).toFunctor.obj X))
      ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv.toNatTrans.app X) =
    CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).inv.toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).inv.toNatTrans.app X)
        ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X))
-- Mathlib.NumberTheory.Divisors
Nat.sup_divisors_id : ∀ (n : ℕ), n.divisors.sup id = n
-- Init.Control.Lawful.MonadAttach.Lemmas
WeaklyLawfulMonadAttach.pbind_eq_bind' : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] {x : m α} {f : α → m β}, (MonadAttach.pbind x fun a x => f a) = x >>= f
-- Mathlib.Data.Num.ZNum
Num.cast_sub' : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (m n : Num), ↑(m.sub' n) = ↑m - ↑n
-- Mathlib.RepresentationTheory.Character
/-- Orthogonality of characters for irreducible representations of finite group over an
algebraically closed field whose characteristic doesn't divide the order of the group.  -/
Representation.char_orthonormal : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Group G] [inst_1 : Field k]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [FiniteDimensional k V] [inst_5 : AddCommGroup W]
  [inst_6 : Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W)
  [inst_8 : Fintype G] [Invertible ↑(Nat.card G)] [IsAlgClosed k] [ρ.IsIrreducible] [σ.IsIrreducible],
  (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g * σ.character g⁻¹ = if Nonempty (σ.Equiv ρ) then 1 else 0
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_lt_natCast : ∀ {p : ℝ} {n : ℕ}, n ≠ 0 → (ENNReal.ofReal p < ↑n ↔ p < ↑n)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.toList_empty : ∀ {α : Type u} {β : Type v}, ∅.toList = []
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.stalkIsoₗ_inv : ∀ (R M : Type u) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  (AlgebraicGeometry.StructureSheaf.stalkIsoₗ✝ R M x).inv = AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ✝ R M x
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst_assoc : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g)
  {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp T.SpecTensorTo
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map T.tensorInl)
      (CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField T.x) h)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [inst_4 : Inhabited β] {f : α → β → Bool} {k : α} (h : m.WF),
  Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.filter f m) k =
    ((Std.DHashMap.Raw.Const.get? m k).pfilter fun x h' => f (m.getKey k ⋯) x).get!
-- Mathlib.CategoryTheory.Join.Sum
_private.Mathlib.CategoryTheory.Join.Sum.0.CategoryTheory.sum.match_3.eq_2 : ∀ (C : Type u_1) (D : Type u_2) (motive : C ⊕ D → Sort u_3) (X : D) (h_1 : (X : C) → motive (Sum.inl X))
  (h_2 : (X : D) → motive (Sum.inr X)),
  (match Sum.inr X with
    | Sum.inl X => h_1 X
    | Sum.inr X => h_2 X) =
    h_2 X
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.isoMk_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} (e : (i : ι) → D₁.obj i ≅ D₂.obj i)
  (comm :
    autoParam
      (∀ (i₁ i₂ : ι),
        CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom) (D₂.hom i₁ i₂) =
          CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom))
      CategoryTheory.Pseudofunctor.DescentData'.isoMk._auto_1)
  (i : ι), (CategoryTheory.Pseudofunctor.DescentData'.isoMk e comm).hom.hom i = (e i).hom
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothPresheafAddGroup.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],
  smoothPresheafAddGroup IM I M G =
    { obj := fun U => AddGrpCat.of ((smoothSheaf IM I M G).presheaf.obj U),
      map := fun {X Y} h => AddGrpCat.ofHom (ContMDiffMap.restrictAddMonoidHom IM I G ⋯), map_id := ⋯, map_comp := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- Given a proof that `A.det` has a constructive inverse, lift `A` to `(Matrix n n α)ˣ`  -/
Matrix.unitOfDetInvertible : {n : Type u'} →
  {α : Type v} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommRing α] → (A : Matrix n n α) → [Invertible A.det] → (Matrix n n α)ˣ
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.sr.injEq : ∀ {n : ℕ} (a a_1 : ZMod n), (DihedralGroup.sr a = DihedralGroup.sr a_1) = (a = a_1)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric.0.CovariantDerivative.tensorial_derivMetricTensorAux₁ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] {V : M → Type u_5}
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → NormedAddCommGroup (V x)]
  [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] [inst_10 : FiberBundle F V] (cov : CovariantDerivative I F V)
  [inst_11 : VectorBundle ℝ F V] [IsContMDiffRiemannianBundle I 1 F V] {x : M} (τ : (x : M) → V x),
  MDiffAt (T% τ) x → TensorialAt I F (fun x_1 => CovariantDerivative.derivMetricTensorAux✝ I cov x_1 τ x) x
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
/-- **Alias** of `MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal`. -/
MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} [inst : ENorm ε] {μ : MeasureTheory.Measure α},
  p ≠ 0 → p ≠ ⊤ → ∀ {f : α → ε}, MeasureTheory.eLpNorm f p μ = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
-- Lean.Expr
/-- Strict implicit binder annotation, e.g., `⦃x : α⦄`  -/
Lean.BinderInfo.strictImplicit : Lean.BinderInfo
-- Mathlib.Topology.Order.LawsonTopology
Topology.isLawson_le_isScott : ∀ {α : Type u_1} [inst : Preorder α] (L S : TopologicalSpace α) [Topology.IsLawson α] [Topology.IsScott α Set.univ],
  L ≤ S
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.instReflectsEffectiveEpiFamiliesComp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.ReflectsEffectiveEpiFamilies]
  [G.ReflectsEffectiveEpiFamilies], (F.comp G).ReflectsEffectiveEpiFamilies
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
IsIntegrallyClosed.minpoly_smul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [inst_3 : Algebra R S]
  [IsIntegrallyClosed R] [IsDomain S] [Module.IsTorsionFree R S] {r : R},
  r ≠ 0 → ∀ {s : S}, IsIntegral R s → minpoly R (r • s) = (minpoly R s).scaleRoots r
-- Mathlib.Order.CompleteLattice.Defs
/-- Any `CompleteSemilatticeInf` is in fact a `CompleteLattice`.

Note that this construction has bad definitional properties:
see the doc-string on `completeLatticeOfInf`.
 -/
completeLatticeOfCompleteSemilatticeInf : (α : Type u_8) → [CompleteSemilatticeInf α] → CompleteLattice α
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₂₁_single_ρ_add_single_inv_mul : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g h : G) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ A))
      ((fun₀ | (g, h) => (A.ρ g) a) + fun₀ | (g⁻¹, g * h) => a) =
    (fun₀ | g => (A.ρ g) a) + fun₀ | g⁻¹ => a
-- Init.Data.List.Basic
List.beq_cons_nil : ∀ {α : Type u} [inst : BEq α] {a : α} {as : List α}, (a :: as).beq [] = false
-- Mathlib.Analysis.BoxIntegral.Partition.Split
/-- Given a box `I` and `x ∈ (I.lower i, I.upper i)`, the hyperplane `{y : ι → ℝ | y i = x}` splits
`I` into two boxes. `BoxIntegral.Box.splitLower I i x` is the box `I ∩ {y | y i ≤ x}`
(if it is nonempty). As usual, we represent a box that may be empty as
`WithBot (BoxIntegral.Box ι)`.  -/
BoxIntegral.Box.splitLower : {ι : Type u_1} → BoxIntegral.Box ι → ι → ℝ → WithBot (BoxIntegral.Box ι)
-- Lean.LibrarySuggestions.SymbolFrequency
_private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.LibrarySuggestions.instAddNameMapNat : Add (Lean.NameMap ℕ)
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.const.injEq : ∀ {α : Type} (a a_1 : Bool), (Std.Tactic.BVDecide.BoolExpr.const a = Std.Tactic.BVDecide.BoolExpr.const a_1) = (a = a_1)
-- Mathlib.Topology.Baire.Lemmas
/-- In a nonempty Baire space, a residual set is not meagre.  -/
not_isMeagre_of_mem_residual : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] [Nonempty X] {s : Set X}, s ∈ residual X → ¬IsMeagre s
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Lex.instInfSetLexForall : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [(i : ι) → CompleteLinearOrder (α i)] → [WellFoundedLT ι] → InfSet (Lex ((i : ι) → (fun i => α i) i))
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.mk : (toLocallyRingedSpace : AlgebraicGeometry.LocallyRingedSpace) →
  (∀ (x : ↑toLocallyRingedSpace.toTopCat),
      ∃ U R,
        Nonempty (toLocallyRingedSpace.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))) →
    AlgebraicGeometry.Scheme
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.hasRightDualUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.HasRightDual (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.isSubgraph_iff : ∀ {α : Type u_1} {β : Type u_2} (H G : Graph α β),
  H.IsSubgraph G ↔
    autoParam (H.vertexSet ⊆ G.vertexSet) Graph.IsSubgraph.vertexSet_mono._autoParam ∧
      autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, H.IsLink e x y → G.IsLink e x y) Graph.IsSubgraph.isLink_mono._autoParam
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_mul_of_le_of_lt : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftStrictMono α] [MulRightMono α] {a b c d : α},
  a ≤ b → c < d → a * c < b * d
-- Mathlib.Algebra.Group.Pi.Lemmas
Set.piecewise_neg : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Neg (f i)] (s : Set I) [inst_1 : (i : I) → Decidable (i ∈ s)]
  (f₁ g₁ : (i : I) → f i), s.piecewise (-f₁) (-g₁) = -s.piecewise f₁ g₁
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.forget₂_bialgebra_obj : ∀ {R : Type u} [inst : CommRing R] (X : HopfAlgCat R),
  (CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj X = BialgCat.of R X.carrier
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.exists_open_set_nhds_of_compactsNhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K : TopologicalSpace.Compacts α} (L : ↑K.compactNhds),
  ∃ U, ↑K ⊆ ↑U ∧ ↑U ⊆ ↑↑L
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.notStrictValue.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instLEAbs : {α : Type u_1} → [inst : Field α] → [inst_1 : LinearOrder α] → [inst_2 : IsStrictOrderedRing α] → LE (CauSeq α abs)