mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- Type-alias for modifications between oplax transformations of lax functors. This is the type
used for the 2-homomorphisms in the bicategory of lax functors equipped with oplax
transformations.  -/
CategoryTheory.Lax.OplaxTrans.Hom : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → (F ⟶ G) → (F ⟶ G) → Type (max u₁ w₂)
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.mk_refl : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X),
  Path.Homotopic.Quotient.mk (Path.refl x) = Path.Homotopic.Quotient.refl x
-- Std.Data.DTreeMap.Basic
/-- Returns the number of mappings present in the map.  -/
Std.DTreeMap.size : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → ℕ
-- Mathlib.Algebra.Order.Hom.Ring
/-- Any type satisfying `OrderRingIsoClass` can be cast into `OrderRingIso` via
`OrderRingIsoClass.toOrderRingIso`.  -/
instCoeTCOrderRingIsoOfOrderIsoClassOfRingEquivClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : EquivLike F α β] →
        [inst_1 : Mul α] →
          [inst_2 : Add α] →
            [inst_3 : LE α] →
              [inst_4 : Mul β] →
                [inst_5 : Add β] → [inst_6 : LE β] → [OrderIsoClass F α β] → [RingEquivClass F α β] → CoeTC F (α ≃+*o β)
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinOnBall.const_smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {R : Type u_9} [inst_5 : NormedRing R]
  [inst_6 : Module R F] [inst_7 : IsBoundedSMul R F] [inst_8 : SMulCommClass 𝕜 R F] {c : R},
  HasFPowerSeriesWithinOnBall f pf s x r → HasFPowerSeriesWithinOnBall (c • f) (c • pf) s x r
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The natural inclusion of a subrepresentation into the ambient representation.  -/
Rep.subtype : {k : Type u} →
  {G : Type v} →
    [inst : Ring k] →
      [inst_1 : Monoid G] →
        (A : Rep.{u_1, u, v} k G) →
          (W : Submodule k ↑A) →
            (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) → A.subrepresentation W le_comap ⟶ A
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The transfinite iteration of `succStruct W Z` to the power `κ.ord.ToType`.  -/
CategoryTheory.OrthogonalReflection.reflectionObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      C →
        [inst_1 : CategoryTheory.Limits.HasPushouts C] →
          [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
            [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
              [∀ (Z : C),
                    CategoryTheory.Limits.HasMulticoequalizer
                      (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] →
                (κ : Cardinal.{w}) →
                  [OrderBot κ.ord.ToType] → [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] → C
-- Init.Data.Vector.Lemmas
Vector.foldl_eq_apply_foldr : ∀ {α : Type u_1} {n : ℕ} {init x : α} {xs : Vector α n} {f : α → α → α} [Std.Associative f]
  [Std.LawfulRightIdentity f init], Vector.foldl f x xs = f x (Vector.foldr f init xs)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instOrdRequestID : Ord Lean.JsonRpc.RequestID
-- Mathlib.Analysis.Complex.Norm
Complex.norm_nonneg : ∀ (z : ℂ), 0 ≤ ‖z‖
-- Mathlib.CategoryTheory.Yoneda
/-- A functor `F : C ⥤ Type v₁` is corepresentable if there is object `X` so `F ≅ coyoneda.obj X`.
 -/
CategoryTheory.Functor.IsCorepresentable : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor C (Type v) → Prop
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.ext'_iff : ∀ {α : Type u} [inst : AddGroup α] {f g : AddGroupTopology α}, f = g ↔ TopologicalSpace.IsOpen = TopologicalSpace.IsOpen
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord : ∀ {n : Type u} {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) (i : n),
  (CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.AffineSpace.homOfVector f v)))
      (AlgebraicGeometry.AffineSpace.coord S i) =
    v i
-- Mathlib.Analysis.Real.Pi.Bounds
Real.sqrtTwoAddSeries_step_down : ∀ (a b : ℕ) {c d n : ℕ} {z : ℝ},
  z ≤ (↑a / ↑b).sqrtTwoAddSeries n →
    0 < b → 0 < d → a ^ 2 * d ≤ (2 * d + c) * b ^ 2 → z ≤ (↑c / ↑d).sqrtTwoAddSeries (n + 1)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.mul_star_eq_coe : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R], a * star a = ↑(a * star a).re
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.sdiff_singleton_isBasis : ∀ {α : Type u_1} {M : Matroid α} {C : Set α} {e : α}, M.IsCircuit C → e ∈ C → M.IsBasis (C \ {e}) C
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.coe_injective : ∀ {α : Type u}, Function.Injective WithZero.coe
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The `n`th object of the standard resolution of `k` is definitionally isomorphic to `k[Gⁿ⁺¹]`
equipped with the representation induced by the diagonal action of `G`.  -/
Rep.standardComplex.xIso : (k G : Type u) →
  [inst : CommRing k] →
    [inst_1 : Monoid G] → (n : ℕ) → (Rep.standardComplex k G).X n ≅ Rep.ofMulAction k G (Fin (n + 1) → G)
-- Mathlib.CategoryTheory.Category.Quiv
/-- Category of quivers.  -/
CategoryTheory.Quiv : Type (max (u + 1) u (v + 1))
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.DefEqM.Context.unify : Lean.Meta.Sym.DefEqM.Context✝ → Bool
-- Mathlib.Algebra.Homology.Embedding.Restriction
ComplexShape.Embedding.restrictionFunctor_obj : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3)
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : e.IsRelIff]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c'),
  (e.restrictionFunctor C).obj K = K.restriction e
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valued.toNormedField.norm_le_one_iff : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne] {x : L}, ‖x‖ ≤ 1 ↔ Valued.v x ≤ 1
-- Init.Data.Fin.Lemmas
Fin.val_two : ∀ {n : ℕ}, ↑2 = 2
-- Mathlib.ModelTheory.Fraisse
/-- A Fraïssé class is a nonempty, essentially countable class of structures satisfying the
hereditary, joint embedding, and amalgamation properties.  -/
FirstOrder.Language.IsFraisse : {L : FirstOrder.Language} → Set (CategoryTheory.Bundled L.Structure) → Prop
-- Init.PropLemmas
/-- `∧` distributes over `∨` (on the right).  -/
or_and_right : ∀ {a b c : Prop}, (a ∨ b) ∧ c ↔ a ∧ c ∨ b ∧ c
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.trans_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {e f g : C ⟶ D} (h : Homotopy e f) (k : Homotopy f g) (i j : ι),
  (h.trans k).hom i j = h.hom i j + k.hom i j
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.join₁_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (f : σ → MvPolynomial τ R)
  (φ : MvPolynomial σ R), MvPolynomial.join₁ ((MvPolynomial.rename f) φ) = (MvPolynomial.bind₁ f) φ
-- Init.Data.Float.Float32
/-- Checks whether a floating-point number is finite, that is, whether it is normal, subnormal, or zero,
but not infinite or `NaN`.

This function has a logical model in terms of `Float32.Model`. It is compiled to the C operator `isfinite`.
 -/
Float32.isFinite : Float32 → Bool
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The image of a function in `FunSpace` is contained within a closed ball.  -/
ODE.FunSpace.mem_closedBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L : NNReal}
  {α : ODE.FunSpace t₀ x₀ r L},
  ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r → ∀ {t : ↑(Set.Icc tmin tmax)}, α.toFun t ∈ Metric.closedBall x₀ ↑a
-- Mathlib.Algebra.Homology.ExactSequence
/-- The composable arrows associated to a short complex.  -/
CategoryTheory.ShortComplex.toComposableArrows : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      CategoryTheory.ShortComplex C → CategoryTheory.ComposableArrows C 2
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.map_cast_binomial_real_zero : ∀ {R : Type u_1} [inst : MeasurableSpace R] [inst_1 : AddMonoidWithOne R] [MeasurableSingletonClass R] [CharZero R]
  (n : ℕ) (p : ↑unitInterval),
  (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p)).real {0} = (1 - ↑p) ^ n
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_le_iff' : ∀ {x y z : ENNReal}, y ≠ 0 → y ≠ ⊤ → (x / y ≤ z ↔ x ≤ y * z)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Real.continuousAt_rpow : ∀ (p : ℝ × ℝ), p.1 ≠ 0 ∨ 0 < p.2 → ContinuousAt (fun p => p.1 ^ p.2) p
-- Mathlib.Data.Set.Pairwise.Basic
/-- **Alias** of the forward direction of `pairwise_subtype_iff_pairwise_set`. -/
Pairwise.set_of_subtype : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), (Pairwise fun x y => r ↑x ↑y) → s.Pairwise r
-- Mathlib.Geometry.Manifold.Notation
/-- Elaborator for sections in a fibre bundle: converts a section `s : Π x : M, V x` as a dependent
function to a non-dependent function into the total space. This handles the cases of
- sections of a trivial bundle
- vector fields on a manifold (i.e., sections of the tangent bundle)
- sections of an explicit fibre bundle
- turning a bare function `E → E'` into a section of the trivial bundle `Bundle.Trivial E E'`

This elaborator searches the local context for suitable hypotheses for the above cases by matching
on the expression structure, avoiding `isDefEq`. Therefore, it should be fast enough to always run.
The search can be traced with `set_option Elab.DiffGeo.TotalSpaceMk true`.
 -/
Manifold.«termT%_» : Lean.ParserDescr
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub_intCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIocMod hp (a - ↑m * p) b = toIocMod hp a b - ↑m * p
-- Mathlib.RingTheory.IsGaloisGroup.Basic
IsGaloisGroup.isScalarTower_mulSemiringActionQuotient : ∀ (G : Type u_1) [inst : Group G] (B : Type u_3) (C : Type u_4) [inst_1 : Semiring C] [inst_2 : MulSemiringAction G C]
  (N : Subgroup G) [inst_3 : CommSemiring B] [inst_4 : Algebra B C] [inst_5 : FaithfulSMul B C]
  [inst_6 : MulSemiringAction G B] [SMulDistribClass G B C] [inst_8 : IsGaloisGroup (↥N) B C] [inst_9 : N.Normal],
  IsScalarTower G (G ⧸ N) B
-- Init.Data.List.MapIdx
_private.Init.Data.List.MapIdx.0.Option.getD.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : α) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match some x with
    | some x => h_1 x
    | none => h_2 ()) =
    h_1 x
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- The first generator of an intermediate field of the form `K⟮x, y⟯`.  -/
IntermediateField.AdjoinPair.gen₁ : (K : Type u_1) → {L : Type u_2} → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → (x y : L) → ↥K⟮x, y⟯
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun_precomp_of_bijective : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι' : Type u_6} {g : ι' → ι}
  {β : ι → Type u_7} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  Function.Bijective g → (ProbabilityTheory.iIndepFun (fun i => f (g i)) μ ↔ ProbabilityTheory.iIndepFun f μ)
-- Mathlib.Data.Int.Cast.Lemmas
Int.cast_eq_zero : ∀ {α : Type u_3} [inst : AddGroupWithOne α] [CharZero α] {n : ℤ}, ↑n = 0 ↔ n = 0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.comp_add_left : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  [TopologicalSpace.PseudoMetrizableSpace ε],
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ (c : ℝ),
      autoParam (‖f (min a b)‖ₑ ≠ ⊤) IntervalIntegrable.comp_add_left._auto_1 →
        IntervalIntegrable (fun x => f (c + x)) MeasureTheory.volume (a - c) (b - c)
-- Mathlib.Analysis.LocallyConvex.Separation
RCLike.geometric_hahn_banach_open_open : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  {s t : Set E} [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E],
  Convex ℝ s →
    IsOpen s →
      Convex ℝ t → IsOpen t → Disjoint s t → ∃ f u, (∀ a ∈ s, RCLike.re (f a) < u) ∧ ∀ b ∈ t, u < RCLike.re (f b)
-- Mathlib.Algebra.Category.AlgCat.Monoidal
AlgCat.hom_whiskerRight : ∀ {R : Type u} [inst : CommRing R] {L M : AlgCat R} (f : L ⟶ M) (N : AlgCat R),
  AlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N) =
    Algebra.TensorProduct.map (AlgCat.Hom.hom f) (AlgHom.id R ↑N)
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.mem_of_one_mem : ∀ {S : Type u_2} [inst : CommRing S] {I : Ideal S}, 1 ∈ I → ∀ (x : S), x ∈ I
-- Mathlib.Algebra.Group.Basic
one_div_mul_one_div : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α), 1 / a * (1 / b) = 1 / (a * b)
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_add_closedBall : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x y : E),
  {x} + Metric.closedBall y δ = Metric.closedBall (x + y) δ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.all_eq_false_iff_exists_mem_get : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {p : (a : α) → β a → Bool}, m.WF → (m.all p = false ↔ ∃ a, ∃ (h : a ∈ m), p a (m.get a h) = false)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKeyD t.maxKey! fallback = t.maxKey!
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.instInhabitedLeCnstr : Inhabited Lean.Meta.Grind.Arith.Cutsat.LeCnstr
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.uniqueRingEquiv.eq_1 : ∀ {R : Type u_1} (M : Type u_4) [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : Subsingleton M],
  AddMonoidAlgebra.uniqueRingEquiv M =
    { toEquiv := (AddMonoidAlgebra.coeffAddEquiv.trans (Finsupp.uniqueAddEquiv 0)).toEquiv, map_mul' := ⋯,
      map_add' := ⋯ }
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_map : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {k : β → α} {l : Filter β}, f =O[Filter.map k l] g ↔ (f ∘ k) =O[l] (g ∘ k)
-- Mathlib.Data.List.Basic
List.mem_getLast?_eq_getLast : ∀ {α : Type u} {l : List α} {x : α}, x ∈ l.getLast? → ∃ (h : l ≠ []), x = l.getLast h
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.refl.eq_1 : ∀ (M : Type u_1) [inst : TopologicalSpace M] [inst_1 : Mul M],
  ContinuousMulEquiv.refl M = { toMulEquiv := MulEquiv.refl M, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- Assume that the set `s` spans over `ℤ` a discrete set. Then its `ℝ`-rank is equal to its `ℤ`-rank.
 -/
Real.finrank_eq_int_finrank_of_discrete : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E},
  DiscreteTopology ↥(Submodule.span ℤ s) → Set.finrank ℝ s = Set.finrank ℤ s
-- Init.Data.Int.Order
Int.add_le_zero_iff_le_neg' : ∀ {a b : ℤ}, a + b ≤ 0 ↔ b ≤ -a
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.mul : (α : Type u) → [Mul α] → Mul (FreeAbelianGroup α)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
instIsGaloisGroupIntRingOfIntegersOfRat : ∀ (L : Type u_1) [inst : Field L] [inst_1 : NumberField L] (G : Type u_2) [inst_2 : Group G]
  [inst_3 : MulSemiringAction G L] [IsGaloisGroup G ℚ L], IsGaloisGroup G ℤ (NumberField.RingOfIntegers L)
-- Mathlib.Topology.Order.IntermediateValue
/-- In a dense conditionally complete linear order, the set of preconnected sets is exactly
the set of the intervals `Icc`, `Ico`, `Ioc`, `Ioo`, `Ici`, `Ioi`, `Iic`, `Iio`, `(-∞, +∞)`,
or `∅`. Though one can represent `∅` as `(sInf s, sInf s)`, we include it into the list of
possible cases to improve readability.  -/
setOfPred_isPreconnected_eq_of_ordered : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α],
  {s | IsPreconnected s} =
    Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪ Set.range (Function.uncurry Set.Ioc) ∪
        Set.range (Function.uncurry Set.Ioo) ∪
      (Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪ {Set.univ, ∅})
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF_congr : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal} {Y : Ω → ℝ},
  X =ᵐ[ν.bind ⇑κ] Y →
    (ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν ↔ ProbabilityTheory.Kernel.HasSubgaussianMGF Y c κ ν)
-- Mathlib.CategoryTheory.Idempotents.Basic
CategoryTheory.Idempotents.split_iff_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X X' : C} (φ : X ≅ X') (p : X ⟶ X) (p' : X' ⟶ X'),
  CategoryTheory.CategoryStruct.comp p φ.hom = CategoryTheory.CategoryStruct.comp φ.hom p' →
    ((∃ Y i e,
        CategoryTheory.CategoryStruct.comp i e = CategoryTheory.CategoryStruct.id Y ∧
          CategoryTheory.CategoryStruct.comp e i = p) ↔
      ∃ Y' i' e',
        CategoryTheory.CategoryStruct.comp i' e' = CategoryTheory.CategoryStruct.id Y' ∧
          CategoryTheory.CategoryStruct.comp e' i' = p')
-- Mathlib.Order.Hom.Lattice
LatticeHom.instLatticeHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β], LatticeHomClass (LatticeHom α β) α β
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.ofFun_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg β] (f : α → β), UniformFun.ofFun (-f) = -UniformFun.ofFun f
-- Lean.Data.Lsp.Capabilities
/-- Whether the client supports `DiagnosticWith.isSilent = true`.
If `none` or `false`, silent diagnostics will not be served to the client.
 -/
Lean.Lsp.LeanClientCapabilities.silentDiagnosticSupport? : Lean.Lsp.LeanClientCapabilities → Option Bool
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_C : ∀ {R : Type u_1} [inst : Semiring R] (a : R), ↑(Polynomial.C a) = PowerSeries.C a
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.continuousWithinAt_stieltjesFunctionAux_Ici : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α],
  ProbabilityTheory.IsMeasurableRatCDF f →
    ∀ (a : α) (x : ℝ), ContinuousWithinAt (ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a) (Set.Ici x) x
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.right_unitality_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (n : M)
  (X : C) [inst_3 : F.Monoidal] {Z : C} (h : (F.obj n).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.ε F).app ((F.obj n).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.LaxMonoidal.μ F n (CategoryTheory.MonoidalCategoryStruct.tensorUnit M)).app X)
        (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor n).hom).app X)
          h)) =
    h
-- Std.Sat.AIG.RelabelNat
_private.Std.Sat.AIG.RelabelNat.0.Std.Sat.AIG.RelabelNat.State.ofAIGAux.go.match_1.eq_2 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1)
  (h_1 : (a : α) → Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.atom a → motive (Std.Sat.AIG.Decl.atom a))
  (h_2 : Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_3 :
    (lhs rhs : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match hdecl : Std.Sat.AIG.Decl.false with
    | Std.Sat.AIG.Decl.atom a => h_1 a hdecl
    | Std.Sat.AIG.Decl.false => h_2 hdecl
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs hdecl) =
    h_2 ⋯
-- Mathlib.Algebra.Homology.Localization
instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasBinaryBiproducts C],
  (HomotopyCategory.quotient C (ComplexShape.up ℤ)).IsLocalization
    (HomologicalComplex.homotopyEquivalences C (ComplexShape.up ℤ))
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instPartialOrder : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → PartialOrder (OpenAddSubgroup G)
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.changeOriginSeriesTerm.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p p_1 : FormalMultilinearSeries 𝕜 E F),
  p = p_1 →
    ∀ (k l : ℕ) (s s_1 : Finset (Fin (k + l))) (e_s : s = s_1) (hs : s.card = l),
      p.changeOriginSeriesTerm k l s hs = p_1.changeOriginSeriesTerm k l s_1 ⋯
-- Mathlib.Data.Ordmap.Invariants
/-- The `Sized` property asserts that all the `size` fields in nodes match the actual size of the
respective subtrees.  -/
Ordnode.Sized : {α : Type u_1} → Ordnode α → Prop
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
IsSelfAdjoint.le_algebraMap_norm_self : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : A},
  autoParam (IsSelfAdjoint a) IsSelfAdjoint.le_algebraMap_norm_self._auto_1 → a ≤ (algebraMap ℝ A) ‖a‖
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.Consumer.mk : {α : Type} → IO.Promise Bool → Option (Std.Async.Waiter (Option α)) → Std.CloseableChannel.Bounded.Consumer✝ α
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.id_apply : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] (x : A), (ContinuousAlgHom.id R A) x = x
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_iter_choose : ∀ (j k : ℕ), ((fwdDiff 1)^[k] fun x => ↑(x.choose (k + j))) = fun x => ↑(x.choose j)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)),
  ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).obj Y).hom = Y.hom.2
-- Mathlib.CategoryTheory.Triangulated.Functor
/-- Two isomorphic functors `F₁` and `F₂` induce isomorphic functors
`F₁.mapTriangle` and `F₂.mapTriangle` if the isomorphism `F₁ ≅ F₂` is compatible
with the shifts.  -/
CategoryTheory.Functor.mapTriangleIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.HasShift C ℤ] →
          [inst_3 : CategoryTheory.HasShift D ℤ] →
            {F₁ F₂ : CategoryTheory.Functor C D} →
              (e : F₁ ≅ F₂) →
                [inst_4 : F₁.CommShift ℤ] →
                  [inst_5 : F₂.CommShift ℤ] →
                    [CategoryTheory.NatTrans.CommShift e.hom ℤ] → F₁.mapTriangle ≅ F₂.mapTriangle