mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.SplitCandidate : Type
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.map_injective : ∀ {R : Type u_3} {S : Type u_4} {F : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : FunLike F (Polynomial R) (Polynomial S)] [inst_3 : MonoidHomClass F (Polynomial R) (Polynomial S)] (φ : F)
  (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))),
  Function.Injective ⇑φ → Function.Injective ⇑(RatFunc.map φ hφ)
-- Std.Http.Data.URI.Encoding
/-- Checks if a byte is a valid character in a percent-encoded URI component. Valid characters are
unreserved characters or the percent sign (for escape sequences).
 -/
Std.Http.URI.isEncodedChar : (UInt8 → Bool) → UInt8 → Bool
-- Mathlib.Tactic.GCongr.Core
/-- The keys under which the lemma is stored. This is usually one key,
but for `gcongr strict` lemmas, this stores two keys, for the LHS and RHS respectively.  -/
Mathlib.Tactic.GCongr.GCongrLemma.keys : Mathlib.Tactic.GCongr.GCongrLemma → List Mathlib.Tactic.GCongr.GCongrKey
-- Mathlib.Topology.NhdsWithin
eventuallyEq_nhdsWithin_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f g : α → β} {s : Set α} {a : α},
  f =ᶠ[nhdsWithin a s] g ↔ ∀ᶠ (x : α) in nhds a, x ∈ s → f x = g x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_piMap' : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_4} {φ : ι → Type u_5} [inst_1 : (i : ι) → TopologicalSpace (φ i)]
  [inst_2 : (i : ι) → AddCommMonoid (φ i)] [inst_3 : (i : ι) → Module R (φ i)] {ψ : ι → Type u_6}
  [inst_4 : (i : ι) → TopologicalSpace (ψ i)] [inst_5 : (i : ι) → AddCommMonoid (ψ i)]
  [inst_6 : (i : ι) → Module R (ψ i)] (f : (i : ι) → φ i →L[R] ψ i),
  ⇑(ContinuousLinearMap.piMap f) = Pi.map fun i => ⇑(f i)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.checkKnowsType : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Mathlib.Analysis.Normed.Group.NullSubmodule
isClosed_nullSubmodule : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedRing 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : IsBoundedSMul 𝕜 E], IsClosed ↑(nullSubmodule 𝕜 E)
-- Mathlib.FieldTheory.Normal.Defs
Normal.algHomEquivAut_apply : ∀ (F : Type u_1) [inst : Field F] (K₁ : Type u_3) [inst_1 : Field K₁] [inst_2 : Algebra F K₁] (E : Type u_6)
  [inst_3 : Field E] [inst_4 : Algebra F E] [inst_5 : Algebra E K₁] [inst_6 : IsScalarTower F E K₁]
  [inst_7 : Normal F E] (σ : E →ₐ[F] K₁), (Normal.algHomEquivAut F K₁ E) σ = σ.restrictNormal' E
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.MeasurePreserving.integrable_comp_of_integrable : ∀ {α : Type u_1} {δ : Type u_4} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : MeasurableSpace δ] [inst_1 : TopologicalSpace ε] [inst_2 : ContinuousENorm ε] {ν : MeasureTheory.Measure δ}
  {g : δ → ε} {f : α → δ},
  MeasureTheory.MeasurePreserving f μ ν → MeasureTheory.Integrable g ν → MeasureTheory.Integrable (g ∘ f) μ
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.op_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : Cᵒᵖ),
  P.op X ↔ P (Opposite.unop X)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.isBasis_empty_iff : ∀ {α : Type u_1} {I : Set α} (M : Matroid α), M.IsBasis I ∅ ↔ I = ∅
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- A continuous alternating map from `ι → M` to `N`, denoted `M [⋀^ι]→L[R] N`,
is a continuous map that is

- multilinear : `f (update m i (c • x)) = c • f (update m i x)` and
  `f (update m i (x + y)) = f (update m i x) + f (update m i y)`;
- alternating : `f v = 0` whenever `v` has two equal coordinates.
 -/
ContinuousAlternatingMap : (R : Type u_1) →
  (M : Type u_2) →
    (N : Type u_3) →
      Type u_4 →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [Module R M] →
              [TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] → [Module R N] → [TopologicalSpace N] → Type (max (max u_2 u_3) u_4)
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_mul_X_zero : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), (p * Polynomial.X).coeff 0 = 0
-- Mathlib.Data.Fin.Tuple.Basic
/-- Equivalence between tuples of length `n + 1` and pairs of an element and a tuple of length `n`
given by separating out the last element of the tuple.

This is `Fin.snoc` as an `Equiv`.  -/
Fin.snocEquiv : {n : ℕ} → (α : Fin (n + 1) → Type u_2) → α (Fin.last n) × ((i : Fin n) → α i.castSucc) ≃ ((i : Fin (n + 1)) → α i)
-- Mathlib.Data.Fintype.Order
Directed.finite_set_le : ∀ {α : Type u_2} {r : α → α → Prop} [IsTrans α r] {γ : Type u_3} [Nonempty γ] {f : γ → α},
  Directed r f → ∀ {s : Set γ}, s.Finite → ∃ z, ∀ i ∈ s, r (f i) (f z)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insertIfNew!_le_minKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β k} {fallback : α},
        (compare ((Std.DTreeMap.Internal.Impl.insertIfNew! k v t).minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.imp_antisymm : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ : L.BoundedFormula α n},
  T.Imp φ ψ → T.Imp ψ φ → T.Iff φ ψ
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- By definition, if we have `OneMemClass S M`, we have `1 ∈ s` for all `s : S`.  -/
OneMemClass.one_mem : ∀ {S : Type u_3} {M : outParam (Type u_4)} {inst : One M} {inst_1 : SetLike S M} [self : OneMemClass S M] (s : S), 1 ∈ s
-- Mathlib.Data.NNReal.Defs
NNReal.instSub : Sub NNReal
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonUnitalNonAssocRing : {R : Type u_1} → {M : Type u_4} → [inst : Ring R] → [Add M] → NonUnitalNonAssocRing (AddMonoidAlgebra R M)
-- Mathlib.Data.Nat.Factorial.Basic
Nat.succ_descFactorial_succ : ∀ (n k : ℕ), (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial k
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.addPolynomial_slope : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  W.Equation x₁ y₁ →
    W.Equation x₂ y₂ →
      ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) →
        W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) =
          -((Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C x₂) *
              (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
/-- When `f₁`, `f₂` and `f₃` are composable morphisms, this is the canonical
morphism `Z^n(f₂, f₃) ⟶ opZ^{n+1}(f₁, f₂)` that is induced both
by `δ : H^n(f₂ ≫ f₃) ⟶ H^{n+1}(f₁)` (see `toCycles_Ψ`) and
by `δ : H^n(f₃) ⟶ H^{n+1}(f₁ ≫ f₂)` (see `Ψ_fromOpcycles`).
See the lemma `πE_d_ιE` for the relation between this definition
and the differentials `d`.  -/
CategoryTheory.Abelian.SpectralObject.Ψ : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (n₀ n₁ : ℤ) →
                      autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.Ψ._auto_1 →
                        (X.cycles f₂ f₃ n₀ ⟶ X.opcycles f₁ f₂ n₁)
-- Init.Data.String.TakeDrop
/-- If `pat` matches a suffix of `s`, returns the remainder. Returns `none` otherwise.

Use `String.dropSuffix` to return the slice
unchanged when `pat` does not match a suffix.

This is a cheap operation because it does not allocate a new string to hold the result.
To convert the result into a string, use `String.Slice.copy`.

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".dropSuffix? " blue" == some "red green".toSlice`

* `"red green blue".dropSuffix? "bluu " == none`

* `"red green blue".dropSuffix? 'e' == some "red green blu".toSlice`

* `"red green blue".dropSuffix? Char.isLower == some "red green blu".toSlice`
 -/
String.dropSuffix? : {ρ : Type} → String → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → Option String.Slice
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getKey?.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a a_1 : α) (b : β a_1) (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getKey? a (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    if (a_1 == a) = true then some a_1 else Std.DHashMap.Internal.AssocList.getKey? a es
-- Mathlib.Topology.Compactness.Compact
/-- The intersection of a compact set and a closed set is a compact set.  -/
IsCompact.inter_right : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsCompact s → IsClosed t → IsCompact (s ∩ t)
-- Mathlib.Data.Stream.Init
Stream'.eq_or_mem_of_mem_cons : ∀ {α : Type u} {a b : α} {s : Stream' α}, a ∈ Stream'.cons b s → a = b ∨ a ∈ s
-- Lean.Elab.App
/-- Like `const`, but with `fvar` instead of `constName`.
The `baseName` is the base name of the type to search for in the parameter list.  -/
Lean.Elab.Term.LValResolution.localRec : Lean.Name → Lean.Expr → Lean.Elab.Term.LValResolution
-- Mathlib.Topology.Algebra.Group.Units
/-- The isomorphism of topological additive groups between the additive units of a
product and the product of the additive units.  -/
ContinuousAddEquiv.piAddUnits : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → AddMonoid (M i)] →
      [inst_1 : (i : ι) → TopologicalSpace (M i)] → AddUnits ((i : ι) → M i) ≃ₜ+ ((i : ι) → AddUnits (M i))
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.isZariskiLocalAtSource : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q],
  (∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsAffine Y] (𝒰 : X.OpenCover),
      Q f ↔ ∀ (i : 𝒰.I₀), Q (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) →
    AlgebraicGeometry.IsZariskiLocalAtSource P
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instNontrivial : ∀ {G : Type u_1} [inst : AddGroup G] [Nontrivial G], Nontrivial (AddSubgroup G)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instInhabited : Inhabited Complex.UnitDisc
-- Mathlib.Analysis.Normed.Operator.Banach
/-- A useful form of the **closed graph theorem** : let `f` be a linear map between two Banach
spaces. To show that `f` is continuous, it suffices to show that for any convergent sequence
`uₙ ⟶ x`, if `f(uₙ) ⟶ y` then `y = f(x)`.  -/
LinearMap.continuous_of_seq_closed_graph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F]
  [CompleteSpace F] (g : E →ₗ[𝕜] F),
  (∀ (u : ℕ → E) (x : E) (y : F),
      Filter.Tendsto u Filter.atTop (nhds x) → Filter.Tendsto (⇑g ∘ u) Filter.atTop (nhds y) → y = g x) →
    Continuous ⇑g
-- Lean.Environment
_private.Lean.Environment.0.Lean.saveModuleDataParts.unsafe_1 : Lean.Name → Option Lean.Compactor → System.FilePath → Lean.ModuleData → IO Lean.Compactor
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isTrail_map_iff_of_injective : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v},
  Function.Injective ⇑f → ((SimpleGraph.Walk.map f p).IsTrail ↔ p.IsTrail)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.refl : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation.below ⋯
-- Std.Time.Internal.Bounded
/-- Convert a `Bounded.LE` to a `Fin`.
 -/
Std.Time.Internal.Bounded.LE.toFin : {lo hi : ℤ} → Std.Time.Internal.Bounded.LE lo hi → 0 ≤ lo → Fin (hi + 1).toNat
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is twice differentiable on `ℝ`, and `f''` is nonnegative on `ℝ`,
then `f` is convex on `ℝ`.  -/
convexOn_univ_of_deriv2_nonneg : ∀ {f : ℝ → ℝ}, Differentiable ℝ f → Differentiable ℝ (deriv f) → (∀ (x : ℝ), 0 ≤ deriv^[2] f x) → ConvexOn ℝ Set.univ f
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.finite_coeffs : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ), P.coeffs.Finite
-- Init.Data.Option.Array
Option.toArray_filter : ∀ {α : Type u_1} {o : Option α} {p : α → Bool}, (Option.filter p o).toArray = Array.filter p o.toArray
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mk.sizeOf_spec : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] [inst_1 : SizeOf M] (carrier : Set M)
  (fun_mem : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f carrier),
  sizeOf { carrier := carrier, fun_mem := fun_mem } = 1
-- Mathlib.RingTheory.RingHom.Unramified
RingHom.FormallyUnramified.ofLocalizationPrime : RingHom.OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.bicategory_homCategory_comp_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  (a b : CategoryTheory.Bicategory.InducedBicategory C F) {X Y Z : a ⟶ b}
  (u : CategoryTheory.Bicategory.InducedBicategory.Hom₂ X Y) (v : CategoryTheory.Bicategory.InducedBicategory.Hom₂ Y Z),
  (CategoryTheory.CategoryStruct.comp u v).hom = CategoryTheory.CategoryStruct.comp u.hom v.hom
-- Init.Data.Ord.Basic
Ordering.forall : ∀ {p : Ordering → Prop}, (∀ (o : Ordering), p o) ↔ p Ordering.lt ∧ p Ordering.eq ∧ p Ordering.gt
-- Mathlib.RingTheory.Congruence.Defs
/-- A coercion from a congruence relation to its underlying binary relation.  -/
RingCon.instFunLikeForallProp : {R : Type u_1} → [inst : Add R] → [inst_1 : Mul R] → FunLike (RingCon R) R (R → Prop)
-- Init.Data.Format.Basic
/-- Creates the format `"[" ++ f ++ "]"` with a flattening group, nesting by one space.

`sbracket` is short for “square bracket”.
 -/
Std.Format.sbracket : Std.Format → Std.Format
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.instMonoidalFDRepFGModuleCatForget₂HomSubtypeLinearMapIdCarrierObjModuleCatIsFGV : {k G : Type u} →
  [inst : CommRing k] → [inst_1 : Group G] → (CategoryTheory.forget₂ (FDRep k G) (FGModuleCat k)).Monoidal
-- Lean.Environment
/-- Safest access mode, writes and reads the extension state to/from the full `checked`
environment. This mode ensures the observed state is identical independently of whether or how
parallel elaboration is used but `getState` will block on all prior environment branches by
waiting for `checked`. `setState` and `modifyState` do not block.

While a safe fallback for when `mainOnly` is not sufficient, any extension that reasonably could
be used in parallel elaboration contexts should opt for a weaker mode to avoid blocking unless
there is no way to access the correct state without waiting for all prior environment branches, in
which case its data management should be restructured if at all possible.
 -/
Lean.EnvExtension.AsyncMode.sync : Lean.EnvExtension.AsyncMode
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.toPiNatHomeo_apply_ofPiNat : ∀ {ι : Type u_2} (X : Type u_3) (Y : ι → Type u_4) (f : (i : ι) → X → Y i) [inst : Encodable ι]
  [inst_1 : (i : ι) → MetricSpace (Y i)] [inst_2 : TopologicalSpace X] [inst_3 : CompactSpace X]
  (continuous_f : ∀ (i : ι), Continuous (f i)) (separating_f : Pairwise fun x y => ∃ i, f i x ≠ f i y) (ofPiNat : X),
  ((Metric.PiNatEmbed.toPiNatHomeo X Y f continuous_f separating_f) ofPiNat).ofPiNat = ofPiNat
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- An open ball centred at the origin in a valued ring is clopen.  -/
Valued.isClopen_ball : ∀ (R : Type u) [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀]
  (r : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀), IsClopen {x | Valued.v.restrict x < r}
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Context : Type u → Type u
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_subset_Ioo_iff : ∀ {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₁ ≤ b₁ → (Finset.Icc a₁ b₁ ⊆ Finset.Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.indexHom_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (g : P.Aut),
  (RootPairing.Equiv.indexHom P) g = (↑g).indexEquiv
-- Mathlib.Order.Lattice
/-- Pointwise maximum of two antitone functions is an antitone function.  -/
AntitoneOn.max : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α},
  AntitoneOn f s → AntitoneOn g s → AntitoneOn (fun x => max (f x) (g x)) s
-- Mathlib.Topology.CWComplex.Classical.Finite
Topology.CWComplex.mkFiniteType_map : ∀ {X : Type u} [inst : TopologicalSpace X] (C : Set X) (cell : ℕ → Type u)
  (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) (finite_cell : ∀ (n : ℕ), Finite (cell n))
  (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1)
  (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1))
  (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target)
  (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1)
  (mapsTo :
    ∀ (n : ℕ) (i : cell n),
      Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1))
  (closed' : ∀ A ⊆ C, (∀ (n : ℕ) (j : cell n), IsClosed (A ∩ ↑(map n j) '' Metric.closedBall 0 1)) → IsClosed A)
  (union' : ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C) (n : ℕ) (i : cell n),
  Topology.CWComplex.map n i = map n i
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.coeff_restriction' : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {n : ℕ}, ↑(p.restriction.coeff n) = p.coeff n
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a b : α} (hab : (a == b) = true) {h' : a ∈ m}, m[a] = m[b]
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.DischargeResult.ofNat : ℕ → Lean.Meta.Simp.DischargeResult
-- Mathlib.Data.Fintype.Pi
Fintype.eval_image_piFinset_subset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} (t : (a : α) → Finset (δ a)) (a : α)
  [inst_2 : DecidableEq (δ a)], Finset.image (fun f => f a) (Fintype.piFinset t) ⊆ t a
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The sheaf condition for a single morphism is the same as the canonical fork diagram being
limiting.  -/
CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {X Y : C}
  {f : X ⟶ Y} (c : CategoryTheory.Limits.PullbackCone f f) (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton f) ↔
    Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (F.map f.op) ⋯))
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.count_finsuppProd : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  (exps : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ),
  FractionalIdeal.count K v (exps.prod fun x1 x2 => ↑x1.asIdeal ^ x2) = exps v
-- Mathlib.Data.Analysis.Topology
Ctop.mk.sizeOf_spec : ∀ {α : Type u_1} {σ : Type u_2} [inst : SizeOf α] [inst_1 : SizeOf σ] (f : σ → Set α) (top : α → σ)
  (top_mem : ∀ (x : α), x ∈ f (top x)) (inter : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ)
  (inter_mem : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (inter a b x h))
  (inter_sub : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (inter a b x h) ⊆ f a ∩ f b),
  sizeOf { f := f, top := top, top_mem := top_mem, inter := inter, inter_mem := inter_mem, inter_sub := inter_sub } = 1
-- Init.Data.Bool
Bool.not_or_eq_left_iff_and : ∀ {a b : Bool}, (!a || b) = a ↔ a = true ∧ b = true
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.LawfulOperator.denote_input_entry : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → Type}
  {f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α} [Std.Sat.AIG.LawfulOperator α β f] {assign : α → Bool}
  (entry : Std.Sat.AIG.Entrypoint α) {input : β entry.aig} {h : entry.ref.gate < (f entry.aig input).aig.decls.size},
  ⟦assign,
      { aig := (f entry.aig input).aig, ref := { gate := entry.ref.gate, invert := entry.ref.invert, hgate := h } }⟧ =
    ⟦assign, entry⟧
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- If a compact closed set is everywhere positive with respect to a left-invariant measure on a
topological additive group, then it is a Gδ set. This is nontrivial, as there is no
second-countability or metrizability assumption in the statement, so a general compact closed set
has no reason to be a countable intersection of open sets.  -/
MeasureTheory.Measure.IsEverywherePos.IsGdelta_of_isAddLeftInvariant : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G},
  μ.IsEverywherePos k → IsCompact k → IsClosed k → IsGδ k
-- Mathlib.Data.Sym.Sym2
Sym2.pmap_eq_map : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : α → β) (z : Sym2 α) (h : ∀ a ∈ z, P a),
  Sym2.pmap (fun a x => f a) z h = Sym2.map f z
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientAddGroup.norm_lt_iff : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M} {x : M ⧸ S} {r : ℝ},
  ‖x‖ < r ↔ ∃ m, ↑m = x ∧ ‖m‖ < r
-- Lean.HeadIndex
_private.Lean.HeadIndex.0.Lean.Expr.headNumArgs.go : Lean.Expr → ℕ → ℕ
-- Mathlib.Algebra.CharP.Frobenius
iterateFrobenius_eq_pow : ∀ (R : Type u_1) [inst : CommSemiring R] (p n : ℕ) [inst_1 : ExpChar R p], iterateFrobenius R p n = frobenius R p ^ n
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.eqOn : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj), Set.EqOn (Prod.fst ∘ ↑e) proj e.source
-- Mathlib.Algebra.Group.Graph
/-- The graph of a monoid homomorphism as a submonoid.

See also `AddMonoidHom.graph` for the graph as a subgroup.  -/
AddMonoidHom.mgraph : {G : Type u_1} → {H : Type u_2} → [inst : AddMonoid G] → [inst_1 : AddMonoid H] → (G →+ H) → AddSubmonoid (G × H)
-- Mathlib.Topology.Closure
closure_sdiff_interior : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), closure s \ interior s = frontier s
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_sub_left : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (x x' y : M),
  QuadraticMap.polar (⇑Q) (x - x') y = QuadraticMap.polar (⇑Q) x y - QuadraticMap.polar (⇑Q) x' y