mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Complex.GammaSeq.eq_1 : ∀ (s : ℂ) (n : ℕ), s.GammaSeq n = ↑n ^ s * ↑n.factorial / ∏ j ∈ Finset.range (n + 1), (s + ↑j)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.prod.instIsHaarMeasure : ∀ {G : Type u_3} [inst : Group G] [inst_1 : TopologicalSpace G] {x : MeasurableSpace G} {H : Type u_4}
  [inst_2 : Group H] [inst_3 : TopologicalSpace H] {x_1 : MeasurableSpace H} (μ : MeasureTheory.Measure G)
  (ν : MeasureTheory.Measure H) [μ.IsHaarMeasure] [ν.IsHaarMeasure] [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  [MeasurableMul G] [MeasurableMul H], (μ.prod ν).IsHaarMeasure
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.of_irreducible_expand : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {p : ℕ},
  p ≠ 0 → ∀ {f : Polynomial R}, Irreducible ((Polynomial.expand R p) f) → Irreducible f
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
minpoly.ToAdjoin.injective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [inst_3 : Algebra R S]
  [IsIntegrallyClosed R] [IsDomain S] [Module.IsTorsionFree R S] {x : S},
  IsIntegral R x → Function.Injective ⇑(AdjoinRoot.Minpoly.toAdjoin R x)
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.PointsWithCircumcenterIndex.pointIndex.injEq : ∀ {n : ℕ} (a a_1 : Fin (n + 1)),
  (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a =
      Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a_1) =
    (a = a_1)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_eq_getD_default : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m).WF → ∀ {a : α}, Std.DHashMap.Internal.Raw₀.Const.get! m a = Std.DHashMap.Internal.Raw₀.Const.getD m a default
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.tryRecv' : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT (ST IO.RealWorld) m] →
      [MonadLiftT BaseIO m] → Std.AtomicT Std.Http.Body.Channel.State✝ m (Option Std.Http.Chunk)
-- Init.Data.String.Lemmas.Slice
String.Slice.Pos.get?_eq_dif : ∀ {s : String.Slice} {p : s.Pos}, p.get? = if h : p = s.endPos then none else some (p.get h)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_insertIfNew_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, k ∈ m.insertIfNew k v
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_zero_eval_zero : ∀ (S : Type u) [inst : Semiring S], Polynomial.eval 0 (ascPochhammer S 0) = 1
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.of_ne_zero : ∀ {α : Type u_1} (a : α), FreeAddMonoid.of a ≠ 0
-- Mathlib.Analysis.Complex.LocallyUniformLimit
Complex.norm_cderiv_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {z : ℂ} {M r : ℝ} {f : ℂ → E},
  0 < r → (∀ w ∈ Metric.sphere z r, ‖f w‖ ≤ M) → ‖Complex.cderiv r f z‖ ≤ M / r
-- Mathlib.Data.Nat.MaxPowDiv
/-- Divide `n` by the maximal power of `p` that divides `n`.  -/
Nat.divMaxPow : ℕ → ℕ → ℕ
-- Init.Data.List.Lex
List.instLawfulOrderLTOfAsymmLt : ∀ {α : Type u_1} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2], Std.LawfulOrderLT (List α)
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.AnalyzeResult.mk : Option FBinopElab.SRec → Bool → FBinopElab.AnalyzeResult✝
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_ediv_of_nonneg : ∀ {x y z : ℤ}, 0 ≤ y → x / y / z = x / (y * z)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.ComposableArrows.threeδ₁Toδ₀.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {i j k l : C} (f₁ f₁_1 : i ⟶ j) (e_f₁ : f₁ = f₁_1) (f₂ : j ⟶ k)
  (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂),
  CategoryTheory.ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂ =
    CategoryTheory.ComposableArrows.threeδ₁Toδ₀ f₁_1 f₂ f₃ f₁₂ ⋯
-- Lean.Parser.Extra
/-- No-op parser combinator that advises the pretty printer to emit a `Format.fill` node.  -/
Lean.Parser.ppRealFill : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.of_div_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t : Finset α}, (s / t).Nonempty → s.Nonempty
-- Mathlib.RingTheory.Polynomial.ScaleRoots
/-- **Alias** of `Polynomial.isCoprime_scaleRoots`. -/
IsCoprime.scaleRoots : ∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) (r : R),
  IsUnit r → IsCoprime p q → IsCoprime (p.scaleRoots r) (q.scaleRoots r)
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- `Splitting` of a group extension is a section homomorphism.  -/
GroupExtension.Splitting : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] → [inst_1 : Group E] → [inst_2 : Group G] → GroupExtension N E G → Type (max u_2 u_3)
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.disjoint_image_image_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {U V : Set α},
  Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_insertMany_list : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)},
  List.Pairwise (fun a b => (a.1 == b.1) = false) l →
    (∀ a ∈ m, (List.map Prod.fst l).contains a = false) → (m.insertMany l).size = m.size + l.length
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_lt_rpow_iff : ∀ {x y : ENNReal} {z : ℝ}, 0 < z → (x ^ z < y ^ z ↔ x < y)
-- Mathlib.Topology.Sober
/-- In a sober space, the generic points corresponds bijectively to irreducible components  -/
genericPoints.equiv : {α : Type u_1} →
  [inst : TopologicalSpace α] → [T0Space α] → [QuasiSober α] → ↑(genericPoints α) ≃ ↑(irreducibleComponents α)
-- Mathlib.LinearAlgebra.Complex.Module
/-- Two `ℝ`-algebra homomorphisms from `ℂ` are equal if they agree on `Complex.I`.  -/
Complex.algHom_ext : ∀ {A : Type u_3} [inst : Semiring A] [inst_1 : Algebra ℝ A] ⦃f g : ℂ →ₐ[ℝ] A⦄, f Complex.I = g Complex.I → f = g
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.IsSymm.map : ∀ {α : Type u_1} {β : Type u_2} {n : Type u_3} {A : Matrix n n α}, A.IsSymm → ∀ (f : α → β), (A.map f).IsSymm
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Limits.WeightedCone.coyoneda_π_app : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (F : CategoryTheory.Functor J C) (j : J) (u : (CategoryTheory.coyoneda.obj (Opposite.op j)).Elements),
  (CategoryTheory.Limits.WeightedCone.coyoneda F j).π.app u = F.map u.snd
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.ext : ∀ {𝒮 : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {x y : F.Grothendieck},
  x.base = y.base → x.fiber ≍ y.fiber → x = y
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.pi32 : Std.Internal.Parsec.ByteArray.Parser ℤ
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_infty_iff_fderiv_of_isOpen : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F}, IsOpen s → (ContDiffOn 𝕜 (↑⊤) f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑⊤) (fderiv 𝕜 f) s)
-- Mathlib.Analysis.Normed.Group.Basic
coe_nnnorm' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), ↑‖a‖₊ = ‖a‖
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.liftEquiv_apply : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra S C] [inst_11 : Algebra R C] [inst_12 : IsScalarTower R S C]
  (fg : { fg // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) }),
  Algebra.TensorProduct.liftEquiv fg = Algebra.TensorProduct.lift (↑fg).1 (↑fg).2 ⋯
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Outside the usual range of `qaryEntropy`, it is negative. This is due to `log p = log |p|`.  -/
Real.qaryEntropy_neg_of_neg : ∀ {q : ℕ} {p : ℝ}, p < 0 → Real.qaryEntropy q p < 0
-- Init.Prelude
/-- Create array `#[a₁, a₂, a₃, a₄, a₅, a₆, a₇]`  -/
Array.mkArray7 : {α : Type u} → α → α → α → α → α → α → α → Array α
-- Init.Data.List.Zip
List.zip_map_left : ∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {f : α → γ} {l₁ : List α} {l₂ : List β},
  (List.map f l₁).zip l₂ = List.map (Prod.map f id) (l₁.zip l₂)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.mapMulticospan_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F)
  (x : CategoryTheory.Limits.WalkingMulticospan E.multicospanShape),
  f.mapMulticospan.obj x =
    match x with
    | CategoryTheory.Limits.WalkingMulticospan.left i => CategoryTheory.Limits.WalkingMulticospan.left (f.s₀ i)
    | CategoryTheory.Limits.WalkingMulticospan.right i => CategoryTheory.Limits.WalkingMulticospan.right (f.s₁' i)
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_dvd_of_le_left : ∀ {E : Type v} [inst : Field E] {A B : Subfield E} (C : Subfield E), A ≤ B → B.relfinrank C ∣ A.relfinrank C
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- Given `h : CoreSmallCategoryOfSet Ω C`,
the obvious functor `h.smallCategoryOfSet.obj ⥤ C` is fully faithful.  -/
CategoryTheory.CoreSmallCategoryOfSet.fullyFaithfulFunctor : {Ω : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (h : CategoryTheory.CoreSmallCategoryOfSet Ω C) → h.functor.FullyFaithful
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.natAddLEFunctor_obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n k l : ℕ} (h : k + l ≤ n)
  (F : CategoryTheory.ComposableArrows C n) {X Y : Fin (l + 1)} (f : X ⟶ Y),
  ((CategoryTheory.ComposableArrows.natAddLEFunctor h).obj F).map f = F.map ((Fin.natAddLEFunctor h).map f)
-- Init.Data.Option.Lemmas
Option.filter_beq_self : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α] {p : α → Bool} {o : Option α}, (Option.filter p o == o) = Option.all p o
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewFact.eq.inj : ∀ {lhs rhs proof : Lean.Expr} {isHEq : Bool} {lhs_1 rhs_1 proof_1 : Lean.Expr} {isHEq_1 : Bool},
  Lean.Meta.Grind.NewFact.eq lhs rhs proof isHEq = Lean.Meta.Grind.NewFact.eq lhs_1 rhs_1 proof_1 isHEq_1 →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ proof = proof_1 ∧ isHEq = isHEq_1
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.le_linearGrowthInf_comp : ∀ {u : ℕ → EReal} {v : ℕ → ℕ},
  0 ≤ᶠ[Filter.atTop] u →
    Filter.Tendsto v Filter.atTop Filter.atTop →
      (LinearGrowth.linearGrowthInf fun n => ↑(v n)) * LinearGrowth.linearGrowthInf u ≤
        LinearGrowth.linearGrowthInf (u ∘ v)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- The equivalence relation on `M × S` where `(m1, s1) ≈ (m2, s2)` if and only if
for some (u : S), u * (s2 • m1 - s1 • m2) = 0  -/
LocalizedModule.r : {R : Type u} →
  [inst : CommSemiring R] →
    (S : Submonoid R) → (M : Type v) → [inst_1 : AddCommMonoid M] → [Module R M] → M × ↥S → M × ↥S → Prop
-- Mathlib.Order.Partition.Finpartition
Finpartition.part_surjOn : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s), Set.SurjOn P.part ↑s ↑P.parts
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.hasLeftResolutions_of_iso_of_essSurj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {W₁' : CategoryTheory.MorphismProperty D₁}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [R.functor.EssSurj] [W₂'.RespectsIso]
  (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor) [T.HasLeftResolutions], B.HasLeftResolutions
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainBotCoeff_eq_sSup : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    RootPairing.chainBotCoeff i j = sSup {k | P.root j - k • P.root i ∈ Set.range ⇑P.root}
-- Init.Data.Fin.Fold
/-- Folds a monadic function over `Fin n` from right to left, starting with `n-1`.

It is the sequence of steps:
```
Fin.foldrM n f xₙ = do
  let xₙ₋₁ ← f (n-1) xₙ
  let xₙ₋₂ ← f (n-2) xₙ₋₁
  ...
  let x₀ ← f 0 x₁
  pure x₀
```
 -/
Fin.foldrM : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → (n : ℕ) → (Fin n → α → m α) → α → m α
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The Gaussian distribution pdf integrates to 1 when the variance is not zero.  -/
ProbabilityTheory.integral_gaussianPDFReal_eq_one : ∀ (μ : ℝ) {v : NNReal}, v ≠ 0 → ∫ (x : ℝ), ProbabilityTheory.gaussianPDFReal μ v x = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getEntryGE?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryGE? k = t₂.getEntryGE? k
-- Std.Async.System
Std.Async.System.OSInfo.mk.injEq : ∀ (name release version machine name_1 release_1 version_1 machine_1 : String),
  ({ name := name, release := release, version := version, machine := machine } =
      { name := name_1, release := release_1, version := version_1, machine := machine_1 }) =
    (name = name_1 ∧ release = release_1 ∧ version = version_1 ∧ machine = machine_1)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- Two morphisms `T ⟶ T'` between distinguished triangles must coincide when
they coincide on the middle object, and there are integers `a ≤ b` such that
for a t-structure, we have `T.obj₁ ≤ a` and `T'.obj₃ ≥ b`.  -/
CategoryTheory.Triangulated.TStructure.triangle_map_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {T T' : CategoryTheory.Pretriangulated.Triangle C} {f₁ f₂ : T ⟶ T'},
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
      ∀ (a b : ℤ),
        t.IsLE T.obj₁ a →
          t.IsGE T'.obj₃ b →
            autoParam (f₁.hom₂ = f₂.hom₂) CategoryTheory.Triangulated.TStructure.triangle_map_ext._auto_1 →
              autoParam (a ≤ b) CategoryTheory.Triangulated.TStructure.triangle_map_ext._auto_3 → f₁ = f₂
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Endowing the space `WithLp p (α × β)` with the `L^p` pseudoemetric structure. This definition is
not satisfactory, as it does not register the fact that the topology and the uniform structure
coincide with the product one. Therefore, we do not register it as an instance. Using this as a
temporary pseudoemetric space instance, we will show that the uniform structure is equal (but not
defeq) to the product one, and then register an instance in which we replace the uniform structure
by the product one using this pseudoemetric space and `PseudoEMetricSpace.replaceUniformity`.  -/
WithLp.prodPseudoEMetricAux : (p : ENNReal) →
  (α : Type u_2) →
    (β : Type u_3) →
      [hp : Fact (1 ≤ p)] → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → PseudoEMetricSpace (WithLp p (α × β))
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableWithinAt.finsum_section_of_locallyFinite : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {u : Set B} {x₀ : B}
  {ι : Type u_9} {t : ι → (x : B) → E x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) →
    (∀ (i : ι), MDiffAt[u] (T% t) x₀) → (MDiffAt[u] fun x => ⟨x, ∑ᶠ (i : ι), t i x⟩) x₀
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
eq_one_of_one_le_mul_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : PartialOrder α] [MulLeftMono α] {a b : α},
  a ≤ 1 → b ≤ 1 → 1 ≤ a * b → a = 1
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- The sum of two functions `f g : ι → M` over finite sets `s₁ s₂ : Finset ι`
are equal if the functions agree on `s₁ ∩ s₂`, `f = 0` and `g = 0` on the respective
set differences.  -/
Finset.sum_congr_of_eq_on_inter : ∀ {ι : Type u_5} {M : Type u_6} {s₁ s₂ : Finset ι} {f g : ι → M} [inst : AddCommMonoid M],
  (∀ a ∈ s₁, a ∉ s₂ → f a = 0) →
    (∀ a ∈ s₂, a ∉ s₁ → g a = 0) → (∀ a ∈ s₁, a ∈ s₂ → f a = g a) → ∑ a ∈ s₁, f a = ∑ a ∈ s₂, g a
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.SheafedSpace C) {Y : TopCat}
  {f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace),
  AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U =
    CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U))
-- Std.Http.Data.Status
Std.Http.Status.continue.sizeOf_spec : sizeOf Std.Http.Status.continue = 1
-- Init.Control.State
instMonadStateOfStateTOfMonad : {σ : Type u} → {m : Type u → Type v} → [Monad m] → MonadStateOf σ (StateT σ m)
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_map : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory B]
  [inst_1 : CategoryTheory.Bicategory.IsLocallyDiscrete B] [inst_2 : CategoryTheory.Bicategory C] (obj : B → C)
  (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b'))
  (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b))
  (mapComp :
    {b₀ b₁ b₂ : B} →
      (f : b₀ ⟶ b₁) →
        (g : b₁ ⟶ b₂) →
          map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (map f) (map g))
  (map₂_associator :
    autoParam
      (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h))
              (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) =
          CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h))
              (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom))
      CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_1)
  (map₂_left_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f))
              (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_3)
  (map₂_right_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁))
              (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_5)
  {X Y : B} (a : X ⟶ Y),
  (CategoryTheory.oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor
          map₂_right_unitor).map
      a =
    map a
-- Init.Data.UInt.Lemmas
UInt32.ofFin_mk : ∀ {n : ℕ} (hn : n < UInt32.size), UInt32.ofFin ⟨n, hn⟩ = UInt32.ofNatLT n hn
-- Mathlib.LinearAlgebra.Determinant
/-- If a basis is multiplied columnwise by scalars `w : ι → Rˣ`, then the determinant with respect
to this basis is multiplied by the product of the inverse of these scalars.  -/
Module.Basis.det_unitsSMul : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Module.Basis ι R M) (w : ι → Rˣ),
  (e.unitsSMul w).det = ↑(∏ i, w i)⁻¹ • e.det
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.ofIsoI_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.MonoFactorisation f) {I' : C} (e : F.I ≅ I'), (F.ofIsoI e).I = I'
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.add_apply : ∀ {α : Type u_1} {_m : MeasurableSpace α} (μ₁ μ₂ : MeasureTheory.Measure α) (s : Set α), (μ₁ + μ₂) s = μ₁ s + μ₂ s
-- Mathlib.Data.List.Infix
List.IsSuffix.flatten : ∀ {α : Type u_1} {l₁ l₂ : List (List α)}, l₁ <:+ l₂ → l₁.flatten <:+ l₂.flatten
-- Mathlib.Data.ENNReal.Operations
ENNReal.biSup_add_biSup_le' : ∀ {ι : Sort u_1} {κ : Sort u_2} {f : ι → ENNReal} {a : ENNReal} {p : ι → Prop} {q : κ → Prop},
  (∃ i, p i) →
    (∃ j, q j) →
      ∀ {g : κ → ENNReal},
        (∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a) → (⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a
-- Init.Data.Slice.Lemmas
Std.Slice.length_toListRev_eq_size : ∀ {γ : Type u} {α β : Type v} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  {s : Std.Slice γ} [inst_2 : Std.IteratorLoop α Id Id] [inst_3 : Std.Slice.SliceSize γ] [Std.Slice.LawfulSliceSize γ]
  [Std.Iterators.Finite α Id] [Std.LawfulIteratorLoop α Id Id], s.toListRev.length = s.size
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_filterMap_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.isEmpty = true ↔
    ∀ (k : α) (h : Std.DTreeMap.Internal.Impl.contains k t = true), f k (t.get k h) = none
-- Mathlib.Algebra.Order.Archimedean.Basic
add_one_pow_unbounded_of_pos : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {y : R} (x : R),
  0 < y → ∃ n, x < (y + 1) ^ n
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalAddGroup.exist_openAddSubgroup_sub_clopen_nhds_of_zero : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G]
  {W : Set G}, IsClopen W → 0 ∈ W → ∃ H, ↑H ⊆ W
-- Mathlib.Algebra.Order.Hom.Ring
/-- The identity as an ordered ring homomorphism.  -/
OrderRingHom.id : (α : Type u_2) → [inst : NonAssocSemiring α] → [inst_1 : Preorder α] → α →+*o α