mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.addBottom_modifyNth : ∀ {K : Type u_1} {Γ : K → Type u_2} (f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k))
  (L : Turing.ListBlank ((k : K) → Option (Γ k))) (n : ℕ),
  Turing.ListBlank.modifyNth (fun a => (a.1, f a.2)) n (Turing.TM2to1.addBottom L) =
    Turing.TM2to1.addBottom (Turing.ListBlank.modifyNth f n L)
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_map : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E} {F : Type u_2} [inst_4 : NormedAddCommGroup F]
  [inst_5 : InnerProductSpace ℝ F] [inst_6 : MeasurableSpace F] [inst_7 : BorelSpace F] [SecondCountableTopology F]
  [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp id 2 μ →
    ∀ (L : E →L[ℝ] F) (u v : F),
      ((ProbabilityTheory.covarianceBilin (MeasureTheory.Measure.map (⇑L) μ)) u) v =
        ((ProbabilityTheory.covarianceBilin μ) ((ContinuousLinearMap.adjoint L) u)) ((ContinuousLinearMap.adjoint L) v)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.instMax.eq_1 : ∀ {E : Type u_3} [inst : AddGroup E],
  AddGroupNorm.instMax =
    {
      max := fun p q =>
        let __src := p.toAddGroupSeminorm ⊔ q.toAddGroupSeminorm;
        { toAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := ⋯ } }
-- Mathlib.Topology.Category.Stonean.Basic
/-- ```
               X
               |
              (f)
               |
               \/
  Z ---(e)---> Y
```
If `Z` is a Stonean space, `f : X ⟶ Y` an epi in `CompHaus` and `e : Z ⟶ Y` is arbitrary, then
`lift e f` is a fixed (but arbitrary) lift of `e` to a morphism `Z ⟶ X`. It exists because
`Z` is a projective object in `CompHaus`.
 -/
CompHaus.lift : {X Y : CompHaus} → {Z : Stonean} → (Z.compHaus ⟶ Y) → (f : X ⟶ Y) → [CategoryTheory.Epi f] → Z.compHaus ⟶ X
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.hasDerivAt_tan : ∀ {x : ℝ}, Real.cos x ≠ 0 → HasDerivAt Real.tan (1 / Real.cos x ^ 2) x
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.zero_of_nonpos : ∀ {x : ℝ}, x ≤ 0 → x.smoothTransition = 0
-- Mathlib.Topology.Order.IntermediateValue
/-- Suppose `f : [a, b] → δ` is continuous and injective. Then `f` is strictly monotone
or antitone (increasing or decreasing).  -/
ContinuousOn.strictMonoOn_of_injOn_Icc' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ},
  a ≤ b →
    ContinuousOn f (Set.Icc a b) →
      Set.InjOn f (Set.Icc a b) → StrictMonoOn f (Set.Icc a b) ∨ StrictAntiOn f (Set.Icc a b)
-- Mathlib.Data.Fin.Tuple.Reflection
_private.Mathlib.Data.Fin.Tuple.Reflection.0.FinVec.sum.match_1.eq_1 : ∀ {α : Type u_2} (motive : (x : ℕ) → (Fin x → α) → Sort u_1) (x : Fin 0 → α) (h_1 : (x : Fin 0 → α) → motive 0 x)
  (h_2 : (v : Fin 1 → α) → motive 1 v) (h_3 : (n : ℕ) → (v : Fin (n + 2) → α) → motive n.succ.succ v),
  (match 0, x with
    | 0, x => h_1 x
    | 1, v => h_2 v
    | n.succ.succ, v => h_3 n v) =
    h_1 x
-- Lean.Server.ServerTask
Lean.Server.ServerTask.hasFinished : {α : Type u_1} → Lean.Server.ServerTask α → BaseIO Bool
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.range_aleph : Set.range ⇑Cardinal.aleph = Set.Ici Cardinal.aleph0
-- Mathlib.RingTheory.Multiplicity
lt_emultiplicity_of_lt_multiplicity : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {n : ℕ}, n < multiplicity a b → ↑n < emultiplicity a b
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Icc_mul_Ico_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [MulLeftStrictMono α]
  [MulRightStrictMono α] [inst_5 : LocallyFiniteOrder α] (a b c d : α),
  Finset.Icc a b * Finset.Ico c d ⊆ Finset.Ico (a * c) (b * d)
-- Std.Http.Internal.ChunkedBuffer
Std.Http.Internal.ChunkedBuffer.mk.sizeOf_spec : ∀ (data : Array ByteArray) (size : ℕ), sizeOf { data := data, size := size } = 1 + sizeOf data + sizeOf size
-- Mathlib.Data.Num.ZNum
Num.pred_succ : ∀ (n : ZNum), n.pred.succ = n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insertManyIfNewUnit_empty_list : ∀ {α : Type u} {instOrd : Ord α} {l : List α} {k : α}
  {h :
    Std.DTreeMap.Internal.Impl.contains k
        ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯) =
      true},
  Std.DTreeMap.Internal.Impl.Const.get
      (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯)) k h =
    ()
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.homMk'_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} (u : X ⟶ P)
  (v : Y ⟶ Q)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp u g = CategoryTheory.CategoryStruct.comp f v)
      CategoryTheory.Arrow.homMk'._auto_1),
  (CategoryTheory.Arrow.homMk' u v w).left = u
-- Init.Data.BitVec.Bitblast
/-- Show that `x.sshiftRight y` can be written in terms of `sshiftRightRec`.
This can be unfolded in terms of `sshiftRightRec_zero_eq`, `sshiftRightRec_succ_eq` for bit blasting.
 -/
BitVec.sshiftRight_eq_sshiftRightRec : ∀ {w₁ w₂ i : ℕ} (x : BitVec w₁) (y : BitVec w₂), (x.sshiftRight' y).getLsbD i = (x.sshiftRightRec y (w₂ - 1)).getLsbD i
-- Mathlib.Algebra.Group.Int.TypeTags
Int.ofAdd_mul : ∀ (a b : ℤ), Multiplicative.ofAdd (a * b) = Multiplicative.ofAdd a ^ b
-- Mathlib.Combinatorics.Graph.Basic
/-- Two graphs with the same vertex set and binary incidences are equal.
(We use this as the default extensionality lemma rather than adding `@[ext]`
to the definition of `Graph`, so it doesn't require equality of the edge sets.)  -/
Graph.ext : ∀ {α : Type u_1} {β : Type u_2} {G₁ G₂ : Graph α β},
  G₁.vertexSet = G₂.vertexSet → (∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y) → G₁ = G₂
-- Init.Data.SInt.Lemmas
Int32.eq_sub_iff_add_eq : ∀ {a b c : Int32}, a = c - b ↔ a + b = c
-- Mathlib.Topology.MetricSpace.Isometry
/-- The group of isometries.  -/
IsometryEquiv.instGroup : {α : Type u} → [inst : PseudoEMetricSpace α] → Group (α ≃ᵢ α)
-- Init.SimpLemmas
and_self : ∀ (p : Prop), (p ∧ p) = p
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorArbitraryShiftTargetBlastArithShiftRight : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.ArbitraryShiftTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The universal cover of the classifying space of `G` as a simplicial set, augmented by the map
from `Fin 1 → G` to the terminal object in `Type u`.  -/
classifyingSpaceUniversalCover.compForgetAugmented : (G : Type u) → [Monoid G] → CategoryTheory.SimplicialObject.Augmented (Type u)
-- Mathlib.Topology.Covering.Quotient
IsAddQuotientCoveringMap.toContinuousConstVAdd : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E], IsAddQuotientCoveringMap f G → ContinuousConstVAdd G E
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.stronglyAdapted_densityProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (a : α) {s : Set β},
  MeasurableSet s →
    MeasureTheory.StronglyAdapted (ProbabilityTheory.countableFiltration γ) fun n x => κ.densityProcess ν n a x s
-- Mathlib.Analysis.ODE.Basic
isIntegralCurveOn_univ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E},
  IsIntegralCurveOn γ v Set.univ ↔ IsIntegralCurve γ v
-- Lean.Meta.MatchUtil
Lean.Meta.matchFalse : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Analysis.Normed.Operator.Asymptotics
ContinuousLinearEquiv.isBigO_sub : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] (e : E ≃SL[σ₁₂] F) [RingHomIsometric σ₁₂]
  (l : Filter E) (x : E), (fun x' => e (x' - x)) =O[l] fun x' => x' - x
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {A : Type u_1} [inst_1 : SeminormedRing A]
  [inst_2 : NormedAlgebra 𝕜 A], 0 < n → ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ 1
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.minOn.eq_1 : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β) (x : α) (xs : List α)
  (h_2 : x :: xs ≠ []), List.minOn f (x :: xs) h_2 = List.foldl (minOn f) x xs
-- Mathlib.RingTheory.WittVector.Teichmuller
/-- The `n`-th ghost component of `teichmuller p r` is `r ^ p ^ n`.  -/
WittVector.ghostComponent_teichmuller : ∀ (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (r : R) (n : ℕ),
  (WittVector.ghostComponent n) ((WittVector.teichmuller p) r) = r ^ p ^ n
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.arr_empty : Batteries.UnionFind.empty.arr = #[]
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Construct a `LinearIsometry` from a `LinearMap` satisfying `Isometry`.  -/
LinearMap.toLinearIsometry : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E : Type u_5} →
      {E₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              [inst_2 : SeminormedAddCommGroup E] →
                [inst_3 : SeminormedAddCommGroup E₂] →
                  [inst_4 : Module R E] → [inst_5 : Module R₂ E₂] → (f : E →ₛₗ[σ₁₂] E₂) → Isometry ⇑f → E →ₛₗᵢ[σ₁₂] E₂
-- Mathlib.Order.Hom.Lattice
InfHom.dual.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Min β],
  InfHom.dual =
    { toFun := fun f => { toFun := ⇑f, map_sup' := ⋯ }, invFun := fun f => { toFun := ⇑f, map_inf' := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A finite union of countably compact sets is countably compact.  -/
Finset.isCountablyCompact_biUnion : ∀ {ι : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] (s : Finset ι) {f : ι → Set E},
  (∀ i ∈ s, IsCountablyCompact (f i)) → IsCountablyCompact (⋃ i ∈ s, f i)
-- Mathlib.Algebra.Group.Submonoid.DistribMulAction
/-- The action by a submonoid is the action by the underlying monoid.  -/
Submonoid.distribMulAction : {M : Type u_1} →
  {α : Type u_2} →
    [inst : Monoid M] → [inst_1 : AddMonoid α] → [DistribMulAction M α] → (S : Submonoid M) → DistribMulAction (↥S) α
-- Mathlib.NumberTheory.Divisors
Int.divisorsAntidiagonal_one : Int.divisorsAntidiag 1 = {(1, 1), (-1, -1)}
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteAddGrp.ProfiniteCompletion.etaFn_injective_iff_residuallyFinite : ∀ (G : AddGrpCat), Function.Injective (ProfiniteAddGrp.ProfiniteCompletion.etaFn G) ↔ AddGroup.ResiduallyFinite ↑G
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- Transport a pre-submersive presentation along an algebra isomorphism.  -/
Algebra.PreSubmersivePresentation.ofAlgEquiv : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              Algebra.PreSubmersivePresentation R S ι σ →
                {T : Type u_1} →
                  [inst_3 : CommRing T] →
                    [inst_4 : Algebra R T] → (S ≃ₐ[R] T) → Algebra.PreSubmersivePresentation R T ι σ
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_one_add_smoothingFn_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < 1 + AkraBazziRecurrence.smoothingFn ↑n
-- Mathlib.Util.DischargerAsTactic
/-- Wrap a simp discharger (a function `Expr → SimpM (Option Expr)`) as a tactic,
so that it can be passed as an argument to `simp (discharger := foo)`.
This is inverse to `mkDischargeWrapper`.  -/
wrapSimpDischarger : Lean.Meta.Simp.Discharge → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.mem_inf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {S T : NonUnitalStarSubalgebra R A} {x : A}, x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
instLieGroupOfNatWithTopENatOfIsTopologicalGroup : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] [IsTopologicalGroup G], LieGroup I 0 G
-- Init.Grind.Order
Lean.Grind.Order.eq_of_le_of_le_0 : ∀ {α : Type u_1} [inst : LE α] [Std.IsPartialOrder α] [inst_2 : Lean.Grind.Ring α] {a b : α},
  a ≤ b + ↑0 → b ≤ a + ↑0 → a = b
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- If `p < ⊤` is a subspace of a vector space `V`, then there exists a nonzero linear map
`f : V →ₗ[K] K` such that `p ≤ ker f`.  -/
Submodule.exists_le_ker_of_lt_top : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  ∀ p < ⊤, ∃ f, f ≠ 0 ∧ p ≤ f.ker
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
UpperHalfPlane.IsZeroAtImInfty.eq_1 : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : TopologicalSpace α] (f : UpperHalfPlane → α),
  UpperHalfPlane.IsZeroAtImInfty f = UpperHalfPlane.atImInfty.ZeroAtFilter f
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instStar : {ι : 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 : (i : ι) → Star (G i)] →
                  [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] → Star (DirectLimit G f)
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- **Alias** of `Irreducible.maximalIdeal_pow_eq_setOfPred_le_v_coe_pow`. -/
Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow : ∀ {K : Type u_1} {Γ₀ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀)
  [inst_2 : IsDiscreteValuationRing ↥v.integer] {ϖ : ↥v.integer},
  Irreducible ϖ → ∀ (n : ℕ), ↑(IsLocalRing.maximalIdeal ↥v.integer ^ n) = {y | v ↑y ≤ v ↑ϖ ^ n}
-- Init.MetaTypes
/-- If true (default: true), reuse local declarations that have syntactically equal values.
Note that even when false, the caching strategy for `extract_lets` may result in fewer extracted let bindings than expected.  -/
Lean.Meta.ExtractLetsConfig.merge : Lean.Meta.ExtractLetsConfig → Bool
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.cyclesMap'_sub : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.ShortComplex.cyclesMap' (φ - φ') h₁ h₂ =
    CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂ - CategoryTheory.ShortComplex.cyclesMap' φ' h₁ h₂
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- A CW complex that was constructed using `RelCWComplex.mkFiniteType` is of finite type.  -/
Topology.RelCWComplex.finiteType_mkFiniteType : ∀ {X : Type u} [inst : TopologicalSpace X] (C : Set X) (D : outParam (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)
  (disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' Metric.ball 0 1) D)
  (mapsTo :
    ∀ (n : ℕ) (i : cell n),
      Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (D ∪ ⋃ 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 ∩ D) → IsClosed A)
  (isClosedBase : IsClosed D) (union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C),
  Topology.RelCWComplex.FiniteType C
-- Init.Data.List.Nat.Range
List.getLast_range' : ∀ {s n : ℕ} (h : List.range' s n ≠ []), (List.range' s n).getLast h = s + n - 1
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_sum : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] {ι' : Type u_5} (s : Finset ι')
  (f : ι' → M), (DirectSum.decompose ℳ) (∑ i ∈ s, f i) = ∑ i ∈ s, (DirectSum.decompose ℳ) (f i)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.edgeSet_nil : ∀ {V : Type u} {G : SimpleGraph V} (u : V), SimpleGraph.Walk.nil.edgeSet = ∅
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- An auxiliary construction for `mkHom`.

Here we build by induction a family of commutative squares,
but don't require at the type level that these successive commutative squares actually agree.
They do in fact agree, and we then capture that at the type level (i.e. by constructing a chain map)
in `mkHom`.
 -/
CochainComplex.mkHomAux : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (P Q : CochainComplex V ℕ) →
        (zero : P.X 0 ⟶ Q.X 0) →
          (one : P.X 1 ⟶ Q.X 1) →
            CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) = CategoryTheory.CategoryStruct.comp (P.d 0 1) one →
              ((n : ℕ) →
                  (p :
                      (f : P.X n ⟶ Q.X n) ×'
                        (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
                          CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) =
                            CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f') →
                    (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
                      CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) =
                        CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f'') →
                (n : ℕ) →
                  (f : P.X n ⟶ Q.X n) ×'
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
                      CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) =
                        CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f'
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The valuation on the completion agrees with the global valuation on elements of the field.  -/
IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (k : K),
  Valued.v { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm k) } =
    (IsDedekindDomain.HeightOneSpectrum.valuation K v) k
-- Mathlib.Topology.Homeomorph.Defs
Equiv.toHomeomorphOfContinuousClosed_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ Y)
  (h₁ : Continuous ⇑e) (h₂ : IsClosedMap ⇑e), ⇑(e.toHomeomorphOfContinuousClosed h₁ h₂).symm = ⇑e.symm
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_le_encard : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.eRk X ≤ X.encard
-- Mathlib.Topology.Category.Profinite.Basic
/-- Finite types are given the discrete topology.  -/
FintypeCat.botTopology : (A : FintypeCat) → TopologicalSpace A.obj
-- Std.Data.DTreeMap.Internal.Def
Std.DTreeMap.Internal.Impl.toListModel_inner : ∀ {α : Type u} {β : α → Type v} {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k v l r).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel
-- Mathlib.Computability.Language
instCompleteAtomicBooleanAlgebraLanguage : (α : Type u_1) → CompleteAtomicBooleanAlgebra (Language α)
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.id_of_comp_left_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (f : X ⟶ X),
  (∀ {Y : C} (g : X ⟶ Y), CategoryTheory.CategoryStruct.comp f g = g) → f = CategoryTheory.CategoryStruct.id X
-- Mathlib.Analysis.Calculus.Rademacher
/-- A real-valued function on a finite-dimensional space which is Lipschitz on a set is
differentiable almost everywhere in this set. Superseded by
`LipschitzOnWith.ae_differentiableWithinAt_of_mem` which works for functions taking value in any
finite-dimensional space.  -/
LipschitzOnWith.ae_differentiableWithinAt_of_mem_of_real : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {C : NNReal} {f : E → ℝ} {s : Set E} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  LipschitzOnWith C f s → ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.range_eq_top : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : NonUnitalSemiring B]
  [inst_6 : StarRing B] [inst_7 : Module R B] [inst_8 : FunLike F A B] [inst_9 : NonUnitalAlgHomClass F R A B]
  [inst_10 : StarHomClass F A B] [inst_11 : IsScalarTower R B B] [inst_12 : SMulCommClass R B B]
  [inst_13 : StarModule R B] (f : F), NonUnitalStarAlgHom.range f = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib.MeasureTheory.Function.EssSup
essInf_const_top : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : CompleteLattice β],
  essInf (fun x => ⊤) μ = ⊤
-- Lean.Elab.Tactic.Omega.Core
/-- The result of `combine` on two `Justifications`.  -/
Lean.Elab.Tactic.Omega.Justification.combine : {s t : Lean.Omega.Constraint} →
  {c : Lean.Omega.Coeffs} →
    Lean.Elab.Tactic.Omega.Justification s c →
      Lean.Elab.Tactic.Omega.Justification t c → Lean.Elab.Tactic.Omega.Justification (s.combine t) c
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.of_exists_root : ∀ (k : Type u) [inst : Field k],
  (∀ (p : Polynomial k), p.Monic → Irreducible p → p.Separable → ∃ x, Polynomial.eval x p = 0) → IsSepClosed k
-- Mathlib.Logic.IsEmpty.Defs
/-- subtypes by an all-false predicate are false.  -/
Subtype.isEmpty_of_false : ∀ {α : Sort u} {p : α → Prop}, (∀ (a : α), ¬p a) → IsEmpty (Subtype p)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.range_coeFn_eq : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂],
  Set.range DFunLike.coe = {f | Continuous f} ∩ Set.range DFunLike.coe