mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.SInt.Lemmas
Int64.ofIntLE_eq_ofInt : ∀ {n : ℤ} (h₁ : Int64.minValue.toInt ≤ n) (h₂ : n ≤ Int64.maxValue.toInt), Int64.ofIntLE n h₁ h₂ = Int64.ofInt n
-- Lean.Meta.Tactic.SolveByElim
/-- Call `constructor` when no lemmas apply.  -/
Lean.Meta.SolveByElim.SolveByElimConfig.constructorAfter : optParam Lean.Meta.SolveByElim.SolveByElimConfig { } → Lean.Meta.SolveByElim.SolveByElimConfig
-- Lean.Parser.Extra
Lean.Parser.mkAntiquot.parenthesizer : String → Lean.SyntaxNodeKind → optParam Bool true → optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.Valid.toEnd : ∀ (it : String.Legacy.Iterator), it.toEnd.Valid
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by weight, strict inequality version:
if the total weight of a finite set of pigeons is less than `n • b`, they are sorted into some
pigeonholes, and for all but `n` pigeonholes the total weight of the pigeons there is nonnegative,
then for at least one of these `n` pigeonholes, the total weight of the pigeons in this pigeonhole
is less than `b`.  -/
Finset.exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M}
  {b : M} [inst_1 : AddCommMonoid M] [inst_2 : LinearOrder M] [IsOrderedCancelAddMonoid M],
  (∀ y ∉ t, 0 ≤ ∑ x ∈ s with f x = y, w x) → ∑ x ∈ s, w x < t.card • b → ∃ y ∈ t, ∑ x ∈ s with f x = y, w x < b
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.smul : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {𝕜 : Type u_8}
  [inst_2 : NormedAddCommGroup 𝕜] [inst_3 : SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E] (c : 𝕜),
  μ.Integrable f → μ.Integrable (c • f)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.symm : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y : CategoryTheory.FreeMonoidalCategory C} (f g : X.Hom Y) (a : CategoryTheory.FreeMonoidalCategory.HomEquiv f g),
  CategoryTheory.FreeMonoidalCategory.HomEquiv.below a →
    motive f g a → CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getD : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [LawfulBEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → β a → β a
-- Mathlib.RingTheory.Coalgebra.Basic
/-- Transfer `Coalgebra` across an `Equiv`.  -/
Equiv.coalgebra : (R : Type u_1) →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid B] → [inst_2 : Module R B] → [Coalgebra R B] → (e : A ≃ B) → Coalgebra R A
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instContinuousConstSMulIdOfIsScalarTower : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] [inst_5 : ContinuousConstSMul 𝕜₂ F] {S : Type u_5}
  [inst_6 : DistribSMul S F] [inst_7 : SMulCommClass 𝕜₂ S F] [inst_8 : ContinuousConstSMul S F] [inst_9 : SMul S 𝕜₂]
  [IsScalarTower S 𝕜₂ 𝕜₂] [IsScalarTower S 𝕜₂ F], ContinuousConstSMul S (F →WOT[𝕜₂] F)
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanDeclIdent.mk.inj : ∀ {module decl module_1 decl_1 : Lean.Name},
  { module := module, decl := decl } = { module := module_1, decl := decl_1 } → module = module_1 ∧ decl = decl_1
-- Mathlib.Algebra.Lie.Rank
LieAlgebra.isRegular_iff_finrank_engel_eq_rank : ∀ (K : Type u_7) {L : Type u_8} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : Module.Finite K L] (x : L),
  LieAlgebra.IsRegular K x ↔ Module.finrank K ↥(LieSubalgebra.engel K x) = LieAlgebra.rank K L
-- Mathlib.Topology.Convenient.HomSpace
Topology.ContinuousMapGeneratedBy.continuous_precomp : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Z : Type v'} [inst_1 : TopologicalSpace Z]
  {T : Type v''} [inst_2 : TopologicalSpace T] {i : ι} (f : C(X i, Z)),
  Continuous (Topology.ContinuousMapGeneratedBy.precomp f)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.toList_emptyWithCapacity : ∀ {α : Type u} {c : ℕ} {β : Type v},
  Std.DHashMap.Raw.Const.toList ↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity c) = []
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply : ∀ (X : AlgebraicGeometry.Scheme) (R : CommRingCat) [inst : IsLocalRing ↑R]
  (xf : (x : ↥X) × { f // IsLocalHom (CommRingCat.Hom.hom f) }),
  (AlgebraicGeometry.SpecToEquivOfLocalRing X R).symm xf =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map ↑xf.snd) (X.fromSpecStalk xf.fst)
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.mk.inj : ∀ {perm : Mathlib.Tactic.Translate.Permutation} {argReorders : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder)}
  {perm_1 : Mathlib.Tactic.Translate.Permutation} {argReorders_1 : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder)},
  { perm := perm, argReorders := argReorders } = { perm := perm_1, argReorders := argReorders_1 } →
    perm = perm_1 ∧ argReorders = argReorders_1
-- Mathlib.Algebra.Homology.DifferentialObject
/-- The counit isomorphism for `dgoEquivHomologicalComplex`.
 -/
HomologicalComplex.dgoEquivHomologicalComplexCounitIso : {β : Type u_1} →
  [inst : AddCommGroup β] →
    (b : β) →
      (V : Type u_2) →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} V] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] →
            (HomologicalComplex.homologicalComplexToDGO b V).comp (HomologicalComplex.dgoToHomologicalComplex b V) ≅
              CategoryTheory.Functor.id (HomologicalComplex V (ComplexShape.up' b))
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.skewProd_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommGroup M₄] {module_M : Module R M}
  {module_M₂ : Module R M₂} {module_M₃ : Module R M₃} {module_M₄ : Module R M₄} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄)
  (f : M →ₗ[R] M₄) (x : M × M₃), (e₁.skewProd e₂ f) x = (e₁ x.1, e₂ x.2 + f x.1)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyι_comp_asIsoHomologyι_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [inst_2 : S.HasHomology] {Z : C} (h : S.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.homologyι (CategoryTheory.CategoryStruct.comp (S.asIsoHomologyι hg).inv h) = h
-- Mathlib.RingTheory.DedekindDomain.GaussLemma
Polynomial.contentIdeal.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.contentIdeal = Ideal.span ↑p.coeffs
-- Mathlib.Analysis.InnerProductSpace.TwoDim
_private.Mathlib.Analysis.InnerProductSpace.TwoDim.0.Orientation.termJ_1 : Lean.ParserDescr
-- Lean.Language.Lean.Types
/-- Resulting parser state.  -/
Lean.Language.Lean.CommandParsedSnapshot.parserState : Lean.Language.Lean.CommandParsedSnapshot → Lean.Parser.ModuleParserState
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A pointed and salient cone defines a partial order.  -/
ConvexCone.toPartialOrder : {R : Type u_2} →
  {G : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : AddCommGroup G] → [inst_3 : SMul R G] → (C : ConvexCone R G) → C.Pointed → C.Salient → PartialOrder G
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.subst.sizeOf_spec : ∀ (x : Int.Internal.Linear.Var) (c₁ : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) (c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.subst x c₁ c₂) = 1 + sizeOf x + sizeOf c₁ + sizeOf c₂
-- Mathlib.Algebra.Group.Defs
instIsDedekindFiniteMonoidOfIsMulCommutative : ∀ (M : Type u_2) [inst : MulOne M] [IsMulCommutative M], IsDedekindFiniteMonoid M
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Given a colimit cocone for the pair `f g : X ⟶ Y`, for any `Z`, morphisms from the cocone point
to `Z` are in bijection with morphisms `h : Y ⟶ Z` such that `f ≫ h = g ≫ h`.
Further, this bijection is natural in `Z`: see `Cofork.IsColimit.homIso_natural`.
This is a special case of `IsColimit.homIso'`, often useful to construct adjunctions.
 -/
CategoryTheory.Limits.Cofork.IsColimit.homIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        {t : CategoryTheory.Limits.Cofork f g} →
          CategoryTheory.Limits.IsColimit t →
            (Z : C) →
              (t.pt ⟶ Z) ≃ { h // CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h }
-- Mathlib.Data.Option.Basic
Option.casesOn'_some : ∀ {α : Type u_1} {β : Type u_2} (x : β) (f : α → β) (a : α), (some a).casesOn' x f = f a
-- Init.Grind.Tactics
/-- `sym` enters an interactive symbolic simulation mode built on `grind`.
Unlike `grind =>`, it does not eagerly introduce hypotheses or apply by-contradiction,
giving the user explicit control over `intro`, `apply`, and `internalize` steps.

Example:
```
example (x : Nat) : myP x → myQ x := by
  sym [myP_myQ] =>
    intro h
    finish
```
 -/
Lean.Parser.Tactic.sym : Lean.ParserDescr
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.toListRev_zip_of_finite_right : ∀ {α₁ α₂ β₁ β₂ : Type u_1} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂] {it₁ : Std.Iter β₁}
  {it₂ : Std.Iter β₂} [Std.Iterators.Productive α₁ Id] [Std.Iterators.Finite α₂ Id],
  (it₁.zip it₂).toListRev = ((Std.Iter.take it₂.toList.length it₁).toList.zip it₂.toList).reverse
-- Mathlib.Order.Category.HeytAlg
HeytAlg.mk.injEq : ∀ (carrier : Type u_1) [str : HeytingAlgebra carrier] (carrier_1 : Type u_1) (str_1 : HeytingAlgebra carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsLinearSet.vadd : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M} (a : M), IsLinearSet s → IsLinearSet (a +ᵥ s)
-- Mathlib.CategoryTheory.Abelian.Opposite
/-- The cokernel of `g.unop` is the opposite of `kernel g`.  -/
CategoryTheory.cokernelUnopOp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {A B : Cᵒᵖ} → (g : A ⟶ B) → Opposite.op (CategoryTheory.Limits.cokernel g.unop) ≅ CategoryTheory.Limits.kernel g
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.shiftIso_zero_inv_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (a : A) (X : C),
  (F.shiftIso 0 a a ⋯).inv.app X = (CategoryTheory.shiftFunctorZero D A).inv.app ((F.functor a).1 X)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_indicator_sub_indicator : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (s t : Set α) (f : α → E),
  MeasureTheory.eLpNorm (s.indicator f - t.indicator f) p μ = MeasureTheory.eLpNorm ((symmDiff s t).indicator f) p μ
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
/-- Typeclass for clauses. An instance `[Clause α β]` indicates that `β` is the type of a clause with
variables of type `α`.
 -/
Std.Tactic.BVDecide.LRAT.Internal.Clause : outParam (Type u) → Type v → Type (max u v)
-- Mathlib.Data.Finset.Piecewise
Finset.update_piecewise : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f g : (i : ι) → π i) [inst : (j : ι) → Decidable (j ∈ s)]
  [inst_1 : DecidableEq ι] (i : ι) (v : π i),
  Function.update (s.piecewise f g) i v = s.piecewise (Function.update f i v) (Function.update g i v)
-- Init.Prelude
instLTFin : {n : ℕ} → LT (Fin n)
-- Init.Data.List.Nat.Modify
List.modifyHead_eq_nil_iff : ∀ {α : Type u_1} {f : α → α} {l : List α}, List.modifyHead f l = [] ↔ l = []
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- Given two consecutive edges `f`, `g`  in a 2-truncated quasicategory, nonconstructively choose
an edge that is the diagonal of a 2-simplex with spine given by `f` and `g`. The `CompStruct`
witnessing this property is given by `Edge.composeStruct`.
 -/
SSet.Truncated.Edge.comp : {A : SSet.Truncated 2} →
  [A.Quasicategory₂] →
    {x y z : A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })} →
      SSet.Truncated.Edge x y → SSet.Truncated.Edge y z → SSet.Truncated.Edge x z
-- Qq.MatchImpl
Qq.Impl.PatVarDecl.fvarTy : Qq.Impl.PatVarDecl → Q(Type)
-- Mathlib.Geometry.Convex.Set
Convexity.subtypeVal_iConvexComb : ∀ {I : Type u_2} {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R X] (s : Set X) (hs : Convexity.IsConvexSet R s)
  (w : Convexity.StdSimplex R I) (f : I → ↑s), ↑(Convexity.iConvexComb w f) = Convexity.iConvexComb w fun i => ↑(f i)
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curryFinFinset_symm_apply : ∀ {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] {k l : ℕ} {s : Finset (Fin n)}
  (hk : s.card = k) (hl : sᶜ.card = l) (f : G [×k]→L[𝕜] G [×l]→L[𝕜] G') (m : Fin n → G),
  ((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl).symm f) m =
    (f fun i => m ((finSumEquivOfFinset hk hl) (Sum.inl i))) fun i => m ((finSumEquivOfFinset hk hl) (Sum.inr i))
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to1.tr.match_1.splitter : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      (motive : Turing.TM1to1.Λ' Γ Λ σ → Sort u_4) →
        (x : Turing.TM1to1.Λ' Γ Λ σ) →
          ((l : Λ) → motive (Turing.TM1to1.Λ'.normal l)) →
            ((a : Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1to1.Λ'.write a q)) → motive x
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
CategoryTheory.ShortComplex.ShortExact.exactAt_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)},
  S.ShortExact →
    ∀ (j : ι),
      autoParam (CategoryTheory.Mono (HomologicalComplex.homologyMap S.g j))
          CategoryTheory.ShortComplex.ShortExact.exactAt_X₁._auto_1 →
        autoParam (∀ (i : ι), c.Rel i j → CategoryTheory.Epi (HomologicalComplex.homologyMap S.g i))
            CategoryTheory.ShortComplex.ShortExact.exactAt_X₁._auto_3 →
          S.X₁.ExactAt j
-- Mathlib.MeasureTheory.Measure.TightNormed
/-- In a proper pseudo-metric space, a set of measures `S` is tight if and only if
the function `r ↦ ⨆ μ ∈ S, μ (Metric.closedBall x r)ᶜ` tends to `0` at infinity.  -/
MeasureTheory.isTightMeasureSet_iff_tendsto_measure_compl_closedBall : ∀ {E : Type u_1} {mE : MeasurableSpace E} {S : Set (MeasureTheory.Measure E)} [inst : PseudoMetricSpace E]
  [ProperSpace E] (x : E),
  MeasureTheory.IsTightMeasureSet S ↔
    Filter.Tendsto (fun r => ⨆ μ ∈ S, μ (Metric.closedBall x r)ᶜ) Filter.atTop (nhds 0)
-- Mathlib.Data.Finsupp.PointwiseSMul
/-- **Alias** of `AddMonoidAlgebra.smul_apply_addAction`. -/
Finsupp.smul_apply_addAction : ∀ {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [inst : AddGroup G] [inst_1 : AddAction G P]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid V] [inst_4 : SMulWithZero R V] (f : AddMonoidAlgebra R G) (x : P → V)
  (p : P), (f • x) p = ∑ i ∈ f.coeff.support, f.coeff i • x (-i +ᵥ p)
-- Mathlib.Order.Basic
strongLT_of_le_of_strongLT : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → Preorder (π i)] {a b c : (i : ι) → π i},
  c ≤ b → StrongLT b a → StrongLT c a
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
SSet.hasDimensionLT_of_isColimit : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} J] [CategoryTheory.Limits.HasColimitsOfShape J (Type u)]
  {F : CategoryTheory.Functor J SSet} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  {n : ℕ}, (∀ (j : J), (F.obj j).HasDimensionLT n) → c.pt.HasDimensionLT n
-- Mathlib.Analysis.Normed.Group.Uniform
uniformContinuous_nnnorm : ∀ {E : Type u_2} [inst : SeminormedAddGroup E], UniformContinuous fun a => ‖a‖₊
-- Mathlib.Algebra.Algebra.RestrictScalars
instSemiringRestrictScalars : (R : Type u_1) → (S : Type u_2) → (A : Type u_4) → [I : Semiring A] → Semiring (RestrictScalars R S A)
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
/-- A wrapper for promoting any category to a bicategory,
with the only 2-morphisms being equalities.
 -/
CategoryTheory.LocallyDiscrete.as : {C : Type u} → CategoryTheory.LocallyDiscrete C → C
-- Mathlib.Analysis.Calculus.BumpFunction.Convolution
/-- If `φ` is a bump function, compute `(φ ⋆ g) x₀`
if `g` is constant on `Metric.ball x₀ φ.rOut`.  -/
ContDiffBump.convolution_eq_right : ∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] {g : G → E'} [inst_1 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} [inst_2 : NormedSpace ℝ E'] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace ℝ G]
  [CompleteSpace E'] {φ : ContDiffBump 0} [inst_6 : HasContDiffBump G] {x₀ : G},
  (∀ x ∈ Metric.ball x₀ φ.rOut, g x = g x₀) →
    MeasureTheory.convolution (↑φ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀ = MeasureTheory.integral μ ↑φ • g x₀
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.eq_succMany?_of_toArray_eq_append_append : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff),
  cur = (Std.PRange.succMany? (pref.size + 1) r.lower).get ⋯
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_range_right : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {f : Quotient (QuotientAddGroup.rightRel H) → G},
  (∀ (q : Quotient (QuotientAddGroup.rightRel H)), Quotient.mk'' (f q) = q) →
    AddSubgroup.IsComplement (↑H) (Set.range f)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The underlying profinite topological space.  -/
ProfiniteGrp.toProfinite : ProfiniteGrp.{u} → Profinite
-- Mathlib.Tactic.Tauto
Mathlib.Tactic.Tauto.Config.mk.sizeOf_spec : sizeOf { } = 1
-- Mathlib.Algebra.Module.ULift
ULift.smulWithZero' : {R : Type u} →
  {M : Type v} → [inst : Zero R] → [inst_1 : Zero M] → [SMulWithZero R M] → SMulWithZero R (ULift.{u_1, v} M)
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit.match_1.eq_6 : ∀ (motive : Lean.Expr → Sort u_1) (u : Lean.Level) (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a))
  (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (f a : Lean.Expr) → motive (f.app a))
  (h_8 : (data : Lean.MData) → (a : Lean.Expr) → motive (Lean.Expr.mdata data a))
  (h_9 : (typeName : Lean.Name) → (idx : ℕ) → (a : Lean.Expr) → motive (Lean.Expr.proj typeName idx a))
  (h_10 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName d b binderInfo))
  (h_11 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.lam binderName d b binderInfo))
  (h_12 :
    (declName : Lean.Name) → (t v b : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE declName t v b nondep)),
  (match Lean.Expr.sort u with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | f.app a => h_7 f a
    | Lean.Expr.mdata data a => h_8 data a
    | Lean.Expr.proj typeName idx a => h_9 typeName idx a
    | Lean.Expr.forallE binderName d b binderInfo => h_10 binderName d b binderInfo
    | Lean.Expr.lam binderName d b binderInfo => h_11 binderName d b binderInfo
    | Lean.Expr.letE declName t v b nondep => h_12 declName t v b nondep) =
    h_6 u
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.liftFOne.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Y ⟶ Z)
  (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z),
  CategoryTheory.ProjectiveResolution.liftFOne f P Q =
    ⋯.liftFromProjective
      (CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (CategoryTheory.ProjectiveResolution.liftFZero f P Q)) ⋯
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LocalPresentationAt.mk : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_4} →
      {H : Type u_6} →
        {G : Type u_8} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 F G} →
                            {M : Type u_10} →
                              {N : Type u_12} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} →
                                              {P :
                                                  (M → N) →
                                                    OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} →
                                                (domChart : OpenPartialHomeomorph M H) →
                                                  (codChart : OpenPartialHomeomorph N G) →
                                                    x ∈ domChart.source →
                                                      f x ∈ codChart.source →
                                                        domChart ∈ IsManifold.maximalAtlas I n M →
                                                          codChart ∈ IsManifold.maximalAtlas J n N →
                                                            domChart.source ⊆ f ⁻¹' codChart.source →
                                                              P f domChart codChart →
                                                                Manifold.LocalPresentationAt I J n f x P
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.Integrable.sub : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f g : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.Integrable I l f vol → BoxIntegral.Integrable I l g vol → BoxIntegral.Integrable I l (f - g) vol