mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Category.Pairwise
/-- Auxiliary definition for `diagram`.  -/
CategoryTheory.Pairwise.diagramMap : {ι : Type v} →
  {α : Type u} →
    (U : ι → α) →
      [inst : SemilatticeInf α] →
        {o₁ o₂ : CategoryTheory.Pairwise ι} →
          (o₁ ⟶ o₂) → (CategoryTheory.Pairwise.diagramObj U o₁ ⟶ CategoryTheory.Pairwise.diagramObj U o₂)
-- Init.Data.String.Defs
String.endValidPos : (s : String) → s.Pos
-- Batteries.Data.Char.AsciiCasing
Char.beqCaseInsensitiveAsciiOnly.eq_1 : ∀ (c₁ c₂ : Char), c₁.beqCaseInsensitiveAsciiOnly c₂ = (c₁.caseFoldAsciiOnly == c₂.caseFoldAsciiOnly)
-- Mathlib.Order.CompleteLattice.Defs
OrderDual.infSet : (α : Type u_8) → [h : SupSet α] → InfSet αᵒᵈ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.whiskerRight_left_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T) {Z : C} (h : R.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerRight f R))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd T.hom R.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd S.hom R.hom) h
-- Mathlib.RingTheory.Multiplicity
Int.natCast_emultiplicity : ∀ (a b : ℕ), emultiplicity ↑a ↑b = emultiplicity a b
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.comap_incl_eq_top : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N N₂ : LieSubmodule R L M},
  LieSubmodule.comap N.incl N₂ = ⊤ ↔ N ≤ N₂
-- Mathlib.Topology.Closure
disjoint_frontier_iff_isOpen : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, Disjoint (frontier s) s ↔ IsOpen s
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.of_compl : ∀ {α : Type u_1} {s : Set α} {m : MeasurableSpace α}, MeasurableSet sᶜ → MeasurableSet s
-- Init.Data.String.Subslice
String.Slice.Subslice.mk.injEq : ∀ {s : String.Slice} (startInclusive endExclusive : s.Pos)
  (startInclusive_le_endExclusive : startInclusive ≤ endExclusive) (startInclusive_1 endExclusive_1 : s.Pos)
  (startInclusive_le_endExclusive_1 : startInclusive_1 ≤ endExclusive_1),
  ({ startInclusive := startInclusive, endExclusive := endExclusive,
        startInclusive_le_endExclusive := startInclusive_le_endExclusive } =
      { startInclusive := startInclusive_1, endExclusive := endExclusive_1,
        startInclusive_le_endExclusive := startInclusive_le_endExclusive_1 }) =
    (startInclusive = startInclusive_1 ∧ endExclusive = endExclusive_1)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.any_eq_not_all_not : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {p : α → β → Bool},
  m.WF → m.any p = !m.all fun a b => !p a b
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.prod.fst.match_1.eq_2 : ∀ (motive : (x : ℕ) → TypeVec.{u_1} x → TypeVec.{u_1} x → Fin2 x → Sort u_2) (n : ℕ) (x x_1 : TypeVec.{u_1} n.succ)
  (h_1 : (n : ℕ) → (α β : TypeVec.{u_1} n.succ) → (i : Fin2 n) → motive n.succ α β i.fs)
  (h_2 : (n : ℕ) → (x x_2 : TypeVec.{u_1} n.succ) → motive n.succ x x_2 Fin2.fz),
  (match n.succ, x, x_1, Fin2.fz with
    | n.succ, α, β, i.fs => h_1 n α β i
    | n.succ, x, x_2, Fin2.fz => h_2 n x x_2) =
    h_2 n x x_1
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_eq_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] {M : Matrix m n α},
  M.conjTranspose = 0 ↔ M = 0
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.process.processConstApp : Lean.Name → Lean.Expr → Lean.Expr → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.exists : ∀ {p : Complex.UnitClosedDisc → Prop}, (∃ z, p z) ↔ ∃ z, ∃ (hz : ‖z‖ ≤ 1), p (Complex.UnitClosedDisc.mk z hz)
-- Mathlib.Order.DirectedInverseSystem
/-- The predicate that says a family of equivalences between `F j` and `piLT X j`
is a natural transformation.  -/
InverseSystem.IsNatEquiv : {ι : Type u_1} →
  [inst : Preorder ι] →
    {F : ι → Type u_4} →
      {X : ι → Type u_5} →
        (⦃i j : ι⦄ → i ≤ j → F j → F i) → {s : Set ι} → ((j : ↑s) → F ↑j ≃ InverseSystem.piLT X ↑j) → Prop
-- Mathlib.RingTheory.WittVector.StructurePolynomial
wittStructureRat_rec_aux : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℚ) (n : ℕ),
  wittStructureRat p Φ n * MvPolynomial.C (↑p ^ n) =
    (MvPolynomial.bind₁ fun b => (MvPolynomial.rename fun i => (b, i)) (wittPolynomial p ℚ n)) Φ -
      ∑ i ∈ Finset.range n, MvPolynomial.C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
-- Mathlib.CategoryTheory.Triangulated.Yoneda
CategoryTheory.Pretriangulated.instShiftSequenceOppositeAddCommGrpCatObjFunctorPreadditiveYonedaInt : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
          (B : C) → (CategoryTheory.preadditiveYoneda.obj B).ShiftSequence ℤ
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.volume_uIcc : ∀ (x y : ↑unitInterval), MeasureTheory.volume (Set.uIcc x y) = edist y x
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkAppS₅ : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] →
    [Monad m] → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- `Fork.ofι f pushout.condition` is a limit cone in `Cᵒᵖ` if and only if
`Cofork.ofπ f.op pullback.condition` in `C` is a colimit cocone.  -/
CategoryTheory.Limits.Fork.isLimitForkPushoutEquivIsColimitForkUnopPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : Cᵒᵖ} →
      {f : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasPushout f f] →
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f ⋯) ≃
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f.unop ⋯)
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- As `x → ∞`, `f x` decays faster than any power of `x`.  -/
IsStrongFEPair.hf_top : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {P : WeakFEPair E},
  IsStrongFEPair P → ∀ (r : ℝ), P.f =O[Filter.atTop] fun x => x ^ r
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableSub.measurable_sub_const : ∀ {G : Type u_2} {inst : MeasurableSpace G} {inst_1 : Sub G} [self : MeasurableSub G] (c : G), Measurable fun x => x - c
-- Mathlib.Order.Defs.Unbundled
/-- `IsStrictOrder X r` means that the binary relation `r` on `X` is a strict order, that is,
`Std.Irrefl r` and `IsTrans X r`.  -/
IsStrictOrder : (α : Sort u_1) → (α → α → Prop) → Prop
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.enum.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.enum = 1
-- Mathlib.GroupTheory.CoprodI
/-- Given an index `i : ι`, `Pair M i` is the type of pairs `(head, tail)` where `head : M i` and
`tail : Word M`, subject to the constraint that first letter of `tail` can't be `⟨i, m⟩`.
By prepending `head` to `tail`, one obtains a new word. We'll show that any word can be uniquely
obtained in this way.  -/
Monoid.CoprodI.Word.Pair : {ι : Type u_1} → (M : ι → Type u_2) → [(i : ι) → Monoid (M i)] → ι → Type (max u_1 u_2)
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMapClass.mk : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [inst : TopologicalSpace α]
  [inst_1 : TopologicalSpace β] [inst_2 : FunLike F α β] [toContinuousMapClass : ContinuousMapClass F α β],
  (∀ (f : F), Filter.Tendsto (⇑f) (Filter.cocompact α) (Filter.cocompact β)) → CocompactMapClass F α β
-- Init.Data.SInt.Lemmas
Int64.toInt_toBitVec : ∀ (x : Int64), x.toBitVec.toInt = x.toInt
-- Mathlib.Analysis.Calculus.ImplicitContDiff
IsContDiffImplicitAt.contDiffAt : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  {E₂ : Type u_3} [inst_3 : NormedAddCommGroup E₂] [inst_4 : NormedSpace 𝕜 E₂] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : E₁ × E₂ → F} {f' : E₁ × E₂ →L[𝕜] F}
  {u : E₁ × E₂}, IsContDiffImplicitAt n f f' u → ContDiffAt 𝕜 n f u
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωScottContinuous.const : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] {x : β},
  OmegaCompletePartialOrder.ωScottContinuous (Function.const α x)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- The continuous function `Spec A⁰_f → Proj|D(f)` sending `q` to `{a | aᵢᵐ/fⁱ ∈ q}` where
`m` is the degree of `f`  -/
AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          {𝒜 : ℕ → σ} →
            [inst_3 : GradedRing 𝒜] →
              {f : A} →
                {m : ℕ} →
                  f ∈ 𝒜 m →
                    0 < m →
                      (↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                              (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace ⟶
                        ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toPresheafedSpace)
-- Mathlib.Tactic.FailIfNoProgress
/-- `lctxIsDefEq l₁ l₂` compares two lists of `Option LocalDecl`s (as returned from e.g.
`(← (← getMainGoal).getDecl).lctx.decls.toList`). It returns `true` if they have the same
local declarations in the same order (up to defeq, without setting mvars), and `false` otherwise.

Assumption: this function is run with one of the local contexts as the current `MetaM` local
context, and one of the two lists consists of the `LocalDecl`s of that context.  -/
Mathlib.Tactic.lctxIsDefEq : List (Option Lean.LocalDecl) → List (Option Lean.LocalDecl) → Lean.MetaM Bool
-- Mathlib.Logic.Encodable.Basic
ULower.up_eq_up : ∀ {α : Type u_1} [inst : Encodable α] {a b : ULower α}, a.up = b.up ↔ a = b
-- Lean.Setup
Lean.ImportArtifacts.oleanParts : Bool → Lean.ImportArtifacts → Array System.FilePath
-- Mathlib.Algebra.Lie.AdjointAction.Basic
/-- The adjoint of a nilpotent element is nilpotent.  -/
LieAlgebra.ad_nilpotent_of_nilpotent : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
  IsNilpotent a → IsNilpotent ((LieAlgebra.ad R A) a)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instHasBinaryBiproducts : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G],
  CategoryTheory.Limits.HasBinaryBiproducts (Rep.{w, u, v} k G)
-- Mathlib.Algebra.Order.Field.Basic
one_le_div_iff : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
-- Lean.Meta.AppBuilder
Lean.Meta.mkArrayLit : Lean.Expr → List Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tan_add_pi : ∀ (x : ℂ), Complex.tan (x + ↑Real.pi) = Complex.tan x
-- Mathlib.Algebra.Field.Defs
/-- The default definition of the coercion `ℚ≥0 → K` for a division semiring `K`.

`↑q : K` is defined as `(q.num : K) / (q.den : K)`.

Do not use this directly (instances of `DivisionSemiring` are allowed to override that default for
better definitional properties). Instead, use the coercion.  -/
NNRat.castRec : {K : Type u_1} → [NatCast K] → [Div K] → ℚ≥0 → K
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.le_skipWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos}, pos ≤ pos.skipWhile pat
-- Mathlib.Analysis.Convex.Strict.Extreme
disjoint_interior_extremePoints : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E] [Nontrivial E] (S : Set E), Disjoint (interior S) (Set.extremePoints ℝ S)
-- Mathlib.Data.Set.Lattice
Set.BijOn.iInter_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set β} {t : Set γ} {f : β → γ} (g : γ → Set α),
  Set.BijOn f s t → ⋂ x ∈ s, g (f x) = ⋂ y ∈ t, g y
-- Mathlib.Data.Fintype.Card
Fintype.card_le_of_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : α → β),
  Function.Injective f → Fintype.card α ≤ Fintype.card β
-- Lean.Parser.Term
Lean.Parser.Term.assert.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeContext.mk : Array Lean.Elab.Command.InductiveElabStep2 →
  Lean.MetavarContext →
    List Lean.Name →
      Array Lean.Expr →
        Lean.LocalContext →
          Lean.LocalInstances → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.Elab.Command.FinalizeContext✝
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt8.size ≤ n →
    (UInt8.ofNatClamp n).toUInt16 = UInt16.ofNatLT (UInt8.size - 1) UInt8.toUInt16_ofNatClamp_of_le._proof_1
-- Mathlib.Data.Seq.Defs
Stream'.Seq.terminatedAt_nil : ∀ {α : Type u} {n : ℕ}, Stream'.Seq.nil.TerminatedAt n
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsCondKernelCDF.measurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → StieltjesFunction ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsCondKernelCDF f κ ν → ∀ (x : ℝ), Measurable fun p => ↑(f p) x
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousSemilinearEquivClass.instHomeomorphClass : ∀ (F : Type u_1) {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (σ : R →+* S) {σ' : S →+* R}
  [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] (M : Type u_4) [inst_4 : TopologicalSpace M]
  [inst_5 : AddCommMonoid M] (M₂ : Type u_5) [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R M] [inst_9 : Module S M₂] [inst_10 : EquivLike F M M₂]
  [s : ContinuousSemilinearEquivClass F σ M M₂], HomeomorphClass F M M₂
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Zero is a right absorbing element for multiplication  -/
MonoidWithZero.mul_zero : ∀ {M₀ : Type u} [self : MonoidWithZero M₀] (a : M₀), a * 0 = 0
-- Mathlib.CategoryTheory.Functor.FunctorHom
/-- The morphism `F.obj c ⟶ G.obj c` associated with `a : A.obj c`.  -/
CategoryTheory.Functor.HomObj.app : {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} →
          {A : CategoryTheory.Functor C (Type w)} → F.HomObj G A → (c : C) → A.obj c → (F.obj c ⟶ G.obj c)
-- Mathlib.Data.Num.ZNum
/-- This tactic tries to prove (in)equalities about `ZNum`s by transferring them to the `Int` world and
then trying to call `simp`.
```lean
example (n : ZNum) (m : ZNum) : n ≤ n + m * m := by
  transfer
  exact mul_self_nonneg _
```
 -/
ZNum.transfer : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Basic
AddMonoidHom.liftOfRightInverseAux.eq_1 : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] [inst_2 : AddGroup G₃]
  (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker),
  f.liftOfRightInverseAux f_inv hf g hg = { toFun := fun b => g (f_inv b), map_zero' := ⋯, map_add' := ⋯ }
-- Lean.CoreM
/-- Current environment.  -/
Lean.Core.State.env : Lean.Core.State → Lean.Environment
-- Init.Data.Iterators.Consumers.Monadic.Collect
/-- Traverses the given iterator and stores the emitted values in an array.

This function is deprecated. Instead of `it.allowNontermination.toArray`, use `it.toArray`.
 -/
Std.IterM.Partial.toArray : {α : Type w} →
  {m : Type w → Type w'} → {β : Type w} → [Monad m] → [Std.Iterator α m β] → Std.IterM.Partial m β → m (Array β)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz
/-- The **Zarankiewicz function** of natural numbers `m`, `n`, `s`, and `t` is the maximum
number of edges in a `completeBipartiteGraph (Fin s) (Fin t)`-free bipartite graph with parts of
size `m` and `n`.

This is the *extremal graph theory* version of the **Zarankiewicz function**.  -/
SimpleGraph.zarankiewicz : ℕ → ℕ → ℕ → ℕ → ℕ
-- Mathlib.Data.Fin.Tuple.Embedding
/-- Adding a new element at the end of an injective n-tuple, to get an injective n+1-tuple.  -/
Fin.Embedding.snoc : {α : Type u_1} → {n : ℕ} → (x : Fin n ↪ α) → {a : α} → a ∉ Set.range ⇑x → Fin (n + 1) ↪ α
-- Mathlib.RingTheory.OreLocalization.NonZeroDivisors
OreLocalization.inv_zero : ∀ {R : Type u_1} [inst : MonoidWithZero R] [inst_1 : Nontrivial R] [inst_2 : OreLocalization.OreSet (nonZeroDivisors R)]
  [inst_3 : NoZeroDivisors R], 0⁻¹ = 0
-- Init.Omega.Constraint
Lean.Omega.Constraint.scale.eq_1 : ∀ (k : ℤ) (c : Lean.Omega.Constraint),
  Lean.Omega.Constraint.scale k c =
    if k = 0 then if c.isImpossible = true then c else { lowerBound := some 0, upperBound := some 0 }
    else if 0 < k then c.map fun x => k * x else c.flip.map fun x => k * x
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_singleton_mul_eq_span_singleton_mul : ∀ {R : Type u} [inst : CommSemiring R] {x y : R} (I J : Ideal R),
  Ideal.span {x} * I = Ideal.span {y} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ) ∧ ∀ zJ ∈ J, ∃ zI ∈ I, x * zI = y * zJ
-- Mathlib.Data.Set.Image
Function.Injective.image_strictMono : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → StrictMono (Set.image f)
-- Mathlib.Data.Opposite
/-- The canonical map `α → αᵒᵖ`.  -/
Opposite.op : {α : Sort u} → α → αᵒᵖ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.LeibnizAdjunction.adj_unit_app_left : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) (adj₂ : F ⊣₂ G) (X₁ : CategoryTheory.Arrow C₁)
  [inst_3 : CategoryTheory.Limits.HasPullbacks C₂] [inst_4 : CategoryTheory.Limits.HasPushouts C₃]
  (X₂ : CategoryTheory.Arrow C₂),
  ((CategoryTheory.Functor.LeibnizAdjunction.adj F G adj₂ X₁).unit.app X₂).left =
    adj₂.homEquiv (CategoryTheory.Limits.pushout.inl ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom))
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.zero_hom : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G}, Rep.Hom.hom 0 = 0
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.frobeniusRotation_nonzero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  {a₁ a₂ : WittVector p k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0), WittVector.frobeniusRotation p ha₁ ha₂ ≠ 0
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.hasDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) (x : 𝕜) (s : Set 𝕜),
  HasDerivWithinAt (fun x => Polynomial.eval x p) (Polynomial.eval x (Polynomial.derivative p)) s x
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A subalgebra of a seminormed ring is also a seminormed ring, with the restriction of the
norm.  -/
SubalgebraClass.seminormedRing : {S : Type u_5} →
  {𝕜 : Type u_6} →
    {E : Type u_7} →
      [inst : CommRing 𝕜] →
        [inst_1 : SeminormedRing E] →
          [inst_2 : Algebra 𝕜 E] →
            [inst_3 : SetLike S E] → [SubringClass S E] → [SMulMemClass S 𝕜 E] → (s : S) → SeminormedRing ↥s
-- Mathlib.Order.LiminfLimsup
Filter.mono_bliminf' : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p : β → Prop} {u v : β → α},
  (∀ᶠ (x : β) in f, p x → u x ≤ v x) → Filter.bliminf u f p ≤ Filter.bliminf v f p
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.lift_apply_mk : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P) (x : FreeMonoid (M ⊕ N)),
  (Monoid.Coprod.lift f g) (Monoid.Coprod.mk x) = (FreeMonoid.lift (Sum.elim ⇑f ⇑g)) x
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.import : Lean.Parser.Parser
-- Mathlib.Data.Nat.Prime.Defs
Nat.prime_three : Nat.Prime 3
-- Mathlib.Analysis.Convolution
MeasureTheory.convolutionExistsAt_flip : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'} {x : G}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  {L : E →L[𝕜] E' →L[𝕜] F} [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddCommGroup G]
  [MeasurableNeg G] [μ.IsAddLeftInvariant] [MeasurableAdd G] [μ.IsNegInvariant],
  MeasureTheory.ConvolutionExistsAt g f x L.flip μ ↔ MeasureTheory.ConvolutionExistsAt f g x L μ
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_hom_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.op =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Opposite.op X)).inv
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
/-- The Radon-Nikodym derivative `∂(μ.map g)/∂(ν.map g)` of the pushforward of measures by
a function `g : 𝓧 → 𝓨` evaluated at `g x` is a.e.-equal to the conditional expectation of `∂μ/∂ν`
with respect to the comap by `g` of the sigma-algebra on `𝓨`.

See `toReal_rnDeriv_map_ae_eq_trim` for the same statement, but with a.e. equality with respect to
the trimmed measure `ν.trim hg.comap_le`.  -/
MeasureTheory.toReal_rnDeriv_map : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  [MeasureTheory.IsFiniteMeasure μ],
  μ.AbsolutelyContinuous ν →
    ∀ {g : 𝓧 → 𝓨},
      Measurable g →
        ∀ [hσ : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map g ν)],
          (fun a => ((MeasureTheory.Measure.map g μ).rnDeriv (MeasureTheory.Measure.map g ν) (g a)).toReal) =ᵐ[ν]
            ν[fun a => (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? ISize
-- Mathlib.Topology.Compactness.Compact
IsCompact.inf_nhdsSet_eq_biSup : ∀ {X : Type u} [inst : TopologicalSpace X] {K : Set X},
  IsCompact K → ∀ (l : Filter X), l ⊓ nhdsSet K = ⨆ x ∈ K, l ⊓ nhds x
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.instFaithfulForget : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], (CategoryTheory.CommGrp.forget C).Faithful
-- Qq.Delab
Qq.Impl.delabQuotedDefEq : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Topology.IndicatorConstPointwise
/-- The indicator functions of `Asᵢ` evaluated at `x` tend to the indicator function of `A`
evaluated at `x` if and only if we eventually have the equivalence `x ∈ Asᵢ ↔ x ∈ A`.  -/
tendsto_indicator_const_apply_iff_eventually : ∀ {α : Type u_1} {A : Set α} {β : Type u_2} [inst : Zero β] [inst_1 : TopologicalSpace β] {ι : Type u_3} (L : Filter ι)
  {As : ι → Set α} [T1Space β] (b : β) [NeZero b] (x : α),
  Filter.Tendsto (fun i => (As i).indicator (fun x => b) x) L (nhds (A.indicator (fun x => b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A