mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_swap_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C]
  {Z : C} (h : Y ⨿ B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map g (CategoryTheory.CategoryStruct.id B)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map g (CategoryTheory.CategoryStruct.id A))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id Y) f) h)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.div_singleton : ∀ {α : Type u_2} [inst : Div α] {s : Set α} {b : α}, s / {b} = (fun x => x / b) '' s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α}, (m.erase k).getKey? a = if (k == a) = true then none else m.getKey? a
-- Mathlib.Logic.Relator
Relator.BiTotal.rel_forall : ∀ {α : Sort u₁} {β : Sort u₂} {R : α → β → Prop},
  Relator.BiTotal R → Relator.LiftFun (Relator.LiftFun R Iff) Iff (fun p => ∀ (i : α), p i) fun q => ∀ (i : β), q i
-- Mathlib.Topology.IsLocalHomeomorph
/-- A homeomorphism is a local homeomorphism.  -/
Homeomorph.isLocalHomeomorph : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X ≃ₜ Y),
  IsLocalHomeomorph ⇑f
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_comap : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} (M : Matroid β) (X : Set α), (M.comap f).eRk X = M.eRk (f '' X)
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_iff_isIso_leftHomologyMap' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂)
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
Set.Countable.preimage_circleMap : ∀ {s : Set ℂ}, s.Countable → ∀ (c : ℂ) {R : ℝ}, R ≠ 0 → (circleMap c R ⁻¹' s).Countable
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.continuous_iff_of_isColimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat}
  (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c) {X : Type u'}
  [inst_1 : TopologicalSpace X] (f : ↑c.pt → X),
  Continuous f ↔ ∀ (j : J), Continuous (f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j)))
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.instMonoScheme : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsPreimmersion f], CategoryTheory.Mono f
-- Mathlib.RingTheory.DedekindDomain.SInteger
Set.integer.eq_1 : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R))
  (K : Type v) [inst_2 : Field K] [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K],
  S.integer K =
    {
      toSubsemiring :=
        ((⨅ v, ⨅ (_ : v ∉ S), (IsDedekindDomain.HeightOneSpectrum.valuation K v).valuationSubring.toSubring).copy
            {x | ∀ v ∉ S, (IsDedekindDomain.HeightOneSpectrum.valuation K v) x ≤ 1} ⋯).toSubsemiring,
      algebraMap_mem' := ⋯ }
-- Mathlib.Data.Finset.Image
Finset.image_val_of_injOn : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α},
  Set.InjOn f ↑s → (Finset.image f s).val = Multiset.map f s.val
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
/-- Given a category `D` equipped with a shift by an additive monoid `M`, this
structure `CommShift₂Setup D M` allows to define what it means for a bifunctor
`C₁ ⥤ C₂ ⥤ D` to commute with shifts by `M` with respect to both variables.
This structure consists of a `TwistShiftData` for the shift by `M × M` on `D`
obtained by pulling back the addition map `M × M →+ M`, with two axioms `z_zero₁`
and `z_zero₂`. We also require an additional data of `ε m n : (CatCenter D)ˣ`
for `m` and `n`: even though this is determined by the `z` field of `TwistShiftData`,
we make it a separate field so as to have control on its definitional properties.  -/
CategoryTheory.CommShift₂Setup : (D : Type u_5) →
  [inst : CategoryTheory.Category.{v_5, u_5} D] →
    (M : Type u_6) → [inst_1 : AddCommMonoid M] → [CategoryTheory.HasShift D M] → Type (max (max u_5 u_6) v_5)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_add : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f g : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b →
    IntervalIntegrable g μ a b → ∫ (x : ℝ) in a..b, f x + g x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in a..b, g x ∂μ
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
/-- Instantiates the right `.brecOn` for the given type former index,
including universe parameters and fixed prefix.   -/
Lean.Elab.Structural.IndGroupInfo.brecOnName : Lean.Elab.Structural.IndGroupInfo → ℕ → Lean.Name
-- Mathlib.Data.FunLike.Equiv
/-- This lemma is only supposed to be used in the generic context, when working with instances
of classes extending `EquivLike`.
For concrete isomorphism types such as `Equiv`, you should use `Equiv.symm_apply_apply`
or its equivalent.

TODO: define a generic form of `Equiv.symm`.  -/
EquivLike.inv_apply_apply : ∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [inst : EquivLike E α β] (e : E) (a : α), EquivLike.inv e (e a) = a
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.instLinearHomologicalComplexIntUpShiftFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℤ) {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C],
  CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n)
-- Mathlib.Data.Finset.Basic
Finset.range_union_range : ∀ (m n : ℕ), Finset.range m ∪ Finset.range n = Finset.range (max m n)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
PresheafOfModules.free_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat)
  (F : CategoryTheory.Functor Cᵒᵖ (Type u)), (PresheafOfModules.free R).obj F = PresheafOfModules.freeObj F
-- Mathlib.Computability.DFA
DFA.evalFrom.eq_1 : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ), M.evalFrom s = List.foldl M.step s
-- Init.Data.Vector.Lemmas
Vector.toArray_mapM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m] {f : α → m β}
  {xs : Vector α n}, Vector.toArray <$> Vector.mapM f xs = Array.mapM f xs.toArray
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.zero_mem : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), 0 ∈ A
-- Init.Data.UInt.Lemmas
UInt16.sub_lt : ∀ {a b : UInt16}, 0 < b → b ≤ a → a - b < a
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.val_step_takeWhile.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- Given `f(A) = f(B)`, `ker f ≤ A`, and `ker f ≤ B`, deduce that `A = B`.  -/
AddSubgroup.map_injective_of_ker_le : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) {H K : AddSubgroup G},
  f.ker ≤ H → f.ker ≤ K → AddSubgroup.map f H = AddSubgroup.map f K → H = K
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.struct.injEq : ∀ (leanTypeName : Option Lean.Name) (types : Array Lean.IR.IRType) (leanTypeName_1 : Option Lean.Name)
  (types_1 : Array Lean.IR.IRType),
  (Lean.IR.IRType.struct leanTypeName types = Lean.IR.IRType.struct leanTypeName_1 types_1) =
    (leanTypeName = leanTypeName_1 ∧ types = types_1)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- The ideal `I` equals the inf `⨅_v v^(val_v(I))`.  -/
Ideal.iInf_maxPowDividing_eq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I : Ideal R}, I ≠ 0 → ⨅ i, i.maxPowDividing I = I
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Functor.map_comp_heq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z},
  F.obj X = G.obj X →
    F.obj Y = G.obj Y →
      F.obj Z = G.obj Z →
        F.map f ≍ G.map f →
          F.map g ≍ G.map g →
            F.map (CategoryTheory.CategoryStruct.comp f g) ≍ G.map (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Data.Part
Part.mem_eq : ∀ {α : Type u_1} (a : α) (o : Part α), (a ∈ o) = ∃ (h : o.Dom), o.get h = a
-- Mathlib.RingTheory.Finiteness.Defs
/-- See also `Module.Finite.exists_fin'`.  -/
Module.Finite.exists_fin : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Finite R M], ∃ n s, Submodule.span R (Set.range s) = ⊤
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inlCompInrCompInverseAssociator.eq_1 : ∀ (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],
  CategoryTheory.sum.inlCompInrCompInverseAssociator C D E =
    (CategoryTheory.Sum.inl_ D E).isoWhiskerLeft (CategoryTheory.sum.inrCompInverseAssociator C D E) ≪≫
      ((CategoryTheory.Sum.inr_ C D).comp (CategoryTheory.Sum.inl_ (C ⊕ D) E)).inlCompSum'
        (CategoryTheory.Sum.inr_ (C ⊕ D) E)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Pi.map_epi : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) [∀ (j : J), CategoryTheory.Epi (p j)],
  CategoryTheory.Epi (CategoryTheory.Limits.Pi.map p)
-- Mathlib.CategoryTheory.Generator.Basic
/-- We say that `G` is a separator if the functor `C(G, -)` is faithful.  -/
CategoryTheory.IsSeparator : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Prop
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- The sequence `log ∘ stirlingSeq ∘ succ` is monotone decreasing  -/
Stirling.log_stirlingSeq'_antitone : Antitone (Real.log ∘ Stirling.stirlingSeq ∘ Nat.succ)
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.comp_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel β γ), κ.comp 0 = 0
-- Mathlib.RingTheory.Perfection
/-- `Perfection R p` as a subsemiring of `ℕ → R`.  -/
Perfection.subsemiring : (R : Type u_1) → [inst : CommSemiring R] → (p : ℕ) → [hp : Fact (Nat.Prime p)] → [CharP R p] → Subsemiring (ℕ → R)
-- Mathlib.Topology.Algebra.Ring.Basic
instIsTopologicalRingULift : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalNonAssocRing R] [IsTopologicalRing R],
  IsTopologicalRing (ULift.{u_2, u_1} R)
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_zero : ∀ {α : Type u_1} [inst : Zero α], SymAlg.sym 0 = 0
-- Lean.Parser.Extra
Lean.ppLine.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Finset.Update
Function.restrict_updateFinset : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : DecidableEq ι] {s : Finset ι} (x : (i : ι) → π i) (y : (i : ↥s) → π ↑i),
  s.restrict (Function.updateFinset x s y) = y
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- The circumsphere of a triangle may be expressed explicitly in terms of two points and the
angle at the third point.  -/
Affine.Triangle.circumsphere_eq_of_dist_of_oangle : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        Affine.Simplex.circumsphere t =
          {
            center :=
              ((EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).tan⁻¹ / 2) •
                  (EuclideanGeometry.o.rotation ↑(Real.pi / 2)) (t.points i₃ -ᵥ t.points i₁) +ᵥ
                midpoint ℝ (t.points i₁) (t.points i₃),
            radius :=
              dist (t.points i₁) (t.points i₃) /
                  |(EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).sin| /
                2 }
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.coeff.eq_2 : ∀ (x : Int.Internal.Linear.Var) (k : ℤ), (Int.Internal.Linear.Poly.num k).coeff x = 0
-- Mathlib.Order.Basic
/-- **Alias** of `ge_trans`. -/
LE.le.trans' : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, b ≤ a → c ≤ b → c ≤ a
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  (E E_1 : J.ZeroHypercover S) (e_E : E = E_1) [inst_1 : E.Small], E.restrictIndexOfSmall = E_1.restrictIndexOfSmall
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.lastStep.congr_simp : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p p_1 : Besicovitch.TauPackage β α),
  p = p_1 → p.lastStep = p_1.lastStep
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.edist_eq_sum : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → EDist (β i)] {p : ENNReal},
  0 < p.toReal → ∀ (f g : PiLp p β), edist f g = (∑ i, edist (f.ofLp i) (g.ofLp i) ^ p.toReal) ^ (1 / p.toReal)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_add_succ_right_eq_append : ∀ {m n : ℕ}, (m...=m + n + 1).toList = (m...=m + n).toList ++ [m + n + 1]
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKeyD_modify_eq_maxKeyD : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : β → β} {fallback : α},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).maxKeyD fallback = t.maxKeyD fallback
-- Lean.Elab.DefView
Lean.Elab.DefsParsedSnapshot.mk.inj : ∀ {toSnapshot : Lean.Language.Snapshot} {defs : Array Lean.Elab.DefParsed} {toSnapshot_1 : Lean.Language.Snapshot}
  {defs_1 : Array Lean.Elab.DefParsed},
  { toSnapshot := toSnapshot, defs := defs } = { toSnapshot := toSnapshot_1, defs := defs_1 } →
    toSnapshot = toSnapshot_1 ∧ defs = defs_1
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.sup_apply : ∀ {E : Type u_3} [inst : AddGroup E] (p q : AddGroupSeminorm E) (x : E), (p ⊔ q) x = max (p x) (q x)
-- Lean.Parser.Types
Lean.Parser.ParserInfo.mk.sizeOf_spec : ∀ (collectTokens : List Lean.Parser.Token → List Lean.Parser.Token)
  (collectKinds : Lean.Parser.SyntaxNodeKindSet → Lean.Parser.SyntaxNodeKindSet)
  (firstTokens : Lean.Parser.FirstTokens),
  sizeOf { collectTokens := collectTokens, collectKinds := collectKinds, firstTokens := firstTokens } =
    1 + sizeOf firstTokens
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt16.reduceToNat : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.unop_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Fork f g), c.unop.π = c.ι.unop
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_map_mapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → n γ} {g : γ → δ} {it : Std.IterM m β},
  (Std.IterM.map g (Std.IterM.mapM f it)).toListRev =
    (Std.IterM.mapM
        (fun b => do
          let __do_lift ← f b
          pure (g __do_lift))
        it).toListRev
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.throwInvalidNamedArgs : {α : Type} → (ctx : Lean.Elab.Term.CollectPatternVars.Context) → (!ctx.namedArgs.isEmpty) = true → Lean.MetaM α
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsRegular.nil : ∀ (R : Type u_1) (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial M],
  RingTheory.Sequence.IsRegular M []
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_univ : ∀ {ι : Type u_1} {π : ι → Sort u_2} [inst : Fintype ι] [inst_1 : (i : ι) → Decidable (i ∈ Finset.univ)]
  (f g : (i : ι) → π i), Finset.univ.piecewise f g = f
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- Suppose `a : X → Set A` is continuous and `a x` satisfies the predicate `p` for all `x`.
Suppose further that `s : X → Set 𝕜` is a family of compact sets `s x₀` contains the spectrum of
`a x` for all sufficiently close `x`. If `f : 𝕜 → 𝕜` is continuous on each `s x` and `f 0 = 0`, then
`fun x ↦ cfc f (a x)` is continuous.  -/
Continuous.cfcₙ : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [ContinuousStar A] [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [inst_8 : TopologicalSpace X]
  {s : X → Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A},
  Continuous a →
    (∀ (x : X), IsCompact (s x)) →
      (∀ (x₀ : X), ∀ᶠ (x : X) in nhds x₀, quasispectrum 𝕜 (a x) ⊆ s x₀) →
        autoParam (∀ (x : X), ContinuousOn f (s x)) Continuous.cfcₙ._auto_1 →
          autoParam (f 0 = 0) Continuous.cfcₙ._auto_3 →
            autoParam (∀ (x : X), p (a x)) Continuous.cfcₙ._auto_5 → Continuous fun x => cfcₙ f (a x)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_spec' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (x : M) (y : ↥S), f ↑y + f.mk' x y = f x
-- Mathlib.Data.DFinsupp.Defs
/-- Reindexing terms of a dfinsupp.

This is the dfinsupp version of `Equiv.piCongrLeft'`.  -/
DFinsupp.equivCongrLeft : {ι : Type u} →
  {β : ι → Type v} →
    {κ : Type u_1} → [inst : (i : ι) → Zero (β i)] → (h : ι ≃ κ) → (Π₀ (i : ι), β i) ≃ Π₀ (k : κ), β (h.symm k)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.and_const_left' : ∀ {w a : ℕ} {b : BitVec w} {c : ℕ},
  BitVec.ofNat w a &&& b &&& BitVec.ofNat w c = BitVec.ofNat w a &&& BitVec.ofNat w c &&& b
-- Mathlib.Data.Set.Card
Set.Infinite.ncard : ∀ {α : Type u_1} {s : Set α}, s.Infinite → s.ncard = 0
-- Mathlib.SetTheory.Cardinal.Finite
ENat.one_le_card_iff_nonempty : ∀ (α : Type u_3), 1 ≤ ENat.card α ↔ Nonempty α
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.of_toList_perm : ∀ {α : Type u} {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}, m₁.toList.Perm m₂.toList → m₁.Equiv m₂
-- Mathlib.Algebra.Group.Submonoid.Units
/-- A Galois coinsertion exists between the coercion from a subgroup of units to a submonoid and
the reduction from a submonoid to its unit group.  -/
ofUnits_units_gci : {M : Type u_1} → [inst : Monoid M] → GaloisCoinsertion Subgroup.ofUnits Submonoid.units
-- Init.Data.Vector.Lemmas
Vector.foldl_map_hom : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Vector α n},
  (∀ (x y : α), f' (g x) (g y) = g (f x y)) → Vector.foldl f' (g a) (Vector.map g xs) = g (Vector.foldl f a xs)
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.insertListIfNewUnit : ∀ {α : Type u} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys (Std.Internal.List.insertListIfNewUnit l toInsert)
-- Lean.Parser.Extension
Lean.Parser.addBuiltinParser : Lean.Name → Lean.Name → Bool → Lean.Parser.Parser → ℕ → IO Unit
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.dsimpLocation.go : Lean.Meta.Simp.Context → Lean.Meta.Simp.SimprocsArray → Array Lean.FVarId → Bool → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G A : C} {M : ModuleCat (CategoryTheory.End G)ᵐᵒᵖ}
  (g : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ A)),
  CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d g =
    CategoryTheory.Limits.Sigma.desc fun m => (CategoryTheory.ConcreteCategory.hom g) m
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} {h' : k ∈ Std.DTreeMap.Raw.filterMap f t} (h : t.WF),
  (Std.DTreeMap.Raw.filterMap f t).getKey k h' = t.getKey k ⋯
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.step_filterMap : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {f : β → Option γ},
  (Std.Iter.filterMap f it).step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ =>
      match h' : f out with
      | none => Std.PlausibleIterStep.skip (Std.Iter.filterMap f it') ⋯
      | some out' => Std.PlausibleIterStep.yield (Std.Iter.filterMap f it') out' ⋯
    | ⟨Std.IterStep.skip it', h⟩ => Std.PlausibleIterStep.skip (Std.Iter.filterMap f it') ⋯
    | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯
-- Mathlib.Topology.Algebra.Ring.Compact
IsLocalRing.finite_residueField_of_compactSpace : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R]
  [inst_5 : IsLocalRing R] [IsNoetherianRing R], Finite (IsLocalRing.ResidueField R)
-- Init.Data.Array.GetLit
List.drop.eq_1 : ∀ {α : Type u} (x : List α), List.drop 0 x = x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.eq_d₂₃_comp_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₂ A).inv
      ((groupCohomology.inhomogeneousCochains A).d 2 3) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.d₂₃ A) (groupCohomology.cochainsIso₃ A).inv
-- Init.Data.String.Slice
/-- Returns the position at the start of the longest suffix of `s` for which `pat` matches
\(potentially repeatedly\).
 -/
String.Slice.skipSuffixWhile : {ρ : Type} → (s : String.Slice) → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → s.Pos
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_integral_indicator : ∀ {X : Type u_1} {Y : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure X} {mY : MeasurableSpace Y} {ν : MeasureTheory.Measure Y}
  (f : X → Y → E) {s : Set X},
  MeasurableSet s → ∫ (x : X), ∫ (y : Y), s.indicator (fun x => f x y) x ∂ν ∂μ = ∫ (x : X) in s, ∫ (y : Y), f x y ∂ν ∂μ
-- Init.Data.Bool
/-- If the return values are propositions, there is no harm in simplifying a `bif` to an `if`.  -/
Bool.cond_prop : ∀ {b : Bool} {p q : Prop}, (bif b then p else q) ↔ if b = true then p else q
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_eq_of_eq_mul_left : ∀ {a b c : ℤ}, b ≠ 0 → a = c * b → a / b = c
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_left_split_dvd1_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℤ → Bool