mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.FibrantObject.instIsFibrantObjFibrantObjects : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.FibrantObject C),
  HomotopicalAlgebra.IsFibrant X.obj
-- Mathlib.Combinatorics.SimpleGraph.Hasse
/-- The subgraph of a path is isomorphic to the path graph with the same number of vertices  -/
SimpleGraph.Walk.IsPath.pathGraphIsoToSubgraph : {V : Type u_3} →
  [DecidableEq V] →
    {G : SimpleGraph V} →
      {u v : V} → {w : G.Walk u v} → w.IsPath → SimpleGraph.pathGraph (w.length + 1) ≃g w.toSubgraph.coe
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.hadamard_smul : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_4} (A B : Matrix m n α) [inst : Mul α] [inst_1 : SMul R α]
  [SMulCommClass R α α] (k : R), A.hadamard (k • B) = k • A.hadamard B
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.mk.inj : ∀ {Γ : Type u_8} {R : Type u_9} {inst : PartialOrder Γ} {inst_1 : AddCommMonoid R} {α : Type u_7}
  {toFun : α → HahnSeries Γ R} {isPWO_iUnion_support' : (⋃ a, (toFun a).support).IsPWO}
  {finite_co_support' : ∀ (g : Γ), {a | (toFun a).coeff g ≠ 0}.Finite} {toFun_1 : α → HahnSeries Γ R}
  {isPWO_iUnion_support'_1 : (⋃ a, (toFun_1 a).support).IsPWO}
  {finite_co_support'_1 : ∀ (g : Γ), {a | (toFun_1 a).coeff g ≠ 0}.Finite},
  { toFun := toFun, isPWO_iUnion_support' := isPWO_iUnion_support', finite_co_support' := finite_co_support' } =
      { toFun := toFun_1, isPWO_iUnion_support' := isPWO_iUnion_support'_1,
        finite_co_support' := finite_co_support'_1 } →
    toFun = toFun_1
-- Std.Time.DateTime
/-- Creates a new `DateTime` by adjusting the `nano` component.
 -/
Std.Time.DateTime.withNanoseconds : Std.Time.DateTime → Std.Time.Nanosecond.Ordinal → Std.Time.DateTime
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.instModuleCarrierObjRestrictScalars : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] → {f : R →+* S} → {M : ModuleCat S} → Module S ↑((ModuleCat.restrictScalars f).obj M)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.Hom.σ.inj : ∀ {n : ℕ} {i i_1 : Fin (n + 1)}, FreeSimplexQuiver.Hom.σ i = FreeSimplexQuiver.Hom.σ i_1 → i = i_1
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Determine whether the explicit parts of two expressions are equal,
and the implicit parts are definitionally equal.  -/
Mathlib.Tactic.LibraryRewrite.isExplicitEq : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instInterOfTransCmp : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Inter (Std.ExtTreeMap α β cmp)
-- Mathlib.Analysis.Normed.Group.AddTorsor
/-- Isometry between the tangent space `V` of a (semi)normed add torsor `P` and `P` given by
subtraction from `x : P`.  -/
IsometryEquiv.constVSub : {V : Type u_2} →
  {P : Type u_3} →
    [inst : SeminormedAddCommGroup V] → [inst_1 : PseudoMetricSpace P] → [NormedAddTorsor V P] → P → P ≃ᵢ V
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_biUnion_eq_iSup : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ι → Set α} {t : Set ι},
  t.Countable → DirectedOn (Function.onFun (fun x1 x2 => x1 ⊆ x2) s) t → μ (⋃ i ∈ t, s i) = ⨆ i ∈ t, μ (s i)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddActionOfAddActionHomClass : {R : Type u_1} →
  {ι : Type u_2} →
    [inst : Preorder ι] →
      {G : ι → Type u_3} →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : AddMonoid R] →
                    [inst_5 : (i : ι) → AddAction R (G i)] →
                      [∀ (i j : ι) (h : i ≤ j), AddActionHomClass (T h) R (G i) (G j)] → AddAction R (DirectLimit G f)
-- Mathlib.Data.List.Cycle
Cycle.next_reverse_eq_prev' : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : s.reverse.Nodup) (x : α) (hx : x ∈ s.reverse),
  s.reverse.next hs x hx = s.prev ⋯ x ⋯
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : Inhabited α] [inst_1 : EquivBEq α]
  [inst_2 : LawfulHashable α] {k a : α}, (m.insert k).get! a = if (k == a) = true ∧ k ∉ m then k else m.get! a
-- Mathlib.Order.Ideal
Order.Ideal.iSup_mem_iff : ∀ {P : Type u_1} [inst : CompleteLattice P] {I : Order.Ideal P} {α : Sort u_2} [Finite α] {f : α → P},
  ⨆ i, f i ∈ I ↔ ∀ (i : α), f i ∈ I
-- Mathlib.Data.NNReal.Defs
NNReal.forall : ∀ {p : NNReal → Prop}, (∀ (x : NNReal), p x) ↔ ∀ (x : ℝ) (hx : 0 ≤ x), p (NNReal.mk x hx)
-- Std.Data.TreeMap.Raw.Basic
/-- Creates a new empty tree map. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree map. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeMap.Raw.empty : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Given a natural transformation `α : F ⟶ G`, we give a morphism from the cone point
of any cone over `F` to the cone point of a limit cone over `G`.  -/
CategoryTheory.Limits.IsLimit.map : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cone F) →
            {t : CategoryTheory.Limits.Cone G} → CategoryTheory.Limits.IsLimit t → (F ⟶ G) → (s.pt ⟶ t.pt)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
measurableSingleton_of_standardBorel : ∀ {α : Type u_1} [inst : MeasurableSpace α] [StandardBorelSpace α], MeasurableSingletonClass α
-- Mathlib.Tactic.CancelDenoms.Core
/-- `cancelDenominatorsInType h` assumes that `h` is of the form `lhs R rhs`,
where `R ∈ {<, ≤, =, ≠, ≥, >}`.
It produces an Expression `h'` of the form `lhs' R rhs'` and a proof that `h = h'`.
Numeric denominators have been canceled in `lhs'` and `rhs'`.
 -/
Mathlib.Tactic.CancelDenoms.cancelDenominatorsInType : Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
CategoryTheory.LocalizerMorphism.hasRightResolutions_arrow_of_functorial_resolutions : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  {ρ : CategoryTheory.Functor C₂ C₁} (i : CategoryTheory.Functor.id C₂ ⟶ ρ.comp Φ.functor),
  (∀ (X₂ : C₂), W₂ (i.app X₂)) → Φ.arrow.HasRightResolutions
-- Lean.Compiler.IR.Basic
Lean.IR.VarId.mk.inj : ∀ {idx idx_1 : Lean.IR.Index}, { idx := idx } = { idx := idx_1 } → idx = idx_1
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.tprodCoeff_eq_smul_tprod : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (z : R) (f : (i : ι) → s i),
  PiTensorProduct.tprodCoeff R z f = z • (PiTensorProduct.tprod R) f
-- Mathlib.Algebra.CharP.Invertible
CharP.isUnit_natCast_iff : ∀ {R : Type u_1} [inst : Ring R] {p : ℕ} [CharP R p] {n : ℕ}, Nat.Prime p → (IsUnit ↑n ↔ ¬p ∣ n)
-- Mathlib.Data.Matrix.Mul
Matrix.submatrix_id_mul_right : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Fintype n] [inst_1 : Fintype o]
  [inst_2 : Mul α] [inst_3 : AddCommMonoid α] {p : Type u_10} (M : Matrix m n α) (N : Matrix o p α) (e₁ : l → p)
  (e₂ : o ≃ n), M.submatrix id ⇑e₂ * N.submatrix id e₁ = M * N.submatrix (⇑e₂.symm) e₁
-- Init.Data.Array.Lemmas
Array.exists_push_of_size_eq_add_one : ∀ {α : Type u_1} {n : ℕ} {xs : Array α}, xs.size = n + 1 → ∃ ys a, xs = ys.push a
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.monic_mapAlg_iff : ∀ {R : Type u} {S : Type v} [inst : Field R] [inst_1 : Semiring S] [Nontrivial S] [inst_3 : Algebra R S]
  {p : Polynomial R}, ((Polynomial.mapAlg R S) p).Monic ↔ p.Monic
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
/-- **Alias** of `SSet.chainComplexFunctor`.

---

The chain complex associated to a simplicial set, with coefficients in `R : C`.
It computes the simplicial homology of a simplicial sets with coefficients
in `R`. One can recover the ordinary simplicial chain complex when `C := Ab`
and `X := ℤ`.
 -/
AlgebraicTopology.SSet.singularChainComplexFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        CategoryTheory.Functor C (CategoryTheory.Functor SSet (ChainComplex C ℕ))
-- Mathlib.Order.Heyting.Basic
GeneralizedCoheytingAlgebra.mk : {α : Type u_4} →
  [toLattice : Lattice α] →
    [toOrderBot : OrderBot α] →
      [toSDiff : SDiff α] → (∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c) → GeneralizedCoheytingAlgebra α
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
/-- Given a morphism of sheaves `f : F ⟶ G`, `H.map f n` is the induced additive map on cohomology
groups `H F n →+ H G n`  -/
CategoryTheory.Sheaf.H.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
        [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] →
          {F G : CategoryTheory.Sheaf J AddCommGrpCat} → (F ⟶ G) → (n : ℕ) → F.H n →+ G.H n
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.centerToMulOpposite.eq_1 : ∀ {M : Type u_2} [inst : MulOneClass M], Submonoid.centerToMulOpposite = Subsemigroup.centerToMulOpposite
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.adjoint_eq_toCLM_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F),
  LinearMap.adjoint A = ↑(ContinuousLinearMap.adjoint (LinearMap.toContinuousLinearMap A))
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.expandReportDbgIssueMacro : Lean.Syntax → Lean.MacroM Lean.DoElem
-- Init.Data.Int.ToString
_private.Init.Data.Int.ToString.0.Int.repr.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (m : ℕ) (h_1 : (m : ℕ) → motive (Int.ofNat m)) (h_2 : (m : ℕ) → motive (Int.negSucc m)),
  (match Int.negSucc m with
    | Int.ofNat m => h_1 m
    | Int.negSucc m => h_2 m) =
    h_2 m
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Functor.isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D), (∀ (X : C), CategoryTheory.Limits.IsZero (F.obj X)) → CategoryTheory.Limits.IsZero F
-- Mathlib.Algebra.Ring.Torsion
IsDomain.instIsAddTorsionFreeOfCharZero : ∀ (R : Type u_1) [inst : Semiring R] [IsDomain R] [CharZero R], IsAddTorsionFree R
-- Mathlib.Topology.Order.OrderClosed
isClosed_Iic : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α] {a : α}, IsClosed (Set.Iic a)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.mk.injEq : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (toFun : M → N)
  (map_fun' :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (toFun ∘ x))
      FirstOrder.Language.Hom.map_fun'._autoParam)
  (map_rel' :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (toFun ∘ x))
      FirstOrder.Language.Hom.map_rel'._autoParam)
  (toFun_1 : M → N)
  (map_fun'_1 :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toFun_1 (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (toFun_1 ∘ x))
      FirstOrder.Language.Hom.map_fun'._autoParam)
  (map_rel'_1 :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (toFun_1 ∘ x))
      FirstOrder.Language.Hom.map_rel'._autoParam),
  ({ toFun := toFun, map_fun' := map_fun', map_rel' := map_rel' } =
      { toFun := toFun_1, map_fun' := map_fun'_1, map_rel' := map_rel'_1 }) =
    (toFun = toFun_1)
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instIsFibrantResolutionObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C),
  HomotopicalAlgebra.IsFibrant (HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj X)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.apply_skipWhile_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {pos : s.Pos} {h : pos.skipWhile P ≠ s.endPos},
  ¬P ((pos.skipWhile P).get h)
-- Mathlib.Analysis.Complex.Schwarz
/-- The **Schwarz Lemma**. Let `f : E → F` be a complex analytic function
on an open ball with center `c` and a positive radius.
If `f` sends this ball to a closed ball with center `f c` and the same radius,
then the norm of the Fréchet derivative of `f` at `c` is at most one.
 -/
Complex.norm_fderiv_le_one_of_mapsTo_ball : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {R : ℝ} {f : E → F} {c : E},
  DifferentiableOn ℂ f (Metric.ball c R) →
    Set.MapsTo f (Metric.ball c R) (Metric.closedBall (f c) R) → 0 < R → ‖fderiv ℂ f c‖ ≤ 1
-- Mathlib.Data.Set.Image
Set.range_quot_lift : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {r : ι → ι → Prop} (hf : ∀ (x y : ι), r x y → f x = f y),
  Set.range (Quot.lift f hf) = Set.range f
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.DLinearMap_apply : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : S),
  (KaehlerDifferential.DLinearMap R S) s = (KaehlerDifferential.ideal R S).toCotangent ⟨1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, ⋯⟩
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Formula.inf_iff_not_sup_not : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ ψ : L.Formula α), T.Iff (φ ⊓ ψ) (φ.not ⊔ ψ.not).not
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.cos_eq_neg_one_iff : ∀ {x : ℂ}, Complex.cos x = -1 ↔ ∃ k, ↑Real.pi + ↑k * (2 * ↑Real.pi) = x
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.stronglyMeasurable_gaussianPDF : ∀ (μ : ℝ) (v : NNReal), MeasureTheory.StronglyMeasurable (ProbabilityTheory.gaussianPDF μ v)
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.sub_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
  (f f' : P ⟶ Q) (g : Q ⟶ R) {Z : C} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f - f') (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp f g - CategoryTheory.CategoryStruct.comp f' g) h
-- Mathlib.Data.Set.Lattice.Image
Set.image_iInter_subset : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} (s : ι → Set α) (f : α → β), f '' ⋂ i, s i ⊆ ⋂ i, f '' s i
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.instZeroTermRing : (α : Type u_2) → Zero (FirstOrder.Language.ring.Term α)
-- Mathlib.Algebra.Homology.DerivedCategory.Fractions
/-- Any morphism `f : Q.obj X ⟶ Q.obj Y` in the derived category can be written
as `f = inv (Q.map s) ≫ Q.map g` with `s : X' ⟶ X` a quasi-isomorphism and `g : X' ⟶ Y`.  -/
DerivedCategory.right_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {X Y : CochainComplex C ℤ} (f : DerivedCategory.Q.obj X ⟶ DerivedCategory.Q.obj Y),
  ∃ X' s,
    ∃ (x : CategoryTheory.IsIso (DerivedCategory.Q.map s)),
      ∃ g,
        f = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (DerivedCategory.Q.map s)) (DerivedCategory.Q.map g)
-- Mathlib.Lean.Meta.CongrTheorems
/-- The subsingleton instance.  -/
Lean.Meta.FastSubsingleton.inst : ∀ {α : Sort u} [self : Lean.Meta.FastSubsingleton α], Subsingleton α
-- Std.Data.TreeSet.Basic
Std.TreeSet.empty_eq_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.TreeSet.empty = ∅
-- Mathlib.Analysis.Calculus.TangentCone.Basic
UniqueDiffWithinAt.accPt : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] {s : Set E} {x : E} [T2Space E] [Nontrivial E],
  UniqueDiffWithinAt 𝕜 s x → AccPt x (Filter.principal s)
-- Init.Data.List.Find
List.lookup_isSome_iff : ∀ {α : Type u_2} [inst : BEq α] {β : Type u_1} {l : List (α × β)} {k : α},
  (List.lookup k l).isSome = true ↔ ∃ p ∈ l, (k == p.1) = true
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_mul_apply_left : ∀ {R : Type u_1} {G : Type u_3} [inst : Semiring R] [inst_1 : AddGroup G] (x y : AddMonoidAlgebra R G) (g : G),
  (x * y).coeff g = x.coeff.sum fun h r => r * y.coeff (-h + g)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant : ∀ {G : Type u_3} {inst : AddGroup G} {inst_1 : TopologicalSpace G} {inst_2 : MeasurableSpace G}
  {μ : MeasureTheory.Measure G} [self : μ.IsAddHaarMeasure], μ.IsAddLeftInvariant
-- Init.Data.List.Monadic
List.forIn'.loop.congr_simp : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : List α)
  (f f_1 : (a : α) → a ∈ as → β → m (ForInStep β)),
  f = f_1 →
    ∀ (as' as'_1 : List α) (e_as' : as' = as'_1) (b b_1 : β),
      b = b_1 → ∀ (a : ∃ bs, bs ++ as' = as), List.forIn'.loop as f as' b a = List.forIn'.loop as f_1 as'_1 b_1 ⋯
-- Mathlib.CategoryTheory.Opposites
/-- Compatibility of `Functor.leftOp` with respect to functor composition.  -/
CategoryTheory.Functor.leftOpComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} E] →
            (F : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor D Eᵒᵖ) → (F.comp G).leftOp ≅ F.op.comp G.leftOp
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.State.mk.inj : ∀ {cache cache_1 : Lean.PersistentExprMap Mathlib.Tactic.BicategoryLike.Mor₁},
  { cache := cache } = { cache := cache_1 } → cache = cache_1
-- Mathlib.Order.CompleteBooleanAlgebra
iSup_iInf_eq : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : CompletelyDistribLattice α] {f : (a : ι) → κ a → α},
  ⨆ a, ⨅ b, f a b = ⨅ g, ⨆ a, f a (g a)
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Finsupp.coe_basisSingleOne : ∀ {R : Type u_1} {ι : Type u_3} [inst : Semiring R], ⇑Finsupp.basisSingleOne = fun i => fun₀ | i => 1
-- Mathlib.Order.RelIso.Basic
RelIso.coe_fn_toEquiv : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s), ⇑f.toEquiv = ⇑f
-- Mathlib.Order.Category.Preord
Preord.instCategory : CategoryTheory.Category.{u, u + 1} Preord
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
CFC.conjSqrt_ringInverse_self : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : SeparatelyContinuousMul A] [IsSemitopologicalRing A] [T2Space A] (c : A),
  autoParam (IsStrictlyPositive c) CFC.conjSqrt_ringInverse_self._auto_1 → (CFC.conjSqrt (Ring.inverse c)) c = 1
-- Lean.Data.Position
_private.Lean.Data.Position.0.Lean.FileMap.toPosition.toColumn : String.Pos.Raw → String → String.Pos.Raw → ℕ → ℕ
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.IsSatisfiable.eq_1 : ∀ {L : FirstOrder.Language} (T : L.Theory), T.IsSatisfiable = Nonempty T.ModelType
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.center_toNonUnitalSubsemiring : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A],
  (NonUnitalSubalgebra.center R A).toNonUnitalSubsemiring = NonUnitalSubsemiring.center A
-- Mathlib.Algebra.Group.AddChar
AddChar.instInhabited : {A : Type u_1} → {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : Monoid M] → Inhabited (AddChar A M)
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.comap_unop_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : M), Filter.comap AddOpposite.unop (nhds x) = nhds (AddOpposite.op x)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.card_support_swap_mul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x : α},
  f x ≠ x → (Equiv.swap x (f x) * f).support.card < f.support.card
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.discreteEquiv_apply : ∀ {α : Type u₁} (self : CategoryTheory.Discrete α), CategoryTheory.discreteEquiv self = self.as
-- Mathlib.Order.GaloisConnection.Basic
/-- **Alias** of `GaloisCoinsertion.u_iSup_of_l_u_eq_self`. -/
GaloisCoinsertion.u_iSup_of_lu_eq_self : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisCoinsertion l u) {ι : Sort x} (f : ι → α), (∀ (i : ι), l (u (f i)) = f i) → u (⨆ i, f i) = ⨆ i, u (f i)
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.eval_C_X_comp_eval₂_map_C_X : ∀ {R : Type u_1} [inst : CommSemiring R],
  (Polynomial.evalRingHom (Polynomial.C Polynomial.X)).comp
      (Polynomial.eval₂RingHom (Polynomial.mapRingHom (algebraMap R (Polynomial (Polynomial R))))
        (Polynomial.C Polynomial.X)) =
    RingHom.id (Polynomial (Polynomial R))
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E} (h : IsIntegral F α),
  (IntermediateField.adjoinRootEquivAdjoin F h).symm (IntermediateField.AdjoinSimple.gen F α) =
    AdjoinRoot.root (minpoly F α)
-- Mathlib.Order.WithBot
WithBot.not_coe_le_bot : ∀ {α : Type u_1} [inst : LE α] (a : α), ¬↑a ≤ ⊥
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.size_toArray_eq_count : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β}, it.toArray.size = it.length
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.iUnion_inv_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s : Set β}, ⋃ g, g⁻¹ • s = ⋃ g, g • s
-- Init.Prelude
instInhabitedSort : Inhabited (Sort u)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Braided.instSubsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : CategoryTheory.BraidedCategory C]
  [inst_5 : CategoryTheory.BraidedCategory D], Subsingleton F.Braided
-- Init.Data.Nat.Lemmas
Nat.instLawfulIdentityMaxOfNat : Std.LawfulIdentity max 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCallHierarchyOutgoingCall : Lean.ToJson Lean.Lsp.CallHierarchyOutgoingCall