mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.le_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (∀ (k' : α), t.minKey? = some k' → (cmp k k').isLE = true) ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- `single` as an `AddMonoidHom`.  -/
lp.singleAddMonoidHom : {α : Type u_3} →
  {E : α → Type u_4} →
    [inst : (i : α) → NormedAddCommGroup (E i)] → [DecidableEq α] → (p : ENNReal) → (i : α) → E i →+ ↥(lp E p)
-- Mathlib.Algebra.Order.UpperLower
UpperSet.coe_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α], ↑0 = Set.Ici 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
/-- An element in a non-unital C⋆-algebra is selfadjoint if and only if it is normal and its
quasispectrum is contained in `ℝ`.  -/
isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal]
  {a : A}, IsSelfAdjoint a ↔ IsStarNormal a ∧ QuasispectrumRestricts a ⇑Complex.reCLM
-- Mathlib.Analysis.Meromorphic.Basic
/-- `MeromorphicOn` is invariant under translation.  -/
MeromorphicOn.meromorphicOn_comp_sub_const_iff_meromorphicOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {U : Set 𝕜},
  MeromorphicOn (f ∘ fun x => x - c) U ↔ MeromorphicOn f (U - {c})
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.sdiff_adj : ∀ {V : Type u_2} (x y : Digraph V) (v w : V), (x \ y).Adj v w ↔ x.Adj v w ∧ ¬y.Adj v w
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.lintegral_condCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (x : ℝ),
  ∫⁻ (a : α), ENNReal.ofReal (↑(ProbabilityTheory.condCDF ρ a) x) ∂ρ.fst = ρ (Set.univ ×ˢ Set.Iic x)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
smul_add : ∀ {M : Type u_1} {A : Type u_7} [inst : AddZeroClass A] [inst_1 : DistribSMul M A] (a : M) (b₁ b₂ : A),
  a • (b₁ + b₂) = a • b₁ + a • b₂
-- Mathlib.Data.PNat.Basic
/-- Strong induction on `ℕ+`, with `n = 1` treated separately.  -/
PNat.caseStrongInductionOn : {p : ℕ+ → Sort u_1} → (a : ℕ+) → p 1 → ((n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)) → p a
-- Mathlib.Order.WellFounded
Function.not_lt_argmin : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) [inst : LT β] [inst_1 : WellFoundedLT β] [inst_2 : Nonempty α] (a : α),
  ¬f a < f (Function.argmin f)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.le_nfp : ∀ (f : Ordinal.{u_1} → Ordinal.{u_1}) (a : Ordinal.{u_1}), a ≤ Ordinal.nfp f a
-- Mathlib.Data.Finset.Prod
Finset.product_disjUnion : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t t' : Finset β} (ht : Disjoint t t'),
  s ×ˢ t.disjUnion t' ht = (s ×ˢ t).disjUnion (s ×ˢ t') ⋯
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_mul : ∀ {R : Type u} {M : Type v} [inst : Mul R] [inst_1 : Add M] [inst_2 : SMul R M] [inst_3 : SMul Rᵐᵒᵖ M]
  (x₁ x₂ : TrivSqZeroExt R M), (x₁ * x₂).snd = x₁.fst • x₂.snd + MulOpposite.op x₂.fst • x₁.snd
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.nontrivial_iff_exists_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 0
-- Mathlib.Topology.VectorBundle.Basic
Bundle.zeroSection_snd : ∀ {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [inst : (x : B) → Zero (E x)] (x : B),
  (Bundle.zeroSection F E x).snd = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {l : List α} {k : α},
  k ∈ t → (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).getKey! k = t.getKey! k
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (y, x / y)` sends `μ × ν` to `ν × μ`.  -/
MeasureTheory.measurePreserving_prod_div_swap : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulRightInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.2, z.1 / z.2)) (μ.prod ν) (ν.prod μ)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RoiSliceData.mk : {α : Type u} →
  [inst : Ord α] → (Std.DTreeMap.Internal.Impl α fun x => Unit) → Std.Roi α → Std.DTreeMap.Internal.Unit.RoiSliceData α
-- Mathlib.Order.OrderIsoNat
/-- `Nat.Subtype.ofNat` as an order isomorphism between `ℕ` and an infinite subset. See also
`Nat.nth` for a version where the subset may be finite.  -/
Nat.Subtype.orderIsoOfNat : (s : Set ℕ) → [Infinite ↑s] → ℕ ≃o ↑s
-- Mathlib.Analysis.Complex.Norm
Complex.norm_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ‖OfNat.ofNat n‖ = OfNat.ofNat n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSignatureHelpTriggerKind : Lean.FromJson Lean.Lsp.SignatureHelpTriggerKind
-- Mathlib.Algebra.Group.Hom.Defs
iterate_map_sub : ∀ {M : Type u_10} {F : Type u_11} [inst : AddGroup M] [inst_1 : FunLike F M M] [AddMonoidHomClass F M M] (f : F) (n : ℕ)
  (x y : M), (⇑f)^[n] (x - y) = (⇑f)^[n] x - (⇑f)^[n] y
-- Mathlib.Order.CompleteLattice.SetLike
CompleteSublattice.mem_sSup : ∀ {X : Type u_1} {L : CompleteSublattice (Set X)} {𝒮 : Set ↥L} {x : X}, x ∈ sSup 𝒮 ↔ ∃ T ∈ 𝒮, x ∈ T
-- Mathlib.Data.Multiset.Defs
Multiset.coe_attach : ∀ {α : Type u_1} (l : List α), (↑l).attach = ↑l.attach
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryEquivClass.mk : ∀ {𝓕 : Type u_11} {R : outParam (Type u_12)} {R₂ : outParam (Type u_13)} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : outParam (R →+* R₂)} {σ₂₁ : outParam (R₂ →+* R)} [inst_2 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {E : outParam (Type u_14)} {E₂ : outParam (Type u_15)}
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  [inst_8 : EquivLike 𝓕 E E₂] [toSemilinearEquivClass : SemilinearEquivClass 𝓕 σ₁₂ E E₂],
  (∀ (f : 𝓕) (x : E), ‖f x‖ = ‖x‖) → SemilinearIsometryEquivClass 𝓕 σ₁₂ E E₂
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.instSMul : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} →
              {K : TopologicalSpace.Compacts E} →
                {R : Type u_5} →
                  [inst_4 : Semiring R] →
                    [inst_5 : Module R F] →
                      [SMulCommClass ℝ R F] → [ContinuousConstSMul R F] → SMul R (ContDiffMapSupportedIn E F n K)
-- Lean.LibrarySuggestions.Basic
/-- Apply `f` to every constant occurring in `e` once, skipping instance arguments and proofs.  -/
Lean.Expr.foldRelevantConstants : {α : Type} → Lean.Expr → α → (Lean.Name → α → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_univ : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] [Nonempty R] {l u : ℝ},
  Filter.Tendsto (↑f) Filter.atBot (nhds l) →
    Filter.Tendsto (↑f) Filter.atTop (nhds u) → f.measure Set.univ = ENNReal.ofReal (u - l)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.keyword : String → Lean.ParseImports.Parser
-- Std.Http.Protocol.H1.Writer
/-- Checks if the writer has completed processing a request.
 -/
Std.Http.Protocol.H1.Writer.isComplete : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Bool
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ),
  ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).inv.app X).hom₁ =
    CategoryTheory.CategoryStruct.id X.obj₁
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.weakPullback.lift.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] (h h_1 : W ⟶ X) (e_h : h = h_1) (k k_1 : W ⟶ Y) (e_k : k = k_1)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.Limits.weakPullback.lift h k w = CategoryTheory.Limits.weakPullback.lift h_1 k_1 ⋯
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
CategoryTheory.Functor.instEffectiveEpiEffectiveEpiOver : ∀ {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] (F : CategoryTheory.Functor C D) [inst_2 : F.EffectivelyEnough]
  (X : D), CategoryTheory.EffectiveEpi (F.effectiveEpiOver X)
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_fun_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (s : Set 𝕜) (c : F), derivWithin (fun x => c) s = 0
-- Init.Coe
CoeOut.mk : {α : Sort u} → {β : semiOutParam (Sort v)} → (α → β) → CoeOut α β
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
Preorder.frestrictLe₂.congr_simp : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} [inst_1 : LocallyFiniteOrderBot α] {a b : α} (hab : a ≤ b)
  (f f_1 : (i : ↥(Finset.Iic b)) → π ↑i),
  f = f_1 → ∀ (i : ↥(Finset.Iic a)), Preorder.frestrictLe₂ hab f i = Preorder.frestrictLe₂ hab f_1 i
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- (Implementation). `sheafCoyonedaHom` but the order of the arguments of the functor are swapped.
 -/
CategoryTheory.Functor.IsCoverDense.sheafYonedaHom : {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} →
          {A : Type u_4} →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
              {G : CategoryTheory.Functor C D} →
                [G.IsCoverDense K] →
                  [G.IsLocallyFull K] →
                    {ℱ : CategoryTheory.Functor Dᵒᵖ A} →
                      {ℱ' : CategoryTheory.Sheaf K A} →
                        (G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) →
                          (ℱ.comp CategoryTheory.yoneda ⟶ ℱ'.obj.comp CategoryTheory.yoneda)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_restrict : ∀ {α : Type u_1} {E I : Set α},
  I ⊆ E → ∀ (R : Set α), (Matroid.uniqueBaseOn I E).restrict R = Matroid.uniqueBaseOn (I ∩ R) R
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_var : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} (v : α → M) (k : α),
  FirstOrder.Language.Term.realize v (FirstOrder.Language.var k) = v k
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.dropWhile : ∀ {l m r : List Char} (p : Char → Bool) {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s →
    Substring.Raw.ValidFor (l ++ List.takeWhile p m) (List.dropWhile p m) r (s.dropWhile p)
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.bind_assoc : ∀ {α : Type u} {β : Type v} {γ : Type w} (s : Stream'.Seq1 α) (f : α → Stream'.Seq1 β) (g : β → Stream'.Seq1 γ),
  (s.bind f).bind g = s.bind fun x => (f x).bind g
-- Std.Time.Date.Unit.Month
Std.Time.Month.instInhabitedOrdinal : Inhabited Std.Time.Month.Ordinal
-- Mathlib.Data.Nat.Sqrt
Nat.le_three_of_sqrt_eq_one : ∀ {n : ℕ}, n.sqrt = 1 → n ≤ 3
-- Mathlib.CategoryTheory.Sites.Plus
/-- `(P ⟶ P⁺)⁺ = P⁺ ⟶ P⁺⁺`  -/
CategoryTheory.GrothendieckTopology.plusMap_toPlus : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (P : CategoryTheory.Functor Cᵒᵖ D) [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D],
  J.plusMap (J.toPlus P) = J.toPlus (J.plusObj P)
-- Mathlib.FieldTheory.Finite.Basic
ZMod.eq_one_or_isUnit_sub_one : ∀ {n p k : ℕ} [Fact (Nat.Prime p)], n = p ^ k → ∀ (a : ZMod n), (orderOf a).Coprime n → a = 1 ∨ IsUnit (a - 1)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.TacticMVarKind.term.sizeOf_spec : sizeOf Lean.Elab.Term.TacticMVarKind.term = 1
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.ext : ∀ {α : Type u_3} {d₁ d₂ : MeasurableSpace.DynkinSystem α}, (∀ (s : Set α), d₁.Has s ↔ d₂.Has s) → d₁ = d₂
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_inv_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f] [inst_6 : CategoryTheory.Limits.HasCokernel f]
  [inst_7 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_8 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_9 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_10 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_11 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_12 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_13 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))]
  [inst_14 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))],
  (CategoryTheory.Abelian.PreservesCoimageImageComparison.iso F f).inv.left =
    (CategoryTheory.Abelian.PreservesCoimage.iso F f).inv
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.decompId_i_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Idempotents.Karoubi C),
  P.decompId_i.f = P.p
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.opcyclesMap'_neg : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.ShortComplex.opcyclesMap' (-φ) h₁ h₂ = -CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- The context for evaluating expressions.  -/
Mathlib.Tactic.Monoidal.Context : Type
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.degrees_neg : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (p : MvPolynomial σ R), (-p).degrees = p.degrees
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.mem_normalizer_iff_addConj_image_eq : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G} {g : G}, g ∈ AddSubgroup.normalizer s ↔ ⇑(AddAut.addConj g) '' s = s
-- Mathlib.Geometry.Manifold.SmoothEmbedding
_private.Mathlib.Geometry.Manifold.SmoothEmbedding.0.Manifold.Diffeomorph.isSmoothEmbedding : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E₁ : Type u_2} →
      [inst_1 : NormedAddCommGroup E₁] →
        [inst_2 : NormedSpace 𝕜 E₁] →
          {H : Type u_6} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E₁ H} →
                {M : Type u_10} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {n : WithTop ℕ∞} →
                        [IsManifold I n M] →
                          (φ : Diffeomorph I I M M n) → ProofWanted (Manifold.IsSmoothEmbedding I I n ⇑φ)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.isometry_iff_adjoint_comp_self : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] {K : Type u_6} [inst_4 : NormedAddCommGroup K] [inst_5 : InnerProductSpace 𝕜 K]
  [inst_6 : CompleteSpace K] (u : H →L[𝕜] K), Isometry ⇑u ↔ ContinuousLinearMap.adjoint u ∘SL u = 1
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (toPresheafedSpace : AlgebraicGeometry.PresheafedSpace C)
  (IsSheaf : toPresheafedSpace.presheaf.IsSheaf) (toPresheafedSpace_1 : AlgebraicGeometry.PresheafedSpace C)
  (IsSheaf_1 : toPresheafedSpace_1.presheaf.IsSheaf),
  ({ toPresheafedSpace := toPresheafedSpace, IsSheaf := IsSheaf } =
      { toPresheafedSpace := toPresheafedSpace_1, IsSheaf := IsSheaf_1 }) =
    (toPresheafedSpace = toPresheafedSpace_1)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.allM_map : ∀ {α β β' : Type w} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α Id m] [LawfulMonad m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {f : β → β'}
  {p : β' → m Bool}, Std.Iter.allM p (Std.Iter.map f it) = Std.Iter.allM (fun x => p (f x)) it
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instIsLeftCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsLeftCancelAdd α], IsLeftCancelAdd αᵒᵈ
-- Lean.DocString.Add
Lean.VersoDocResult.mk.sizeOf_spec : ∀ (toVersoDocString : Lean.VersoDocString) (deferredChecks : Array Lean.Doc.DeferredCheck),
  sizeOf { toVersoDocString := toVersoDocString, deferredChecks := deferredChecks } =
    1 + sizeOf toVersoDocString + sizeOf deferredChecks
-- Init.Data.Int.Basic
/-- Addition of integers, usually accessed via the `+` operator.

This function is overridden by the compiler with an efficient implementation. This definition is
the logical model.

Examples:
 * `(7 : Int) + (6 : Int) = 13`
 * `(6 : Int) + (-6 : Int) = 0`
 -/
Int.add : ℤ → ℤ → ℤ
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.instInhabited : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → Inhabited (J.Cover X)
-- Mathlib.Algebra.Tropical.BigOperators
Finset.trop_inf : ∀ {R : Type u_1} {S : Type u_2} [inst : LinearOrder R] [inst_1 : OrderTop R] (s : Finset S) (f : S → R),
  Tropical.trop (s.inf f) = ∑ i ∈ s, Tropical.trop (f i)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.IsBilimit.mk.sizeOf_spec : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {B : CategoryTheory.Limits.Bicone F}
  [inst_2 : SizeOf J] [inst_3 : SizeOf C] (isLimit : CategoryTheory.Limits.IsLimit B.toCone)
  (isColimit : CategoryTheory.Limits.IsColimit B.toCocone),
  sizeOf { isLimit := isLimit, isColimit := isColimit } = 1 + sizeOf isLimit + sizeOf isColimit
-- Mathlib.Data.List.Forall2
List.forall₂_reverse_iff : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : List β},
  List.Forall₂ R l₁.reverse l₂.reverse ↔ List.Forall₂ R l₁ l₂
-- Mathlib.Data.ENat.Lattice
ENat.iSup_add_iSup_of_monotone : ∀ {ι : Type u_4} [inst : Preorder ι] [IsDirectedOrder ι] {f g : ι → ℕ∞},
  Monotone f → Monotone g → iSup f + iSup g = ⨆ a, f a + g a
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.«feature(_)» : Lean.ParserDescr
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instFinite : ∀ {R : Type u_1} (a b : R) [inst : Semiring R], Module.Finite R (QuadraticAlgebra R a b)
-- Mathlib.Order.CompleteLattice.Lemmas
ULift.up_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : SupSet α] (f : ι → α), { down := ⨆ i, f i } = ⨆ i, { down := f i }
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → t.get! t.min! = t.min!
-- Mathlib.Analysis.Normed.Operator.Basic
LinearIsometry.coe_toSpanSingleton : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] {v : E} (hv : ‖v‖ = 1),
  (LinearIsometry.toSpanSingleton 𝕜 E hv).toLinearMap = LinearMap.toSpanSingleton 𝕜 E v
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.mono : ∀ {𝕜 : 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 → s ⊆ t → HasDerivWithinAt f f' s x
-- Mathlib.Geometry.Polygon.Basic
Polygon.mk.sizeOf_spec : ∀ {P : Type u_1} {n : ℕ} [inst : SizeOf P] (vertices : Fin n → P), sizeOf { vertices := vertices } = 1
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- If the derivative of a function defined on the real line is integrable close to `+∞`, then
the function has a limit at `+∞`.  -/
MeasureTheory.tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi : ∀ {E : Type u_1} {f f' : ℝ → E} {a : ℝ} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E],
  (∀ x ∈ Set.Ioi a, HasDerivAt f (f' x) x) →
    MeasureTheory.IntegrableOn f' (Set.Ioi a) MeasureTheory.volume →
      Filter.Tendsto f Filter.atTop (nhds (Filter.atTop.limUnder f))
-- Init.Data.List.Perm
List.Perm.pairwise_iff : ∀ {α : Type u_1} {R : α → α → Prop},
  (∀ {x y : α}, R x y → R y x) → ∀ {l₁ l₂ : List α}, l₁.Perm l₂ → (List.Pairwise R l₁ ↔ List.Pairwise R l₂)
-- Mathlib.Data.Finsupp.ToDFinsupp
/-- `Finsupp.split` is an equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`.  -/
sigmaFinsuppEquivDFinsupp : {ι : Type u_1} → {η : ι → Type u_4} → {N : Type u_5} → [inst : Zero N] → ((i : ι) × η i →₀ N) ≃ Π₀ (i : ι), η i →₀ N
-- Init.Data.Option.Lemmas
Option.get_of_eq_some : ∀ {α : Type u_1} {a : α} {o : Option α} (h : o.isSome = true), o = some a → o.get h = a
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioo.pos : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] (x : ↑(Set.Ioo 0 1)), 0 < ↑x
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.algHom_commutes : ∀ {A : Type u_4} [inst : CommRing A] {B : Type u_6} [inst_1 : CommRing B] [inst_2 : Algebra A B] {K₁ : Type u_8}
  {K₂ : Type u_9} [inst_3 : Field K₁] [inst_4 : Field K₂] [inst_5 : Algebra A K₁] [inst_6 : Algebra A K₂]
  [IsFractionRing A K₁] {L₁ : Type u_10} {L₂ : Type u_11} [inst_8 : Field L₁] [inst_9 : Field L₂]
  [inst_10 : Algebra B L₁] [inst_11 : Algebra B L₂] [inst_12 : Algebra K₁ L₁] [inst_13 : Algebra K₂ L₂]
  [inst_14 : Algebra A L₁] [inst_15 : Algebra A L₂] [IsScalarTower A K₁ L₁] [IsScalarTower A K₂ L₂]
  [IsScalarTower A B L₁] [IsScalarTower A B L₂] (e : K₁ →ₐ[A] K₂) (f : L₁ →ₐ[B] L₂) (x : K₁),
  (algebraMap K₂ L₂) (e x) = f ((algebraMap K₁ L₁) x)
-- Mathlib.Algebra.Order.Module.Defs
OrderIso.smulRight_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : MulAction α β] [inst_4 : PosSMulMono α β] [inst_5 : PosSMulReflectLE α β] {a : α} (ha : 0 < a) (b : β),
  (RelIso.symm (OrderIso.smulRight ha)) b = a⁻¹ • b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal.0.Polynomial.Chebyshev.negOnePow_mul_negOnePow_mul_cancel : ∀ {α β : ℝ} {i : ℕ}, (-1) ^ i * α * ((-1) ^ i * β) = α * β
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.mkNoImplicitLambdaAnnotation : Lean.Expr → Lean.Expr
-- Mathlib.Probability.ProductMeasure
MeasureTheory.piContent_eq_measure_pi : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [inst : Fintype ι] {s : Set ((i : ι) → X i)},
  MeasurableSet s → (MeasureTheory.piContent μ) s = (MeasureTheory.Measure.pi μ) s