mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.ResiduallyFinite
AddGroup.exists_finiteIndexNormalAddSubgroup_of_residuallyFinite : ∀ {G : Type u_1} [inst : AddGroup G] [AddGroup.ResiduallyFinite G] (g h : G), g ≠ h → ∃ H, ↑g ≠ ↑h
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_eq_back_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.maxKey he = t.keysArray.back ⋯
-- Init.Data.Nat.Lemmas
Nat.eq_of_dvd_of_lt_two_mul : ∀ {a b : ℕ}, a ≠ 0 → b ∣ a → a < 2 * b → a = b
-- Mathlib.Data.Num.Lemmas
Num.cast_zero' : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α], ↑Num.zero = 0
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
summable_of_ne_finset_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  {f : β → α} {s : Finset β}, (∀ b ∉ s, f b = 0) → ∀ [L.HasSupport], Summable f L
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_vsub : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ p₂ p : P), midpoint R p₁ p₂ -ᵥ p = ⅟2 • (p₁ -ᵥ p) + ⅟2 • (p₂ -ᵥ p)
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.one_half_lt_eulerMascheroniSeq_six : 1 / 2 < Real.eulerMascheroniSeq 6
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Problem.mk.inj : ∀ {mvarId : Lean.MVarId} {vars : List Lean.Expr} {alts : List Lean.Meta.Match.Alt}
  {examples : List Lean.Meta.Match.Example} {mvarId_1 : Lean.MVarId} {vars_1 : List Lean.Expr}
  {alts_1 : List Lean.Meta.Match.Alt} {examples_1 : List Lean.Meta.Match.Example},
  { mvarId := mvarId, vars := vars, alts := alts, examples := examples } =
      { mvarId := mvarId_1, vars := vars_1, alts := alts_1, examples := examples_1 } →
    mvarId = mvarId_1 ∧ vars = vars_1 ∧ alts = alts_1 ∧ examples = examples_1
-- Lean.Server.ServerTask
Lean.Server.instInhabitedServerTask : {a : Type u_1} → [Inhabited a] → Inhabited (Lean.Server.ServerTask a)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_id : ∀ {R : Type u} [inst : Ring R] {M : ModuleCat R}, ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id M) = LinearMap.id
-- Mathlib.GroupTheory.MonoidLocalization.Lemmas
AddSubmonoid.IsLocalizationMap.pi : ∀ {ι : Type u_1} {M : ι → Type u_2} {N : ι → Type u_3} [inst : (i : ι) → AddCommMonoid (M i)]
  [inst_1 : (i : ι) → AddCommMonoid (N i)] (S : (i : ι) → AddSubmonoid (M i)) {f : (i : ι) → M i → N i},
  (∀ (i : ι), (S i).IsLocalizationMap (f i)) → (AddSubmonoid.pi Set.univ S).IsLocalizationMap (Pi.map f)
-- Init.Data.SInt.Lemmas
Int16.neg_zero : -0 = 0
-- Mathlib.Topology.Separation.Connected
TotallyDisconnectedSpace.t1Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [h : TotallyDisconnectedSpace X], T1Space X
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.augment_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) (X₀ : C)
  (f : X₀ ⟶ X.obj { len := 0 })
  (w :
    ∀ (i : SimplexCategory) (g₁ g₂ : { len := 0 } ⟶ i),
      CategoryTheory.CategoryStruct.comp f (X.map g₁) = CategoryTheory.CategoryStruct.comp f (X.map g₂))
  (x : SimplexCategory),
  (X.augment X₀ f w).hom.app x = CategoryTheory.CategoryStruct.comp f (X.map ({ len := 0 }.const x 0))
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.ConvolutionExistsAt.convolution_smul : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} [inst : Monoid M] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : Module S E] [inst_5 : Module S E'] {F : Type u_10}
  [inst_6 : AddCommMonoid F] [inst_7 : Module S F] [inst_8 : TopologicalSpace F] [ContinuousConstSMul S F] [T2Space F]
  {c : S} {f : M → E} {g : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F),
  DiscreteConvolution.ConvolutionExistsAt L f g x →
    DiscreteConvolution.convolution L f (c • g) x = c • DiscreteConvolution.convolution L f g x
-- Mathlib.Data.W.Basic
WType.brecOn.eq : ∀ {α : Type u_1} {β : α → Type u_2} {motive : WType β → Sort u} (t : WType β)
  (F_1 : (t : WType β) → WType.below t → motive t), WType.brecOn t F_1 = F_1 t (WType.brecOn.go t F_1).2
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.findSome?_eq_match_step : ∀ {α β : Type w} {γ : Type x} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id]
  [Std.Iterators.Finite α Id] [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → Option γ},
  it.findSome? f =
    match ↑it.step with
    | Std.IterStep.yield it' out =>
      match f out with
      | none => it'.findSome? f
      | some fx => some fx
    | Std.IterStep.skip it' => it'.findSome? f
    | Std.IterStep.done => none
-- Mathlib.Algebra.Group.Units.Equiv
AddUnits.addLeft_symm : ∀ {M : Type u_3} [inst : AddMonoid M] (u : AddUnits M), Equiv.symm u.addLeft = (-u).addLeft
-- Mathlib.Algebra.Notation
/-- The *negative part* of an element `a`.  -/
«term_⁻» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommMonoidWithTop.mk : {α : Type u_3} →
  [toAddCommMonoid : AddCommMonoid α] →
    [toLinearOrder : LinearOrder α] →
      [toIsOrderedAddMonoid : IsOrderedAddMonoid α] →
        [toOrderTop : OrderTop α] →
          (∀ (x : α), ⊤ + x = ⊤) → (∀ ⦃x : α⦄, x ≠ ⊤ → IsAddLeftRegular x) → LinearOrderedAddCommMonoidWithTop α
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.fst_comp_prod : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [inst : SMul M α] [inst_1 : SMul N γ]
  [inst_2 : SMul N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ), (MulActionHom.fst N γ δ).comp (f.prod g) = f
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.proj_reflectsIsomorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D}, (CategoryTheory.StructuredArrow.proj S T).ReflectsIsomorphisms
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_sub_cancel : ∀ {α : Type u} [inst : SubtractionCommMonoid α] {a : α}, IsAddUnit a → ∀ (b : α), a + (b - a) = b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.minKey! = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.evalHom_germ : ∀ {𝕜 : 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] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (U : TopologicalSpace.Opens ↑(TopCat.of M)) (x : M) (hx : x ∈ U)
  (f : ↑((smoothSheafCommRing IM I M R).presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (smoothSheafCommRing.evalHom IM I M R x))
      ((CategoryTheory.ConcreteCategory.hom ((smoothSheafCommRing IM I M R).presheaf.germ U x hx)) f) =
    ↑f ⟨x, hx⟩
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertEntry_append_of_not_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.containsKey k l' = false →
    Std.Internal.List.insertEntry k v (l ++ l') = Std.Internal.List.insertEntry k v l ++ l'
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_graphOn : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddCommGroup β] [inst_2 : FunLike F α β]
  [AddMonoidHomClass F α β] (x : α × β) (s : Set α) (f : F),
  x +ᵥ Set.graphOn (⇑f) s = Set.graphOn (fun a => x.2 - f x.1 + f a) (x.1 +ᵥ s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- The right unitor isomorphism for categorical cospan transformations.  -/
CategoryTheory.Limits.CatCospanTransform.termρ_ : Lean.ParserDescr
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsLoop.mem_closure : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsLoop e → ∀ (X : Set α), e ∈ M.closure X
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
Rat.HeightOneSpectrum.prime_natGenerator : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ]
  (v : IsDedekindDomain.HeightOneSpectrum R), Nat.Prime (Rat.HeightOneSpectrum.natGenerator v)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
/-- For a function `f` with support in `s`, the Lᵖ norms of `f` with respect to `μ` and
`μ.restrict s` are the same.  -/
MeasureTheory.eLpNorm_restrict_eq_of_support_subset : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {s : Set α} {f : α → ε},
  Function.support f ⊆ s → MeasureTheory.eLpNorm f p (μ.restrict s) = MeasureTheory.eLpNorm f p μ
-- Mathlib.Algebra.Ring.Int.Parity
Int.natCast_pow_pred : ∀ (b p : ℕ), 0 < b → ↑(b ^ p - 1) = ↑b ^ p - 1
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.instInhabited : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → Inhabited (M →ₚₗ[R] N)
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.forget_map_apply : ∀ {R S : RingCat} (f : R ⟶ S) (x : (CategoryTheory.forget RingCat).obj R),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget RingCat).map f)) x =
    (CategoryTheory.ConcreteCategory.hom f) x
-- Init.Data.SInt.Lemmas
USize.toISize_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toISize = OfNat.ofNat n
-- Lean.Data.NameMap.Basic
Lean.NameMap.instRepr : {α : Type} → [Repr α] → Repr (Lean.NameMap α)
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.qp_eq : ∀ (u : PNat.XgcdType), u.r = 0 → u.q = u.qp + 1
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.unit.sizeOf_spec : ∀ {R : Type u} [inst : SizeOf R], sizeOf Rack.PreEnvelGroup.unit = 1
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.instIsLeftAdjointRestrictScalars : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  (ModuleCat.restrictScalars f).IsLeftAdjoint
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- Transport a `HasColimitsOfSize` instance across an equivalence.  -/
CategoryTheory.Adjunction.has_colimits_of_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : CategoryTheory.Functor C D) [E.IsEquivalence] [CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₂, u₂} D],
  CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₁, u₁} C
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.reduce_append_reduce_reduce : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.reduce (FreeGroup.reduce L₁ ++ FreeGroup.reduce L₂) = FreeGroup.reduce (L₁ ++ L₂)
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Returns the minimum element of the tree, or panics if the tree is empty.  -/
RBTree.RBSet.min! : {α : Type u_1} → {cmp : α → α → Ordering} → [Inhabited α] → RBTree.RBSet α cmp → α
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_apply : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α)
  (k : Equiv.Perm ↑(Function.fixedPoints ⇑g)) (v : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)),
  ((Equiv.Perm.OnCycleFactors.kerParam g) (k, v)).cycleType = k.cycleType + ∑ c, (↑(v c)).cycleType
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_submatrix_equiv_equiv : ∀ {n : Type u_1} {m : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommSemiring R] (s : ℤˣ) (A : Matrix n n R) (f g : m ≃ n),
  Matrix.detp s (A.submatrix ⇑f ⇑g) = Matrix.detp (s * Equiv.Perm.sign (f.symm.trans g)) A
-- Init.Data.List.Lemmas
List.eq_of_mem_singleton : ∀ {α : Type u_1} {b a : α}, a ∈ [b] → a = b
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.instInhabitedPreDefinition : Inhabited Lean.Elab.PreDefinition
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The category of sheaves of modules over a scheme.  -/
AlgebraicGeometry.Scheme.Modules : AlgebraicGeometry.Scheme → Type (u + 1)
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
/-- The category of coalgebras over an additive comonad on a preadditive category is preadditive.  -/
CategoryTheory.Comonad.coalgebraPreadditive : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (U : CategoryTheory.Comonad C) → [U.Additive] → CategoryTheory.Preadditive U.Coalgebra
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_add_ofNat_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIocDiv hp a (b + OfNat.ofNat m * p) = toIocDiv hp a b + OfNat.ofNat m
-- Init.Data.SInt.Basic
/-- Decides whether one 8-bit signed integer is less than or equal to another. Usually accessed via the
`DecidableLE Int8` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if ((-7) : Int8) ≤ 7 then "yes" else "no") = "yes"`
 * `(if (15 : Int8) ≤ 15 then "yes" else "no") = "yes"`
 * `(if (15 : Int8) ≤ 5 then "yes" else "no") = "no"`
 * `show (7 : Int8) ≤ 7 by decide`
 -/
Int8.decLe : (a b : Int8) → Decidable (a ≤ b)
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital subalgebra of a non-unital seminormed ring is also a non-unital seminormed ring,
with the restriction of the norm.  -/
NonUnitalSubalgebra.nonUnitalSeminormedRing : {𝕜 : Type u_5} →
  [inst : CommRing 𝕜] →
    {E : Type u_6} →
      [inst_1 : NonUnitalSeminormedRing E] →
        [inst_2 : Module 𝕜 E] → (s : NonUnitalSubalgebra 𝕜 E) → NonUnitalSeminormedRing ↥s
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedAddMonoid.add_le_add_right : ∀ {α : Type u_2} {inst : AddCommMonoid α} {inst_1 : Preorder α} [self : IsOrderedAddMonoid α] (a b : α),
  a ≤ b → ∀ (c : α), c + a ≤ c + b
-- Mathlib.NumberTheory.Dioph
Dioph.inject_dummies_lem : ∀ {α β γ : Type u} (f : β → γ) (g : γ → Option β),
  (∀ (x : β), g (f x) = some x) →
    ∀ (p : Poly (α ⊕ β)) (v : α → ℕ),
      (∃ t, p (Sum.elim v t) = 0) ↔ ∃ t, (Poly.map (Sum.elim Sum.inl (Sum.inr ∘ f)) p) (Sum.elim v t) = 0
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.val_apply_mem_smul_top_iff : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {m n : ℕ} {x : AdicCompletion I M}, n ≤ m → (↑x m ∈ I ^ n • ⊤ ↔ ↑x n = 0)
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.snd_mem_orbit_of_mem_orbit : ∀ {M : Type u} [inst : Monoid M] {α : Type v} [inst_1 : MulAction M α] {β : Type u_1} [inst_2 : MulAction M β]
  {x y : α × β}, x ∈ MulAction.orbit M y → x.2 ∈ MulAction.orbit M y.2
-- Mathlib.Topology.Defs.Filter
/-- Two points `x` and `y` in a topological space are `Inseparable`, or *topologically
indistinguishable*, if any of the following equivalent properties hold:

- `𝓝 x = 𝓝 y`; we use this property as the definition;
- for any open set `s`, `x ∈ s ↔ y ∈ s`, see `inseparable_iff_forall_isOpen`;
- for any closed set `s`, `x ∈ s ↔ y ∈ s`, see `inseparable_iff_forall_isClosed`;
- `x ∈ closure {y}` and `y ∈ closure {x}`, see `inseparable_iff_mem_closure`;
- `closure {x} = closure {y}`, see `inseparable_iff_closure_eq`.
 -/
Inseparable : {X : Type u_1} → [TopologicalSpace X] → X → X → Prop
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.naturality_φ₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) {Z : C} (h : S₂.L₂.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S₁.φ₂ (CategoryTheory.CategoryStruct.comp f.f₂.τ₂ h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.SnakeInput.functorP.map f)
      (CategoryTheory.CategoryStruct.comp S₂.φ₂ h)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
/-- The curve integral of a closed 1-form along the boundary of the image of a unit square
under a smooth map is zero, a version stated in terms of `DiffContOnC1`.

This theorem is stated in terms of a `C^2` homotopy between two paths.  -/
ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_diffContOnCl : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  [inst_6 : NormedSpace ℝ F] {a b c d : E} {γ₁ : Path a b} {γ₂ : Path c d} {t : Set E} {ω : E → E →L[𝕜] F}
  (φ : (↑γ₁).Homotopy ↑γ₂),
  (∀ a_1 ∈ Set.Ioo 0 1, ∀ b_1 ∈ Set.Ioo 0 1, φ (a_1, b_1) ∈ t) →
    DiffContOnCl ℝ ω t →
      (∀ x ∈ t,
          ∀ u ∈ tangentConeAt ℝ t x,
            ∀ v ∈ tangentConeAt ℝ t x, ((fderivWithin ℝ ω t x) u) v = ((fderivWithin ℝ ω t x) v) u) →
        ContDiffOn ℝ 2 (fun xy => Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2) (Set.Icc 0 1) →
          ∫ᶜ (x : E) in γ₁, ω x + ∫ᶜ (x : E) in φ.evalAt 1, ω x = ∫ᶜ (x : E) in γ₂, ω x + ∫ᶜ (x : E) in φ.evalAt 0, ω x
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.toBialgHom_comp : ∀ {R : Type u} [inst : CommRing R] {X Y Z : HopfAlgCat R} (f : X ⟶ Y) (g : Y ⟶ Z),
  HopfAlgCat.Hom.toBialgHom (CategoryTheory.CategoryStruct.comp f g) =
    (HopfAlgCat.Hom.toBialgHom g).comp (HopfAlgCat.Hom.toBialgHom f)
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Submodule.exists_le_ker_of_notMem : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {p : Submodule K V} {v : V}, v ∉ p → ∃ f, f v ≠ 0 ∧ p ≤ f.ker
-- Init.Data.Nat.Lemmas
Nat.decidableBallLE : (n : ℕ) →
  (P : (k : ℕ) → k ≤ n → Prop) →
    [(n_1 : ℕ) → (h : n_1 ≤ n) → Decidable (P n_1 h)] → Decidable (∀ (n_1 : ℕ) (h : n_1 ≤ n), P n_1 h)
-- Mathlib.Algebra.Homology.Embedding.Boundary
/-- The upper boundary of an embedding `e : Embedding c c'`, as a predicate on `ι`.
It is satisfied by `j : ι` when there exists `k' : ι'` not in the image of `e.f`
such that `c'.Rel (e.f j) k'`.  -/
ComplexShape.Embedding.BoundaryLE : {ι : Type u_1} → {ι' : Type u_2} → {c : ComplexShape ι} → {c' : ComplexShape ι'} → c.Embedding c' → ι → Prop
-- Std.Sync.Broadcast
Std.instInhabitedSlot.default : {α : Type} → Std.Slot✝ α
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_tprod_eq_mulSingle : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (f : β → γ → α)
  (b : β) (c : γ),
  (∀ (b' : β), b' ≠ b → f b' c = 1) →
    (∀ (b' : β) (c' : γ), c' ≠ c → f b' c' = 1) → ∏' (b' : β) (c' : γ), f b' c' = f b c
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanIsoMk_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
  (z : F.obj CategoryTheory.Limits.WalkingCospan.one ≅ G.obj CategoryTheory.Limits.WalkingCospan.one)
  (l : F.obj CategoryTheory.Limits.WalkingCospan.left ≅ G.obj CategoryTheory.Limits.WalkingCospan.left)
  (r : F.obj CategoryTheory.Limits.WalkingCospan.right ≅ G.obj CategoryTheory.Limits.WalkingCospan.right)
  (hl :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl) z.hom =
        CategoryTheory.CategoryStruct.comp l.hom (G.map CategoryTheory.Limits.WalkingCospan.Hom.inl))
      CategoryTheory.Limits.cospanIsoMk._auto_1)
  (hr :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr) z.hom =
        CategoryTheory.CategoryStruct.comp r.hom (G.map CategoryTheory.Limits.WalkingCospan.Hom.inr))
      CategoryTheory.Limits.cospanIsoMk._auto_3)
  (X : CategoryTheory.Limits.WalkingCospan),
  (CategoryTheory.Limits.cospanIsoMk z l r hl hr).hom.app X =
    (Option.rec z (fun val => CategoryTheory.Limits.WalkingPair.rec l r val) X).hom
-- Mathlib.Combinatorics.Quiver.Covering
Quiver.starEquivCostar_symm_apply_snd : ∀ {U : Type u_1} [inst : Quiver U] [inst_1 : Quiver.HasInvolutiveReverse U] (u : U) (e : Quiver.Costar u),
  ((Quiver.starEquivCostar u).symm e).snd = Quiver.reverse e.snd
-- Mathlib.RingTheory.RingHom.QuasiFinite
RingHom.QuasiFinite.ofLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] => RingHom.QuasiFinite
-- Init.Data.Option.Lemmas
Option.lawfulBEq_iff : ∀ {α : Type u_1} [inst : BEq α], LawfulBEq (Option α) ↔ LawfulBEq α
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.toArray_iterFromIdx : ∀ {β : Type w} {n : ℕ} {xs : Vector β n} {pos : ℕ}, (xs.iterFromIdx pos).toArray = xs.toArray.extract pos n
-- Lean.Message
Lean.MessageLog.mk : Lean.PersistentArray Lean.Message → Lean.PersistentArray Lean.Message → Lean.NameSet → Lean.MessageLog
-- Init.Data.SInt.Lemmas
UInt16.toInt16_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt16 = OfNat.ofNat n
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `none` if no such pair exists.
 -/
Std.TreeMap.Raw.getEntryGT? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → Option (α × β)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.nnnorm_exp_I_mul_ofReal_sub_one_le : ∀ {x : ℝ}, ‖Complex.exp (Complex.I * ↑x) - 1‖₊ ≤ ‖x‖₊
-- Std.Http.Protocol.H1.Config
/-- Maximum number of spaces in delimiter sequences (default: 16).
 -/
Std.Http.Protocol.H1.Config.maxSpaceSequence : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.Analysis.Normed.Group.Basic
dist_prod_prod_le_of_le : ∀ {ι : Type u_3} {E : Type u_5} [inst : SeminormedCommGroup E] (s : Finset ι) {f a : ι → E} {d : ι → ℝ},
  (∀ b ∈ s, dist (f b) (a b) ≤ d b) → dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b
-- Mathlib.CategoryTheory.Sums.Basic
/-- `inl_` is the functor `X ↦ inl X`.  -/
CategoryTheory.Sum.inl_ : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C (C ⊕ D)
-- Mathlib.Algebra.Group.Basic
div_mul_eq_div_div : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a / (b * c) = a / b / c
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.degBound_zero : ∀ (k : ℕ) (D : ℕ → ℕ), ChevalleyThm.MvPolynomialC.degBound k D 0 = 1
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- An orthogonal basis with respect to a left-separating bilinear map has no self-orthogonal
elements.  -/
LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft : ∀ {n : Type u_19} {R : Type u_20} {M : Type u_21} {M₁ : Type u_22} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module R M] [inst_4 : Module R M₁] {I I' : R →+* R} {B : M →ₛₗ[I] M →ₛₗ[I'] M₁}
  [Nontrivial R] {v : Module.Basis n R M}, B.IsOrthoᵢ ⇑v → B.SeparatingLeft → ∀ (i : n), (B (v i)) (v i) ≠ 0
-- Init.Grind.Interactive
/-- Anchor with an ordinal disambiguator. Distinct case-split candidates may have the same anchor.
For example, two candidates that differ only in inaccessible variables have identical anchors.
`#a56e/2` refers to the second candidate (in the case-split candidate list) matching the anchor `#a56e`.
 -/
Lean.Parser.Tactic.Grind.«grind_ref__/__» : Lean.ParserDescr
-- Aesop.Script.Tactic
Aesop.Script.STactic.numSubgoals : Aesop.Script.STactic → ℕ