mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.mk.sizeOf_spec : ∀ {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₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃}
  {f₃ : X₃ ⟶ Y₃} [inst_3 : SizeOf C₁] [inst_4 : SizeOf C₂] [inst_5 : SizeOf C₃] (pt : C₂)
  (fst : pt ⟶ (G.obj (Opposite.op X₁)).obj X₃) (snd : pt ⟶ (G.obj (Opposite.op Y₁)).obj Y₃)
  (isPullback : CategoryTheory.IsPullback fst snd ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃))
  (π : (G.obj (Opposite.op Y₁)).obj X₃ ⟶ pt)
  (π_fst :
    autoParam (CategoryTheory.CategoryStruct.comp π fst = (G.map f₁.op).app X₃)
      CategoryTheory.Functor.PullbackObjObj.π_fst._autoParam)
  (π_snd :
    autoParam (CategoryTheory.CategoryStruct.comp π snd = (G.obj (Opposite.op Y₁)).map f₃)
      CategoryTheory.Functor.PullbackObjObj.π_snd._autoParam),
  sizeOf { pt := pt, fst := fst, snd := snd, isPullback := isPullback, π := π, π_fst := π_fst, π_snd := π_snd } =
    1 + sizeOf pt + sizeOf fst + sizeOf snd + sizeOf isPullback + sizeOf π + sizeOf π_fst + sizeOf π_snd
-- Mathlib.Topology.Homotopy.HSpaces
unitInterval.qRight.eq_1 : ∀ (p : ↑unitInterval × ↑unitInterval),
  unitInterval.qRight p = Set.projIcc 0 1 unitInterval.qRight._proof_1 (2 * ↑p.1 / (1 + ↑p.2))
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_ofClass : ∀ {S : Type u_1} {R : Type u_2} [inst : NonAssocSemiring R] [inst_1 : SetLike S R] [inst_2 : SubsemiringClass S R]
  (s : S), ↑(Subsemiring.ofClass s) = ↑s
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.idx.congr_simp : ∀ {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.Scheme.JointlySurjective K] (𝒰 : AlgebraicGeometry.Scheme.Cover K X) (x x_1 : ↥X),
  x = x_1 → 𝒰.idx x = 𝒰.idx x_1
-- Mathlib.Order.Interval.Set.Disjoint
IsGLB.biUnion_Ici_eq_Ici : ∀ {α : Type v} [inst : LinearOrder α] {s : Set α} {a : α}, IsGLB s a → a ∈ s → ⋃ x ∈ s, Set.Ici x = Set.Ici a
-- Mathlib.Analysis.Complex.ValueDistribution.Cartan
/-- Qualitative version of **Cartan's formula**: Away from the point `0`, the difference between
`characteristic f ⊤` and `fun R ↦ circleAverage (logCounting f · R) 0 1` is constant. This
qualitative version of Cartan's formula exists because the specific value of the constant does not
matter in practice.
 -/
ValueDistribution.characteristic_top_eq_circleAverage_add_const : ∀ {f : ℂ → ℂ},
  Meromorphic f →
    ∃ const,
      ∀ (R : ℝ),
        R ≠ 0 →
          ValueDistribution.characteristic f ⊤ R =
            Real.circleAverage (fun x => ValueDistribution.logCounting f (↑x) R) 0 1 + const
-- Mathlib.Data.ZMod.IntUnitsPower
instSMulZModOfNatNatAdditiveUnitsInt : SMul (ZMod 2) (Additive ℤˣ)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadIso.toNatIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Monad C} (h : M ≅ N),
  (CategoryTheory.MonadIso.toNatIso h).inv = (CategoryTheory.monadToFunctor C).map h.inv
-- Mathlib.Condensed.Basic
/-- **Alias** of `Condensed.comp_hom`. -/
Condensed.comp_val : ∀ {C : Type w} [inst : CategoryTheory.Category.{v, w} C] {X Y Z : Condensed C} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
GradedAlgebra.coe_algebraMap_apply : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : Semiring A] [inst_6 : Algebra R A]
  (𝒜 : ι → Submodule R A) [inst_7 : GradedAlgebra 𝒜] (s : S),
  ↑((algebraMap S ↥(Submodule.baseChange S (𝒜 0))) s) = s ⊗ₜ[R] 1
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasFiniteRange.add : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Ring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [IsNoetherianRing K] {f g : V →ₗ[K] V₂},
  f.HasFiniteRange → g.HasFiniteRange → (f + g).HasFiniteRange
-- Init.Data.Vector.DecidableEq
Vector.isEqv_eq_decide : ∀ {α : Type u_1} {n : ℕ} (xs ys : Vector α n) (r : α → α → Bool),
  xs.isEqv ys r = decide (∀ (i : ℕ) (h' : i < n), r xs[i] ys[i] = true)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.one_le_eval_T_real : ∀ (n : ℤ) {x : ℝ}, 1 ≤ x → 1 ≤ Polynomial.eval x (Polynomial.Chebyshev.T ℝ n)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_le_ceil : ∀ {r : ENNReal}, ⌊r⌋ₑ ≤ ⌈r⌉ₑ
-- Mathlib.Data.ENNReal.Basic
ENNReal.max_zero_left : ∀ {a : ENNReal}, max 0 a = a
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_comp_iff : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : Star α] {A : Matrix m m (Matrix n n α)},
  ((Matrix.comp m m n n α) A).IsHermitian ↔ A.IsHermitian
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- If the angle between the line `p q` and the radius at `p` equals `π / 2`, then the line `p q` is
tangent to the sphere at `p`.  -/
EuclideanGeometry.Sphere.IsTangentAt_of_angle_eq_pi_div_two : ∀ {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} {p q : P},
  EuclideanGeometry.angle q p s.center = Real.pi / 2 → p ∈ s → s.IsTangentAt p line[ℝ, p, q]
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.arrowCongr.eq_1 : ∀ {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [inst : Mul P] [inst_1 : Mul Q] (f : M ≃ N)
  (g : P ≃* Q),
  MulEquiv.arrowCongr f g =
    { toFun := fun h n => g (h (f.symm n)), invFun := fun k m => g.symm (k (f m)), left_inv := ⋯, right_inv := ⋯,
      map_mul' := ⋯ }
-- Mathlib.Probability.Independence.CharacteristicFunction
/-- **Alias** of `ProbabilityTheory.iIndepFun.charFun_map_fun_finsetSum_eq_prod`. -/
ProbabilityTheory.iIndepFun.charFun_map_fun_finset_sum_eq_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {s : Finset ι} {E : Type u_3}
  [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : ι → Ω → E}
  [inst_4 : InnerProductSpace ℝ E],
  (∀ i ∈ s, AEMeasurable (X i) P) →
    ProbabilityTheory.iIndepFun (s.restrict X) P →
      MeasureTheory.charFun (MeasureTheory.Measure.map (fun ω => ∑ i ∈ s, X i ω) P) =
        ∏ i ∈ s, MeasureTheory.charFun (MeasureTheory.Measure.map (X i) P)
-- Init.Data.Array.BasicAux
_private.Init.Data.Array.BasicAux.0.List.toArrayAux.match_1.splitter : {α : Type u_1} →
  (motive : List α → Array α → Sort u_2) →
    (x : List α) →
      (x_1 : Array α) →
        ((xs : Array α) → motive [] xs) →
          ((a : α) → (as : List α) → (xs : Array α) → motive (a :: as) xs) → motive x x_1
-- Mathlib.Topology.Constructions
Topology.IsClosedEmbedding.sigmaMk : ∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {i : ι},
  Topology.IsClosedEmbedding (Sigma.mk i)
-- Init.Data.List.Sublist
List.reverse_suffix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse <:+ l₂.reverse ↔ l₁ <+: l₂
-- Lean.Widget.UserWidget
_private.Lean.Widget.UserWidget.0.Lean.Widget.evalUserWidgetDefinitionUnsafe : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] → [Lean.MonadOptions m] → [Lean.MonadError m] → Lean.Name → m Lean.Widget.UserWidgetDefinition
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
Lean.Meta.RefinedDiscrTree.instInhabitedMatchResult.default : {α : Type} → Lean.Meta.RefinedDiscrTree.MatchResult α
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.rotate_rotate : ∀ {n : ℕ} {x : BitVec n}, BitVec.Signed.rotate✝ (BitVec.Signed.rotate✝ x) = x
-- Lean.Expr
/-- Polymorphic operation for generating unique/fresh free variable identifiers.
It is available in any monad `m` that implements the interface `MonadNameGenerator`.
 -/
Lean.mkFreshFVarId : {m : Type → Type} → [Monad m] → [Lean.MonadNameGenerator m] → m Lean.FVarId
-- Lean.Elab.Term.TermElabM
/-- Auxiliary datatype for presenting a Lean lvalue modifier.
We represent an unelaborated lvalue as a `Syntax` (or `Expr`) and `List LVal`.
Example: `a.foo.1` is represented as the `Syntax` `a` and the list
`[LVal.fieldName "foo", LVal.fieldIdx 1]`.
 -/
Lean.Elab.Term.LVal : Type
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.hasBasis_self_subset : ∀ {α : Type u_1} {l : Filter α} {p : Set α → Prop},
  l.HasBasis (fun s => s ∈ l ∧ p s) id → ∀ {V : Set α}, V ∈ l → l.HasBasis (fun s => s ∈ l ∧ p s ∧ s ⊆ V) id
-- Mathlib.Analysis.Calculus.Deriv.Inverse
not_differentiableAt_of_local_left_inverse_hasDerivAt_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {a : 𝕜},
  HasDerivAt f 0 (g a) → f ∘ g =ᶠ[nhds a] id → ¬DifferentiableAt 𝕜 g a
-- Mathlib.Tactic.Order
/-- Args for the `order` tactic.  -/
Mathlib.Tactic.Order.orderArgs : Lean.ParserDescr
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ofList_cons : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α} {v : β} {tl : List (α × β)},
  Std.ExtTreeMap.ofList ((k, v) :: tl) cmp = (∅.insert k v).insertMany tl
-- Mathlib.Topology.Semicontinuity.Defs
LowerSemicontinuousOn.lowerSemicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {x : α} {s : Set α},
  LowerSemicontinuousOn f s → x ∈ s → LowerSemicontinuousWithinAt f s x
-- Mathlib.Algebra.Ring.Defs
ite_zero_mul : ∀ {α : Type u} [inst : MulZeroClass α] (P : Prop) [inst_1 : Decidable P] (a b : α),
  (if P then a else 0) * b = if P then a * b else 0
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Try adding the local hypothesis to the `RefinedDiscrTree`.  -/
Mathlib.Tactic.LibraryRewrite.addLocalRewriteEntry : Lean.LocalDecl →
  Lean.MetaM
    (List ((Lean.FVarId × Bool) × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))
-- Lean.Declaration
Lean.RecursorVal.mk : Lean.ConstantVal → List Lean.Name → ℕ → ℕ → ℕ → ℕ → List Lean.RecursorRule → Bool → Bool → Lean.RecursorVal
-- Lean.Meta.CongrTheorems
Lean.Meta.instInhabitedCongrArgKind : Inhabited Lean.Meta.CongrArgKind
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
sum_eq_tsum_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α) (s : Finset β)
  (L : optParam (SummationFilter β) (SummationFilter.unconditional β)) [L.LeAtTop],
  ∑ x ∈ s, f x = ∑'[L] (x : β), (↑s).indicator f x
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.truncTotal_mul_sub_mul_truncTotal_mem_pow_idealOfVars : ∀ {σ : Type u_1} {R : Type u_2} {n : ℕ} [inst : CommRing R] [inst_1 : Finite σ] (p q : MvPowerSeries σ R),
  (MvPowerSeries.truncTotal n) (p * q) - (MvPowerSeries.truncTotal n) p * (MvPowerSeries.truncTotal n) q ∈
    MvPolynomial.idealOfVars σ R ^ n
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.restrictScalarsEquivalenceOfRingEquiv_functor : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
  (AlgCat.restrictScalarsEquivalenceOfRingEquiv e).functor = AlgCat.restrictScalars e.toRingHom
-- Mathlib.RingTheory.Etale.Pi
Algebra.FormallyEtale.pi_iff : ∀ {R : Type u_1} {I : Type u_2} (A : I → Type u_3) [inst : CommRing R] [inst_1 : (i : I) → CommRing (A i)]
  [inst_2 : (i : I) → Algebra R (A i)] [Finite I],
  Algebra.FormallyEtale R ((i : I) → A i) ↔ ∀ (i : I), Algebra.FormallyEtale R (A i)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_congr : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f₁ f₂ : α → E}
  {g₁ g₂ : α → F}, f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → (f₁ =o[l] g₁ ↔ f₂ =o[l] g₂)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.fst_comp_prod : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [inst : VAdd M α] [inst_1 : VAdd N γ]
  [inst_2 : VAdd N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ), (AddActionHom.fst N γ δ).comp (f.prod g) = f
-- Mathlib.LinearAlgebra.PiTensorProduct.Generators
PiTensorProduct.ext_of_span_eq_top : ∀ {R : Type u_1} {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {N : Type u_4} {γ : ι → Type u_5} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
  [inst_4 : Module R N] {g : ⦃i : ι⦄ → γ i → M i},
  (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) →
    ∀ {φ φ' : (PiTensorProduct R fun i => M i) →ₗ[R] N},
      (∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))) → φ = φ'
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.pi_apply : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M₁ i)]
  [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : (i : ι) → TopologicalSpace (M₁ i)] {ι' : Type u_1} {M' : ι' → Type u_2}
  [inst_4 : (i : ι') → AddCommMonoid (M' i)] [inst_5 : (i : ι') → TopologicalSpace (M' i)]
  [inst_6 : (i : ι') → Module R (M' i)] (f : (i : ι') → ContinuousMultilinearMap R M₁ (M' i)) (m : (i : ι) → M₁ i)
  (j : ι'), (ContinuousMultilinearMap.pi f) m j = (f j) m
-- Lean.Server.ServerTask
Lean.Server.ServerTask.join : {α : Type u_1} → Array (Lean.Server.ServerTask α) → Lean.Server.ServerTask (Array α)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).hom.hom₁ =
    CategoryTheory.CategoryStruct.id X₁
-- Lean.Parser.Types
Lean.Parser.ParserState.hasError : Lean.Parser.ParserState → Bool
-- Init.Data.Order.Factories
/-- If an `LE α` instance is reflexive and transitive, then it represents a preorder.
 -/
Std.IsPreorder.of_le : ∀ {α : Type u} [inst : LE α],
  autoParam (Std.Refl fun x1 x2 => x1 ≤ x2) Std.IsPreorder.of_le._auto_1 →
    ∀
      (le_trans :
        autoParam (Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2)
          Std.IsPreorder.of_le._auto_3),
      Std.IsPreorder α
-- Mathlib.Logic.Pairwise
pairwise_fin_succ_iff : ∀ {n : ℕ} {R : Fin n.succ → Fin n.succ → Prop},
  Pairwise R ↔ (∀ (i : Fin n), R i.succ 0) ∧ (∀ (j : Fin n), R 0 j.succ) ∧ Pairwise fun i j => R i.succ j.succ
-- Init.Data.UInt.Bitwise
UInt16.not_eq_comm : ∀ {a b : UInt16}, ~~~a = b ↔ a = ~~~b
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.isOpenMap_iff : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [inst : TopologicalSpace β] {B : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis B → ∀ {f : α → β}, IsOpenMap f ↔ ∀ s ∈ B, IsOpen (f '' s)
-- Mathlib.Algebra.Group.Conj
/-- The setoid of the relation `IsConj` iff there is a unit `u` such that `u * x = y * u`  -/
IsConj.setoid : (α : Type u_1) → [Monoid α] → Setoid α
-- Aesop.ElabM
Aesop.ElabM.Context.goal : Aesop.ElabM.Context → Lean.MVarId
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The raw definition of a Turing machine does not require that
`Γ` and `Λ` are finite, and in practice we will be interested
in the infinite `Λ` case. We recover instead a notion of
"effectively finite" Turing machines, which only make use of a
finite subset of their states. We say that a set `S ⊆ Λ`
supports a Turing machine `M` if `S` is closed under the
transition function and contains the initial state.  -/
Turing.TM0.Supports : {Γ : Type u_1} → {Λ : Type u_2} → [inst : Inhabited Λ] → Turing.TM0.Machine Γ Λ → Set Λ → Prop
-- Mathlib.Geometry.Euclidean.Altitude
/-- The height of a 1-dimensional simplex equals to the distance between the two vertices.  -/
Affine.Simplex.height_eq_dist : ∀ {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 : Affine.Simplex ℝ P 1) (i : Fin 2), s.height i = dist (s.points 0) (s.points 1)
-- Mathlib.Algebra.Group.TypeTags.Hom
/-- Reinterpret `α →+ Additive β` as `Multiplicative α →* β`.  -/
AddMonoidHom.toMultiplicativeLeft : {α : Type u_3} →
  {β : Type u_4} → [inst : AddZeroClass α] → [inst_1 : MulOneClass β] → (α →+ Additive β) ≃ (Multiplicative α →* β)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.tendsto_valuation : ∀ (K : Type u_2) [inst : Field K]
  (a : IsDedekindDomain.HeightOneSpectrum.adicCompletion (RatFunc K) (Polynomial.idealX K)),
  Filter.Tendsto (⇑Valued.v)
    (Filter.comap
      (fun x =>
        {
          toCompletion :=
            ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (Polynomial.idealX K))).symm
                x) })
      (nhds a))
    (nhds (Valued.v a))
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.Relation.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S : C} →
      {E : CategoryTheory.PreZeroHypercover S} →
        {i j : E.I₀} →
          (obj : C) →
            (fst : obj ⟶ E.X i) →
              (snd : obj ⟶ E.X j) →
                CategoryTheory.CategoryStruct.comp fst (E.f i) = CategoryTheory.CategoryStruct.comp snd (E.f j) →
                  E.Relation i j
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_nonneg : ∀ {R : Type u_1} [inst : AddCommGroupWithOne R] [inst_1 : PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] {n : ℤ},
  0 ≤ n → 0 ≤ ↑n
-- Std.Http.Data.URI.Basic
/-- Absolute-form request target containing a complete URI. Used when making requests through a proxy.
Example: `http://example.com:8080/path?key=value`
 -/
Std.Http.RequestTarget.absoluteForm : Std.Http.URI → Std.Http.RequestTarget
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- The logarithmic counting function associated with the divisor of `f` is the difference between
`logCounting f 0` and `logCounting f ⊤`.
 -/
ValueDistribution.log_counting_zero_sub_logCounting_top : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : 𝕜 → E},
  Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f Set.univ) =
    ValueDistribution.logCounting f 0 - ValueDistribution.logCounting f ⊤
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k} {fallback : α},
      Std.Internal.List.minKeyD (Std.Internal.List.insertEntryIfNew k v l) fallback =
        (Std.Internal.List.minKey? l).elim k fun k' => if compare k k' = Ordering.lt then k else k'
-- Mathlib.LinearAlgebra.CrossProduct
/-- The cross product of two vectors is perpendicular to the second vector.  -/
dot_cross_self : ∀ {R : Type u_1} [inst : CommRing R] (v w : Fin 3 → R), w ⬝ᵥ (crossProduct v) w = 0
-- Mathlib.Algebra.Order.Group.Cone
/-- Construct a linear order by designating a maximal cone in an abelian group.  -/
LinearOrder.mkOfAddGroupCone : {S : Type u_1} →
  {G : Type u_2} →
    [inst : AddCommGroup G] →
      [inst_1 : SetLike S G] →
        (C : S) → [AddGroupConeClass S G] → [HasMemOrNegMem C] → [DecidablePred fun x => x ∈ C] → LinearOrder G
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_natAdd_uIcc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (Fin.natAdd m) (Finset.uIcc i j) = Finset.uIcc (Fin.natAdd m i) (Fin.natAdd m j)
-- Lean.Parser.Basic
/-- The `ws` parser requires that there is some whitespace at this location.
For example, the parser `"foo" ws "+"` parses `foo +` or `foo/- -/+` but not `foo+`.

This parser has arity 0 - it does not capture anything.  -/
Lean.Parser.checkWsBefore : optParam String "space before" → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.isoApp_refl : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I),
  CategoryTheory.Pi.isoApp (CategoryTheory.Iso.refl X) i = CategoryTheory.Iso.refl (X i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {k : α},
  t.WF →
    (List.find? (fun x => compare x.fst k == Ordering.eq) t.toList = none ↔
      Std.DTreeMap.Internal.Impl.contains k t = false)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.addCommGroup : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddCommGroup (β i)] → AddCommGroup (Π₀ (i : ι), β i)
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.gcd_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α], Multiset.gcd 0 = 0
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.deriv_mgf_zero : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  0 ∈ interior (ProbabilityTheory.integrableExpSet X μ) → deriv (ProbabilityTheory.mgf X μ) 0 = ∫ (x : Ω), X x ∂μ
-- Mathlib.Logic.Function.Basic
/-- A congruence lemma for `Function.update`, specialized for the non-dependent case. Without this,
`simp` can't rewrite in the fourth argument `a` because the result type depends on `a`.
See also https://github.com/leanprover/lean4/issues/12478.
 -/
Function.update_congr : ∀ {α : Sort u} [inst : DecidableEq α] {β : Sort u_1} {f₁ f₂ : α → β},
  f₁ = f₂ →
    ∀ {a'₁ a'₂ : α},
      a'₁ = a'₂ →
        ∀ {v₁ v₂ : β}, v₁ = v₂ → ∀ {a₁ a₂ : α}, a₁ = a₂ → Function.update f₁ a'₁ v₁ a₁ = Function.update f₂ a'₂ v₂ a₂
-- Qq.Match
/-- Pattern variables can be functions; if so, this is their arity.  -/
Qq.Impl.PatternVar.arity : Qq.Impl.PatternVar → ℕ
-- Init.System.IO
/-- Checks whether the child has exited. Returns `none` if the process has not exited, or its exit code
if it has.
 -/
IO.Process.Child.tryWait : {cfg : IO.Process.StdioConfig} → IO.Process.Child cfg → IO (Option UInt32)
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.nnnorm_rankOne : ∀ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x : E) (y : F),
  ‖((InnerProductSpace.rankOne 𝕜) x) y‖₊ = ‖x‖₊ * ‖y‖₊
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.presheafIso_inv_app_hom_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} [inst_2 : G.IsCoverDense K] [inst_3 : G.IsLocallyFull K]
  {ℱ ℱ' : CategoryTheory.Sheaf K (Type v)} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) (X : Dᵒᵖ)
  (x : ℱ'.obj.obj (Opposite.op (Opposite.unop X))),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.IsCoverDense.Types.presheafIso i).inv.app X)) x =
    ⋯.amalgamate
      (fun x_1 x_2 hf =>
        (CategoryTheory.ConcreteCategory.hom (ℱ.obj.map (Nonempty.some hf).lift.op))
          ((CategoryTheory.ConcreteCategory.hom (i.inv.app (Opposite.op (Nonempty.some hf).1)))
            ((CategoryTheory.ConcreteCategory.hom (ℱ'.obj.map (Nonempty.some hf).map.op)) x)))
      ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffine_of_singular : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  ¬W.Nonsingular P → WeierstrassCurve.Projective.Point.toAffine W P = 0
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop_apply : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f : L.PartialEquiv M N} (h : f.dom = ⊤) (m : M),
  (FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop h) m = ↑(f.toEquiv ⟨m, ⋯⟩)