mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Lemmas
List.foldrRecOn_nil : ∀ {β : Type u_1} {α : Type u_2} {b : β} {motive : β → Sort u_3} {op : α → β → β} (hb : motive b)
  (hl : (b : β) → motive b → (a : α) → a ∈ [] → motive (op a b)), List.foldrRecOn [] op hb hl = hb
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.singleTriangle.mor₂ = (DerivedCategory.singleFunctor C 0).map S.g
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- **Alias** of `Set.image_finsetSum_pi`.

---

The n-ary version of `Set.add_image_prod`.  -/
Set.image_finset_sum_pi : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (l : Finset ι) (S : ι → Set α),
  (fun f => ∑ i ∈ l, f i) '' (↑l).pi S = ∑ i ∈ l, S i
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.exists_girth_eq_length : ∀ {α : Type u_1} {G : SimpleGraph α}, (∃ a w, w.IsCycle ∧ G.girth = w.length) ↔ ¬G.IsAcyclic
-- Mathlib.Data.Rat.Cast.Order
Rat.preimage_cast_Ioi : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (q : ℚ),
  Rat.cast ⁻¹' Set.Ioi ↑q = Set.Ioi q
-- Mathlib.Data.Rat.Defs
Rat.num_neg_eq_neg_num : ∀ (q : ℚ), (-q).num = -q.num
-- Init.Core
instDecidableEqProd : {α : Type u_1} → {β : Type u_2} → [DecidableEq α] → [DecidableEq β] → DecidableEq (α × β)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.ofHom.eq_1 : ∀ {X Y : Type u} [inst : AddGroup X] [inst_1 : TopologicalSpace X] [inst_2 : IsTopologicalAddGroup X]
  [inst_3 : CompactSpace X] [inst_4 : TotallyDisconnectedSpace X] [inst_5 : AddGroup Y] [inst_6 : TopologicalSpace Y]
  [inst_7 : IsTopologicalAddGroup Y] [inst_8 : CompactSpace Y] [inst_9 : TotallyDisconnectedSpace Y] (f : X →ₜ+ Y),
  ProfiniteAddGrp.ofHom f = CategoryTheory.ConcreteCategory.ofHom f
-- Mathlib.RingTheory.Ideal.Colon
Ideal.colon_span : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} {S : Set R},
  Submodule.colon I ↑(Ideal.span S) = Submodule.colon I S
-- Mathlib.Topology.Instances.ENat
ContinuousAt.enatSub : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f g : X → ℕ∞} {x : X},
  ContinuousAt f x → ContinuousAt g x → f x ≠ ⊤ ∨ g x ≠ ⊤ → ContinuousAt (fun x => f x - g x) x
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁_apply_mul : ∀ {p t x : ℝ}, p ∈ Set.Ioo 0 1 → 0 ≤ t → 0 ≤ x → p.rpowIntegrand₀₁ (x * t) x = p.rpowIntegrand₀₁ t 1 * x ^ (p - 1)
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α →+*o β) (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Order.Filter.Extr
isMaxFilter_dual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter (⇑OrderDual.toDual ∘ f) l a ↔ IsMinFilter f l a
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.outerMeasure_of_isOpen : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (U : Set G) (hU : IsOpen U),
  μ.outerMeasure U = μ.innerContent { carrier := U, is_open' := hU }
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_smul_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) (f : α → ENNReal),
  (r • μ).withDensity f = r • μ.withDensity f
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.eq_zero_of_smul_mem_span : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M],
  LinearIndependent R v → ∀ (i : ι) (a : R), a • v i ∈ Submodule.span R (v '' (Set.univ \ {i})) → a = 0
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.orElse_EStateM : ∀ {α ε σ : Type u_1} {x : EStateM ε σ α} {h : Unit → EStateM ε σ α}
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))),
  ⦃fun s =>
    (Std.Do.wp x).apply
      (Q.1, fun x s' => (Std.Do.wp (h ())).apply Q (EStateM.Backtrackable.restore s' (EStateM.Backtrackable.save s)),
        Q.2.2)
      s⦄
    OrElse.orElse x h ⦃Q⦄
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.Const.getD.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (a : α) (fallback : β) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.Const.getD ⟨{ size := size, buckets := buckets }, hm⟩ a fallback =
    Std.DHashMap.Internal.AssocList.getD a fallback buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))]
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.IdentDistrib.truncation : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} [inst : MeasurableSpace β]
  {ν : MeasureTheory.Measure β} {f : α → ℝ} {g : β → ℝ},
  ProbabilityTheory.IdentDistrib f g μ ν →
    ∀ {A : ℝ}, ProbabilityTheory.IdentDistrib (ProbabilityTheory.truncation f A) (ProbabilityTheory.truncation g A) μ ν
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
card_Ico_one_mul : ∀ {M : Type u_1} [inst : CancelCommMonoid M] [inst_1 : LinearOrder M] [IsOrderedMonoid M]
  [inst_3 : LocallyFiniteOrder M] [ExistsMulOfLE M] (a b : M),
  1 ≤ a → 1 ≤ b → (Finset.Ico 1 (a * b)).card = (Finset.Ico 1 a).card + (Finset.Ico 1 b).card
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, k ∈ m.insert k v
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.δ_comp_δ'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) {Z : C} (h : X.obj { len := n + 1 + 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (X.δ j) h) =
    CategoryTheory.CategoryStruct.comp (X.δ (j.pred ⋯)) (CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) h)
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.Hom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : CategoryTheory.Center C} →
        (f : X.fst ⟶ Y.fst) →
          autoParam
              (∀ (U : C),
                CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f U)
                    (Y.snd.β U).hom =
                  CategoryTheory.CategoryStruct.comp (X.snd.β U).hom
                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U f))
              CategoryTheory.Center.Hom.comm._autoParam →
            X.Hom Y
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.congrRight_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D),
  e.congrRight.inverse = (CategoryTheory.Functor.whiskeringRight E D C).obj e.inverse
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algEquivOfCompEqX_symm : ∀ {R : Type u} [inst : CommSemiring R] (p q : Polynomial R) (hpq : p.comp q = Polynomial.X)
  (hqp : q.comp p = Polynomial.X), (p.algEquivOfCompEqX q hpq hqp).symm = q.algEquivOfCompEqX p hqp hpq
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.isEdgeConnected_one : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsEdgeConnected 1 ↔ G.Preconnected
-- Lean.Meta.Tactic.SolveByElim
/-- Enable backtracking search.  -/
Lean.Meta.SolveByElim.SolveByElimConfig.backtracking : Lean.Meta.SolveByElim.SolveByElimConfig → Bool
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_toMonoidHomEquiv_symm : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : Multiplicative A →* M),
  ⇑(AddChar.toMonoidHomEquiv.symm ψ) = ⇑ψ ∘ ⇑Multiplicative.ofAdd
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- We say that `F` preserves colimits of shape `J` if `F` preserves colimits for every diagram
`K : J ⥤ C`, i.e., `F` maps colimit cocones over `K` to colimit cocones.  -/
CategoryTheory.Limits.PreservesColimitsOfShape : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) → [CategoryTheory.Category.{w', w} J] → CategoryTheory.Functor C D → Prop
-- Mathlib.CategoryTheory.RegularCategory.Basic
/-- A regular category is a category with finite limits, such that every kernel pair has a coequalizer,
and such that regular epimorphisms are stable under base change.
 -/
CategoryTheory.Regular : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Data.DFinsupp.Multiset
DFinsupp.toMultiset_sup : ∀ {α : Type u_1} [inst : DecidableEq α] (f g : Π₀ (_a : α), ℕ),
  DFinsupp.toMultiset (f ⊔ g) = DFinsupp.toMultiset f ∪ DFinsupp.toMultiset g
-- Lean.Environment
Lean.EnvExtensionEntry : Type
-- Mathlib.Order.Hom.Basic
OrderHom.symm_dual_id : ∀ {α : Type u_2} [inst : Preorder α], OrderHom.dual.symm OrderHom.id = OrderHom.id
-- Mathlib.CategoryTheory.Limits.Indization.Products
CategoryTheory.Limits.isIndObject_limit_of_discrete : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type v},
  (∀ (g : α → C), CategoryTheory.Limits.IsIndObject (∏ᶜ CategoryTheory.yoneda.obj ∘ g)) →
    ∀ (F : CategoryTheory.Functor (CategoryTheory.Discrete α) (CategoryTheory.Functor Cᵒᵖ (Type v))),
      (∀ (a : CategoryTheory.Discrete α), CategoryTheory.Limits.IsIndObject (F.obj a)) →
        CategoryTheory.Limits.IsIndObject (CategoryTheory.Limits.limit F)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- In the specific case of continuous multilinear maps on spaces indexed by `Fin (n+1)`, where one
can build an element of `(i : Fin (n+1)) → M i` using `cons`, one can express directly the
multiplicativity of a multilinear map along the first variable.  -/
ContinuousMultilinearMap.cons_smul : ∀ {R : Type u} {n : ℕ} {M : Fin n.succ → Type w} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂]
  [inst_5 : (i : Fin n.succ) → TopologicalSpace (M i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M M₂) (m : (i : Fin n) → M i.succ) (c : R) (x : M 0),
  f (Fin.cons (c • x) m) = c • f (Fin.cons x m)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Iso.hom_inv_id_triangle_hom₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (e : A ≅ B) {Z : C} (h : A.obj₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp e.hom.hom₂ (CategoryTheory.CategoryStruct.comp e.inv.hom₂ h) = h
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsPerfectMatching.isAlternating_symmDiff_right : ∀ {V : Type u_1} {G G' : SimpleGraph V} {M : G.Subgraph} {M' : G'.Subgraph},
  M.IsPerfectMatching → M'.IsPerfectMatching → (symmDiff M.spanningCoe M'.spanningCoe).IsAlternating M'.spanningCoe
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardDistinctFactors_one : ArithmeticFunction.cardDistinctFactors 1 = 0
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.instContinuousInvAutFunctorFintypeCat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat),
  ContinuousInv (CategoryTheory.Aut F)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.Scheme.emptyTo_c_app : ∀ (X : AlgebraicGeometry.Scheme) (x : (TopologicalSpace.Opens ↥X)ᵒᵖ),
  X.emptyTo.c.app x = CommRingCat.punitIsTerminal.from (X.presheaf.obj x)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.snd_toProd : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] (x : AddMonoid.Coprod M N),
  (AddMonoid.Coprod.toProd x).2 = AddMonoid.Coprod.snd x
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.instMin : {α : Type u_1} → [inst : CommMonoidWithZero α] → [UniqueFactorizationMonoid α] → Min (Associates α)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.of_cancel_lt : ∀ (ctx : Nat.Internal.Linear.Context) (a b c d : Nat.Internal.Linear.Expr),
  a.inc.toNormPoly.cancel b.toNormPoly = (c.inc.toPoly, d.toPoly) →
    (Nat.Internal.Linear.Expr.denote ctx a < Nat.Internal.Linear.Expr.denote ctx b) =
      (Nat.Internal.Linear.Expr.denote ctx c < Nat.Internal.Linear.Expr.denote ctx d)
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.colimit_add_mk_eq' : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J] {j : J} (x y : ↑(F.obj j)),
  AddMonCat.FilteredColimits.M.mk F ⟨j, x⟩ + AddMonCat.FilteredColimits.M.mk F ⟨j, y⟩ =
    AddMonCat.FilteredColimits.M.mk F ⟨j, x + y⟩
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.instIsPreimmersionFromSpecResidueField : ∀ {X : AlgebraicGeometry.Scheme} (x : ↥X), AlgebraicGeometry.IsPreimmersion (X.fromSpecResidueField x)
-- Init.Core
imp_congr_ctx : ∀ {a b c d : Prop}, (a ↔ c) → (c → (b ↔ d)) → (a → b ↔ c → d)
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Finset.sum_comm_cycle : ∀ {κ : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] {s : Finset γ} {t : Finset α}
  {u : Finset κ} {f : γ → α → κ → β}, ∑ x ∈ s, ∑ y ∈ t, ∑ z ∈ u, f x y z = ∑ z ∈ u, ∑ x ∈ s, ∑ y ∈ t, f x y z
-- Mathlib.Logic.Relator
Relator.rel_eq : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop},
  Relator.BiUnique r →
    Relator.LiftFun r (Relator.LiftFun r fun x1 x2 => x1 ↔ x2) (fun x1 x2 => x1 = x2) fun x1 x2 => x1 = x2
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.liftRel_const_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} [l.NeBot] {r : β → γ → Prop} {x : β} {y : γ},
  Filter.Germ.LiftRel r ↑x ↑y ↔ r x y
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsFiniteMeasureOnCompacts.neg : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [ContinuousNeg G] [MeasureTheory.IsFiniteMeasureOnCompacts μ],
  MeasureTheory.IsFiniteMeasureOnCompacts μ.neg
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.defEq.inj : ∀ {lhs : ℕ} {rhs : Lean.Meta.Grind.CnstrRHS} {lhs_1 : ℕ} {rhs_1 : Lean.Meta.Grind.CnstrRHS},
  Lean.Meta.Grind.EMatchTheoremConstraint.defEq lhs rhs = Lean.Meta.Grind.EMatchTheoremConstraint.defEq lhs_1 rhs_1 →
    lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.GroupTheory.DoubleCoset
/-- Map from `G` to `H \ G / K`  -/
DoubleCoset.mk : {G : Type u_1} → [inst : Group G] → (H K : Subgroup G) → G → DoubleCoset.Quotient ↑H ↑K
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
IsCovariantDerivativeOn.leibniz : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V]
  {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {s : optParam (Set M) Set.univ},
  IsCovariantDerivativeOn F cov s →
    ∀ {σ : (x : M) → V x} {g : M → 𝕜} {x : M},
      MDiffAt (T% σ) x →
        MDiffAt g x →
          autoParam (x ∈ s) IsCovariantDerivativeOn._auto_3 → cov (g • σ) x = g x • cov σ x + (d% g x).smulRight (σ x)
-- Mathlib.Order.Hom.Basic
OrderIso.complementedLattice_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : α ≃o β), ComplementedLattice α ↔ ComplementedLattice β
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The functor `Fin n ⥤ Fin (n + 1)` which sends `i` to `i.succ`.  -/
Fin.succFunctor : (n : ℕ) → CategoryTheory.Functor (Fin n) (Fin (n + 1))
-- Mathlib.Topology.Piecewise
Continuous.piecewise : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  [inst_2 : (a : α) → Decidable (a ∈ s)],
  (∀ a ∈ frontier s, f a = g a) → Continuous f → Continuous g → Continuous (s.piecewise f g)
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.forgetful_map : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] (𝒳 : CategoryTheory.BasedCategory 𝒮)
  (𝒴 : CategoryTheory.BasedCategory 𝒮) {X Y : CategoryTheory.BasedFunctor 𝒳 𝒴} (α : X ⟶ Y),
  (CategoryTheory.BasedNatTrans.forgetful 𝒳 𝒴).map α = α.toNatTrans
-- Mathlib.Topology.ContinuousMap.Basic
/-- Giving a continuous map out of a disjoint union is the same as giving a continuous map out of
each term. This is a version of `Equiv.piCurry` for continuous maps.
 -/
ContinuousMap.sigmaEquiv : {I : Type u_5} →
  (A : Type u_6) →
    (X : I → Type u_7) →
      [inst : TopologicalSpace A] →
        [inst_1 : (i : I) → TopologicalSpace (X i)] → ((i : I) → C(X i, A)) ≃ C((i : I) × X i, A)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.forIn_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} {δ : Type w}
  {m : Type w → Type w'} [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {b : δ}
  {f : (a : α) × β a → δ → m (ForInStep δ)}, t₁.Equiv t₂ → forIn t₁ b f = forIn t₂ b f
-- Mathlib.Data.Finset.Basic
Finset.filter_union_filter_of_codisjoint : ∀ {α : Type u_1} (p q : α → Prop) [inst : DecidablePred p] [inst_1 : DecidablePred q] [inst_2 : DecidableEq α]
  (s : Finset α), Codisjoint p q → Finset.filter p s ∪ Finset.filter q s = s
-- Mathlib.Analysis.Meromorphic.Basic
/-- Finprods of meromorphic functions are meromorphic.  -/
MeromorphicOn.finprod : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} {ι : Type u_5} {f : ι → 𝕜 → 𝕜'},
  (∀ (σ : ι), MeromorphicOn (f σ) U) → MeromorphicOn (∏ᶠ (n : ι), f n) U
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffWithinAt_finsetProd : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι}
  {f : ι → M → G},
  (∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) → ContMDiffWithinAt I' I n (fun x => ∏ i ∈ t, f i x) s x
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.radius_bot : ∀ {α : Type u_1} [Nontrivial α], ⊥.radius = ⊤
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_diff_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α} {fallback : β k}, m₁.contains k = false → (m₁.diff m₂).getD k fallback = fallback
-- Lean.Data.Lsp.Basic
/-- Title of the command, like `save`.  -/
Lean.Lsp.Command.title : Lean.Lsp.Command → String
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_nonneg_of_ae : ∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ}, a ≤ b → 0 ≤ᵐ[μ] f → 0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.LFunction_def_odd : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ},
  Function.Odd Φ →
    ∀ (s : ℂ), ZMod.LFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * HurwitzZeta.hurwitzZetaOdd (ZMod.toAddCircle j) s
-- Mathlib.RingTheory.Etale.Descent
Algebra.Unramified.of_unramified_tensorProduct_of_faithfullyFlat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [Module.FaithfullyFlat R T] [Algebra.Unramified T (TensorProduct R T S)],
  Algebra.Unramified R S
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGetEntryLTD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : α × β},
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.getEntryLTD t₁ k fallback = Std.DTreeMap.Raw.Const.getEntryLTD t₂ k fallback
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Indep.of_restrict : ∀ {α : Type u_1} {M : Matroid α} {R I : Set α}, (M.restrict R).Indep I → M.Indep I
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- If the support of the simple graph `G` is a subset of the set `s`, then the degree of vertices
in the induced subgraph of `s` are the same as in `G`.  -/
SimpleGraph.degree_induce_of_support_subset : ∀ {V : Type u_1} {s : Set V} [inst : DecidablePred fun x => x ∈ s] [inst_1 : Fintype V] {G : SimpleGraph V}
  [inst_2 : DecidableRel G.Adj], G.support ⊆ s → ∀ (v : ↑s), (SimpleGraph.induce s G).degree v = G.degree ↑v
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCommCStarAlgebra.toCStarRing : ∀ {A : Type u_1} [self : NonUnitalCommCStarAlgebra A], CStarRing A
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The preimage of the normalizer is contained in the normalizer of the preimage.  -/
Subgroup.le_normalizer_comap : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {N : Type u_5} [inst_1 : Group N] (f : N →* G),
  Subgroup.comap f (Subgroup.normalizer ↑H) ≤ Subgroup.normalizer ↑(Subgroup.comap f H)
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
Metric.inseparable_iff_nndist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α}, Inseparable x y ↔ nndist x y = 0
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isClosed_infty : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsClosed {OnePoint.infty}
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Auxiliary definition for the lemma `OneHypercoverDenseData.isSheaf_iff`.  -/
_private.Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense.0.CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.isLimit : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] →
                    {data : (X : C) → F.OneHypercoverDenseData J₀ J X} →
                      {G : CategoryTheory.Functor Cᵒᵖ A} →
                        CategoryTheory.Presheaf.IsSheaf J₀ (F.op.comp G) →
                          ((X : C) → CategoryTheory.Limits.IsLimit ((data X).toOneHypercover.multifork G)) →
                            {X : C} → (S : J.Cover X) → CategoryTheory.Limits.IsLimit (S.multifork G)