mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.BifunctorHomotopy
/-- Auxiliary definition for `mapBifunctorMapHomotopy₂`.  -/
HomologicalComplex.mapBifunctorMapHomotopy.hom₂ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      {I₁ : Type u_4} →
        {I₂ : Type u_5} →
          {J : Type u_6} →
            [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.Preadditive C₁] →
                    [inst_4 : CategoryTheory.Preadditive C₂] →
                      [inst_5 : CategoryTheory.Preadditive D] →
                        {c₁ : ComplexShape I₁} →
                          {c₂ : ComplexShape I₂} →
                            {K₁ L₁ : HomologicalComplex C₁ c₁} →
                              (K₁ ⟶ L₁) →
                                {K₂ L₂ : HomologicalComplex C₂ c₂} →
                                  {f₂ f₂' : K₂ ⟶ L₂} →
                                    Homotopy f₂ f₂' →
                                      (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                        [inst_6 : F.Additive] →
                                          [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] →
                                            (c : ComplexShape J) →
                                              [inst_8 : DecidableEq J] →
                                                [inst_9 : TotalComplexShape c₁ c₂ c] →
                                                  [inst_10 : K₁.HasMapBifunctor K₂ F c] →
                                                    [inst_11 : L₁.HasMapBifunctor L₂ F c] →
                                                      (j j' : J) →
                                                        (K₁.mapBifunctor K₂ F c).X j ⟶ (L₁.mapBifunctor L₂ F c).X j'
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k fallback : α}, (List.map Prod.fst l).contains k = false → (Std.HashMap.Raw.ofList l).getKeyD k fallback = fallback
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The strictly positive cone of an ordered module is always salient.  -/
ConvexCone.salient_strictlyPositive : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup M]
  [inst_3 : PartialOrder M] [inst_4 : IsOrderedAddMonoid M] [inst_5 : Module R M] [inst_6 : PosSMulStrictMono R M],
  (ConvexCone.strictlyPositive R M).Salient
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
/-- (Implementation): If `M = R^ι` and `ι` is finite, we may construct an inverse to
`ofTensorProduct I (ι → R)`.  -/
AdicCompletion.ofTensorProductInvOfPiFintype : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (ι : Type u_4) →
        [Fintype ι] →
          [DecidableEq ι] → AdicCompletion I (ι → R) ≃ₗ[AdicCompletion I R] TensorProduct R (AdicCompletion I R) (ι → R)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_rightUnitor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (g : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom =
    f
-- Mathlib.Data.EReal.Operations
EReal.coe_sub : ∀ (x y : ℝ), ↑(x - y) = ↑x - ↑y
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Real.continuousAt_rpow_of_ne : ∀ (p : ℝ × ℝ), p.1 ≠ 0 → ContinuousAt (fun p => p.1 ^ p.2) p
-- Mathlib.CategoryTheory.IsConnected
/-- A possibly empty category for which every functor to a discrete category is constant.
 -/
CategoryTheory.IsPreconnected.iso_constant : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} [self : CategoryTheory.IsPreconnected J] {α : Type u₁}
  (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j : J),
  Nonempty (F ≅ (CategoryTheory.Functor.const J).obj (F.obj j))
-- Mathlib.Logic.Basic
Iff.ne : ∀ {α : Sort u_1} {β : Sort u_2} {a b : α} {c d : β}, (a = b ↔ c = d) → (a ≠ b ↔ c ≠ d)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.Const.ofList l cmp) k = none
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_of_contains_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k : α},
  (Std.ExtDTreeMap.map f t).contains k = true → t.contains k = true
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.HasUnifEigenvector.hasUnifEigenvalue : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ∞} {x : M}, f.HasUnifEigenvector μ k x → f.HasUnifEigenvalue μ k
-- Mathlib.Data.Fin.SuccPred
Fin.castSucc_pos_iff : ∀ {n : ℕ} [inst : NeZero n] {i : Fin n}, 0 < i.castSucc ↔ 0 < i
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.swapTR.go.match_1.eq_4 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Array α → Sort u_2) (a : α) (xs : List α) (i : ℕ) (acc : Array α)
  (h_1 : (x x_1 : ℕ) → (x_2 : Array α) → motive [] x x_1 x_2)
  (h_2 : (head : α) → (tail : List α) → (x : Array α) → motive (head :: tail) 0 0 x)
  (h_3 : (a : α) → (xs : List α) → (i : ℕ) → (acc : Array α) → motive (a :: xs) 0 i.succ acc)
  (h_4 : (a : α) → (xs : List α) → (i : ℕ) → (acc : Array α) → motive (a :: xs) i.succ 0 acc)
  (h_5 : (a : α) → (xs : List α) → (i j : ℕ) → (acc : Array α) → motive (a :: xs) i.succ j.succ acc),
  (match a :: xs, i.succ, 0, acc with
    | [], x, x_1, x_2 => h_1 x x_1 x_2
    | head :: tail, 0, 0, x => h_2 head tail x
    | a :: xs, 0, i.succ, acc => h_3 a xs i acc
    | a :: xs, i.succ, 0, acc => h_4 a xs i acc
    | a :: xs, i.succ, j.succ, acc => h_5 a xs i j acc) =
    h_4 a xs i acc
-- Mathlib.Data.ZMod.Basic
ZMod.val_mul_iff_lt : ∀ {n : ℕ} [NeZero n] (a b : ZMod n), (a * b).val = a.val * b.val ↔ a.val * b.val < n
-- Mathlib.RingTheory.Localization.Ideal
Module.IsTorsionFree.of_isLocalization : ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain R]
  [IsDomain S] {Rₚ : Type u_3} {Sₚ : Type u_4} [inst_5 : CommRing Rₚ] [IsDomain Rₚ] [inst_7 : CommRing Sₚ]
  [inst_8 : Algebra R Rₚ] [inst_9 : Algebra R Sₚ] [inst_10 : Algebra S Sₚ] [inst_11 : Algebra Rₚ Sₚ]
  [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] {M : Submonoid R},
  M ≤ nonZeroDivisors R →
    ∀ [IsLocalization M Rₚ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [Module.IsTorsionFree R S],
      Module.IsTorsionFree Rₚ Sₚ
-- Init.Data.Range.Polymorphic.Basic
/-- If the smallest value in the range satisfies the upper bound and has a successor, the size is
  one larger than the size of the range starting at the successor.  -/
Std.Rxi.LawfulHasSize.size_eq_succ_of_succ?_eq_some : ∀ {α : Type u} {inst : Std.PRange.UpwardEnumerable α} {inst_1 : Std.Rxi.HasSize α} [self : Std.Rxi.LawfulHasSize α]
  (lo lo' : α), Std.PRange.succ? lo = some lo' → Std.Rxi.HasSize.size lo = Std.Rxi.HasSize.size lo' + 1
-- Mathlib.Combinatorics.Additive.SmallTripling
/-- If `A` has small tripling, say with constant `K`, then `A` has small alternating powers, in the
sense that `|±A ± ... ± A|` is at most `|A|` times a constant exponential in the number of
terms in the product.

When `A` is symmetric (`-A = A`), the base of the exponential can be lowered from `K ^ 3` to `K`,
where `K` is the tripling constant. See `Finset.small_nsmul_of_small_tripling`.  -/
Finset.small_alternating_nsmul_of_small_tripling : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] {A : Finset G} {K : ℝ} {m : ℕ},
  3 ≤ m →
    ↑(3 • A).card ≤ K * ↑A.card →
      ∀ (ε : Fin m → ℤ),
        (∀ (i : Fin m), |ε i| = 1) →
          ↑(List.map (fun i => ε i • A) (List.finRange m)).sum.card ≤ K ^ (3 * (m - 2)) * ↑A.card
-- Mathlib.Algebra.Quaternion
Quaternion.equivTuple_apply : ∀ (R : Type u_1) [inst : Zero R] [inst_1 : One R] [inst_2 : Neg R] (x : Quaternion R),
  (Quaternion.equivTuple R) x = ![x.re, x.imI, x.imJ, x.imK]
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multicospan_obj_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (b : J.R),
  I.multicospan.obj (CategoryTheory.Limits.WalkingMulticospan.right b) = I.right b
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_zero' : ∀ (α : Type u_1) (G : Type u_5) [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α}, MeasureTheory.integral μ 0 = 0
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `MultipliableLocallyUniformly f` means that the product `∏' i, f i b` converges locally
uniformly to something.  -/
MultipliableLocallyUniformly : {α : Type u_1} →
  {β : Type u_2} → {ι : Type u_3} → [CommMonoid α] → (ι → β → α) → [UniformSpace α] → [TopologicalSpace β] → Prop
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mrange_comp : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {O : Type u_5} [inst_2 : MulOneClass O]
  (f : N →* O) (g : M →* N), MonoidHom.mrange (f.comp g) = Submonoid.map f (MonoidHom.mrange g)
-- Init.Data.Nat.Bitwise.Basic
Nat.shiftRight_eq_zero : ∀ (m n : ℕ), m < 2 ^ n → m >>> n = 0
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- For an open immersion `f : X ⟶ Y` and an open set `U ⊆ X`, we have the map `X(U) ⟶ Y(U)`.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : AlgebraicGeometry.PresheafedSpace C} →
      (f : X ⟶ Y) →
        [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] →
          (U : TopologicalSpace.Opens ↑↑X) →
            X.presheaf.obj (Opposite.op U) ⟶
              Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj U))
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Canon.State.mk.injEq : ∀ (cache cacheInType cache_1 cacheInType_1 : Std.HashMap Lean.Expr Lean.Expr),
  ({ cache := cache, cacheInType := cacheInType } = { cache := cache_1, cacheInType := cacheInType_1 }) =
    (cache = cache_1 ∧ cacheInType = cacheInType_1)
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.proetaleTopology_le_fpqcTopology : AlgebraicGeometry.Scheme.proetaleTopology ≤ AlgebraicGeometry.Scheme.fpqcTopology
-- Mathlib.GroupTheory.Index
Subgroup.not_finiteIndex_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, ¬H.FiniteIndex ↔ H.index = 0
-- Init.Data.SInt.Lemmas
Int16.sub_eq_iff_eq_add : ∀ {a b c : Int16}, a - b = c ↔ a = c + b
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.irreducible_p : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], Irreducible ↑p
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquash.mk'.injEq : ∀ {α : Type v} [small : Std.Internal.Small α] (inner inner_1 : Std.Internal.ComputableSmall.Target α),
  ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
/-- The indicators of closed δ-thickenings of a set tend pointwise to the indicator
of the set, as δ tends to zero.  -/
tendsto_indicator_cthickening_indicator_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
  (f : α → β) (E : Set α),
  Filter.Tendsto (fun δ => (Metric.cthickening δ E).indicator f) (nhds 0) (nhds ((closure E).indicator f))
-- Mathlib.Topology.Connected.LocallyPathConnected
pathComponent_eq_connectedComponent : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] (x : X),
  pathComponent x = connectedComponent x
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜},
  x ∈ s → UniqueDiffOn 𝕜 s → iteratedDerivWithin n id s x = if n = 0 then x else if n = 1 then 1 else 0
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.sub_fst : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : AddCommGroup β]
  (x y : WithLp p (α × β)), (x - y).fst = x.fst - y.fst
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
tateComplex_d_neg_one : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] (M : Rep.{u, u, u} R G),
  (tateComplex M).d (-1) 0 = M.tateNorm
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The morphism from `K.opcycles i` that is induced by an "opcycle", i.e. a morphism
from `K.X i` whose precomposition with the differential is zero.  -/
HomologicalComplex.descOpcycles' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            {i : ι} →
              [inst_2 : K.HasHomology i] →
                {A : C} →
                  (k : K.X i ⟶ A) →
                    (j : ι) → c.Rel j i → CategoryTheory.CategoryStruct.comp (K.d j i) k = 0 → (K.opcycles i ⟶ A)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.head.eq_1 : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl), ms.head = Stream'.Seq.head ms
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxi.Iterator.instIteratorLoop.match_1.splitter : {α : Type u_1} →
  [inst : Std.PRange.UpwardEnumerable α] →
    {n : Type u_1 → Type u_3} →
      (γ : Type u_1) →
        (Pl : α → γ → ForInStep γ → Prop) →
          (motive :
              (it : Std.IterM Id α) →
                ((b : α) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) → Sort u_2) →
            (it : Std.IterM Id α) →
              (f : (b : α) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) →
                ((next : α) →
                    (f :
                        (b : α) →
                          { internalState := { next := some next } }.IsPlausibleIndirectOutput b →
                            (c : γ) → n (Subtype (Pl b c))) →
                      motive { internalState := { next := some next } } f) →
                  ((f :
                        (b : α) →
                          { internalState := { next := none } }.IsPlausibleIndirectOutput b →
                            (c : γ) → n (Subtype (Pl b c))) →
                      motive { internalState := { next := none } } f) →
                    motive it f
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- We can prove two cone points `(s : Cone F).pt` and `(t : Cone G).pt` are isomorphic if
* both cones are limit cones
* their indexing categories are equivalent via some `e : J ≌ K`,
* the triangle of functors commutes up to a natural isomorphism: `e.functor ⋙ G ≅ F`.

This is the most general form of uniqueness of cone points,
allowing relabelling of both the indexing category (up to equivalence)
and the functor (up to natural isomorphism).
 -/
CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {s : CategoryTheory.Limits.Cone F} →
                {G : CategoryTheory.Functor K C} →
                  {t : CategoryTheory.Limits.Cone G} →
                    CategoryTheory.Limits.IsLimit s →
                      CategoryTheory.Limits.IsLimit t → (e : J ≌ K) → (e.functor.comp G ≅ F) → (s.pt ≅ t.pt)
-- Mathlib.Algebra.Group.Finsupp
Finsupp.instSub : {ι : Type u_1} → {G : Type u_6} → [inst : SubNegZeroMonoid G] → Sub (ι →₀ G)
-- Lean.Elab.Command
Lean.Elab.Command.getLevelNames : Lean.Elab.Command.CommandElabM (List Lean.Name)
-- Mathlib.Data.Nat.Nth
Nat.lt_card_toFinset_of_nth_ne_zero : ∀ {p : ℕ → Prop} {n : ℕ}, Nat.nth p n ≠ 0 → ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- **Alias** of `continuousWithinAt_toIcoMod_Ici`.

---

`toIcoMod` is continuous on the right at every point.  -/
continuous_right_toIcoMod : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜),
  ContinuousWithinAt (toIcoMod hp a) (Set.Ici x) x
-- Mathlib.Analysis.Normed.Module.Bases
SchauderBasis.RankOneDecomposition.mk.injEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (P : ℕ → X →L[𝕜] X) (e : ℕ → X) (proj_zero : P 0 = 0)
  (finrank_range : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n)
  (proj_comp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x)
  (proj_tendsto : ∀ (x : X), Filter.Tendsto (fun n => (P n) x) Filter.atTop (nhds x))
  (e_mem_range : ∀ (n : ℕ), e n ∈ (↑(SchauderBasis.succSub P n)).range) (e_ne_zero : ∀ (n : ℕ), e n ≠ 0)
  (P_1 : ℕ → X →L[𝕜] X) (e_1 : ℕ → X) (proj_zero_1 : P_1 0 = 0)
  (finrank_range_1 : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P_1 n)).range = n)
  (proj_comp_1 : ∀ (n m : ℕ) (x : X), (P_1 n) ((P_1 m) x) = (P_1 (min n m)) x)
  (proj_tendsto_1 : ∀ (x : X), Filter.Tendsto (fun n => (P_1 n) x) Filter.atTop (nhds x))
  (e_mem_range_1 : ∀ (n : ℕ), e_1 n ∈ (↑(SchauderBasis.succSub P_1 n)).range) (e_ne_zero_1 : ∀ (n : ℕ), e_1 n ≠ 0),
  ({ P := P, e := e, proj_zero := proj_zero, finrank_range := finrank_range, proj_comp := proj_comp,
        proj_tendsto := proj_tendsto, e_mem_range := e_mem_range, e_ne_zero := e_ne_zero } =
      { P := P_1, e := e_1, proj_zero := proj_zero_1, finrank_range := finrank_range_1, proj_comp := proj_comp_1,
        proj_tendsto := proj_tendsto_1, e_mem_range := e_mem_range_1, e_ne_zero := e_ne_zero_1 }) =
    (P = P_1 ∧ e = e_1)
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
/-- If `F` preserves the initial object and binary coproducts, then it preserves colimits of shape
`Discrete (Fin n)`.
 -/
CategoryTheory.preservesShape_fin_of_preserves_binary_and_initial : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F]
  [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ),
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete (Fin n)) F
-- Std.Async.Basic
/-- Similar to `bind`, however `f` has access to the `EIO` monad. If `f` throws an error, the returned
`ETask` resolves to that error.
 -/
Std.Async.ETask.bindEIO : {ε α β : Type} →
  Std.Async.ETask ε α →
    (α → EIO ε (Std.Async.ETask ε β)) →
      optParam Task.Priority Task.Priority.default → optParam Bool false → EIO ε (Std.Async.ETask ε β)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.notMem_range_coe_iff : ∀ {X : Type u_1} {x : OnePoint X}, x ∉ Set.range OnePoint.some ↔ x = OnePoint.infty
-- Init.Data.UInt.Basic
instMulUInt16 : Mul UInt16
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.find?_some_mem : ∀ {α : Type u_1} {cut : α → Ordering} {x : α} {t : RBTree.RBNode α}, x ∈ RBTree.RBNode.find? cut t → x ∈ t
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.instEssSurjCompPreRight : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T)
  (L : CategoryTheory.Functor A T) [F.EssSurj], (CategoryTheory.Comma.preRight L F R).EssSurj
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.instIsGoodSymmOfRespectsIsoCofibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [P.IsGood] [(HomotopicalAlgebra.cofibrations C).RespectsIso], P.symm.IsGood
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1_of_aestronglyMeasurable' : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] {f : α → F'}
  [CompleteSpace F'],
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.Integrable f μ → ↑↑(MeasureTheory.condExpL1 hm μ f) =ᵐ[μ] f
-- Mathlib.Tactic.Coe
/-- Partially applied type coercion.  Equivalent to the η-reduction of `(↥ ·)`  -/
Lean.Elab.Term.CoeImpl.«term(↥)» : Lean.ParserDescr
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.isMulCommutative_toNonUnitalSubalgebra : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] (S : NonUnitalStarSubalgebra R A) [IsMulCommutative ↥S],
  IsMulCommutative ↥S.toNonUnitalSubalgebra
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.instCategory : CategoryTheory.Category.{u, u + 1} FinBddDistLat
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.instAddHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M₁ M₂ : PresheafOfModules R} → Add (M₁ ⟶ M₂)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.norm_seminormedAddCommGroupToPi : ∀ (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) [inst : Fact (1 ≤ p)] [inst_1 : Fintype ι]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (α i)] (x : (i : ι) → α i), ‖x‖ = ‖WithLp.toLp p x‖
-- Mathlib.LinearAlgebra.Basis.Fin
Module.Basis.coe_mkFinCons : ∀ {R : Type u_3} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ}
  {N : Submodule R M} (y : M) (b : Module.Basis (Fin n) R ↥N) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0)
  (hsp : ∀ (z : M), ∃ c, z + c • y ∈ N), ⇑(Module.Basis.mkFinCons y b hli hsp) = Fin.cons y (Subtype.val ∘ ⇑b)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited α] {f : α → β → Option γ} {k : α},
  (Std.DTreeMap.filterMap f t).getKey! k =
    ((t.getKey? k).pfilter fun x h' => (f x (Std.DTreeMap.Const.get t x ⋯)).isSome).get!
-- Lean.Environment
_private.Lean.Environment.0.Lean.setImportedEntries.unsafe_impl_2 : Array Lean.ModuleData →
  Lean.PersistentEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState →
    Array Lean.EnvExtensionState → Array Lean.EnvExtensionState
-- Mathlib.Data.Rat.Floor
Rat.isRat_intFract_of_isRat_negOfNat : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (r : α)
  (n d : ℕ), Mathlib.Meta.NormNum.IsRat r (Int.negOfNat n) d → Mathlib.Meta.NormNum.IsRat (Int.fract r) (-↑n % ↑d) d