mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the largest key that is less than the given key,
returning `none` if no such key exists.
 -/
Std.DTreeMap.getKeyLT? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Option α
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
/-- The unit establishing the equivalence `StructuredArrow.commaMapEquivalence`.  -/
CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor C T} →
              {R : CategoryTheory.Functor D T} →
                {C' : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] →
                    {D' : Type u₅} →
                      [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] →
                        {T' : Type u₆} →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] →
                            {L' : CategoryTheory.Functor C' T'} →
                              {R' : CategoryTheory.Functor D' T'} →
                                {F₁ : CategoryTheory.Functor C C'} →
                                  {F₂ : CategoryTheory.Functor D D'} →
                                    {F : CategoryTheory.Functor T T'} →
                                      (α : F₁.comp L' ⟶ L.comp F) →
                                        (β : R.comp F ⟶ F₂.comp R') →
                                          [inst_6 : CategoryTheory.IsIso β] →
                                            (X : CategoryTheory.Comma L' R') →
                                              CategoryTheory.Functor.id
                                                  (CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)) ≅
                                                (CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X).comp
                                                  (CategoryTheory.StructuredArrow.commaMapEquivalenceInverse α β X)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateRow_add : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} [inst : Add α] (v w : m → α),
  Matrix.replicateRow ι (v + w) = Matrix.replicateRow ι v + Matrix.replicateRow ι w
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Under.instHasFiniteColimitsTopOfHasFiniteWidePushouts : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T)
  [CategoryTheory.Limits.HasPushouts T] [P.IsStableUnderComposition] [P.ContainsIdentities]
  [P.IsStableUnderCobaseChange] [P.HasOfPrecompProperty P] [CategoryTheory.Limits.HasFiniteWidePushouts T],
  CategoryTheory.Limits.HasFiniteColimits (P.Under ⊤ X)
-- Mathlib.Order.UpperLower.Relative
IsRelUpperSet.iUnion₂ : ∀ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {P : α → Prop} [inst : LE α] {f : (i : ι) → κ i → Set α},
  (∀ (i : ι) (j : κ i), IsRelUpperSet (f i j) P) → IsRelUpperSet (⋃ i, ⋃ j, f i j) P
-- Mathlib.Algebra.Ring.Parity
/-- An element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  -/
Odd : {α : Type u_2} → [Semiring α] → α → Prop
-- Std.Net.Addr
/-- Represents an interface address, including details such as the interface name,
whether it is internal, the associated address, and the network mask.
 -/
Std.Net.InterfaceAddress : Type
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sqrtTwoAddSeries.eq_def : ∀ (x : ℝ) (x_1 : ℕ),
  x.sqrtTwoAddSeries x_1 =
    match x_1 with
    | 0 => x
    | n.succ => √(2 + x.sqrtTwoAddSeries n)
-- Mathlib.Order.Monotone.Defs
StrictMonoOn.monotoneOn : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn f s → MonotoneOn f s
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.presheafIso.congr_simp : ∀ {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}
  {G : CategoryTheory.Functor C D} [inst_2 : G.IsCoverDense K] [inst_3 : G.IsLocallyFull K]
  {ℱ ℱ' : CategoryTheory.Sheaf K (Type v)} (i i_1 : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj),
  i = i_1 →
    CategoryTheory.Functor.IsCoverDense.Types.presheafIso i = CategoryTheory.Functor.IsCoverDense.Types.presheafIso i_1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_neg : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : AddGroup α]
  [inst_3 : SubtractionMonoid β] [inst_4 : FunLike F α β] [AddMonoidHomClass F α β] (f : F) (s : Finset α),
  Finset.image (⇑f) (-s) = -Finset.image (⇑f) s
-- Std.Internal.UV.System
/-- Returns the available memory for allocation in bytes.
 -/
Std.Internal.UV.System.availableMemory : IO UInt64
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
MaximalSpectrum.mapPiLocalization.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f f_1 : R →+* S) (e_f : f = f_1)
  (hf : Function.Bijective ⇑f), MaximalSpectrum.mapPiLocalization f hf = MaximalSpectrum.mapPiLocalization f_1 ⋯
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.ball_inter_range_eq_ball_inter_target : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c),
  Metric.ball (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I =
    Metric.ball (↑(extChartAt I c) c) f.rOut ∩ (extChartAt I c).target
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- If a nonzero vector `w` and a vector `u` are both orthogonal to the same nonzero vector `v`
in a two-dimensional inner product space, then `u` lies in the span of `w`.  -/
Submodule.mem_span_singleton_of_inner_eq_zero_of_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [Fact (Module.finrank 𝕜 E = 2)] {u v w : E}, v ≠ 0 → w ≠ 0 → inner 𝕜 v u = 0 → inner 𝕜 v w = 0 → u ∈ 𝕜 ∙ w
-- Mathlib.Data.Set.Semiring
SetSemiring.down_add : ∀ {α : Type u_1} (s t : SetSemiring α), SetSemiring.down (s + t) = SetSemiring.down s ∪ SetSemiring.down t
-- Init.Data.SInt.Bitwise
Int8.and_assoc : ∀ (a b c : Int8), a &&& b &&& c = a &&& (b &&& c)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α},
  (t.erase k)[a]? = if cmp k a = Ordering.eq then none else t[a]?
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extEquivCohomologyClass_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (x y : CategoryTheory.Abelian.Ext X Y n),
  R.extEquivCohomologyClass (x + y) = R.extEquivCohomologyClass x + R.extEquivCohomologyClass y
-- Lean.Meta.Tactic.FunIndCollect
_private.Lean.Meta.Tactic.FunIndCollect.0.Lean.Meta.FunInd.collect.unsafe_1 : Lean.Meta.FunIndInfo → Lean.MVarId → Lean.MetaM (Array Lean.Expr)
-- Mathlib.Topology.Algebra.ConstMulAction
isOpenMap_smul₀ : ∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [ContinuousConstSMul G₀ α] {c : G₀}, c ≠ 0 → IsOpenMap fun x => c • x
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNorm.ext_iff : ∀ {R : outParam (Type u_1)} {S : outParam (Type u_2)} [inst : SeminormedCommRing R] [inst_1 : Ring S]
  [inst_2 : Algebra R S] {p q : MulAlgebraNorm R S}, p = q ↔ ∀ (x : S), p x = q x
-- Mathlib.GroupTheory.Commutator.Basic
addCommutator_eq_closure : ∀ (G : Type u_1) [inst : AddGroup G], addCommutator G = AddSubgroup.closure (addCommutatorSet G)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
SimpleGraph.edgeDensity.eq_1 : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj], G.edgeDensity = Rel.edgeDensity G.Adj
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 0th group homology of `A`, defined as the 0th homology of the complex of inhomogeneous
chains, is isomorphic to the invariants of the representation on `A`.  -/
groupHomology.H0Iso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → groupHomology.H0 A ≅ (Rep.coinvariantsFunctor k G).obj A
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_le_maxKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {km kmi : α}, t.maxKey? = some km → (t.insert k v).maxKey?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piCongrLeft_symm_apply : ∀ {ι : Type u_7} {ι' : Type u_8} {Y : ι' → Type u_9} [inst : (j : ι') → TopologicalSpace (Y j)] (e : ι ≃ ι'),
  ⇑(Homeomorph.piCongrLeft e).symm = fun x1 x2 => x1 (e x2)
-- Lean.Data.JsonRpc
Lean.JsonRpc.RequestID.num.sizeOf_spec : ∀ (n : Lean.JsonNumber), sizeOf (Lean.JsonRpc.RequestID.num n) = 1 + sizeOf n
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- If we constructed our images from strong epi-mono factorisations, then these images are
strong epi images.  -/
CategoryTheory.Limits.hasStrongEpiImages_of_hasStrongEpiMonoFactorisations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C], CategoryTheory.Limits.HasStrongEpiImages C
-- Mathlib.Algebra.BigOperators.Expect
Fintype.expect_ite_zero : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : Module ℚ≥0 M] (p : ι → Prop)
  [inst_3 : DecidablePred p],
  (∀ (i j : ι), p i → p j → i = j) →
    ∀ (a : M), (Finset.univ.expect fun i => if p i then a else 0) = if ∃ i, p i then (↑(Fintype.card ι))⁻¹ • a else 0
-- Mathlib.GroupTheory.Coset.Basic
/-- Equality of two right cosets `s * a` and `s * b`.  -/
RightCosetEquivalence : {α : Type u_1} → [Mul α] → Set α → α → α → Prop
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_eq_zero : ∀ {a : ENNReal}, a⁻¹ = 0 ↔ a = ⊤
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
CompactCoherentification.t2space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [t : T2Space X], T2Space (CompactCoherentification X)
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallCache.mk'' : Lean.Name →
  Option Lean.Elab.DecreasingBy →
    Array Lean.Elab.WF.GuessLex.BasicMeasure →
      Array Lean.Elab.WF.GuessLex.BasicMeasure →
        Lean.Elab.WF.GuessLex.RecCallWithContext →
          IO.Ref (Array (Array (Option Lean.Elab.WF.GuessLex.GuessLexRel))) → Lean.Elab.WF.GuessLex.RecCallCache
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepSet_iff_measure_inter_eq_mul : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {s t : Set Ω},
  MeasurableSet s →
    MeasurableSet t →
      ∀ (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.indepSet_iff_measure_inter_eq_mul._auto_1)
        [MeasureTheory.IsZeroOrProbabilityMeasure μ], ProbabilityTheory.IndepSet s t μ ↔ μ (s ∩ t) = μ s * μ t
-- Mathlib.Data.Set.Sigma
Set.image_sigmaMk_preimage_sigmaMap_subset : ∀ {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {β : ι' → Type u_4} (f : ι → ι') (g : (i : ι) → α i → β (f i))
  (i : ι) (s : Set (β (f i))), Sigma.mk i '' g i ⁻¹' s ⊆ Sigma.map f g ⁻¹' Sigma.mk (f i) '' s
-- Mathlib.Algebra.Group.Defs
exists_zsmul_surjective : ∀ (G : Type u_2) [inst : SMul ℤ G] [IsAddCyclic G], ∃ g, Function.Surjective fun x => x • g
-- Lean.Meta.AppBuilder
/-- Returns `let_val_congr b h`  -/
Lean.Meta.mkLetValCongr : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.Set.Function
Set.surjOn_of_subsingleton : ∀ {α : Type u_1} [Subsingleton α] (f : α → α) (s : Set α), Set.SurjOn f s s
-- Init.PropLemmas
not_forall_of_exists_not : ∀ {α : Sort u_1} {p : α → Prop}, (∃ x, ¬p x) → ¬∀ (x : α), p x
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.essFiniteType_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : IntermediateField F E},
  Algebra.EssFiniteType F ↥K ↔ K.FG
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.realizeValue.realizeAndReport : Lean.MetaM Dynamic → Lean.Core.Context → Lean.Environment → Lean.Options → BaseIO Dynamic
-- Mathlib.GroupTheory.Nilpotent
Subgroup.comap_upperCentralSeries_quotient_center : ∀ {G : Type u_1} [inst : Group G] (n : ℕ),
  Subgroup.comap (QuotientGroup.mk' (Subgroup.center G)) (Subgroup.upperCentralSeries (G ⧸ Subgroup.center G) n) =
    Subgroup.upperCentralSeries G n.succ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- A `Functor.PullbackObjObj` structure for a functor `G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂` and
morphisms `f₁ : X₁ ⟶ Y₁` and `f₃ : X₃ ⟶ Y₃` when `Y₃` is terminal and both
`G.obj X₁` and `G.obj Y₁` preserve the terminal object.  -/
CategoryTheory.Functor.PullbackObjObj.ofIsTerminal : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) →
              {X₁ Y₁ : C₁} →
                (f₁ : X₁ ⟶ Y₁) →
                  {X₃ Y₃ : C₃} →
                    (f₃ : X₃ ⟶ Y₃) →
                      [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})
                            (G.obj (Opposite.op X₁))] →
                        [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})
                              (G.obj (Opposite.op Y₁))] →
                          CategoryTheory.Limits.IsTerminal Y₃ → G.PullbackObjObj f₁ f₃
-- Mathlib.Data.Nat.BitIndices
Nat.bitIndices_two_pow_mul : ∀ (k n : ℕ), (2 ^ k * n).bitIndices = List.map (fun x => x + k) n.bitIndices
-- Mathlib.Dynamics.BirkhoffSum.Basic
birkhoffSum_one' : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : α → α) (g : α → M), birkhoffSum f g 1 = g
-- Mathlib.CategoryTheory.Bicategory.Opposites
/-- `Bᵒᵖ` preserves the direction of all 2-morphisms in `B`  -/
Bicategory.Opposite.Hom2.unop2 : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] → {a b : Bᵒᵖ} → {f g : a ⟶ b} → Bicategory.Opposite.Hom2 f g → (f.unop ⟶ g.unop)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_eq_empty_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {σ : Equiv.Perm α}, σ.support = ∅ ↔ σ = 1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.compare_getKey_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} (h' : k ∈ t), cmp (t.getKey k h') k = Ordering.eq
-- Mathlib.RingTheory.Localization.FractionRing
/-- The cast from `Int` to `Rat` as a `FractionRing`.  -/
Rat.isFractionRing : IsFractionRing ℤ ℚ
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
/-- Approximate a measurable function by a sequence of simple functions `F n` such that
`F n x ∈ s`.  -/
MeasureTheory.SimpleFunc.approxOn : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : PseudoEMetricSpace α] →
        [OpensMeasurableSpace α] →
          [inst_3 : MeasurableSpace β] →
            (f : β → α) →
              Measurable f →
                (s : Set α) →
                  (y₀ : α) → y₀ ∈ s → [TopologicalSpace.SeparableSpace ↑s] → ℕ → MeasureTheory.SimpleFunc β α
-- Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
isMIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ} [BoundarylessManifold I M],
  ContMDiffAt I I.tangent 1 (fun x => ⟨x, v x⟩) (γ t₀) →
    IsMIntegralCurveAt γ v t₀ → IsMIntegralCurveAt γ' v t₀ → γ t₀ = γ' t₀ → γ =ᶠ[nhds t₀] γ'
-- Mathlib.GroupTheory.Congruence.Basic
/-- This version infers the surjectivity of the function from a
MulEquiv function  -/
AddCon.comapQuotientEquivOfSurj_symm_mk' : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (c : AddCon M) (f : N ≃+ M) (x : N),
  (c.comapQuotientEquivOfSurj ↑f ⋯).symm ⟦f x⟧ = ↑x
-- Mathlib.MeasureTheory.Integral.IntegrableOn
ContinuousLinearMap.integrableAtFilter_comp : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {l : Filter α} {E : Type u_7} {H : Type u_8}
  {𝕜 : Type u_9} {𝕜' : Type u_10} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜' E] [inst_4 : NormedAddCommGroup H] [inst_5 : NormedSpace 𝕜 H]
  {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] {f : α → H} (L : H →SL[σ] E),
  MeasureTheory.IntegrableAtFilter f l μ → MeasureTheory.IntegrableAtFilter (⇑L ∘ f) l μ
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.isOpen_symm_image_iff_of_subset_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {t : Set Y}, t ⊆ e.target → (IsOpen (↑e.symm '' t) ↔ IsOpen t)
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- If `X` is a non-compact space, then `∞` is not an isolated point of `OnePoint X`.  -/
OnePoint.nhdsNE_infty_neBot : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NoncompactSpace X], (nhdsWithin OnePoint.infty {OnePoint.infty}ᶜ).NeBot
-- Mathlib.Analysis.Normed.Group.Continuity
controlled_prod_of_mem_closure_range : ∀ {E : Type u_4} {F : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : SeminormedCommGroup F] {j : E →* F} {b : F},
  b ∈ closure ↑j.range →
    ∀ {f : ℕ → ℝ},
      (∀ (n : ℕ), 0 < f n) →
        ∃ a,
          Filter.Tendsto (fun n => ∏ i ∈ Finset.range (n + 1), j (a i)) Filter.atTop (nhds b) ∧
            ‖(j (a 0))⁻¹ * b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n
-- Init.Data.Ord.Basic
List.isGE_compare_nil_right : ∀ {α : Type u_1} [inst : Ord α] {xs : List α}, (compare xs []).isGE = true
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- An open set is everywhere positive for a measure which is positive on open sets.  -/
IsOpen.isEverywherePos : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}
  [μ.IsOpenPosMeasure], IsOpen s → μ.IsEverywherePos s
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.instQuiverHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] →
      {X Y : CategoryTheory.CatEnrichedOrdinary C} → Quiver (X ⟶ Y)
-- Mathlib.Analysis.Calculus.ContDiff.Basic
ftaylorSeriesWithin_fun_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F],
  (ftaylorSeriesWithin 𝕜 fun x => 0) = 0
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.sum_boole_mul : ∀ {ι : Type u_1} {R : Type u_4} [inst : NonAssocSemiring R] [inst_1 : DecidableEq ι] (s : Finset ι) (f : ι → R) (i : ι),
  ∑ j ∈ s, (if i = j then 1 else 0) * f j = if i ∈ s then f i else 0
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.toMatrix_apply`. -/
BilinForm.toMatrix_apply : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (i j : n), (LinearMap.BilinForm.toMatrix b) B i j = (B (b i)) (b j)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.toMultilinearMap_add : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  [inst_7 : ContinuousAdd M₂] (f g : ContinuousMultilinearMap R M₁ M₂),
  (f + g).toMultilinearMap = f.toMultilinearMap + g.toMultilinearMap
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₂_comp : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K)
  (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C),
  groupHomology.mapCycles₂ (g.comp f) (CategoryTheory.CategoryStruct.comp φ ((Rep.resFunctor f).map ψ)) =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₂ f φ) (groupHomology.mapCycles₂ g ψ)
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
/-- Bowen-Dinaburg's definition of topological entropy using nets is
`⨆ U ∈ 𝓤 X, netEntropyEntourage T F U`. This quantity is the same as the topological entropy using
covers, so there is no need to define a new notion of topological entropy. This version of the
theorem relates the `liminf` versions of topological entropy.  -/
Dynamics.coverEntropyInf_eq_iSup_netEntropyInfEntourage : ∀ {X : Type u_1} [inst : UniformSpace X] (T : X → X) (F : Set X),
  Dynamics.coverEntropyInf T F = ⨆ U ∈ uniformity X, Dynamics.netEntropyInfEntourage T F U
-- Lean.Syntax
/-- Full comparison of syntax structures and source infos.   -/
Lean.Syntax.eqWithInfo : Lean.Syntax → Lean.Syntax → Bool
-- Mathlib.Data.PNat.Factors
PrimeMultiset.ofNatList.eq_1 : ∀ (l : List ℕ) (h : ∀ p ∈ l, Nat.Prime p), PrimeMultiset.ofNatList l h = PrimeMultiset.ofNatMultiset (↑l) h
-- Mathlib.Algebra.Order.Nonneg.Basic
/-- Coercion `{x : α // 0 ≤ x} → α` as an `AddMonoidHom`.  -/
Nonneg.coeAddMonoidHom : {α : Type u_1} → [inst : AddMonoid α] → [inst_1 : Preorder α] → [inst_2 : AddLeftMono α] → { x // 0 ≤ x } →+ α
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- This is the free-living isomorphism as the codiscrete category on `Bool`.  -/
CategoryTheory.WalkingIso : Type w
-- Mathlib.LinearAlgebra.RootSystem.BaseExists
/-- This is really just an auxiliary result en route to `RootPairing.Base.mk'`.  -/
RootPairing.coroot_mem_or_neg_mem_closure_of_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [inst : AddCommGroup M]
  [inst_1 : AddCommGroup N] [inst_2 : Field R] [CharZero R] [inst_4 : Module R M] [inst_5 : Module R N]
  (P : RootPairing ι R M N) [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] (s : Set ι),
  LinearIndepOn R (⇑P.root) s →
    (∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)) →
      ∀ (i : ι),
        P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' s) ∨ -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' s)