mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Bool
Bool.decide_true_eq : ∀ {b : Bool} [inst : Decidable (true = b)], decide (true = b) = b
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
ModuleCat.restrictScalars_η : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (r : R),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.ε (ModuleCat.restrictScalars f))) r = f r
-- Lean.Meta.LitValues
/-- Returns `some n` if `e` is a raw natural number, i.e., it is of the form `.lit (.natVal n)`.  -/
Lean.Meta.getRawNatValue? : Lean.Expr → Option ℕ
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.locallyFinite_tsupport : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s),
  LocallyFinite fun i => tsupport ⇑(f i)
-- Mathlib.Analysis.Calculus.TangentCone.Defs
UniqueDiffWithinAt.mem_closure : ∀ {R : Type u} {E : Type v} [inst : Semiring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : TopologicalSpace E] {s : Set E} {x : E}, UniqueDiffWithinAt R s x → x ∈ closure s
-- Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
homeomorphSphereProd_apply_fst_coe : ∀ (E : Type u_2) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (r : ℝ) (hr : 0 < r) (x : ↑{0}ᶜ),
  ↑((homeomorphSphereProd E r hr) x).1 = r • ‖↑x‖⁻¹ • ↑x
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientMapSubgroupOfOfLe_mk : ∀ {G : Type u} [inst : Group G] {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal]
  [_hBN : (B'.subgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) (x : ↥A),
  (QuotientGroup.quotientMapSubgroupOfOfLe h' h) ↑x = ↑((Subgroup.inclusion h) x)
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- The homotopy category functor `hoFunctor : SSet.{u} ⥤ Cat.{u, u}` is (cartesian) monoidal.  -/
SSet.Truncated.hoFunctor.monoidal : SSet.hoFunctor.Monoidal
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_eq_bot_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E},
  IntermediateField.adjoin F S = ⊥ ↔ S ⊆ ↑⊥
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.MemLp.of_bilin : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.Measure α} {p q r : ENNReal}
  {f : α → E} {g : α → F} (b : E → F → G) (c : NNReal),
  MeasureTheory.MemLp f p μ →
    MeasureTheory.MemLp g q μ →
      MeasureTheory.AEStronglyMeasurable (fun x => b (f x) (g x)) μ →
        (∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊) →
          ∀ [hpqr : p.HolderTriple q r], MeasureTheory.MemLp (fun x => b (f x) (g x)) r μ
-- Init.Sym.DSimp.DSimprocDSL
/-- Projection reduction.  -/
Lean.Parser.Sym.DSimp.proj : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.restrictIndex_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) {ι : Type w'}
  (f : ι → E.I₀) (a : ι), (E.restrictIndex f).X a = (E.X ∘ f) a
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.GeometricallyConnected.iff_geometricallyConnected_fiber : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S),
  AlgebraicGeometry.GeometricallyConnected f ↔
    ∀ (s : ↥S), AlgebraicGeometry.GeometricallyConnected (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f s)
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.surjOn_iff_bijOn_of_mapsTo : ∀ {α : Type u} {s : Set α} {f : α → α}, s.Finite → Set.MapsTo f s s → (Set.SurjOn f s s ↔ Set.BijOn f s s)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDeriv_smul_const_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {A : Type u_4} [inst_5 : NormedRing A] [inst_6 : NormedAlgebra 𝕜 A] [inst_7 : Module A F]
  [inst_8 : IsScalarTower 𝕜 A F] [inst_9 : IsBoundedSMul A F] {i : ℕ} {v : F} {f : E → A},
  ContDiffAt 𝕜 (↑i) f x →
    iteratedFDeriv 𝕜 i (fun y => f y • v) x =
      ((ContinuousLinearMap.id 𝕜 A).smulRight v).compContinuousMultilinearMap (iteratedFDeriv 𝕜 i f x)
-- Mathlib.Topology.Sequences
/-- Subtype of a Fréchet-Urysohn space is a Fréchet-Urysohn space.  -/
Subtype.instFrechetUrysohnSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [FrechetUrysohnSpace X] {p : X → Prop}, FrechetUrysohnSpace (Subtype p)
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.Hom.ext : ∀ {X Y : FinBddDistLat} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Mathlib.GroupTheory.Subgroup.Simple
Subgroup.Normal.eq_bot_or_eq_top : ∀ {G : Type u_1} [inst : Group G] [IsSimpleGroup G] {H : Subgroup G}, H.Normal → H = ⊥ ∨ H = ⊤
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.filter_key_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → Bool},
  m.WF → ((Std.DHashMap.Raw.filter (fun k x => f k) m).Equiv m ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) = true)
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.codisjoint_iff : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α} {a b : ↥L}, Codisjoint a b ↔ Codisjoint ↑a ↑b
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.le_of_opNorm_le : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] {f : E [⋀^ι]→L[𝕜] F} {C : ℝ},
  ‖f‖ ≤ C → ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i, ‖m i‖
-- Batteries.Logic
Eq.congr_right : ∀ {α : Sort u_1} {x y z : α}, x = y → (z = x ↔ z = y)
-- Std.Async.System
/-- Gets the current user's home directory.
 -/
Std.Async.System.getHomeDir : IO System.FilePath
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.lift_mk : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {α : Type u_2} (f : M → α)
  (h : ∀ (a b : M), MulArchimedeanClass.mk a = MulArchimedeanClass.mk b → f a = f b) (a : M),
  MulArchimedeanClass.lift f h (MulArchimedeanClass.mk a) = f a
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context.setMemoize : Lean.Meta.Simp.Context → Bool → Lean.Meta.Simp.Context
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalGroup.exists_mulInvClosureNhd : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [CompactSpace G] {W : Set G},
  IsClopen W → ∃ T, IsTopologicalGroup.mulInvClosureNhd T W
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.instAdd : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Add (AdicCompletion.AdicCauchySequence I M)
-- Init.Data.String.OrderInstances
String.Pos.Raw.instTransLe : Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Init.GrindInstances.ToInt
Lean.Grind.instZeroFinCoOfNatIntCast : ∀ {n : ℕ} [inst : NeZero n], Lean.Grind.ToInt.Zero (Fin n) (Lean.Grind.IntInterval.co 0 ↑n)
-- Mathlib.GroupTheory.Congruence.Basic
/-- Given an `AddMonoid` homomorphism `f`, the induced homomorphism
on the quotient by `f`'s kernel has the same image as `f`.  -/
AddCon.kerLift_range_eq : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {f : M →+ P},
  AddMonoidHom.mrange (AddCon.kerLift f) = AddMonoidHom.mrange f
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Stream.foldr.match_1.splitter : {α : Type u_1} →
  {σ : Sort u_3} →
    (motive : RBTree.RBNode.Stream α → σ → Sort u_2) →
      (x : RBTree.RBNode.Stream α) →
        (x_1 : σ) →
          ((b : σ) → motive RBTree.RBNode.Stream.nil b) →
            ((v : α) →
                (r : RBTree.RBNode α) →
                  (tail : RBTree.RBNode.Stream α) → (b : σ) → motive (RBTree.RBNode.Stream.cons v r tail) b) →
              motive x x_1
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_inv_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}
  [ZeroLEOneClass G₀], 1 < a⁻¹ ↔ 0 < a ∧ a < 1
-- Mathlib.Algebra.Category.CommHopfAlgCat
commHopfAlgCatEquivCogrpCommAlgCat_unitIso_hom_app : ∀ (R : Type u) [inst : CommRing R] (X : CommHopfAlgCat R),
  (commHopfAlgCatEquivCogrpCommAlgCat R).unitIso.hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Combinatorics.Hindman
Hindman.FS.cons' : ∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M) (m : M), Hindman.FS a.tail m → Hindman.FS a (a.head + m)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.or.sizeOf_spec : ∀ (a a_1 : Mathlib.Tactic.ITauto.IProp), sizeOf (a.or a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Geometry.Manifold.Instances.Sphere
instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) ⊤ Circle
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.varFinset.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : DecidableEq α] (l : ℕ) (_f : L.Functions l) (ts : Fin l → L.Term α),
  (FirstOrder.Language.func _f ts).varFinset = Finset.univ.biUnion fun i => (ts i).varFinset
-- Mathlib.RingTheory.KrullDimension.Polynomial
/-- Let `p` be a prime ideal of `R`. If `P` is a maximal ideal of `R[X]` lying over `p`,
`ht(P) = ht(p) + 1`.  -/
Polynomial.height_eq_height_add_one : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (P : Ideal (Polynomial R)) [P.IsMaximal]
  [P.LiesOver p], P.height = p.height + 1
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linear_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), e.symm.linear = e.linear.symm
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Uncurrying in a monoidal closed category.  -/
CategoryTheory.MonoidalClosed.uncurry : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {A X Y : C} →
        [inst_2 : CategoryTheory.Closed A] → (Y ⟶ A ⟹ X) → (CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ X)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_inter_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ ∩ m₂)[k]? = m₁[k]?
-- Mathlib.Analysis.Convex.Join
subset_convexJoin_right : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s t : Set E} [IsOrderedRing 𝕜], s.Nonempty → t ⊆ convexJoin 𝕜 s t
-- Mathlib.Algebra.Opposites
AddOpposite.unop_op : ∀ {α : Type u_1} (x : α), AddOpposite.unop (AddOpposite.op x) = x
-- Mathlib.Algebra.Group.Action.Basic
isUnit_smul_iff : ∀ {α : Type u_5} {β : Type u_6} [inst : Group α] [inst_1 : Monoid β] [inst_2 : MulAction α β] [SMulCommClass α β β]
  [IsScalarTower α β β] (g : α) (m : β), IsUnit (g • m) ↔ IsUnit m
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- If `f` and `g` are absolutely continuous on `uIcc a b`, then `f • g` is absolutely continuous
on `uIcc a b`.  -/
AbsolutelyContinuousOnInterval.smul : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {M : Type u_3} [inst_1 : SeminormedRing M]
  [inst_2 : Module M F] [NormSMulClass M F] {f : ℝ → M} {g : ℝ → F},
  AbsolutelyContinuousOnInterval f a b →
    AbsolutelyContinuousOnInterval g a b → AbsolutelyContinuousOnInterval (f • g) a b
-- Mathlib.Topology.Order.IntermediateValue
/-- A continuous function which tends to `Filter.atBot` along `Filter.atTop` and to `Filter.atTop`
along `Filter.atBot` is surjective.  -/
Continuous.surjective' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {f : α → δ},
  Continuous f →
    Filter.Tendsto f Filter.atBot Filter.atTop → Filter.Tendsto f Filter.atTop Filter.atBot → Function.Surjective f
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.edges_dropLast : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.dropLast.edges = p.edges.dropLast
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.reverse_eq_iff : ∀ {α : Type u_1} {t t' : RBTree.RBNode α}, t.reverse = t' ↔ t = t'.reverse
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.lift_comp_mk : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] {M : Type u_3}
  [inst_3 : Monoid M] {f : GL n R →* M} (hf : f.comp (Matrix.GeneralLinearGroup.scalar n) = 1),
  (Matrix.ProjGenLinGroup.lift f hf).comp Matrix.ProjGenLinGroup.mk = f
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.Spanning.isBase_of_le_cRank : ∀ {α : Type u} {M : Matroid α} {X : Set α} [M.RankFinite], M.Spanning X → Cardinal.mk ↑X ≤ M.cRank → M.IsBase X
-- Mathlib.Data.Finite.Defs
Finite.ofBijective : ∀ {α : Sort u_1} {β : Sort u_2} [Finite α] {f : α → β}, Function.Bijective f → Finite β
-- Mathlib.Tactic.Widget.StringDiagram
/-- Given an 2-morphism or equality between 2-morphisms, return a string diagram.
Otherwise `none`.  -/
Mathlib.Tactic.Widget.StringDiagram.stringMorOrEqM? : Lean.Expr → Lean.MetaM (Option ProofWidgets.Html)
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.augmentedCechNerve_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom],
  f.augmentedCechNerve.right = f.right
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.IsMultiplicative.prodPrimeFactors : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] (f : ℕ → R), (ArithmeticFunction.prodPrimeFactors f).IsMultiplicative
-- Mathlib.Topology.Algebra.InfiniteSum.Group
multipliable_inv_iff : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : CommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalGroup α] {f : β → α}, Multipliable (fun b => (f b)⁻¹) L ↔ Multipliable f L
-- Mathlib.Data.Fin.VecNotation
Matrix.vecAlt1.congr_simp : ∀ {α : Type u} {m n : ℕ} (hm : m = n + n) (v v_1 : Fin m → α),
  v = v_1 → ∀ (k k_1 : Fin n), k = k_1 → Matrix.vecAlt1 hm v k = Matrix.vecAlt1 hm v_1 k_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isEmpty_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k : α}
  {f : β → β}, (Std.DTreeMap.Const.modify t k f).isEmpty = t.isEmpty
-- Mathlib.Topology.Irreducible
PreirreducibleSpace.mk : ∀ {X : Type u_3} [inst : TopologicalSpace X], IsPreirreducible Set.univ → PreirreducibleSpace X
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.multiples_eq_closure : ∀ {M : Type u_1} [inst : AddMonoid M] (n : M), AddSubmonoid.multiples n = AddSubmonoid.closure {n}
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.horn.IsCompatible.lift.congr_simp : ∀ {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f f_1 : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)}
  (e_f : f = f_1) (hf : SSet.horn.IsCompatible f) {Y : SSet} (p p_1 : X ⟶ Y) (e_p : p = p_1)
  [inst : HomotopicalAlgebra.Fibration p] (b b_1 : SSet.stdSimplex.obj { len := n + 1 } ⟶ Y) (e_b : b = b_1)
  (comm :
    ∀ (j : Fin (n + 2)) (hj : j ≠ i),
      CategoryTheory.CategoryStruct.comp (f j hj) p = CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) b),
  hf.lift p b comm = ⋯.lift p_1 b_1 ⋯
-- Mathlib.Topology.MetricSpace.Cover
/-- A compact set admits a finite cover.  -/
Metric.exists_finite_isCover_of_isCompact : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} {s : Set X},
  ε ≠ 0 → IsCompact s → ∃ N ⊆ s, N.Finite ∧ Metric.IsCover ε s N
-- Mathlib.Topology.LocallyFinsupp.Pushforward
Function.locallyFinsupp.map_apply : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (w : X → R) [inst_2 : Semiring R] [inst_3 : PrespectralSpace Y] (hf : IsSpectralMap f)
  (c : Function.locallyFinsupp X R) (y : Y),
  (Function.locallyFinsupp.map f w hf c) y = ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {y}), c x * w x
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.localInverse_eventuallyEq_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x), f ∘ ↑hf.localInverse.toPartialEquiv =ᶠ[nhds (f x)] id
-- Mathlib.LinearAlgebra.Complex.Module
/-- Register as an instance (with low priority) the fact that a complex algebra is also a real
algebra.  -/
Algebra.complexToReal : {A : Type u_1} → [inst : Semiring A] → [Algebra ℂ A] → Algebra ℝ A
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₂.multispanShape_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C] (x : CategoryTheory.OrthogonalReflection.D₂ W Z),
  (CategoryTheory.OrthogonalReflection.D₂.multispanShape W Z).snd x = ()
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.instIsLocalizedEquivalenceFibrantObjectWeakEquivalencesιFibrantObjectLocalizerMorphism : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.BifibrantObject.ιFibrantObjectLocalizerMorphism C).IsLocalizedEquivalence
-- Init.Data.String.Lemmas.Iterate
String.Model.map_get_positionsFrom_startPos : ∀ {s : String}, List.map (fun p => (↑p).get ⋯) (String.Model.positionsFrom s.startPos) = s.toList
-- Mathlib.Order.Interval.Basic
Interval.instNontrivialOfNonempty : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], Nontrivial (Interval α)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  {M N : ↑(F.obj { as := Opposite.op S })},
  F.presheafHomObjHomEquiv =
    ((CategoryTheory.Cat.Hom.toNatIso (F.mapId { as := Opposite.op S })).symm.app M).homCongr
      ((CategoryTheory.Cat.Hom.toNatIso (F.mapId { as := Opposite.op S })).symm.app N)
-- Mathlib.Algebra.DirectSum.Finsupp
/-- The finitely supported functions `ι →₀ M` are in linear equivalence with the direct sum of
copies of M indexed by ι.  -/
finsuppLEquivDirectSum : (R : Type u) →
  (M : Type v) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → (ι : Type u_1) → [DecidableEq ι] → (ι →₀ M) ≃ₗ[R] DirectSum ι fun x => M
-- Mathlib.Data.Multiset.Interval
Multiset.card_Ioo : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α),
  (Finset.Ioo s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, (Multiset.count i t + 1 - Multiset.count i s) - 2
-- Mathlib.LinearAlgebra.Projection
LinearMap.range_eq_of_proj : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p : Submodule R E}
  {f : E →ₗ[R] ↥p}, (∀ (x : ↥p), f ↑x = x) → f.range = ⊤
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_ofInt : ∀ (n : ℤ), ISize.ofBitVec (BitVec.ofInt System.Platform.numBits n) = ISize.ofInt n
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySum.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (B : ℝ),
  NumberField.mixedEmbedding.convexBodySum K B = {x | NumberField.mixedEmbedding.convexBodySumFun x ≤ B}
-- Mathlib.Topology.Bornology.Basic
Bornology.IsCobounded.all : ∀ {α : Type u_2} [inst : Bornology α] [BoundedSpace α] (s : Set α), Bornology.IsCobounded s
-- Init.Data.Rat.Lemmas
Rat.floor_add_one : ∀ {x : ℚ}, (x + 1).floor = x.floor + 1
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.LimitOfShape.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {J : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} J] →
          {X : C} →
            (toLimitPresentation : CategoryTheory.Limits.LimitPresentation J X) →
              (∀ (j : J), P (toLimitPresentation.diag.obj j)) → P.LimitOfShape J X
-- Mathlib.Order.Heyting.Basic
disjoint_compl_left : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a : α}, Disjoint aᶜ a
-- Lean.Environment
Lean.OLeanLevel.ofNat : ℕ → Lean.OLeanLevel
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.Scheme.Hom.finitePresentation_appTop : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y]
  [AlgebraicGeometry.LocallyOfFinitePresentation f],
  (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f)).FinitePresentation
-- Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
HasFDerivWithinAt.of_comp_of_leftInverse : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {f' : F →L[𝕜] G}
  {h' : E →L[𝕜] G} {f'symm : G →L[𝕜] F} {a : E} {s : Set E} {t : Set F},
  Filter.Tendsto g (nhdsWithin a s) (nhdsWithin (g a) t) →
    HasFDerivWithinAt f f' t (g a) →
      HasFDerivWithinAt h h' s a →
        f ∘ g =ᶠ[nhdsWithin a s] h → Function.LeftInverse ⇑f'symm ⇑f' → a ∈ s → HasFDerivWithinAt g (f'symm ∘SL h') s a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.insertManyIfNew_list_equiv_foldl : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ : Std.DTreeMap.Internal.Impl α β} {l : List ((a : α) × β a)}
  (h : t₁.WF),
  (↑(t₁.insertManyIfNew l ⋯)).Equiv
    (List.foldl (fun acc p => Std.DTreeMap.Internal.Impl.insertIfNew! p.fst p.snd acc) t₁ l)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_linear : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), (↑e).linear = ↑e.linear
-- Mathlib.Topology.UniformSpace.Basic
/-- Consider two functions `f` and `g` which coincide on a set `s` and are continuous there.
Then there is an open neighborhood of `s` on which `f` and `g` are uniformly close.  -/
Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : TopologicalSpace β] {r : SetRel α α} {s : Set β}
  {f g : β → α},
  (∀ x ∈ s, ContinuousAt f x) →
    (∀ x ∈ s, ContinuousAt g x) → Set.EqOn f g s → r ∈ uniformity α → ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r