mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- If a function is integrable on a set `s`, and vanishes on `t \ s`, then it is integrable on `t`
if `t` is measurable.  -/
MeasureTheory.IntegrableOn.of_forall_sdiff_eq_zero : ∀ {α : Type u_1} {mα : MeasurableSpace α} {s t : Set α} {μ : MeasureTheory.Measure α} {ε' : Type u_7}
  [inst : TopologicalSpace ε'] [inst_1 : ENormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε'] {f : α → ε'},
  MeasureTheory.IntegrableOn f s μ → MeasurableSet t → (∀ x ∈ t \ s, f x = 0) → MeasureTheory.IntegrableOn f t μ
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable.0.EisensteinSeries.aux_tsum_identity_1 : ∀ (z : UpperHalfPlane) (d : ℕ+),
  ∑' (m : ℤ), (1 / (↑m * ↑z - ↑↑d) - 1 / (↑m * ↑z + ↑↑d)) =
    -(2 / ↑↑d) +
      ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑d) + 1 / (-↑↑m * ↑z + -↑↑d) - 1 / (↑↑m * ↑z + ↑↑d) - 1 / (-↑↑m * ↑z + ↑↑d))
-- Init.Data.Dyadic.Basic
Dyadic.toRat_neg : ∀ (x : Dyadic), (-x).toRat = -x.toRat
-- Mathlib.Algebra.Group.Action.Units
/-- Note that this lemma exists more generally as the global `smul_inv`  -/
Units.smul_inv : ∀ {G : Type u_1} {M : Type u_3} [inst : Group G] [inst_1 : Monoid M] [inst_2 : MulAction G M]
  [inst_3 : SMulCommClass G M M] [inst_4 : IsScalarTower G M M] (g : G) (m : Mˣ), (g • m)⁻¹ = g⁻¹ • m⁻¹
-- Mathlib.Order.Completion
/-- See `DedekindCut.ext'` for a version using the right set instead.  -/
DedekindCut.ext : ∀ {α : Type u_1} [inst : Preorder α] {A B : DedekindCut α}, A.left = B.left → A = B
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_two_pow_sub_one_eq_mod : ∀ (x n : ℕ), x &&& 2 ^ n - 1 = x % 2 ^ n
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of `le_of_le_of_antisymmRel`. -/
LE.le.trans_antisymmRel : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α], a ≤ b → AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → a ≤ c
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_restrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) {U : X.Opens} (hU : Dense ↑U) (hU' : U ≤ f.domain) {x : ↥X}
  (hx : x ∈ U), (f.restrict U hU hU').fromSpecStalkOfMem hx = f.fromSpecStalkOfMem ⋯
-- Mathlib.Data.Complex.BigOperators
Complex.re_comp_balance : ∀ {ι : Type u_2} [inst : Fintype ι] (f : ι → ℂ), Complex.re ∘ Fintype.balance f = Fintype.balance (Complex.re ∘ f)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- The functions satisfying `isLocallyFraction` form a subring of all dependent functions
`Π x : U, HomogeneousLocalization 𝒜 x`.  -/
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.sectionsSubring : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          {𝒜 : ℕ → σ} →
            [inst_3 : GradedRing 𝒜] →
              (U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ) →
                Subring ((x : ↥(Opposite.unop U)) → HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.inj_of_prod_X_sub_C : ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {ι : Type u_1} {f : ι → R} {s : Finset ι},
  (∏ i ∈ s, (Polynomial.X - Polynomial.C (f i))).Separable → ∀ {x y : ι}, x ∈ s → y ∈ s → f x = f y → x = y
-- Mathlib.Analysis.ConstantSpeed
hasConstantSpeedOnWith_iff_variationOnFromTo_eq : ∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l : NNReal},
  HasConstantSpeedOnWith f s l ↔
    LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.exists_cellFrontier_one_eq : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : Topology.CWComplex C]
  (e : Topology.RelCWComplex.cell C 1),
  ∃ x y,
    Topology.RelCWComplex.cellFrontier 1 e = Topology.RelCWComplex.closedCell 0 x ∪ Topology.RelCWComplex.closedCell 0 y
-- Mathlib.RingTheory.Perfection
/-- The valuation `Perfection(O/(p)) → ℝ≥0` as a function.
Given `f ∈ Perfection(O/(p))`, if `f = 0` then output `0`;
otherwise output `preVal(f(n))^(p^n)` for any `n` such that `f(n) ≠ 0`.  -/
PreTilt.valAux : (K : Type u₁) →
  [inst : Field K] →
    Valuation K NNReal →
      (O : Type u₂) →
        [inst_1 : CommRing O] →
          [Algebra O K] → (p : ℕ) → [Fact (Nat.Prime p)] → [Fact ¬IsUnit ↑p] → PreTilt O p → NNReal
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.eq_of_forall_toMeasure_apply_eq : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ ν : MeasureTheory.FiniteMeasure Ω),
  (∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s) → μ = ν
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Functor.rotate_essImageDistTriang : ∀ {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] (L : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_6 : CategoryTheory.Pretriangulated C] [inst_7 : CategoryTheory.HasShift D ℤ] [inst_8 : L.CommShift ℤ]
  [inst_9 : CategoryTheory.Preadditive D] [L.Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
  (T : CategoryTheory.Pretriangulated.Triangle D), T ∈ L.essImageDistTriang ↔ T.rotate ∈ L.essImageDistTriang
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.option : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {v : ι → V} {x : V},
  LinearIndependent K v → x ∉ Submodule.span K (Set.range v) → LinearIndependent K fun o => o.casesOn' x v
-- Mathlib.Algebra.Group.Defs
/-- Despite the asymmetry of `inv_eq_of_mul`, the symmetric version is true thanks to the
involutivity of inversion.  -/
DivisionMonoid.inv_eq_of_mul : ∀ {G : Type u} [self : DivisionMonoid G] (a b : G), a * b = 1 → a⁻¹ = b
-- Mathlib.Data.Complex.Basic
Complex.instNatCast : NatCast ℂ
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.coe_copy : ∀ {M : Type u_1} [inst : Mul M] {S : Subsemigroup M} {s : Set M} (hs : s = ↑S), ↑(S.copy s hs) = s
-- Mathlib.Data.Multiset.ZeroCons
Multiset.nodup_cons : ∀ {α : Type u_1} {a : α} {s : Multiset α}, (a ::ₘ s).Nodup ↔ a ∉ s ∧ s.Nodup
-- Mathlib.Algebra.Module.Presentation.Differentials
/-- The canonical map `(σ →₀ S) →ₗ[S] pres.toExtension.Cotangent`.  -/
Algebra.Presentation.differentials.hom₁ : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] → (pres : Algebra.Presentation R S ι σ) → (σ →₀ S) →ₗ[S] pres.toExtension.Cotangent
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- Given a right inverse for a local homeomorphism `f : M → M'`, endow `M'` with a `ChartedSpace`
structure by pushing forward the `ChartedSpace` structure from `M`.  -/
IsLocalHomeomorph.chartedSpaceOfRightInverse : {H : Type u} →
  {M : Type u_2} →
    {M' : Type u_3} →
      [inst : TopologicalSpace M] →
        [inst_1 : TopologicalSpace M'] →
          [inst_2 : TopologicalSpace H] →
            [ChartedSpace H M] →
              {f : M → M'} → IsLocalHomeomorph f → {g : M' → M} → Function.RightInverse g f → ChartedSpace H M'
-- Mathlib.Algebra.Order.Sub.Defs
/-- **Alias** of the reverse direction of `tsub_nonpos`. -/
tsub_nonpos_of_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommMonoid α] [inst_2 : Sub α] [OrderedSub α] {a b : α},
  a ≤ b → a - b ≤ 0
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.adj_iff_of_neighborSet_equiv : ∀ {V : Type u} {G : SimpleGraph V} {v : V} {H : G.Subgraph} (h : ↑(G.neighborSet v) ≃ ↑(H.neighborSet v)),
  (G.neighborSet v).Finite → ∀ {w : V}, H.Adj v w ↔ G.Adj v w
-- Batteries.Lean.EStateM
EStateM.run'_bind : ∀ {ε σ α β : Type u_1} (x : EStateM ε σ α) (f : α → EStateM ε σ β) (s : σ),
  (x >>= f).run' s =
    match x.run s with
    | EStateM.Result.ok a s => (f a).run' s
    | EStateM.Result.error a a_1 => none
-- Mathlib.Logic.Equiv.Defs
/-- Transfer `LT` across an `Equiv`.  -/
Equiv.lt : {α : Type u_1} → {β : Type u_2} → α ≃ β → [LT β] → LT α
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.elim : Array Lean.Expr → Lean.Expr → Lean.MetavarContext.MkBinding.M Lean.Expr
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.cofibration_op_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C],
  HomotopicalAlgebra.Cofibration f.op ↔ HomotopicalAlgebra.Fibration f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α},
  t.contains a = false → t.getKeyD a fallback = fallback
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] {Y : AlgebraicGeometry.Scheme}
  (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y)
  (h :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij) (g j) = g i)
  (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (𝒰.f i) (𝒰.glueMorphismsOfLocallyDirected g ⋯) = g i
-- Mathlib.Order.Filter.Pi
Filter.pi_eq_bot : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)}, Filter.pi f = ⊥ ↔ ∃ i, f i = ⊥
-- Init.Data.BitVec.Lemmas
BitVec.sub_def : ∀ {n : ℕ} (x y : BitVec n), x - y = BitVec.ofNat n (2 ^ n - y.toNat + x.toNat)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_eq_bot : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} [NoZeroDivisors R], I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥
-- Std.Data.ExtDTreeMap.Basic
/-- Returns the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.ExtDTreeMap.keyAtIdx! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtDTreeMap α β cmp → ℕ → α
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.unitOfList_cons : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {hd : α} {tl : List α},
  Std.ExtTreeMap.unitOfList (hd :: tl) cmp = (∅.insertIfNew hd ()).insertManyIfNewUnit tl
-- Std.Data.DHashMap.Basic
Std.DHashMap.instSingletonSigma : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Singleton ((a : α) × β a) (Std.DHashMap α β)
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.getElem_sdiv.match_1.eq_1 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match false, false with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_1 ()
-- Mathlib.Analysis.Convex.Side
AffineSubspace.isPreconnected_setOfPred_sSameSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P),
  IsPreconnected {y | s.SSameSide x y}
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.instNontrivial : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial M],
  Nontrivial (Module.End R M)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.CodeBlock.toMessageData : Lean.Elab.Term.Do.CodeBlock → Lean.MessageData
-- Init.Data.Float.Float
/-- Computes the arc tangent (inverse tangent) of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`atan`.
 -/
Float.atan : Float → Float
-- Init.Data.SInt.Bitwise
Int8.ofBitVec_xor : ∀ (a b : BitVec 8), Int8.ofBitVec (a ^^^ b) = Int8.ofBitVec a ^^^ Int8.ofBitVec b
-- Mathlib.Algebra.MvPolynomial.NoZeroDivisors
MvPolynomial.dvd_monomial_iff_exists : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommRing R] [NoZeroDivisors R] {p : MvPolynomial σ R} {n : σ →₀ ℕ} {a : R},
  a ≠ 0 → (p ∣ (MvPolynomial.monomial n) a ↔ ∃ m b, m ≤ n ∧ b ∣ a ∧ p = (MvPolynomial.monomial m) b)
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.forall_mem_sup : ∀ {N : Type u_4} [inst : CommMonoid N] {P : N → Prop} {s t : Submonoid N},
  (∀ x ∈ s ⊔ t, P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)
-- Mathlib.Algebra.Group.Invertible.Basic
invOf_units : ∀ {α : Type u} [inst : Monoid α] (u : αˣ) [inst_1 : Invertible ↑u], ⅟↑u = ↑u⁻¹
-- Mathlib.GroupTheory.OrderOfElement
isOfFinOrder_of_finite : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] [Finite G] (x : G), IsOfFinOrder x
-- Mathlib.Order.SuccPred.Limit
SuccOrder.limitRecOn_succ : ∀ {α : Type u_1} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : WellFoundedLT α]
  (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
  (isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a) [inst_3 : NoMaxOrder α]
  (b : α),
  SuccOrder.limitRecOn (Order.succ b) isMin succ isSuccLimit = succ b ⋯ (SuccOrder.limitRecOn b isMin succ isSuccLimit)
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsAddKleinFour.isAddCommutative : ∀ {G : Type u_1} [inst : AddGroup G] [IsAddKleinFour G], IsAddCommutative G
-- Mathlib.Logic.Nonempty
nonempty_sigma : ∀ {α : Type u_1} {γ : α → Type u_3}, Nonempty ((a : α) × γ a) ↔ ∃ a, Nonempty (γ a)
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_eq_one : ∀ {a : ENNReal}, a⁻¹ = 1 ↔ a = 1
-- Mathlib.Tactic.FunProp.Core
/-- Synthesize arguments `xs` either with typeclass synthesis, with `fun_prop` or with
discharger.  -/
Mathlib.Meta.FunProp.synthesizeArgs : Mathlib.Meta.FunProp.Origin →
  Array Lean.Expr →
    (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
      Mathlib.Meta.FunProp.FunPropM Bool
-- Mathlib.Algebra.Module.Torsion.Basic
_private.Mathlib.Algebra.Module.Torsion.Basic.0.Submodule.sup_torsionBySet_ideal_eq_torsionBySet_inf.match_1_1.splitter : (motive : Fin 2 → Sort u_1) → (x : Fin 2) → (Unit → motive 0) → (Unit → motive 1) → motive x
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.IsDetpBalanced.submatrix_equiv : ∀ {n : Type u_1} {m : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommSemiring R] {A : Matrix n n R} {a b : R} (e₁ e₂ : m ≃ n),
  A.IsDetpBalanced a b → (A.submatrix ⇑e₁ ⇑e₂).IsDetpBalanced a b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_get? : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  {h : (m.get? a).isSome = true}, (m.get? a).get h = m.get a ⋯
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.leftOp}
  (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeLeftOp c))
  (s : CategoryTheory.Limits.Cone F.leftOp),
  (CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp F hc).lift s =
    (hc.desc (CategoryTheory.Limits.coconeOfConeLeftOp s)).unop
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.inftyValuation_of_nonzero`. -/
FunctionField.inftyValuation_of_nonzero : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] {x : RatFunc F},
  x ≠ 0 → RatFunc.inftyValuationDef F x = WithZero.exp x.intDegree
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.id_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.Idempotents.Karoubi C},
  (CategoryTheory.CategoryStruct.id P).f = P.p
-- Mathlib.Topology.Algebra.Ring.Basic
Subsemiring.topologicalClosure_mono : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] [inst_2 : IsSemitopologicalSemiring R]
  {s t : Subsemiring R}, s ≤ t → s.topologicalClosure ≤ t.topologicalClosure
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.adjoint_apply_of_not_dense : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F}
  [inst_5 : CompleteSpace E], ¬Dense ↑T.domain → ∀ (y : ↥T.adjoint.domain), ↑T.adjoint y = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'] {Z_1 : C}
  (h : CategoryTheory.Limits.pushout (CategoryTheory.Limits.pushout.inr f g) g' ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f (CategoryTheory.CategoryStruct.comp g g'))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushout.inr f g) g') h
-- Mathlib.Data.EReal.Basic
EReal.image_coe_Ioc : ∀ (x y : ℝ), Real.toEReal '' Set.Ioc x y = Set.Ioc ↑x ↑y
-- Lean.Widget.UserWidget
Lean.Widget.GetWidgetSourceParams : Type
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- When two left extensions `α₁ : LeftExtension L F₁` and `α₂ : LeftExtension L F₂`
are essentially the same via an isomorphism of functors `F₁ ≅ F₂`,
then `α₁` is universal iff `α₂` is.  -/
CategoryTheory.Functor.LeftExtension.isUniversalEquivOfIso₂ : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            {L : CategoryTheory.Functor C D} →
              {F₁ F₂ : CategoryTheory.Functor C H} →
                (α₁ : L.LeftExtension F₁) →
                  (α₂ : L.LeftExtension F₂) →
                    (e : F₁ ≅ F₂) →
                      (e' : CategoryTheory.StructuredArrow.right α₁ ≅ CategoryTheory.StructuredArrow.right α₂) →
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.hom α₁)
                              (L.whiskerLeft e'.hom) =
                            CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.StructuredArrow.hom α₂) →
                          CategoryTheory.StructuredArrow.IsUniversal α₁ ≃ CategoryTheory.StructuredArrow.IsUniversal α₂
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.sum_Ico_add_eq_sum_Icc : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a ≤ b → ∑ x ∈ Finset.Ico a b, f x + f b = ∑ x ∈ Finset.Icc a b, f x
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)),
  (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).functor =
    CategoryTheory.CategoryOfElements.toCostructuredArrow F
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.isBigOWith : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =o[l] g → Asymptotics.IsBigOWith 1 l f g
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `dist (f n) (f (n+1))` is bounded by `C * r^n`, `r < 1`, then the distance from
`f 0` to the limit of `f` is bounded above by `C / (1 - r)`.  -/
dist_le_of_le_geometric_of_tendsto : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] (r C : ℝ) {f : ℕ → α},
  r < 1 →
    (∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) →
      ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), dist (f n) a ≤ C * r ^ n / (1 - r)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k a : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.get? a = if compare k a = Ordering.eq then none else t.get? a
-- Mathlib.Data.W.Constructions
WType.rightInverse_list : ∀ (γ : Type u), Function.RightInverse (WType.ofList γ) (WType.toList γ)
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.ZMod.χ₈.match_1.eq_3 : ∀ (motive : ZMod 8 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 2) (h_3 : Unit → motive 4)
  (h_4 : Unit → motive 6) (h_5 : Unit → motive 1) (h_6 : Unit → motive 7) (h_7 : Unit → motive 3)
  (h_8 : Unit → motive 5),
  (match 4 with
    | 0 => h_1 ()
    | 2 => h_2 ()
    | 4 => h_3 ()
    | 6 => h_4 ()
    | 1 => h_5 ()
    | 7 => h_6 ()
    | 3 => h_7 ()
    | 5 => h_8 ()) =
    h_3 ()
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.eq_append_of_dropSuffix?_bool_eq_some : ∀ {p : Char → Bool} {s res : String.Slice},
  s.dropSuffix? p = some res → ∃ c, s.copy = res.copy ++ String.singleton c ∧ p c = true
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.instIsCancelAddSubtypeLeOfNat : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] [IsCancelAdd α],
  IsCancelAdd { x // 0 ≤ x }
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
/-- An open partial homeomorphism whose source is all of `X` defines an open embedding of `X` into
`Y`. The converse is also true; see `IsOpenEmbedding.toOpenPartialHomeomorph`.  -/
OpenPartialHomeomorph.isOpenEmbedding : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), e.source = Set.univ → Topology.IsOpenEmbedding ↑e
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instAddGroupQuotient : {R : Type u_1} → [inst : AddGroup R] → [inst_1 : Mul R] → (c : RingCon R) → AddGroup c.Quotient
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getD.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (t t_1 : Std.DTreeMap.Internal.Impl α β),
  t = t_1 → ∀ (k : α) (fallback fallback_1 : β k), fallback = fallback_1 → t.getD k fallback = t_1.getD k fallback_1
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.instUnique : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [Subsingleton R] → Unique (AddMonoidAlgebra R M)
-- Mathlib.Order.Types.Defs
OrderType.zero_le : ∀ (o : OrderType.{u_1}), 0 ≤ o
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.span_empty : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieSubalgebra.lieSpan R L ∅ = ⊥
-- Mathlib.Analysis.Calculus.DSlope
DifferentiableAt.of_dslope : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜}, DifferentiableAt 𝕜 (dslope f a) b → DifferentiableAt 𝕜 f b
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- Given sieve `S` and presheaf `P : Cᵒᵖ ⥤ A`, their natural associated cone is a limit cone
iff `Hom (E, P -)` is a sheaf of types for the sieve `S` and all `E : A`.  -/
CategoryTheory.Presheaf.isLimit_iff_isSheafFor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.Sieve X),
  Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSheafFor (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.AddMagmaCat.Hom.mk : {A B : AddMagmaCat} → (↑A →ₙ+ ↑B) → A.Hom B