mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff : ∀ {X : AlgebraicGeometry.Scheme} {I : X.IdealSheafData}
  {J : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))},
  I ≤ AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals J ↔ I.ideal ≤ J
-- Init.Data.Array.Lemmas
Array.size_uset : ∀ {α : Type u_1} {xs : Array α} {v : α} {i : USize} (h : i.toNat < xs.size), (xs.uset i v h).size = xs.size
-- Mathlib.Topology.MetricSpace.Kuratowski
/-- The Kuratowski embedding is an isometric embedding of a separable metric space in `ℓ^∞(ℕ, ℝ)`.
 -/
kuratowskiEmbedding : (α : Type u) → [inst : MetricSpace α] → [TopologicalSpace.SeparableSpace α] → α → ↥(lp (fun x => ℝ) ⊤)
-- Mathlib.Data.Fintype.Card
Fintype.card_ofFinset : ∀ {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p), Fintype.card ↑p = s.card
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.Measure.coe_finsetSum`. -/
MeasureTheory.Measure.coe_finset_sum : ∀ {α : Type u_1} {ι : Type u_5} {_m : MeasurableSpace α} (I : Finset ι) (μ : ι → MeasureTheory.Measure α),
  ⇑(∑ i ∈ I, μ i) = ∑ i ∈ I, ⇑(μ i)
-- Mathlib.Algebra.CharP.Two
CharTwo.multiset_sum_mul_self : ∀ {R : Type u_1} [inst : CommSemiring R] [CharP R 2] (l : Multiset R),
  l.sum * l.sum = (Multiset.map (fun x => x * x) l).sum
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.instConcreteCategorySubtypeNormedAddGroupHomCarrierNormNoninc : CategoryTheory.ConcreteCategory SemiNormedGrp₁ fun X Y => { f // f.NormNoninc }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.polynomialY_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R},
  W'.polynomialY =
    MvPolynomial.C 2 * MvPolynomial.X 1 * MvPolynomial.X 2 +
        MvPolynomial.C W'.a₁ * MvPolynomial.X 0 * MvPolynomial.X 2 +
      MvPolynomial.C W'.a₃ * MvPolynomial.X 2 ^ 2
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
/-- See also `RootPairing.rootForm_restrict_nondegenerate_of_ordered`.

Note that this applies to crystallographic root systems in characteristic zero via
`RootPairing.instIsAnisotropicOfIsCrystallographic`.  -/
RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [P.IsAnisotropic], LinearMap.Nondegenerate (P.RootForm.restrict (P.rootSpan R))
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.comp_of_isOpenImmersion : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.IsOpenImmersion f], P g → P (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Logic.Equiv.Prod
/-- Any `Unique` type is a left identity for type sigma up to equivalence. Compare with `uniqueProd`
which is non-dependent.  -/
Equiv.uniqueSigma : {α : Type u_10} → (β : α → Type u_9) → [inst : Unique α] → (i : α) × β i ≃ β default
-- Aesop.Tree.Data
Aesop.Rapp.setParent : Aesop.GoalRef → Aesop.Rapp → Aesop.Rapp
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
HasCompactSupport.rpow_const : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ},
  HasCompactSupport f → ∀ {r : ℝ}, r ≠ 0 → HasCompactSupport fun x => f x ^ r
-- Mathlib.Data.NNReal.Defs
NNReal.instIsOrderedRing : IsOrderedRing NNReal
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Context : Type
-- Mathlib.Analysis.Meromorphic.Basic
/-- Meromorphy of `f` at `x` (more precisely, on a punctured neighbourhood of `x`; the value at
`x` itself is irrelevant).  -/
MeromorphicAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → 𝕜 → Prop
-- Mathlib.Algebra.Group.Graph
AddMonoidHom.mgraph.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddMonoid G] [inst_1 : AddMonoid H] (f : G →+ H),
  f.mgraph = { carrier := {x | f x.1 = x.2}, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
CategoryTheory.MonoidalClosed.ihomCurryIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y z : C)
  [inst_2 : CategoryTheory.Closed x] [inst_3 : CategoryTheory.Closed y]
  [inst_4 : CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)],
  (CategoryTheory.MonoidalClosed.ihomCurryIso x y z).inv = CategoryTheory.MonoidalClosed.ihomUncurry x y z
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g)
          (CategoryTheory.Limits.pullback.fst f g))
        (CategoryTheory.Limits.pullback.snd f g)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f)
      (CategoryTheory.Limits.pullback.snd g g)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)], t.isEmpty = true → t.get! a = default
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.exists_mem_isCircuit_of_not_isColoop : ∀ {α : Type u_1} {M : Matroid α} {e : α}, e ∈ M.E → ¬M.IsColoop e → ∃ C, M.IsCircuit C ∧ e ∈ C
-- Mathlib.RingTheory.Localization.Ideal
/-- **Alias** of `IsLocalization.under_map_of_isPrime_disjoint`. -/
IsLocalization.comap_map_of_isPrime_disjoint : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {I : Ideal R},
  I.IsPrime → Disjoint ↑M ↑I → Ideal.under R (Ideal.map (algebraMap R S) I) = I
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.instIsStrictlyLEObjIntSingleFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℤ),
  ((CochainComplex.singleFunctor C n).obj A).IsStrictlyLE n
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.Locally.localSeq.congr_simp : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P P_1 : MeasureTheory.Measure Ω}
  (e_P : P = P_1) [inst : LinearOrder ι] {𝓕 𝓕_1 : MeasureTheory.Filtration ι mΩ} (e_𝓕 : 𝓕 = 𝓕_1) {X X_1 : ι → Ω → E}
  (e_X : X = X_1) {p p_1 : (ι → Ω → E) → Prop} (e_p : p = p_1) [inst_1 : OrderBot ι] [inst_2 : TopologicalSpace ι]
  [inst_3 : OrderTopology ι] [inst_4 : Zero E] (hX : ProbabilityTheory.Locally p 𝓕 X P) (a a_1 : ℕ),
  a = a_1 → ∀ (a_2 a_3 : Ω), a_2 = a_3 → hX.localSeq a a_2 = ⋯.localSeq a_1 a_3
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Outside the usual range of `qaryEntropy`, it is negative. This is due to `log p = log |p|`.  -/
Real.qaryEntropy_nonpos_of_nonpos : ∀ {q : ℕ} {p : ℝ}, p ≤ 0 → Real.qaryEntropy q p ≤ 0
-- Std.Http.Data.Body.Full
/-- Builds a request with a binary body.
Sets `Content-Type: application/octet-stream`.
Use `fromBytes` instead if you need to set a different `Content-Type` or none at all.
 -/
Std.Http.Request.Builder.bytes : Std.Http.Request.Builder → ByteArray → Std.Async.Async (Std.Http.Request Std.Http.Body.Full)
-- Mathlib.Tactic.NormNum.Ineq
/-- Identify (as `true` or `false`) expressions of the form `a < b`, where `a` and `b` are numeric
expressions whose evaluations to `NormNum.Result` have already been computed.  -/
_private.Mathlib.Tactic.NormNum.Ineq.0.Mathlib.Meta.NormNum.evalLT.core : {u : Lean.Level} →
  {α : Q(Type u)} →
    (lα : Q(LT «$α»)) →
      {a b : Q(«$α»)} →
        Mathlib.Meta.NormNum.Result a →
          Mathlib.Meta.NormNum.Result b → Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$a» < «$b»))
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.centerCongr_symm_apply_coe : ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] (e : M ≃* N)
  (s : ↥(Subsemigroup.center N)), ↑((Submonoid.centerCongr e).symm s) = e.symm ↑s
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- The sheaf condition for a `F : Presheaf C X` requires that the morphism
`F.obj U ⟶ ∏ᶜ F.obj (U i)` (where `U` is some open set which is the union of the `U i`)
is the equalizer of the two morphisms
`∏ᶜ F.obj (U i) ⟶ ∏ᶜ F.obj (U i) ⊓ (U j)`.
 -/
TopCat.Presheaf.IsSheafEqualizerProducts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasProducts C] → {X : TopCat} → TopCat.Presheaf C X → Prop
-- Std.Sync.Barrier
/-- A `Barrier` will block `n - 1` threads which call `Barrier.wait` and then wake up all threads at
once when the `n`-th thread calls `Barrier.wait`.
 -/
Std.Barrier : Type
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- Dual to `Monad.PreservesColimitOfIsSplitPair`.  -/
CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Algebra.Group.Units.Defs
Units.val_mkOfMulEqOne : ∀ {α : Type u} [inst : Monoid α] [inst_1 : IsDedekindFiniteMonoid α] {a b : α} (h : a * b = 1),
  ↑(Units.mkOfMulEqOne a b h) = a
-- Mathlib.Algebra.Group.Submonoid.DistribMulAction
Submonoid.instMulDistribMulActionSubtypeMem : {M : Type u_1} →
  {α : Type u_2} →
    [inst : Monoid M] →
      {S : Type u_3} →
        [inst_1 : SetLike S M] →
          (s : S) →
            [inst_2 : SubmonoidClass S M] → [inst_3 : Monoid α] → [MulDistribMulAction M α] → MulDistribMulAction (↥s) α
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom_app_assoc : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsDense] (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.leftKanExtensionUnit F).app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.IsDense.leftKanExtensionIso F).hom.app (F.obj X))
        h) =
    CategoryTheory.CategoryStruct.comp (F.rightUnitor.inv.app X) h
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
CategoryTheory.Limits.colimitLimitToLimitColimit_isIso : ∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [inst_2 : Small.{v, u₂} K] [inst_3 : CategoryTheory.FinCategory J] (F : CategoryTheory.Functor (J × K) (Type v))
  [CategoryTheory.IsFiltered K], CategoryTheory.IsIso (CategoryTheory.Limits.colimitLimitToLimitColimit F)
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.instInv.eq_1 : ∀ {M : Type u_2} {G : Type u_5} [inst : MulOneClass M] [inst_1 : CommGroup G],
  MonoidHom.instInv = { inv := fun f => MonoidHom.mk' (fun g => (f g)⁻¹) ⋯ }
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_one_one : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : One M], (MonoidAlgebra.coeff 1) 1 = 1
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.fg_def : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M], FirstOrder.Language.Structure.FG L M ↔ ⊤.FG
-- Lean.Meta.MkIffOfInductiveProp
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.Shape.mk.injEq : ∀ (variablesKept : List Bool) (neqs : Option ℕ) (variablesKept_1 : List Bool) (neqs_1 : Option ℕ),
  ({ variablesKept := variablesKept, neqs := neqs } = { variablesKept := variablesKept_1, neqs := neqs_1 }) =
    (variablesKept = variablesKept_1 ∧ neqs = neqs_1)
-- Mathlib.Algebra.Opposites
MulOpposite.rec'.eq_1 : ∀ {α : Type u_1} {F : αᵐᵒᵖ → Sort u_3} (h : (X : α) → F (MulOpposite.op X)) (X : αᵐᵒᵖ),
  MulOpposite.rec' h X = h (MulOpposite.unop X)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.cancelAux.eq_3 : ∀ (m₂ r₁ r₂ : Nat.Internal.Linear.Poly) (fuel_2 : ℕ),
  (m₂ = [] → False) →
    Nat.Internal.Linear.Poly.cancelAux fuel_2.succ [] m₂ r₁ r₂ = (List.reverse r₁, List.reverse r₂ ++ m₂)
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ X ω ^ n` is
integrable for all `n : ℕ`.  -/
ProbabilityTheory.integrable_pow_of_integrable_exp_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ≠ 0 →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp (-t * X ω)) μ →
        ∀ (n : ℕ), MeasureTheory.Integrable (fun ω => X ω ^ n) μ
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.instDFunLike : (ι : Type u_1) → (β : ι → Type u_2) → [inst : (i : ι) → AddCommMonoid (β i)] → DFunLike (DirectSum ι β) ι β
-- Lean.Server.CodeActions.Provider
/-- Returns `none` if we should not visit this syntax at all, and `some false` if we only
want to visit it in "extended" mode (where we include trailing characters).  -/
_private.Lean.Server.CodeActions.Provider.0.Lean.CodeAction.findTactic?.visit : Lean.Syntax.Range → Lean.Syntax → optParam (Option String.Pos.Raw) none → Option Bool
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- A family of AddHom's `f i : M i →ₙ+ N i` defines an AddHom
`AddHom.piMap f : (Π i, M i) →ₙ+ (Π i, N i)`
given by `AddHom.piMap f x i = f i x`. This is `Pi.map` for `AddHom`s.  -/
AddHom.piMap : {ι : Type u_1} →
  {M : ι → Type u_3} →
    {N : ι → Type u_4} →
      [inst : (i : ι) → Add (M i)] →
        [inst_1 : (i : ι) → Add (N i)] → ((i : ι) → M i →ₙ+ N i) → ((i : ι) → M i) →ₙ+ (i : ι) → N i
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The canonical ring homomorphism from a valuation ring to its field of fractions.  -/
ValuationSubring.subtype : {K : Type u} → [inst : Field K] → (R : ValuationSubring K) → ↥R →+* K
-- Init.Data.Iterators.Basic
Std.IterStep.mapIterator_mapIterator : ∀ {α : Type u} {β : Type w} {α' : Type u'} {α'' : Type u''} {f : α → α'} {g : α' → α''} {step : Std.IterStep α β},
  Std.IterStep.mapIterator g (Std.IterStep.mapIterator f step) = Std.IterStep.mapIterator (g ∘ f) step
-- Init.Data.List.Count
List.count.eq_1 : ∀ {α : Type u} [inst : BEq α] (a : α), List.count a = List.countP fun x => x == a
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.smul_sum : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_5} [inst_1 : AddCommMonoid S] {T : Type u_6} [inst_2 : DistribSMul T S]
  (p : SkewPolynomial R) (b : T) (f : ℕ → R → S), b • p.sum f = p.sum fun n a => b • f n a
-- Mathlib.Topology.Gluing
/-- (Implementation) the restricted transition map to be fed into `TopCat.GlueData`.  -/
TopCat.GlueData.MkCore.t' : (h : TopCat.GlueData.MkCore) →
  (i j k : h.J) →
    CategoryTheory.Limits.pullback (h.V i j).inclusion' (h.V i k).inclusion' ⟶
      CategoryTheory.Limits.pullback (h.V j k).inclusion' (h.V j i).inclusion'
-- Mathlib.NumberTheory.LucasLehmer
/-- Extension for the `positivity` tactic: `mersenne`.  -/
Mathlib.Meta.Positivity.evalMersenne : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.cons_toList : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (m : M i) (w : Monoid.CoprodI.Word M)
  (hmw : w.fstIdx ≠ some i) (h1 : m ≠ 1), (Monoid.CoprodI.Word.cons m w hmw h1).toList = ⟨i, m⟩ :: w.toList
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- A functor `G : (C, J) ⥤ (D, K)` between sites is called cocontinuous (SGA 4 III 2.1)
if for all covering sieves `R` in `D`, `R.pullback G` is a covering sieve in `C`.
 -/
CategoryTheory.Functor.IsCocontinuous : {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] →
        CategoryTheory.Functor C D →
          CategoryTheory.GrothendieckTopology C → CategoryTheory.GrothendieckTopology D → Prop
-- Init.Data.String.Lemmas.Iterate
String.Slice.Model.mem_positionsFrom_startPos : ∀ {s : String.Slice} {q : { q // q ≠ s.endPos }}, q ∈ String.Slice.Model.positionsFrom s.startPos
-- Mathlib.Analysis.Analytic.Within
/-- **Alias** of the forward direction of `analyticWithinAt_iff_exists_analyticAt'`.

---

`f` is analytic within `s` at `x` iff some local extension of `f` is analytic at `x`. In this
version, we make sure that the extension coincides with `f` on all of `insert x s`.  -/
AnalyticWithinAt.exists_analyticAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  {s : Set E} {x : E}, AnalyticWithinAt 𝕜 f s x → ∃ g, f x = g x ∧ Set.EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
-- Mathlib.Topology.Algebra.Ring.Basic
NonUnitalSubsemiring.isClosed_topologicalClosure : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalSemiring R] [inst_2 : IsSemitopologicalSemiring R]
  (s : NonUnitalSubsemiring R), IsClosed ↑s.topologicalClosure
-- Mathlib.Topology.Sheaves.Presheaf
/-- The restriction of a section along an inclusion of open sets.
For `x : F.obj (op V)`, we provide the notation `x |_ₕ i` (`h` stands for `hom`) for `i : U ⟶ V`,
and the notation `x |_ₗ U ⟪i⟫` (`l` stands for `le`) for `i : U ≤ V`.
 -/
TopCat.Presheaf.restrict : {X : TopCat} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {FC : C → C → Type u_1} →
        {CC : C → Type u_2} →
          [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory C FC] →
              {F : TopCat.Presheaf C X} →
                {V : TopologicalSpace.Opens ↑X} →
                  CategoryTheory.ToType (F.obj (Opposite.op V)) →
                    {U : TopologicalSpace.Opens ↑X} → (U ⟶ V) → CategoryTheory.ToType (F.obj (Opposite.op U))
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.truncate_approx : ∀ {F : PFunctor.{uA, uB}} (x : F.M) (n : ℕ), PFunctor.Approx.truncate (x.approx (n + 1)) = x.approx n
-- Init.Data.BitVec.Lemmas
BitVec.neg_le_intMin_of_msb_eq_true : ∀ {w : ℕ} {x : BitVec w}, x.msb = true → -x ≤ BitVec.intMin w
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The oriented angle between two vectors is not zero or `π` if and only if those two vectors
are linearly independent.  -/
Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y ≠ 0 ∧ o.oangle x y ≠ ↑Real.pi ↔ LinearIndependent ℝ ![x, y]
-- Lean.DocString.Types
Lean.Doc.instBEqBlock : {i : Type u_1} → {b : Type u_2} → [BEq i] → [BEq b] → BEq (Lean.Doc.Block i b)
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
AlgebraicGeometry.Scheme.instEtaleFiberToSpecResidueField : ∀ {Y X : AlgebraicGeometry.Scheme} (f : Y ⟶ X) [AlgebraicGeometry.Etale f] (x : ↥X),
  AlgebraicGeometry.Etale (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f x)
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.CustomEliminators.mk.injEq : ∀ (map map_1 : Lean.SMap (Bool × Array Lean.Name) Lean.Name), ({ map := map } = { map := map_1 }) = (map = map_1)
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.disjoint_def' : ∀ {M : Type u_1} [inst : AddZeroClass M] {p₁ p₂ : AddSubmonoid M},
  Disjoint p₁ p₂ ↔ ∀ {x y : M}, x ∈ p₁ → y ∈ p₂ → x = y → x = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- The backwards edge of `coherentIso`.  -/
SSet.coherentIso.inv : SSet.Edge SSet.coherentIso.x₁ SSet.coherentIso.x₀
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.ext_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {c c' : CategoryTheory.Limits.BinaryFan A B}
  (e : c.pt ≅ c'.pt) (h₁ : c.fst = CategoryTheory.CategoryStruct.comp e.hom c'.fst)
  (h₂ : c.snd = CategoryTheory.CategoryStruct.comp e.hom c'.snd),
  (CategoryTheory.Limits.BinaryFan.ext e h₁ h₂).hom.hom = e.hom
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_id : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.CategoryStruct.id Y) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.map_toSubmodule : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {S : Subalgebra R A} {f : A →ₐ[R] B},
  Subalgebra.toSubmodule (Subalgebra.map f S) = Submodule.map f.toLinearMap (Subalgebra.toSubmodule S)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.congr_fun : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f g : α → ε} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f s μ → Set.EqOn f g s → MeasurableSet s → MeasureTheory.IntegrableOn g s μ
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.smul_set_pi₀ : ∀ {M : Type u_3} {ι : Type u_4} {α : ι → Type u_5} [inst : GroupWithZero M] [inst_1 : (i : ι) → MulAction M (α i)]
  {c : M}, c ≠ 0 → ∀ (I : Set ι) (s : (i : ι) → Set (α i)), c • I.pi s = I.pi (c • s)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.mk.injEq : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (toOpenAddSubgroup : OpenAddSubgroup G)
  (isNormal' : autoParam (↑toOpenAddSubgroup).Normal OpenNormalAddSubgroup.isNormal'._autoParam)
  (toOpenAddSubgroup_1 : OpenAddSubgroup G)
  (isNormal'_1 : autoParam (↑toOpenAddSubgroup_1).Normal OpenNormalAddSubgroup.isNormal'._autoParam),
  ({ toOpenAddSubgroup := toOpenAddSubgroup, isNormal' := isNormal' } =
      { toOpenAddSubgroup := toOpenAddSubgroup_1, isNormal' := isNormal'_1 }) =
    (toOpenAddSubgroup = toOpenAddSubgroup_1)
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- Given `c : ι → R` and an index `i` such that `c i = 0`, this is the linear isomorphism sending
the `j`-th standard basis vector to itself plus `c j` multiplied with the `i`-th standard basis
vector (in particular, the `i`-th standard basis vector is kept invariant).  -/
Finsupp.addSingleEquiv : {R : Type u_4} → {ι : Type u_6} → [inst : Ring R] → (i : ι) → (c : ι → R) → c i = 0 → (ι →₀ R) ≃ₗ[R] ι →₀ R
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.TypeDefinitionParams.mk.inj : ∀ {toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams},
  { toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 } →
    toTextDocumentPositionParams = toTextDocumentPositionParams_1
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
ClosedSubmodule.orthogonal_eq_top_iff : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : ClosedSubmodule 𝕜 E), Kᗮ = ⊤ ↔ K = ⊥
-- Mathlib.Logic.Equiv.Defs
Equiv.sumIsLeft_symm_apply_coe : ∀ {α : Type u_1} {β : Type u_2} (a : α), ↑(Equiv.sumIsLeft.symm a) = Sum.inl a
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.isCaratheodory_inter : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ s₂ : Set α},
  m.IsCaratheodory s₁ → m.IsCaratheodory s₂ → m.IsCaratheodory (s₁ ∩ s₂)