mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- The functor `C(X, ·)₀` from non-unital topological star algebras (with non-unital continuous
star homomorphisms) to non-unital star algebras.  -/
ContinuousMapZero.nonUnitalStarAlgHom_postcomp : (X : Type u_1) →
  {M : Type u_3} →
    {R : Type u_4} →
      {S : Type u_5} →
        [inst : Zero X] →
          [inst_1 : CommSemiring M] →
            [inst_2 : TopologicalSpace X] →
              [inst_3 : TopologicalSpace R] →
                [inst_4 : TopologicalSpace S] →
                  [inst_5 : CommSemiring R] →
                    [inst_6 : StarRing R] →
                      [inst_7 : IsTopologicalSemiring R] →
                        [inst_8 : ContinuousStar R] →
                          [inst_9 : CommSemiring S] →
                            [inst_10 : StarRing S] →
                              [inst_11 : IsTopologicalSemiring S] →
                                [inst_12 : ContinuousStar S] →
                                  [inst_13 : Module M R] →
                                    [inst_14 : Module M S] →
                                      [inst_15 : ContinuousConstSMul M R] →
                                        [inst_16 : ContinuousConstSMul M S] →
                                          (φ : R →⋆ₙₐ[M] S) →
                                            Continuous ⇑φ → ContinuousMapZero X R →⋆ₙₐ[M] ContinuousMapZero X S
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.antilipschitz_of_forall_le_inner_map : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_4} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  (f : H →L[𝕜] H) {c : NNReal}, 0 < c → (∀ (x : H), ‖x‖ ^ 2 * ↑c ≤ ‖inner 𝕜 (f x) x‖) → AntilipschitzWith c⁻¹ ⇑f
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.rel_of_countdown : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.Iterators.Productive α m] {it it' : Std.IterM m β},
  it'.internalState.countdown < it.internalState.countdown → Std.Iterators.Types.Take.Rel m it' it
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.diff! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] {t₁ : Std.DTreeMap.Internal.Impl α β},
  t₁.WF → ∀ {t₂ : Std.DTreeMap.Internal.Impl α β}, (t₁.diff! t₂).WF
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- If a point belongs to an open ball, then there is a strictly smaller radius whose ball also
contains it.

See also `exists_lt_subset_ball`.  -/
Metric.exists_lt_mem_ball_of_mem_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, x ∈ Metric.ball y ε → ∃ ε' < ε, x ∈ Metric.ball y ε'
-- Mathlib.Algebra.Order.Sub.Defs
AddLECancellable.add_tsub_cancel_right : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b : α},
  AddLECancellable b → a + b - b = a
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.below.cons_cons : ∀ {motive : (m : ℕ) → (L : List ℕ) → SimplexCategoryGenRel.IsAdmissible m L → Prop} {m a b : ℕ} {L' : List ℕ}
  (hab : a < b) (hbL : SimplexCategoryGenRel.IsAdmissible (m + 1) (b :: L')) (ha : a ≤ m),
  SimplexCategoryGenRel.IsAdmissible.below hbL →
    motive (m + 1) (b :: L') hbL → SimplexCategoryGenRel.IsAdmissible.below ⋯
-- Mathlib.Algebra.Category.Ring.Under.Property
RingHom.HasStableEqualizers.preservesEqualizers_pushout : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => P) →
      (RingHom.HasStableEqualizers fun {R S} [CommRing R] [CommRing S] => P) →
        ∀ [inst : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).IsStableUnderCobaseChange]
          {R S : CommRingCat} (f : R ⟶ S),
          CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair
            (CategoryTheory.MorphismProperty.Under.pushout
              (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P) ⊤ f)
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_iff_isSelfAdjoint : ∀ {α : Type u_1} {n : Type u_4} [inst : Star α] {A : Matrix n n α}, A.IsHermitian ↔ IsSelfAdjoint A
-- Lean.Compiler.IR.Basic
/-- If b is a non terminal, then return a pair `(c, b')` s.t. `b == c <;> b'`,
and c.body == FnBody.nil  -/
Lean.IR.FnBody.split : Lean.IR.FnBody → Lean.IR.FnBody × Lean.IR.FnBody
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.instTop : {α : Type u_1} → [inst : TopologicalSpace α] → [inst_1 : LE α] → Top (ClopenUpperSet α)
-- Batteries.Data.AssocList
Batteries.AssocList.toList_erase : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α) (l : Batteries.AssocList α β),
  (Batteries.AssocList.erase a l).toList = List.eraseP (fun x => x.1 == a) l.toList
-- Init.Data.List.Basic
/-- Returns the list of elements in `l` for which `p` returns `true`.

`O(|l|)`.

Examples:
* `[1, 2, 5, 2, 7, 7].filter (· > 2) = [5, 7, 7]`
* `[1, 2, 5, 2, 7, 7].filter (fun _ => false) = []`
* `[1, 2, 5, 2, 7, 7].filter (fun _ => true) = [1, 2, 5, 2, 7, 7]`
 -/
List.filter : {α : Type u} → (α → Bool) → List α → List α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst_1 : Inhabited (β k)], k ∉ t₁ → (t₁ ∩ t₂).get! k = default
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_mul_cancel_left_of_invertible : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (A : Matrix n n α) (B : Matrix n m α) [Invertible A], A⁻¹ * (A * B) = B
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ΨSq_one : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.ΨSq 1 = 1
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.coneEquiv_counitIso_hom_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)}
  (X_1 : CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)),
  (CategoryTheory.WithTerminal.coneEquiv.counitIso.hom.app X_1).hom = CategoryTheory.CategoryStruct.id X_1.pt
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.comap_comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {P : Type u_6} [inst_2 : Group P] (K : Subgroup P)
  (g : N →* P) (f : G →* N), Subgroup.comap f (Subgroup.comap g K) = Subgroup.comap (g.comp f) K
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- The morphism property in `C` associated to a morphism property in `Cᵒᵖ`  -/
CategoryTheory.MorphismProperty.unop : {C : Type u} →
  [inst : CategoryTheory.CategoryStruct.{v, u} C] →
    CategoryTheory.MorphismProperty Cᵒᵖ → CategoryTheory.MorphismProperty C
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.equiv.congr_simp : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ e₁_1 : c₁.Embedding c} (e_e₁ : e₁ = e₁_1) {e₂ e₂_1 : c₂.Embedding c} (e_e₂ : e₂ = e₂_1)
  (ac : e₁.AreComplementary e₂), ac.equiv = ⋯.equiv
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.liminf_preimage_iterate_ae_eq : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → α},
  MeasureTheory.Measure.QuasiMeasurePreserving f μ μ →
    f ⁻¹' s =ᵐ[μ] s → Filter.liminf (fun n => (Set.preimage f)^[n] s) Filter.atTop =ᵐ[μ] s
-- Mathlib.CategoryTheory.Extensive
/-- In a finitary extensive category, all coproducts are van Kampen  -/
CategoryTheory.FinitaryPreExtensive.universal' : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.FinitaryPreExtensive C] {X Y : C}
  (c : CategoryTheory.Limits.BinaryCofan X Y) (a : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.IsUniversalColimit c
-- Mathlib.Order.RelSeries
/-- If a series ``a₀ -r→ a₁ -r→ ... -r→ aₙ``, then `a₀ -r→ a₁ -r→ ... -r→ aₙ₋₁` is
another series  -/
RelSeries.eraseLast : {α : Type u_1} → {r : SetRel α α} → RelSeries r → RelSeries r
-- Init.Data.List.Pairwise
List.pairwise_pair : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α}, List.Pairwise R [a, b] ↔ R a b
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.norm_coe_unit : ∀ {K : Type u_1} [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K] (u : (↥(Valued.integer K))ˣ),
  ‖↑↑u‖ = 1
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `HasColimit F` represents the mere existence of a colimit for `F`.  -/
CategoryTheory.Limits.HasColimit : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor J C → Prop
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- Typeclass asserting that a summation filter is non-vacuous (if this is not satisfied, then
every function is summable with every possible sum simultaneously).  -/
SummationFilter.NeBot : {β : Type u_2} → SummationFilter β → Prop
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_le_one_of_one_le_of_neg : ∀ {x : ENNReal} {z : ℝ}, 1 ≤ x → z < 0 → x ^ z ≤ 1
-- Lean.Elab.Term.TermElabM
/-- We use synthetic metavariables as placeholders for pending elaboration steps.  -/
Lean.Elab.Term.SyntheticMVarKind : Type
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.zariskiPrecoverage_le_propQCPrecoverage : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.ContainsIdentities]
  [AlgebraicGeometry.IsZariskiLocalAtSource P],
  AlgebraicGeometry.Scheme.zariskiPrecoverage ≤ AlgebraicGeometry.Scheme.propQCPrecoverage P
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Limits.exists_eq_of_preservesColimit_yoneda_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J C} [CategoryTheory.IsCofiltered J]
  {c : CategoryTheory.Limits.Cone D} (hc : CategoryTheory.Limits.IsLimit c) {X : C}
  [CategoryTheory.Limits.PreservesColimit D.op (CategoryTheory.yoneda.obj X)] {i : J} (f g : D.obj i ⟶ X),
  CategoryTheory.CategoryStruct.comp (c.π.app i) f = CategoryTheory.CategoryStruct.comp (c.π.app i) g →
    ∃ j a, CategoryTheory.CategoryStruct.comp (D.map a) f = CategoryTheory.CategoryStruct.comp (D.map a) g
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.functoriality_full`. -/
CategoryTheory.Limits.Cocones.functoriality_full : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) [G.Full] [G.Faithful], (CategoryTheory.Limits.Cocone.functoriality F G).Full
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.re_one : ∀ {d : ℤ}, Zsqrtd.re 1 = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} (h₁ : t₁.WF)
  (h₂ : t₂.WF),
  t₁.Equiv t₂ →
    ∀ {f : (a : α) → β a → Option (γ a)},
      (Std.DTreeMap.Internal.Impl.filterMap f t₁ ⋯).impl.Equiv (Std.DTreeMap.Internal.Impl.filterMap f t₂ ⋯).impl
-- Mathlib.MeasureTheory.Order.Lattice
Finset.measurable_sup' : ∀ {α : Type u_2} {m : MeasurableSpace α} {δ : Type u_3} [inst : MeasurableSpace δ] [inst_1 : SemilatticeSup α]
  [MeasurableSup₂ α] {ι : Type u_4} {s : Finset ι} (hs : s.Nonempty) {f : ι → δ → α},
  (∀ n ∈ s, Measurable (f n)) → Measurable (s.sup' hs f)
-- Aesop.Builder.Basic
Aesop.instInhabitedPhaseSpec.default : Aesop.PhaseSpec
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.cRank_le_card_height : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] [inst_2 : Fintype m]
  (A : Matrix m n R), A.cRank ≤ ↑(Fintype.card m)
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.mono_of_mem_nhdsWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜},
  HasDerivWithinAt f f' t x → t ∈ nhdsWithin x s → HasDerivWithinAt f f' s x
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projectionOnto_comp_subtype`. -/
Submodule.linearProjOfIsCompl_comp_subtype : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q), p.projectionOnto q h ∘ₗ p.subtype = LinearMap.id
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.coeff_mapAddEquiv : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Mul M] (e : R ≃+ S)
  (x : MonoidAlgebra R M) (m : M), ((MonoidAlgebra.mapAddEquiv M e) x).coeff m = e (x.coeff m)
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_ofFin : ∀ (n : Fin UInt32.size), (UInt32.ofFin n).toUInt8 = UInt8.ofNat ↑n
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr₂_comm : ∀ {α : Type u_1} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {s : σ} (xs ys : List.Vector α n) (f : α → α → σ → σ × γ),
  (∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s) → List.Vector.mapAccumr₂ f xs ys s = List.Vector.mapAccumr₂ f ys xs s
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
/-- Do not use this field directly: use the more general
`guitartExact_of_isLeftDerivabilityStructure` instead,
see also the lemma `isLeftDerivabilityStructure_iff`.  -/
CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.guitartExact' : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C₁}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
  [self : Φ.IsLeftDerivabilityStructure],
  CategoryTheory.TwoSquare.GuitartExact
    (CategoryTheory.CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).inv
-- Mathlib.Analysis.Convex.Quasiconvex
QuasilinearOn.monotone_comp : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {β : Type u_6} {γ : Type u_7} [inst_4 : LinearOrder β] [inst_5 : Preorder γ] {s : Set E}
  {f : E → β} {g : β → γ}, Monotone g → QuasilinearOn 𝕜 s f → QuasilinearOn 𝕜 s (g ∘ f)
-- Mathlib.Algebra.GroupWithZero.Defs
CancelMonoidWithZero.toMonoidWithZero : {M₀ : Type u_2} → CancelMonoidWithZero M₀ → MonoidWithZero M₀
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric
QuadraticModuleCat.instBraidedCategory : {R : Type u} → [inst : CommRing R] → [inst_1 : Invertible 2] → CategoryTheory.BraidedCategory (QuadraticModuleCat R)
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.sepBy1IndentSemicolon.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₁.comp.sizeOf_spec : ∀ (e : Lean.Expr) (a a_1 : Mathlib.Tactic.BicategoryLike.Mor₁),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₁.comp e a a_1) = 1 + sizeOf e + sizeOf a + sizeOf a_1
-- Mathlib.Data.Int.Cast.Basic
Int.cast_subNatNat : ∀ {R : Type u} [inst : AddGroupWithOne R] (m n : ℕ), ↑(Int.subNatNat m n) = ↑m - ↑n
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- Centers of the balls  -/
Besicovitch.SatelliteConfig.c : {α : Type u_1} → [inst : MetricSpace α] → {N : ℕ} → {τ : ℝ} → Besicovitch.SatelliteConfig α N τ → Fin N.succ → α
-- Init.Data.ByteArray.Basic
_private.Init.Data.ByteArray.Basic.0.ByteArray.Iterator.remainingBytes.match_1.eq_1 : ∀ (motive : ByteArray.Iterator → Sort u_1) (arr : ByteArray) (i : ℕ)
  (h_1 : (arr : ByteArray) → (i : ℕ) → motive { array := arr, idx := i }),
  (match { array := arr, idx := i } with
    | { array := arr, idx := i } => h_1 arr i) =
    h_1 arr i
-- Lean.DocString.Types
Lean.Doc.instBEqInline : {i : Type u_1} → [BEq i] → BEq (Lean.Doc.Inline i)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instRightCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : RightCancelSemigroup α],
  Colex.instRightCancelSemigroup = { toSemigroup := Colex.instSemigroup, toIsRightCancelMul := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.IsColimit.existsUnique : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Cofork f g}
  (hs : CategoryTheory.Limits.IsColimit s) {W : C} (k : Y ⟶ W),
  CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k →
    ∃! d, CategoryTheory.CategoryStruct.comp s.π d = k
-- Init.Data.Nat.Gcd
Nat.dvd_gcd : ∀ {k m n : ℕ}, k ∣ m → k ∣ n → k ∣ m.gcd n
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.kernelForkOfFork_ofι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y}
  {P : C} (ι : P ⟶ X) (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g),
  CategoryTheory.Preadditive.kernelForkOfFork (CategoryTheory.Limits.Fork.ofι ι w) =
    CategoryTheory.Limits.KernelFork.ofι ι ⋯
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.map_mapRingHom_eval_map : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (p : Polynomial (Polynomial R))
  (q : Polynomial R),
  Polynomial.eval (Polynomial.map f q) (Polynomial.map (Polynomial.mapRingHom f) p) =
    Polynomial.map f (Polynomial.eval q p)
-- Lean.Syntax
Lean.Syntax.isAnyAntiquot : Lean.Syntax → Bool
-- Lean.Setup
Lean.ImportArtifacts.oleanServer? : Lean.ImportArtifacts → Option System.FilePath
-- Mathlib.Analysis.Convex.Strict
/-- The translation of a strictly convex set is also strictly convex.  -/
StrictConvex.preimage_add_left : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCancelCommMonoid E] [ContinuousAdd E] [inst_5 : Module 𝕜 E] {s : Set E},
  StrictConvex 𝕜 s → ∀ (z : E), StrictConvex 𝕜 ((fun x => x + z) ⁻¹' s)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.equiv_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Nonsingular P → W.Nonsingular Q → P 2 = 0 → Q 2 = 0 → P ≈ Q
-- Mathlib.Topology.UniformSpace.CompactConvergence
UniformSpace.replaceTopology.congr_simp : ∀ {α : Type u_2} [i : TopologicalSpace α] (u u_1 : UniformSpace α) (e_u : u = u_1) (h : i = u.toTopologicalSpace),
  u.replaceTopology h = u_1.replaceTopology ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoPullback_inv_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C}
  (h_1 : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp h.isoPullback.inv (CategoryTheory.CategoryStruct.comp fst h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h_1
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.OuterRegular.zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α], MeasureTheory.Measure.OuterRegular 0
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.toOpen_res : ∀ {R : CommRingCat} (M : ModuleCat ↑R) (U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top ↑R))
  (i : V ⟶ U),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.toOpen M U)
      ((AlgebraicGeometry.modulesSpecToSheaf.obj (AlgebraicGeometry.tilde M)).presheaf.map i.op) =
    AlgebraicGeometry.tilde.toOpen M V
-- Init.Data.Array.MapIdx
Array.mapIdx_eq_empty_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {xs : Array α}, Array.mapIdx f xs = #[] ↔ xs = #[]
-- Init.Data.String.Basic
String.toList_ofList : ∀ {l : List Char}, (String.ofList l).toList = l
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.perfectField : ∀ (k : Type u) [inst : Field k] [IsAlgClosed k], PerfectField k
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
_private.Mathlib.NumberTheory.DiophantineApproximation.Basic.0.Real.aux₀ : ∀ {v : ℤ}, 0 < v → 0 < ↑v ∧ 0 < 2 * ↑v - 1
-- Init.Data.Range.Polymorphic.Basic
/-- Returns the number of elements starting from `lo` that satisfy the given upper bound.  -/
Std.Rxi.HasSize.size : {α : Type u} → [self : Std.Rxi.HasSize α] → α → ℕ
-- Aesop.RuleTac.ElabRuleTerm
Aesop.withFullElaboration : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.instInhabited : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [Inhabited Y] → Inhabited (LocallyConstant X Y)
-- Mathlib.Topology.Separation.Regular
instT3Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] [RegularSpace X], T3Space X
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.natCard_extension : ∀ (k : Type u_1) [inst : Field k] [Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [NeZero n], Nat.card (FiniteField.Extension k p n) = Nat.card k ^ n
-- Mathlib.GroupTheory.Congruence.Opposite
AddCon.orderIsoOp_symm_apply : ∀ {M : Type u_1} [inst : Add M] (c : AddCon Mᵃᵒᵖ), (RelIso.symm AddCon.orderIsoOp) c = c.unop
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.subst.injEq : ∀ (x : Lean.Grind.Linarith.Var) (c₁ : Lean.Meta.Grind.Arith.Linear.EqCnstr)
  (c₂ : Lean.Meta.Grind.Arith.Linear.IneqCnstr) (x_1 : Lean.Grind.Linarith.Var)
  (c₁_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr) (c₂_1 : Lean.Meta.Grind.Arith.Linear.IneqCnstr),
  (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.subst x c₁ c₂ =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.subst x_1 c₁_1 c₂_1) =
    (x = x_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
rank_fun_infinite : ∀ {K : Type u} [inst : DivisionRing K] {ι : Type v} [hι : Infinite ι], Module.rank K (ι → K) = Cardinal.mk (ι → K)
-- Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
CategoryTheory.precoherentEffectiveEpiFamilyCompEffectiveEpis : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Precoherent C] {X : C} {α : Type}
  [Finite α] {Y Z : α → C} (π : (a : α) → Y a ⟶ X) [CategoryTheory.EffectiveEpiFamily Y π] (f : (a : α) → Z a ⟶ Y a)
  [h : ∀ (a : α), CategoryTheory.EffectiveEpi (f a)],
  CategoryTheory.EffectiveEpiFamily Z fun a => CategoryTheory.CategoryStruct.comp (f a) (π a)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.ofArray_eq_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} (a : Array (α × β)),
  Std.DHashMap.Const.ofArray a = Std.DHashMap.Const.ofList a.toList
-- Mathlib.Tactic.Linter.TextBased
/-- Whether a collection of lines consists *only* of imports, blank lines and single-line comments.
In practice, this means it's an imports-only file and exempt from almost all linting.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.isImportsOnlyFile : Array String → Bool
-- Mathlib.Data.Int.Bitwise
/-- Defines a function from `ℤ` conditionally, if it is defined for odd and even integers separately
using `bit`.  -/
Int.bitCasesOn : {C : ℤ → Sort u} → (n : ℤ) → ((b : Bool) → (n : ℤ) → C (Int.bit b n)) → C n
-- Std.Internal.Parsec.ByteArray
/-- Parses while a predicate is satisfied.
Fails with `.eof` if input ends while the predicate still holds.
 -/
Std.Internal.Parsec.ByteArray.takeWhile : (UInt8 → Bool) → Std.Internal.Parsec.ByteArray.Parser ByteSlice