mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- `structureMapLM 𝕜 n i` is the `𝕜`-linear-map sending `f : 𝓓^{n}_{K}(E, F)` to its
`i`-th iterated derivative as an element of `E →ᵇ (E [×i]→L[ℝ] F)`. In other words, it
is the composition of `toBoundedContinuousFunctionLM 𝕜` and `iteratedFDerivLM 𝕜 n 0 i`.
This only makes mathematical sense if `i ≤ n`, otherwise we define it as the zero map.

We call these "structure maps" because they define the topology on `𝓓^{n}_{K}(E, F)`.

This is subsumed by `structureMapCLM`, which also bundles the
continuity.  -/
ContDiffMapSupportedIn.structureMapLM : (𝕜 : 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] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] →
                    (n : ℕ∞) →
                      {K : TopologicalSpace.Compacts E} →
                        (i : ℕ) → ContDiffMapSupportedIn E F n K →ₗ[𝕜] BoundedContinuousFunction E (E [×i]→L[ℝ] F)
-- Init.Data.Array.Lemmas
Array.foldr_eq_foldrM : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {b : β} {xs : Array α} {start stop : ℕ},
  Array.foldr f b xs start stop = (Array.foldrM (fun x1 x2 => pure (f x1 x2)) b xs start stop).run
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_iterate_powMonoidHom : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ} (f : Perfection M p) (n m : ℕ),
  (Perfection.coeffMonoidHom M p (n + m)) ((⇑(powMonoidHom p))^[m] f) = (Perfection.coeffMonoidHom M p n) f
-- Mathlib.Topology.Algebra.Ring.Basic
IsTopologicalRing.of_addGroup_of_nhds_zero : ∀ {R : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : TopologicalSpace R] [IsTopologicalAddGroup R],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 * x2) (nhds 0 ×ˢ nhds 0) (nhds 0) →
    (∀ (x₀ : R), Filter.Tendsto (fun x => x₀ * x) (nhds 0) (nhds 0)) →
      (∀ (x₀ : R), Filter.Tendsto (fun x => x * x₀) (nhds 0) (nhds 0)) → IsTopologicalRing R
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquivClass.toCoalgEquivClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : Semiring A} {inst_2 : Semiring B} {inst_3 : Algebra R A} {inst_4 : Algebra R B}
  {inst_5 : CoalgebraStruct R A} {inst_6 : CoalgebraStruct R B} {inst_7 : EquivLike F A B}
  [self : BialgEquivClass F R A B], CoalgEquivClass F R A B
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.aleph0_le_mk_iff : ∀ {α : Type u}, Cardinal.aleph0 ≤ Cardinal.mk α ↔ Infinite α
-- Mathlib.Algebra.BigOperators.Finprod
finsum_option : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : Option α → M},
  Function.HasFiniteSupport (f ∘ some) → ∑ᶠ (o : Option α), f o = f none + ∑ᶠ (a : α), f (some a)
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ` and `f'` is strictly antitone on the
interior, then `f` is strictly concave on `D`.
Note that we don't require differentiability, since it is guaranteed at all but at most
one point by the strict antitonicity of `f'`.  -/
StrictAntiOn.strictConcaveOn_of_deriv : ∀ {D : Set ℝ},
  Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → StrictAntiOn (deriv f) (interior D) → StrictConcaveOn ℝ D f
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.notMem_mutuallySingularSetSlice : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ) (a : α) (x : γ),
  x ∉ κ.mutuallySingularSetSlice η a ↔ κ.rnDerivAux (κ + η) a x < 1
-- Mathlib.Topology.Order.IsLUB
Dense.exists_seq_strictAnti_tendsto : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMaxOrder α] [FirstCountableTopology α] {s : Set α},
  Dense s → ∀ (x : α), ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Set.Ioi x ∩ s) ∧ Filter.Tendsto u Filter.atTop (nhds x)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.shrink_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S),
  E.shrink.I₀ = ↑(Set.range fun i => ⟨E.X i, E.f i⟩)
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsKleinFour.card_four' : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] [IsKleinFour G], Fintype.card G = 4
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.congr_eq_4 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1)
  (step : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n)) (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))) (id : ℕ)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array ℕ)
  (ratHints : Array (ℕ × Array ℕ)),
  step = some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) →
    (match step with
      | none => h_1 ()
      | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
      | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
      | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
      | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) ≍
      h_4 id c pivot rupHints ratHints
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.pp.analyze.trustKnownFOType2TypeHOFuns : Lean.Option Bool
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.ext_iff : ∀ {R : Type u_2} {E : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] {C₁ C₂ : ProperCone R E},
  C₁ = C₂ ↔ ∀ (x : E), x ∈ C₁ ↔ x ∈ C₂
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.mul_one : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {a : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (a * 1) a
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.leftInverse_generateFrom : ∀ {X : Type u_1}, Function.LeftInverse DiffeologicalSpace.generateFrom DiffeologicalSpace.toPlots
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.ennrealVariation.congr_simp : ∀ {X : Type u_1} {mX : MeasurableSpace X} {V : Type u_2} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] (μ μ_1 : MeasureTheory.VectorMeasure X V), μ = μ_1 → μ.ennrealVariation = μ_1.ennrealVariation
-- Mathlib.CategoryTheory.CommSq
/-- The vertical composition of two commutative squares as below is a commutative square.
```
  W ---f---> X
  |          |
  g          h
  |          |
  v          v
  Y ---i---> Z
  |          |
  g'         h'
  |          |
  v          v
  Y'---i'--> Z'

```
 -/
CategoryTheory.CommSq.vert_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Y' Z Z' : C} {f : W ⟶ X} {g : W ⟶ Y} {g' : Y ⟶ Y'}
  {h : X ⟶ Z} {h' : Z ⟶ Z'} {i : Y ⟶ Z} {i' : Y' ⟶ Z'},
  CategoryTheory.CommSq f g h i →
    CategoryTheory.CommSq i g' h' i' →
      CategoryTheory.CommSq f (CategoryTheory.CategoryStruct.comp g g') (CategoryTheory.CategoryStruct.comp h h') i'
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- Convert an integer to a `ℤ√d`  -/
Zsqrtd.ofInt : {d : ℤ} → ℤ → ℤ√d
-- Mathlib.Algebra.Lie.Normalizer
LieSubmodule.mem_normalizer : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (N : LieSubmodule R L M) (m : M), m ∈ N.normalizer ↔ ∀ (x : L), ⁅x, m⁆ ∈ N
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_inj : ∀ {a b : UInt32}, a.toUInt64 = b.toUInt64 ↔ a = b
-- Mathlib.FieldTheory.Normal.Defs
AlgEquiv.transfer_normal : ∀ {F : Type u_1} [inst : Field F] {E : Type u_3} [inst_1 : Field E] [inst_2 : Algebra F E] {E' : Type u_4}
  [inst_3 : Field E'] [inst_4 : Algebra F E'] (f : E ≃ₐ[F] E'), Normal F E ↔ Normal F E'
-- Mathlib.Data.Multiset.Fintype
Multiset.toEnumFinset_mono : ∀ {α : Type u_1} [inst : DecidableEq α] {m₁ m₂ : Multiset α}, m₁ ≤ m₂ → m₁.toEnumFinset ⊆ m₂.toEnumFinset
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.fiber_fac_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (y : ↥Y) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fiberι f y)
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f y)
      (CategoryTheory.CategoryStruct.comp (Y.fromSpecResidueField y) h)
-- Mathlib.Order.Minimal
MaximalFor.le : ∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrder α] {i j : ι} {Q : ι → Prop} {f : ι → α},
  MaximalFor Q f i → Q j → f j ≤ f i
-- Mathlib.Algebra.Category.Ring.Topology
CommRingCat.HomTopology.instCompactSpaceHomOfIsTopologicalRingOfT1SpaceOfCarrier : ∀ {R A : CommRingCat} [inst : TopologicalSpace ↑R] [IsTopologicalRing ↑R] [T1Space ↑R] [CompactSpace ↑R],
  CompactSpace (A ⟶ R)
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
/-- Given a function `f` with an invertible derivative, returns a function that is locally inverse
to `f`.  -/
HasStrictFDerivAt.localInverse : {𝕜 : 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] →
                (f : E → F) → (f' : E ≃L[𝕜] F) → (a : E) → [CompleteSpace E] → HasStrictFDerivAt f (↑f') a → F → E
-- Std.Time.Zoned.ZoneRules
/-- Standard time without adjustments for daylight saving.
 -/
Std.Time.TimeZone.StdWall.standard : Std.Time.TimeZone.StdWall
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.instSmallFunctorOfLocallySmall : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [Small.{w, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  {D : Type u'} [inst_3 : CategoryTheory.Category.{v', u'} D] [Small.{w, u'} D]
  [CategoryTheory.LocallySmall.{w, v', u'} D], Small.{w, max (max (max u' u) v') v} (CategoryTheory.Functor C D)
-- Init.Data.Rat.Basic
/-- Is this rational number integral?  -/
Rat.isInt : ℚ → Bool
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)),
  NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet a = ⟨⋯.choose, ⋯⟩
-- Mathlib.Algebra.FreeAlgebra.Cardinality
FreeAlgebra.cardinalMk_eq_max : ∀ (R : Type u) [inst : CommSemiring R] (X : Type u) [Nonempty X] [Nontrivial R],
  Cardinal.mk (FreeAlgebra R X) = max (max (Cardinal.mk R) (Cardinal.mk X)) Cardinal.aleph0
-- Mathlib.Topology.Compactness.LocallyFinite
/-- If `s` is a compact set in a topological space `X` and `f : ι → Set X` is a locally finite
family of sets, then `f i ∩ s` is nonempty only for a finitely many `i`.  -/
LocallyFinite.finite_nonempty_inter_compact : ∀ {X : Type u_1} {ι : Type u_2} [inst : TopologicalSpace X] {s : Set X} {f : ι → Set X},
  LocallyFinite f → IsCompact s → {i | (f i ∩ s).Nonempty}.Finite
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.prev : ∀ {m₁ : List Char} {c : Char} {m₂ : List Char} {s : Substring.Raw},
  s.Valid →
    s.toString.toList = m₁ ++ c :: m₂ →
      s.prev { byteIdx := String.utf8Len m₁ + c.utf8Size } = { byteIdx := String.utf8Len m₁ }
-- Init.Data.Option.Lemmas
Option.get_ite' : ∀ {α : Type u_1} {b : α} {p : Prop} {x : Decidable p} (h : (if p then none else some b).isSome = true),
  (if p then none else some b).get h = b
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {Y : CategoryTheory.Abelian.SpectralObject C EInt},
  (∀ (i j : EInt) (hij : i ≤ j),
      j ≤ WithBotTop.coe 0 →
        ∀ (n : ℤ),
          CategoryTheory.Limits.IsZero
            ((Y.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hij)))) →
    (∀ (i j : EInt) (hij : i ≤ j) (n : ℤ),
        WithBotTop.coe n < i →
          CategoryTheory.Limits.IsZero
            ((Y.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hij)))) →
      Y.IsFirstQuadrant
-- Mathlib.RingTheory.Ideal.Over
Ideal.instLiesOverUnder_1 : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : CommSemiring B] {C : Type u_4} [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C) (P : Ideal B)
  [𝔓.LiesOver P], P.LiesOver (Ideal.under A 𝔓)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffOn_finsetSum' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {t : Finset ι}
  {f : ι → M → G}, (∀ i ∈ t, ContMDiffOn I' I n (f i) s) → ContMDiffOn I' I n (∑ i ∈ t, f i) s
-- Mathlib.Algebra.Lie.Character
LieAlgebra.lieCharacter_apply_of_mem_derived : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (χ : LieAlgebra.LieCharacter R L) {x : L}, x ∈ LieAlgebra.derivedSeries R L 1 → χ x = 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.norm.sizeOf_spec : ∀ (c₁ : Lean.Meta.Grind.Arith.Linear.IneqCnstr) (k : ℕ),
  sizeOf (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.norm c₁ k) = 1 + sizeOf c₁ + sizeOf k
-- Init.Data.Vector.Lemmas
Vector.replace_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a b : α} {xs : Vector α n}, a ∉ xs → xs.replace a b = xs
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.lt_length : ∀ {n : ℕ} (c : CompositionAsSet n) (i : Fin c.length), ↑i + 1 < c.boundaries.card
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instModule : {α : Type u_1} →
  {l : Filter α} →
    {M : Type u_5} →
      {R : Type u_7} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Module R (l.Germ M)
-- Mathlib.Algebra.Algebra.Bilinear
/-- The multiplication in an algebra is an algebra homomorphism into the endomorphisms on
the algebra.

A weaker version of this for non-unital algebras exists as `NonUnitalAlgHom.lmul`.  -/
Algebra.lmul : (R : Type u_1) →
  (A : Type u_2) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → A →ₐ[R] Module.End R A
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.instFullArrowTopArrowForget : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T),
  (CategoryTheory.MorphismProperty.Arrow.forget P ⊤ ⊤).Full
-- Mathlib.Data.Set.Lattice
Set.iUnion_image_preimage_sigma_mk_eq_self : ∀ {ι : Type u_12} {σ : ι → Type u_13} (s : Set (Sigma σ)), ⋃ i, Sigma.mk i '' Sigma.mk i ⁻¹' s = s
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.SeparatingLeft.toMatrix₂' : ∀ {R : Type u_1} {n : Type u_11} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] {B : (m → R) →ₗ[R] (n → R) →ₗ[R] R},
  B.SeparatingLeft → ((LinearMap.toMatrix₂' R) B).SeparatingLeft
-- Mathlib.Topology.Sheaves.EtaleSpace
/-- Let `F` be a `C`-valued presheaf on `X`.
Let `U` be an open set on `X` such that for each `x ∈ U`, the `germ` map is bijective, i.e.,
every germ can be extended to a unique section over `U`.

Then for each `x ∈ U`, the preimage of `U` under `EtaleSpace.base`
is homeomorphic to the product of `U` and the stalk of `F` at `x` with discrete topology.
 -/
TopCat.Presheaf.EtaleSpace.homeomorph : {X : TopCat} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {CC : C → Type v} →
        {FC : C → C → Type w} →
          [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory C FC] →
              [inst_3 : CategoryTheory.Limits.HasColimits C] →
                {F : TopCat.Presheaf C X} →
                  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] →
                    (U : TopologicalSpace.Opens ↑X) →
                      (∀ (x : ↑X) (hx : x ∈ U),
                          Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (F.germ U x hx))) →
                        (x : ↑X) →
                          x ∈ U →
                            ↑(TopCat.Presheaf.EtaleSpace.base ⁻¹' ↑U) ≃ₜ
                              ↥U × WithDiscreteTopology (CategoryTheory.ToType (F.stalk x))
-- Mathlib.Data.Sigma.Order
Sigma.instPartialOrder : {ι : Type u_1} → {α : ι → Type u_2} → [(i : ι) → PartialOrder (α i)] → PartialOrder ((i : ι) × α i)
-- Mathlib.Analysis.Normed.Ring.WithAbs
AbsoluteValue.LiesOver.mk : ∀ {K : Type u_3} {L : Type u_4} {S : Type u_5} [inst : CommRing K] [inst_1 : IsSimpleRing K] [inst_2 : CommRing L]
  [inst_3 : Algebra K L] [inst_4 : PartialOrder S] [inst_5 : Nontrivial L] [inst_6 : Semiring S] {w : AbsoluteValue L S}
  {v : AbsoluteValue K S}, w.comp ⋯ = v → w.LiesOver v
-- Mathlib.Order.Fin.Basic
/-- `Fin.castLE` as an `OrderEmbedding`.

`castLEEmb h i` embeds `i` into a larger `Fin` type.  -/
Fin.castLEOrderEmb : {m n : ℕ} → n ≤ m → Fin n ↪o Fin m
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_le_of_le_mul : ∀ {a b c : ENNReal}, a ≤ b * c → a / c ≤ b
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.interpolate_eq_add_interpolate_erase : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {i j : ι} {v : ι → F}
  (r : ι → F),
  Set.InjOn v ↑s →
    i ∈ s →
      j ∈ s →
        i ≠ j →
          (Lagrange.interpolate s v) r =
            (Lagrange.interpolate (s.erase j) v) r * Lagrange.basisDivisor (v i) (v j) +
              (Lagrange.interpolate (s.erase i) v) r * Lagrange.basisDivisor (v j) (v i)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- A compositum of algebraic extensions is algebraic  -/
IntermediateField.isAlgebraic_iSup : ∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type u_4}
  {t : ι → IntermediateField K L}, (∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)) → Algebra.IsAlgebraic K ↥(⨆ i, t i)
-- Mathlib.Analysis.Normed.Group.Continuity
SeminormedGroup.toContinuousENorm.eq_1 : ∀ {E : Type u_4} [inst : SeminormedGroup E],
  SeminormedGroup.toContinuousENorm = { toENorm := NNNorm.toENorm, continuous_enorm := ⋯ }
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- A rewrite with a lemma from an imported file  -/
Mathlib.Tactic.LibraryRewrite.Kind.fromCache : Mathlib.Tactic.LibraryRewrite.Kind
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarCoord.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.polarCoord K = NumberField.mixedEmbedding.polarCoord K
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- The absolute value satisfies the triangle inequality  -/
IsAbsoluteValue.abv_add' : ∀ {S : Type u_5} {inst : Semiring S} {inst_1 : PartialOrder S} {R : Type u_6} {inst_2 : Semiring R} {f : R → S}
  [self : IsAbsoluteValue f] (x y : R), f (x + y) ≤ f x + f y
-- Mathlib.Analysis.Normed.Group.Uniform
/-- A homomorphism `f` of seminormed groups is continuous, if there exists a constant
`C` such that for all `x`, one has `‖f x‖ ≤ C * ‖x‖`.  -/
AddMonoidHomClass.continuous_of_bound : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
  [inst_2 : FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ), (∀ (x : E), ‖f x‖ ≤ C * ‖x‖) → Continuous ⇑f
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsHaarMeasure.comap : ∀ {G : Type u_1} {H : Type u_2} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace H] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [BorelSpace G] [MeasurableMul G] [inst_6 : Group H] [inst_7 : TopologicalSpace H]
  [BorelSpace H] {mH : MeasurableMul H} (μ : MeasureTheory.Measure H) [μ.IsHaarMeasure] {f : G →* H},
  Topology.IsOpenEmbedding ⇑f → (MeasureTheory.Measure.comap (⇑f) μ).IsHaarMeasure
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- The tensor product of two orthonormal vectors is orthonormal.  -/
Orthonormal.tmul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {ι₁ : Type u_6}
  {ι₂ : Type u_7} {b₁ : ι₁ → E} {b₂ : ι₂ → F},
  Orthonormal 𝕜 b₁ → Orthonormal 𝕜 b₂ → Orthonormal 𝕜 fun i => b₁ i.1 ⊗ₜ[𝕜] b₂ i.2
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.getElem_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (hk : k ∈ m₁) (h : m₁.Equiv m₂), m₁[k] = m₂[k]
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.op_normalizer : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G), (AddSubgroup.normalizer ↑H).op = AddSubgroup.normalizer ↑H.op
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∉ m₂ → (m₁ ∩ m₂).getKeyD k fallback = fallback
-- Mathlib.Combinatorics.Quiver.SingleObj
/-- Paths in `SingleObj α` quiver correspond to lists of elements of type `α`.  -/
Quiver.SingleObj.pathEquivList : {α : Type u_1} → Quiver.Path (Quiver.SingleObj.star α) (Quiver.SingleObj.star α) ≃ List α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
_private.Mathlib.Algebra.Order.Monoid.Unbundled.Units.0.Units.mul_le_mul_iff_left : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ) {a b : M}, ↑u * a ≤ ↑u * b ↔ a ≤ b
-- Mathlib.Order.Hom.CompleteLattice
/-- Copy of a `sInfHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
sInfHom.copy : {α : Type u_2} →
  {β : Type u_3} → [inst : InfSet α] → [inst_1 : InfSet β] → (f : sInfHom α β) → (f' : α → β) → f' = ⇑f → sInfHom α β