mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_set_coe : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {f : ι → M} (s : Set ι) [inst_1 : Fintype ↑s],
  ∑ i, f ↑i = ∑ i ∈ s.toFinset, f i
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.instHasModelBitVecNumBits : HasModel✝ ISize (BitVec System.Platform.numBits)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.OplaxFunctor B C} (θ : CategoryTheory.Oplax.OplaxTrans G H) {a b c : B} {a' : C}
  (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) {Z : a' ⟶ H.obj c}
  (h_1 :
    CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp (θ.app a) (CategoryTheory.CategoryStruct.comp (H.map g) (H.map h))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.comp g h)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapComp g h)))
        h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapComp g h) (θ.app c)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f
          (CategoryTheory.Bicategory.associator (G.map g) (G.map h) (θ.app c)).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (G.map g) (θ.naturality h)))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft f
              (CategoryTheory.Bicategory.associator (G.map g) (θ.app b) (H.map h)).inv)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft f
                (CategoryTheory.Bicategory.whiskerRight (θ.naturality g) (H.map h)))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.whiskerLeft f
                  (CategoryTheory.Bicategory.associator (θ.app a) (H.map g) (H.map h)).hom)
                h_1)))))
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.le_functorPushforward_pullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve X),
  R ≤ CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.functorPushforward F R)
-- Mathlib.Logic.Equiv.Fin.Basic
prodEquivPiFinTwo_apply : ∀ (α β : Type u), ⇑(prodEquivPiFinTwo α β) = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The composition functor is also the composition on monoid objects.  -/
CategoryTheory.Functor.mapMonCompIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  {F : CategoryTheory.Functor C D} →
                    {G : CategoryTheory.Functor D E} →
                      [inst_6 : F.LaxMonoidal] → [inst_7 : G.LaxMonoidal] → (F.comp G).mapMon ≅ F.mapMon.comp G.mapMon
-- Mathlib.Topology.Constructions.SumProd
/-- A version of `continuous_sInf_dom` for binary functions  -/
continuous_sInf_dom₂ : ∀ {X : Type u_5} {Y : Type u_6} {Z : Type u_7} {f : X → Y → Z} {tas : Set (TopologicalSpace X)}
  {tbs : Set (TopologicalSpace Y)} {tX : TopologicalSpace X} {tY : TopologicalSpace Y} {tc : TopologicalSpace Z},
  tX ∈ tas → tY ∈ tbs → (Continuous fun p => f p.1 p.2) → Continuous fun p => f p.1 p.2
-- Aesop.Tree.Data
Aesop.Goal.safeRapps : Aesop.Goal → BaseIO (Array Aesop.RappRef)
-- Init.Data.Option.Lemmas
Option.or_of_isNone : ∀ {α : Type u_1} {o o' : Option α}, o.isNone = true → o.or o' = o'
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.homologyIso_hom_comp_leftHomologyIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.LeftHomologyData),
  CategoryTheory.CategoryStruct.comp h.homologyIso.hom h.leftHomologyIso.inv = S.leftHomologyIso.inv
-- Mathlib.Data.Fin.SuccPred
Fin.zero_ne_one' : ∀ {n : ℕ} [NeZero n], 0 ≠ 1
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `g` is analytic at `x` and not locally constant, and `f` is meromorphic at `g x`, express the
trailing coefficient of `f ∘ g` at `x` in terms of `g` and `f`.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {g : 𝕜 → 𝕜},
  MeromorphicAt f (g x) →
    AnalyticAt 𝕜 g x →
      ¬Filter.EventuallyConst g (nhds x) →
        meromorphicTrailingCoeffAt (f ∘ g) x =
          meromorphicTrailingCoeffAt (fun x_1 => g x_1 - g x) x ^ (meromorphicOrderAt f (g x)).untop₀ •
            meromorphicTrailingCoeffAt f (g x)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.sin_arccos : ∀ (x : ℝ), Real.sin (Real.arccos x) = √(1 - x ^ 2)
-- Mathlib.Topology.Separation.Regular
exists_mem_nhds_isClosed_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] {x : X} {s : Set X},
  s ∈ nhds x → ∃ t ∈ nhds x, IsClosed t ∧ t ⊆ s
-- Mathlib.Probability.Kernel.Composition.CompProd
/-- Composition-Product of kernels. For s-finite kernels, it satisfies
`∫⁻ bc, f bc ∂(compProd κ η a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)`
(see `ProbabilityTheory.Kernel.lintegral_compProd`).
If either of the kernels is not s-finite, `compProd` is given the junk value 0.  -/
ProbabilityTheory.«term_⊗ₖ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.sup_eq_closure_add : ∀ {G : Type u_2} [inst : AddGroup G] (H K : AddSubgroup G), H ⊔ K = AddSubgroup.closure (↑H + ↑K)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.createModulePreDiscrTree : {α : Type} →
  Lean.Core.Context →
    Lean.NameGenerator →
      Lean.Environment →
        (Lean.Name →
            Lean.ConstantInfo →
              Lean.MetaM (List (α × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))) →
          BaseIO (Lean.Meta.RefinedDiscrTree.InitResults✝ α)
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.pi_mem_of_single_mem : ∀ {η : Type u_3} {f : η → Type u_4} [inst : (i : η) → AddGroup (f i)] [Finite η] [inst_2 : DecidableEq η]
  {H : AddSubgroup ((i : η) → f i)} (x : (i : η) → f i), (∀ (i : η), Pi.single i (x i) ∈ H) → x ∈ H
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- The pullback of a monomorphism is a monomorphism  -/
CategoryTheory.Limits.pullback.snd_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Mono f],
  CategoryTheory.Mono (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_eq_zero : ∀ {c : Cardinal.{u}}, Cardinal.toENat c = 0 ↔ c = 0
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.instNSMul.eq_1 : ∀ {α : Type u_2} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α],
  NonemptyInterval.instNSMul = { smul := fun n s => { toProd := n • s.toProd, fst_le_snd := ⋯ } }
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` creates colimits of shape `J`, and `D` has colimits of shape `J`, then
`C` has colimits of shape `J`.
 -/
CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.CreatesColimitsOfShape J F],
  CategoryTheory.Limits.HasColimitsOfShape J C
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.Functor.mapSkeleton_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful], Function.Injective F.mapSkeleton.obj
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolTag : Type
-- Mathlib.Order.Lattice
Prod.instSemilatticeInf : (α : Type u) → (β : Type v) → [SemilatticeInf α] → [SemilatticeInf β] → SemilatticeInf (α × β)
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyReflectIsomorphisms.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  (∀ {X Y : C} (f : X ⟶ Y) [∀ (i : I), CategoryTheory.IsIso ((F i).map f)], CategoryTheory.IsIso f) →
    CategoryTheory.JointlyReflectIsomorphisms F
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)),
  (F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X)
      ((F.mapId b).inv.toNatTrans.app ((F.map f).toFunctor.obj X))
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.pow_zero : ∀ {n : ℕ} [inst : NeZero n] (a : Fin n), a ^ 0 = 1
-- Mathlib.Data.Finsupp.Basic
Finsupp.piecewise_support : ∀ {α : Type u_1} {M : Type u_12} [inst : Zero M] {P : α → Prop} [inst_1 : DecidablePred P] (f : Subtype P →₀ M)
  (g : { a // ¬P a } →₀ M),
  (f.piecewise g).support =
    (Finset.map (Function.Embedding.subtype P) f.support).disjUnion
      (Finset.map (Function.Embedding.subtype fun a => ¬P a) g.support) ⋯
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.sheafOver_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {J : CategoryTheory.GrothendieckTopology C} (ℱ : CategoryTheory.Sheaf J A) (E : A),
  (CategoryTheory.sheafOver ℱ E).obj = ℱ.obj.comp (CategoryTheory.coyoneda.obj (Opposite.op E))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, k ∉ t₁ → Std.DTreeMap.Const.get? (t₁ ∪ t₂) k = Std.DTreeMap.Const.get? t₂ k
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- The closure is unique.  -/
LinearPMap.IsClosable.existsUnique : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F}, f.IsClosable → ∃! f', f.graph.topologicalClosure = f'.graph
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
/-- An equivalence from `M` to itself determines an invertible linear map.  -/
LinearMap.GeneralLinearGroup.ofLinearEquiv : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (M ≃ₗ[R] M) → LinearMap.GeneralLinearGroup R M
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.edgeSet_map : ∀ {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V),
  (SimpleGraph.map (⇑f) G).edgeSet = ⇑f.sym2Map '' G.edgeSet
-- Mathlib.Algebra.Group.Units.Hom
IsLocalHom.mk : ∀ {R : Type u_2} {S : Type u_3} {F : Type u_5} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : FunLike F R S] {f : F},
  (∀ (a : R), IsUnit (f a) → IsUnit a) → IsLocalHom f
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.IsEisensteinAt.mem : ∀ {R : Type u} [inst : CommSemiring R] {f : Polynomial R} {𝓟 : Ideal R},
  f.IsEisensteinAt 𝓟 → ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
-- Mathlib.CategoryTheory.Adjunction.Lifting.Right
/-- (Implementation)
To construct the right adjoint, we use the equalizer of `U' F η_X` with the composite

`U' F X ⟶ U' F L U' F X ⟶ U' F U F L U' F X ⟶ U' F U F X`

where the first morphism is `ι_U'FX`, the second is `U' F η_LU'FX` and the third is `U' F U δ_FX`.
We will show that this equalizer exists and that it forms the object map for a right adjoint to `L`.
 -/
CategoryTheory.LiftRightAdjoint.otherMap : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {U : CategoryTheory.Functor A B} →
              {F : CategoryTheory.Functor B A} →
                (L : CategoryTheory.Functor C B) →
                  (U' : CategoryTheory.Functor A C) →
                    (F ⊣ U) → (L.comp F ⊣ U') → (X : B) → U'.obj (F.obj X) ⟶ U'.obj (F.obj (U.obj (F.obj X)))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_union! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁.union! m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k)
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
MonoidAlgebra.counit_single : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] {X : Type u_3} [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (x : X) (a : A), CoalgebraStruct.counit (MonoidAlgebra.single x a) = CoalgebraStruct.counit a
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- A function `f : R → ℝ` is a norm on a (nonunital) ring if it is a seminorm and `f x = 0`
implies `x = 0`.  -/
RingNorm : (R : Type u_2) → [NonUnitalNonAssocRing R] → Type u_2
-- Mathlib.Computability.ContextFreeGrammar
/-- Given a context-free grammar `g` and strings `u` and `v`
`g.Derives u v` means that `g` can transform `u` to `v` in some number of rewriting steps.  -/
ContextFreeGrammar.Derives : {T : Type u_1} → (g : ContextFreeGrammar T) → List (Symbol T g.NT) → List (Symbol T g.NT) → Prop
-- Mathlib.RingTheory.ChainOfDivisors
mkFactorOrderIsoOfFactorDvdEquiv_apply_coe : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {N : Type u_2} [inst_1 : CommMonoidWithZero N] [inst_2 : Subsingleton Mˣ]
  [inst_3 : Subsingleton Nˣ] {m : M} {n : N} {d : { l // l ∣ m } ≃ { l // l ∣ n }}
  (hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l') (l : ↑(Set.Iic (Associates.mk m))),
  ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) l) = Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩)
-- Init.Data.Nat.Basic
Nat.sub_add_cancel : ∀ {n m : ℕ}, m ≤ n → n - m + m = n
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_def : ∀ {x : ℝ*}, x.InfiniteNeg ↔ ∀ (r : ℝ), x < ↑r
-- Mathlib.Algebra.Group.Units.Basic
unique_one : ∀ {α : Type u_1} [inst : Unique α] [inst_1 : One α], default = 1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for rotate left on `BitVec`.  -/
BitVec.reduceRotateLeft : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.TaggedPrepartition.isPartition_unionComplToSubordinate : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I)
  (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → ↑(Set.Ioi 0)),
  (π₁.unionComplToSubordinate π₂ hU r).IsPartition
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.lift_unique' : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u_4} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G k] [inst_5 : SMulCommClass G k k]
  (F : SkewMonoidAlgebra k G →ₐ[k] A), F = (SkewMonoidAlgebra.lift k G A) ((↑F).comp (SkewMonoidAlgebra.of k G))
-- Mathlib.Data.ZMod.Basic
ZMod.val_ne_zero : ∀ {n : ℕ} (a : ZMod n), a.val ≠ 0 ↔ a ≠ 0
-- Init.Data.UInt.Lemmas
UInt64.toUSize_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt64.size ≤ n →
    (UInt64.ofNatClamp n).toUSize = USize.ofNatLT (USize.size - 1) UInt64.toUSize_ofNatClamp_of_le._proof_1
-- Mathlib.Analysis.Meromorphic.Basic
/-- `Meromorphic` is invariant under translation.  -/
Meromorphic.meromorphic_comp_sub_const_iff_meromorphic : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜}, Meromorphic (f ∘ fun x => x - c) ↔ Meromorphic f
-- Init.Data.Int.Lemmas
Int.subNatNat_add : ∀ (m n k : ℕ), Int.subNatNat (m + n) k = ↑m + Int.subNatNat n k
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquivClass.toCoalgHomClass : ∀ {F : Type u_5} {R : outParam (Type u_6)} {A : outParam (Type u_7)} {B : outParam (Type u_8)} {inst : CommSemiring R}
  {inst_1 : AddCommMonoid A} {inst_2 : AddCommMonoid B} {inst_3 : Module R A} {inst_4 : Module R B}
  {inst_5 : CoalgebraStruct R A} {inst_6 : CoalgebraStruct R B} {inst_7 : EquivLike F A B}
  [self : CoalgEquivClass F R A B], CoalgHomClass F R A B
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.Literal.mk.inj : ∀ {n : ℕ} {value : BitVec n} {n_1 : ℕ} {value_1 : BitVec n_1},
  { n := n, value := value } = { n := n_1, value := value_1 } → n = n_1 ∧ value ≍ value_1
-- Mathlib.Analysis.Normed.Group.Continuity
NormedCommGroup.toENormedCommMonoid.eq_1 : ∀ {E : Type u_4} [inst : NormedCommGroup E],
  NormedCommGroup.toENormedCommMonoid =
    { toESeminormedMonoid := NormedGroup.toENormedMonoid.toESeminormedMonoid, mul_comm := ⋯, enorm_eq_zero := ⋯ }
-- Mathlib.Order.Category.PartOrd
PartOrd.ofHom_hom : ∀ {X Y : PartOrd} (f : X ⟶ Y), PartOrd.ofHom (PartOrd.Hom.hom f) = f
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.interSmallerFn.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (kv' : (a : α) × β a)
  (h_1 : (kv' : (a : α) × β a) → motive (some kv')) (h_2 : Unit → motive none),
  (match some kv' with
    | some kv' => h_1 kv'
    | none => h_2 ()) =
    h_1 kv'
-- Init.Guard
/-- Alpha-eq matching for `guard_expr`  -/
Lean.Parser.equalA : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.Algebra.SMul
/-- If `G` acts continuously differentiably on `G'` and `G'` acts continuously differentiably on
`M`, then `G` acts continuously differentiably on `M`.  -/
IsScalarTower.contMDiffSMul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {H'' : Type u_6} [inst_7 : TopologicalSpace H''] {E'' : Type u_7}
  [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E''] {I'' : ModelWithCorners 𝕜 E'' H''} {G : Type u_8}
  [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H G] {M : Type u_9} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] (G' : Type u_11) [inst_14 : TopologicalSpace G'] [inst_15 : ChartedSpace H'' G']
  [inst_16 : Monoid G'] [inst_17 : SMul G G'] [inst_18 : MulAction G' M] [inst_19 : SMul G M] [IsScalarTower G G' M]
  {n : WithTop ℕ∞} [ContMDiffSMul I I'' n G G'] [ContMDiffSMul I'' I' n G' M], ContMDiffSMul I I' n G M
-- Mathlib.Algebra.Group.Pointwise.Set.Small
small_neg : ∀ {α : Type u_1} (s : Set α) [inst : InvolutiveNeg α] [Small.{u, u_1} ↑s], Small.{u, u_1} ↑(-s)
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.State.closed.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Writer.State.closed = 1
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- If the point passed to `secondInter` is a vertex of a simplex, lying on the sphere, and all
vertices lie on or inside the sphere, and the vector passed to `secondInter` is given by a
subtraction involving that vertex and a point in the interior of the opposite face, the given
vertex and the result of `secondInter` are on opposite sides of that face.  -/
EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {n : ℕ} [inst_4 : NeZero n]
  {sx : Affine.Simplex ℝ P n} {i : Fin (n + 1)},
  sx.points i ∈ s →
    (∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius) →
      ∀ {p : P},
        p ∈ (sx.faceOpposite i).interior →
          (affineSpan ℝ (Set.range (sx.faceOpposite i).points)).SOppSide (sx.points i)
            (s.secondInter (sx.points i) (p -ᵥ sx.points i))
-- Mathlib.Analysis.LocallyConvex.AbsConvex
subset_absConvexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {s : Set E}, s ⊆ (absConvexHull 𝕜) s
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.stronglyMeasurable_in_set : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Zero β] {s : Set α}
  {f : α → β},
  MeasurableSet s →
    MeasureTheory.StronglyMeasurable f →
      (∀ x ∉ s, f x = 0) →
        ∃ fs,
          (∀ (x : α), Filter.Tendsto (fun n => (fs n) x) Filter.atTop (nhds (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), (fs n) x = 0
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.cnfSatAssignment.eq_1 : ∀ (aig : Std.Sat.AIG ℕ) (assign1 : ℕ → Bool),
  Std.Sat.AIG.toCNF.cnfSatAssignment✝ aig assign1 =
    Std.Sat.AIG.toCNF.mixAssigns✝ assign1 fun idx =>
      ⟦assign1, { aig := aig, ref := { gate := ↑idx, invert := false, hgate := ⋯ } }⟧
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isNonneg_def : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : LE R]
  {B : LinearMap.BilinForm R M}, B.IsNonneg ↔ ∀ (x : M), 0 ≤ (B x) x
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- Probability measures yield elements of the `WeakDual` of bounded continuous nonnegative
functions via `MeasureTheory.FiniteMeasure.testAgainstNN`, i.e., integration.  -/
MeasureTheory.ProbabilityMeasure.toWeakDualBCNN : {Ω : Type u_1} →
  [inst : MeasurableSpace Ω] →
    [inst_1 : TopologicalSpace Ω] →
      [OpensMeasurableSpace Ω] →
        MeasureTheory.ProbabilityMeasure Ω → WeakDual NNReal (BoundedContinuousFunction Ω NNReal)
-- Mathlib.Algebra.Group.Center
/-- associative property for right addition  -/
IsAddCentral.right_assoc : ∀ {M : Type u_1} [inst : Add M] {z : M}, IsAddCentral z → ∀ (a b : M), a + b + z = a + (b + z)
-- Mathlib.Order.BooleanAlgebra.Set
Set.notMem_sdiff_of_mem : ∀ {α : Type u_1} {s t : Set α} {x : α}, x ∈ t → x ∉ s \ t
-- Lean.Meta.Tactic.Grind.Internalize
/-- Given an application `e` of the form `f a_1 ... a_n`,
adds entry `f ↦ e` to `appMap`. Recall that `appMap` is a multi-map.
 -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.updateAppMap : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.instInhabitedCotangent : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → Inhabited I.Cotangent