mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Consumers.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Collect.0.Std.Iter.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.mk'.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α]
  [inst_3 : (a : α) → SizeOf (β a)] (inner : Quotient (Std.DHashMap.isSetoid α β)),
  sizeOf { inner := inner } = 1 + sizeOf inner
-- Lean.Declaration
Lean.OpaqueVal.mk.sizeOf_spec : ∀ (toConstantVal : Lean.ConstantVal) (value : Lean.Expr) (isUnsafe : Bool) (all : List Lean.Name),
  sizeOf { toConstantVal := toConstantVal, value := value, isUnsafe := isUnsafe, all := all } =
    1 + sizeOf toConstantVal + sizeOf value + sizeOf isUnsafe + sizeOf all
-- Mathlib.CategoryTheory.Monoidal.Limits.Colimits
CategoryTheory.Limits.Cocone.tensor_ι_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {J : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} J] {F₁ F₂ : CategoryTheory.Functor J C}
  (c₁ : CategoryTheory.Limits.Cocone F₁) (c₂ : CategoryTheory.Limits.Cocone F₂) (j : J),
  (c₁.tensor c₂).ι.app j = CategoryTheory.MonoidalCategoryStruct.tensorHom (c₁.ι.app j) (c₂.ι.app j)
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Given a set of `AbsoluteLspSemanticToken`, computes the LSP `SemanticTokens` data with
token-relative positioning.
See https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_semanticTokens.
 -/
Lean.Server.FileWorker.computeDeltaLspSemanticTokens : Array Lean.Server.FileWorker.AbsoluteLspSemanticToken → Lean.Lsp.SemanticTokens
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_lt_rpow_of_exponent_gt : ∀ {x : NNReal} {y z : ℝ}, 0 < x → x < 1 → z < y → x ^ y < x ^ z
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_whisker_left : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
  self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η) =
    CategoryTheory.CategoryStruct.comp (self.mapComp f g).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η))
        (self.mapComp f h).inv)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.State : Type
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_filterMap!_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {f : α → β → Option γ},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filterMap! f t).isEmpty = true ↔
      ∀ (k : α) (h : Std.DTreeMap.Internal.Impl.contains k t = true),
        f (t.getKey k h) (Std.DTreeMap.Internal.Impl.Const.get t k h) = none)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Sigma.map_mono : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) [∀ (j : J), CategoryTheory.Mono (p j)],
  CategoryTheory.Mono (CategoryTheory.Limits.Sigma.map p)
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.ext_iff : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {f g : Q₁ →qᵢ Q₂},
  f = g ↔ ∀ (x : M₁), f x = g x
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestRevMatchAt_iff : ∀ {c : Char} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt c pos pos' ↔
    ∃ (h : pos' ≠ s.startPos), pos = pos'.prev h ∧ (pos'.prev h).get ⋯ = c
-- Mathlib.Order.OmegaCompletePartialOrder
Prod.ωSup_snd : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (c : OmegaCompletePartialOrder.Chain (α × β)),
  (OmegaCompletePartialOrder.ωSup c).2 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.snd)
-- Mathlib.Analysis.InnerProductSpace.Calculus
DifferentiableWithinAt.norm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E}
  {s : Set G} {x : G}, DifferentiableWithinAt ℝ f s x → f x ≠ 0 → DifferentiableWithinAt ℝ (fun y => ‖f y‖) s x
-- Mathlib.CategoryTheory.Galois.Equivalence
/-- Any fiber functor `F` induces an equivalence of categories with the category of finite and
discrete `Aut F`-sets.  -/
CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatFunObjFiniteAutFunctorFunctorToContAction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  (CategoryTheory.PreGaloisCategory.functorToContAction F).IsEquivalence
-- Lean.Meta.Tactic.Grind.Types
/-- Number of times a `cases` has been performed on an inductive type/predicate  -/
Lean.Meta.Grind.Counters.case : Lean.Meta.Grind.Counters → Lean.PHashMap Lean.Name ℕ
-- Mathlib.Condensed.Discrete.Basic
/-- A version of `LightCondensed.discrete` in the `LightCondSet` namespace  -/
LightCondSet.discrete : CategoryTheory.Functor (Type u) (LightCondensed (Type u))
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The structure sheaf (valued in `Type`, not yet `CommRingCat`) is the subsheaf consisting of
functions satisfying `isLocallyFraction`.  -/
AlgebraicGeometry.structureSheafInType : (R M : Type u) →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] → [Module R M] → TopCat.Sheaf (Type u) (AlgebraicGeometry.PrimeSpectrum.Top R)
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
/-- Given a cell `γ` in a relative cell complex, this is the corresponding
index in the family of morphisms `basicCell γ.j`.  -/
HomotopicalAlgebra.RelativeCellComplex.Cells.i : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          [inst_3 : SuccOrder J] →
            [inst_4 : WellFoundedLT J] →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} →
                    {X Y : C} →
                      {f : X ⟶ Y} → {c : HomotopicalAlgebra.RelativeCellComplex basicCell f} → (γ : c.Cells) → α γ.j
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDerivWithin_scomp_two : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {g : 𝕜 → E} {f : 𝕜 → 𝕜} {s t : Set 𝕜} {x : 𝕜},
  ContDiffWithinAt 𝕜 2 g t (f x) →
    ContDiffWithinAt 𝕜 2 f s x →
      UniqueDiffOn 𝕜 t →
        UniqueDiffOn 𝕜 s →
          x ∈ s →
            Set.MapsTo f s t →
              iteratedDerivWithin 2 (g ∘ f) s x =
                derivWithin f s x ^ 2 • iteratedDerivWithin 2 g t (f x) +
                  iteratedDerivWithin 2 f s x • derivWithin g t (f x)
-- Mathlib.Order.Category.PartOrd
PartOrd.of.injEq : ∀ (carrier : Type u_1) [str : PartialOrder carrier] (carrier_1 : Type u_1) (str_1 : PartialOrder carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.shortComplexObj_X₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C) (X : C), (Φ.shortComplexObj X).X₃ = Φ.quotient.obj X
-- Lean.Parser.Command
Lean.Parser.Command.visibility : Lean.Parser.Parser
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instLeftCancelSemigroup.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : LeftCancelSemigroup M],
  Filter.Germ.instLeftCancelSemigroup = { toSemigroup := Filter.Germ.instSemigroup, toIsLeftCancelMul := ⋯ }
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α},
  k ∈ Std.ExtHashMap.unitOfList l ↔ l.contains k = true
-- Mathlib.RepresentationTheory.Action
/-- This a type-changing equivalence to avoid abusing defeq.  -/
Representation.linearizeDiagonalEquiv : (k : Type u) →
  (G : Type v) →
    [inst : Monoid G] →
      [inst_1 : Semiring k] →
        (n : ℕ) → (Representation.linearize k G (Action.diagonal G n)).Equiv (Representation.diagonal k G n)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- An identity open partial homeomorphism belongs to the `C^n` groupoid.  -/
ofSet_mem_contDiffGroupoid : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {s : Set H}
  (hs : IsOpen s), OpenPartialHomeomorph.ofSet s hs ∈ contDiffGroupoid n I
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj : ∀ (D : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} D] {X Y : CategoryTheory.Cat} (F : X ⟶ Y)
  (X_1 : CategoryTheory.Join (↑X) D),
  ((CategoryTheory.Join.pseudofunctorLeft D).map F).toFunctor.obj X_1 =
    match X_1 with
    | CategoryTheory.Join.left x => CategoryTheory.Join.left (F.toFunctor.obj x)
    | CategoryTheory.Join.right x => CategoryTheory.Join.right x
-- Mathlib.Algebra.DirectSum.Ring
/-- The canonical map from ℤ to a graded ring extends the canonical map from ℕ to the underlying
graded semiring.  -/
DirectSum.GRing.intCast_ofNat : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddMonoid ι} {inst_1 : (i : ι) → AddCommGroup (A i)}
  [self : DirectSum.GRing A] (n : ℕ), DirectSum.GRing.intCast ↑n = DirectSum.GSemiring.natCast n
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkMDataS : {m : Type → Type} → [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.MData → Lean.Expr → m Lean.Expr
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂_isIso : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g : a ⟶ b} (η : f ⟶ g) [CategoryTheory.IsIso η],
  CategoryTheory.IsIso (F.map₂ η)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_balanceRErase : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size},
  (Std.DTreeMap.Internal.Impl.balanceRErase k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {Z : C} (h : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.homologyIsoImageICyclesCompPOpcycles.hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)) h) =
    CategoryTheory.CategoryStruct.comp S.homologyι h
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKey?_alterKey_eq_self : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {f : Option β → Option β} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.minKey? (Std.Internal.List.Const.alterKey k f l) = some k ↔
      (f (Std.Internal.List.getValue? k l)).isSome = true ∧
        ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Const.alterKey.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (v : β) (h_1 : Unit → motive none) (h_2 : (v : β) → motive (some v)),
  (match some v with
    | none => h_1 ()
    | some v => h_2 v) =
    h_2 v
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonWindowClientCapabilities.toJson : Lean.Lsp.WindowClientCapabilities → Lean.Json
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instZeroHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → (G H : CategoryTheory.AddGrp C) → Zero (G ⟶ H)
-- Std.Internal.Parsec.String
/-- Parse an ASCII letter `a-z` or `A-Z` as a `Char`.
 -/
Std.Internal.Parsec.String.asciiLetter : Std.Internal.Parsec.String.Parser Char
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- `P.IsStableUnderBaseChangeAlong f` states that for any morphism satisfying `P` with the same
codomain as `f`, any pullback of that morphism along `f` also satisfies `P`.  -/
CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlong : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → {X Y : C} → (X ⟶ Y) → Prop
-- Mathlib.Computability.StateTransition
StateTransition.EvalsToInTime.mk.injEq : ∀ {σ : Type u_1} {f : σ → Option σ} {a : σ} {b : Option σ} {m : ℕ} (toEvalsTo : StateTransition.EvalsTo f a b)
  (steps_le_m : toEvalsTo.steps ≤ m) (toEvalsTo_1 : StateTransition.EvalsTo f a b)
  (steps_le_m_1 : toEvalsTo_1.steps ≤ m),
  ({ toEvalsTo := toEvalsTo, steps_le_m := steps_le_m } = { toEvalsTo := toEvalsTo_1, steps_le_m := steps_le_m_1 }) =
    (toEvalsTo = toEvalsTo_1)
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.Pivot.listTransvecRow_getElem : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) {i : ℕ}
  (h : i < (Matrix.Pivot.listTransvecRow M).length),
  (Matrix.Pivot.listTransvecRow M)[i] =
    Matrix.transvection (Sum.inr ()) (Sum.inl ⟨i, ⋯⟩) (-M (Sum.inr ()) (Sum.inl ⟨i, ⋯⟩) / M (Sum.inr ()) (Sum.inr ()))
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff_inj : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x y : M →₀ R},
  AddMonoidAlgebra.ofCoeff x = AddMonoidAlgebra.ofCoeff y ↔ x = y
-- Mathlib.Data.Finset.Sups
Finset.card_sups_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] (s t : Finset α), (s ⊻ t).card ≤ s.card * t.card
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductLimit_lift : ∀ (X Y : Type u) (s : CategoryTheory.Limits.BinaryFan X Y),
  (CategoryTheory.Limits.Types.binaryProductLimit X Y).lift s =
    TypeCat.ofHom fun x =>
      ((CategoryTheory.ConcreteCategory.hom s.fst) x, (CategoryTheory.ConcreteCategory.hom s.snd) x)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.Equiv.beq_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : BEq β] {m₃ m₄ : Std.DHashMap.Raw α fun x => β},
  m₁.WF →
    m₂.WF →
      m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → Std.DHashMap.Raw.Const.beq m₁ m₂ = Std.DHashMap.Raw.Const.beq m₃ m₄
-- Mathlib.Topology.Algebra.Order.Support
HasCompactMulSupport.inf : ∀ {X : Type u_1} {M : Type u_2} [inst : TopologicalSpace X] [inst_1 : One M] [inst_2 : SemilatticeInf M] {f g : X → M},
  HasCompactMulSupport f → HasCompactMulSupport g → HasCompactMulSupport (f ⊓ g)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigOWith_pi : ∀ {α : Type u_1} {F' : Type u_7} [inst : SeminormedAddCommGroup F'] {g' : α → F'} {l : Filter α} {ι : Type u_17}
  [inst_1 : Fintype ι] {E' : ι → Type u_18} [inst_2 : (i : ι) → SeminormedAddCommGroup (E' i)] {f : α → (i : ι) → E' i}
  {C : ℝ}, 0 ≤ C → (Asymptotics.IsBigOWith C l f g' ↔ ∀ (i : ι), Asymptotics.IsBigOWith C l (fun x => f x i) g')
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.mem_map_of_mem : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) {K : AddSubgroup G} {x : G},
  x ∈ K → f x ∈ AddSubgroup.map f K
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofDelabTermInfo : Lean.Elab.DelabTermInfo → Lean.Elab.Info
-- Mathlib.Topology.Algebra.Module.Equiv
/-- If `I` and `J` are complementary index sets, the product of the kernels of the `J`th projections
of `φ` is linearly equivalent to the product over `I`.  -/
ContinuousLinearMap.iInfKerProjEquiv : (R : Type u_1) →
  [inst : Semiring R] →
    {ι : Type u_4} →
      (φ : ι → Type u_5) →
        [inst_1 : (i : ι) → TopologicalSpace (φ i)] →
          [inst_2 : (i : ι) → AddCommMonoid (φ i)] →
            [inst_3 : (i : ι) → Module R (φ i)] →
              {I J : Set ι} →
                [DecidablePred fun i => i ∈ I] →
                  Disjoint I J →
                    Set.univ ⊆ I ∪ J → ↥(⨅ i ∈ J, (↑(ContinuousLinearMap.proj i)).ker) ≃L[R] (i : ↑I) → φ ↑i
-- Mathlib.Order.Interval.Set.Defs
Set.mem_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, x ∈ Set.Ioo a b ↔ a < x ∧ x < b
-- Mathlib.Data.PNat.Defs
PNat.pos : ∀ (n : ℕ+), 0 < ↑n
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.coe_deleteEdges_le : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)), (G'.deleteEdges s).coe ≤ G'.coe
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- A pseudometric space is totally bounded if one can reconstruct up to any ε>0 any element of the
space from finitely many data.  -/
Metric.totallyBounded_of_finite_discretization : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
  (∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε) → TotallyBounded s
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_codRestrict : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {S : Type u_8} [inst_2 : SetLike S N]
  [inst_3 : AddSubmonoidClass S N] (f : G →+ N) (s : S) (h : ∀ (x : G), f x ∈ s), (f.codRestrict s h).ker = f.ker
-- Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
LieHom.toNonUnitalAlgHom_toFun : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (a : L), f.toNonUnitalAlgHom a = f a
-- Init.Prelude
/-- `Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array) with elements
from `α`. This type has special support in the runtime.

Arrays perform best when unshared. As long as there is never more than one reference to an array,
all updates will be performed _destructively_. This results in performance comparable to mutable
arrays in imperative programming languages.

An array has a size and a capacity. The size is the number of elements present in the array, while
the capacity is the amount of memory currently allocated for elements. The size is accessible via
`Array.size`, but the capacity is not observable from Lean code. `Array.emptyWithCapacity n` creates
an array which is equal to `#[]`, but internally allocates an array of capacity `n`. When the size
exceeds the capacity, allocation is required to grow the array.

From the point of view of proofs, `Array α` is just a wrapper around `List α`.
 -/
Array : Type u → Type u
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.zero_smul_finset_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : Zero α] [inst_2 : Zero β] [inst_3 : SMulWithZero α β]
  (s : Finset β), 0 • s ⊆ 0
-- Mathlib.Data.Num.Basic
PosNum.bit1.injEq : ∀ (a a_1 : PosNum), (a.bit1 = a_1.bit1) = (a = a_1)
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
TopCat.δ_zero_toSSetObj₁Equiv.symm : ∀ {X : TopCat} (f : TopCat.I ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj X) 0))
      (TopCat.toSSetObj₁Equiv.symm f) =
    TopCat.toSSetObj₀Equiv.symm ((CategoryTheory.ConcreteCategory.hom f) 1)
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.id_apply : ∀ (X : AddGrpCat) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_map : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R A) (f : F),
  ↑(NonUnitalSubalgebra.map f S) = ⇑f '' ↑S
-- Init.Sym.DSimp.DSimprocDSL
Lean.Parser.Sym.DSimp.sym_dsimproc.quot : Lean.ParserDescr
-- Mathlib.NumberTheory.Height.Projectivization
Projectivization.one_le_mulHeight : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [inst_2 : Finite ι]
  (x : Projectivization K (ι → K)), 1 ≤ x.mulHeight
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.of_hasBinaryCoproduct' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X Y : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] [inst_2 : CategoryTheory.Limits.HasInitial C],
  CategoryTheory.IsPushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y)
    CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- `p' ↦ p -ᵥ p'` as an equivalence.  -/
AffineEquiv.constVSub : (k : Type u_1) →
  {P₁ : Type u_2} →
    {V₁ : Type u_6} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] → [inst_2 : Module k V₁] → [inst_3 : AddTorsor V₁ P₁] → P₁ → P₁ ≃ᵃ[k] V₁
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.coe_decompose_mul_add_of_left_mem : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] (𝒜 : ι → σ) {i j : ι} [inst_4 : AddLeftCancelMonoid ι] [inst_5 : GradedRing 𝒜]
  {a b : A}, a ∈ 𝒜 i → ↑(((DirectSum.decompose 𝒜) (a * b)) (i + j)) = a * ↑(((DirectSum.decompose 𝒜) b) j)
-- Init.Data.Int.DivMod.Lemmas
Int.emod_eq_fmod : ∀ {a b : ℤ}, a % b = a.fmod b - if 0 ≤ b ∨ b ∣ a then 0 else b
-- Mathlib.Algebra.Group.Prod
/-- Given additive magmas `A`, `B`, the natural projection homomorphism
from `A × B` to `B`  -/
AddHom.snd : (M : Type u_3) → (N : Type u_4) → [inst : Add M] → [inst_1 : Add N] → M × N →ₙ+ N
-- Mathlib.Order.Iterate
Monotone.seq_lt_seq_of_le_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x y : ℕ → α},
  Monotone f → ∀ (n : ℕ), x 0 < y 0 → (∀ k < n, x (k + 1) ≤ f (x k)) → (∀ k < n, f (y k) < y (k + 1)) → x n < y n
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.structuralIsoOfExpr_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g : C} (h : C)
  (η : f ⟶ g) (η' : f ≅ g),
  η'.hom = η →
    (CategoryTheory.MonoidalCategory.whiskerRightIso η' h).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight η h
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalExprTransparencyMode : Lean.Elab.ConfigEval.EvalExpr Lean.Meta.TransparencyMode