mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
UniqueMDiffWithinAt.mono : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {s t : Set M},
  UniqueMDiffAt[s] x → s ⊆ t → UniqueMDiffAt[t] x
-- Mathlib.NumberTheory.NumberField.Basic
/-- This instance has to be `CoeHead` because we only want to apply it from `𝓞 K` to `K`.  -/
NumberField.RingOfIntegers.instCoeHead : {K : Type u_1} → [inst : Field K] → CoeHead (NumberField.RingOfIntegers K) K
-- Mathlib.CategoryTheory.Skeletal
/-- Applying `fromThinSkeleton`, `F` and then `toThinSkeleton` is isomorphic to applying `map F`.
 -/
CategoryTheory.ThinSkeleton.fromThinSkeletonCompToThinSkeletonIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : Quiver.IsThin C] →
          (F : CategoryTheory.Functor C D) →
            (CategoryTheory.ThinSkeleton.fromThinSkeleton C).comp (F.comp (CategoryTheory.toThinSkeleton D)) ≅
              CategoryTheory.ThinSkeleton.map F
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.CompSource.assump.inj : ∀ {a a_1 : ℕ}, Mathlib.Tactic.Linarith.CompSource.assump a = Mathlib.Tactic.Linarith.CompSource.assump a_1 → a = a_1
-- Lean.Util.PtrSet
Lean.instHashablePtr : {α : Type u_1} → Hashable (Lean.Ptr α)
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- Length of a column of a Young diagram  -/
YoungDiagram.colLen : YoungDiagram → ℕ → ℕ
-- Lean.Data.Lsp.CodeActions
/-- The reason why code actions were requested.  -/
Lean.Lsp.CodeActionContext.triggerKind? : Lean.Lsp.CodeActionContext → Option Lean.Lsp.CodeActionTriggerKind
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α]
  {f : α → β → γ} {k : α}, (Std.ExtHashMap.map f m)[k]? = Option.map (f k) m[k]?
-- Init.Data.List.Lemmas
List.getElem!_cons_zero : ∀ {α : Type u_1} {a : α} [inst : Inhabited α] {l : List α}, (a :: l)[0]! = a
-- Mathlib.Logic.Embedding.Basic
/-- A right inverse `surjInv` of a surjective function as an `Embedding`.  -/
Function.Embedding.ofSurjective : {α : Sort u_1} → {β : Sort u_2} → (f : β → α) → Function.Surjective f → α ↪ β
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.tensorRightHomEquiv_whiskerRight_comp_evaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasRightDual X] (f : Y ⟶ Xᘁ),
  (CategoryTheory.tensorRightHomEquiv Y X Xᘁ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X) (ε_ X Xᘁ)) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategoryStruct.leftUnitor Xᘁ).inv
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.semiring : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {R : Type u_10} →
                                      [inst_9 : Semiring R] →
                                        [inst_10 : TopologicalSpace R] →
                                          [inst_11 : ChartedSpace H' R] →
                                            [ContMDiffRing I' n R] → Semiring (ContMDiffMap I I' N R n)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instMonoidalLinear : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G], CategoryTheory.MonoidalLinear k (Rep.{u, u, v} k G)
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
/-- A function has finite integral for the counting measure iff its norm is summable.  -/
MeasureTheory.hasFiniteIntegral_count_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup β] [MeasurableSingletonClass α]
  {f : α → β}, MeasureTheory.HasFiniteIntegral f MeasureTheory.Measure.count ↔ Summable fun x => ‖f x‖
-- Init.Data.List.Monadic
List.forIn_cons : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m (ForInStep β)) (a : α)
  (as : List α) (b : β),
  forIn (a :: as) b f = do
    let x ← f a b
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn as b f
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {X : CategoryTheory.SimplicialObject C} {n : ℕ} {Z : C}
  {x y : AlgebraicTopology.DoldKan.MorphComponents X n Z}, x = y ↔ x.a = y.a ∧ x.b = y.b
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Valuation.Compatible.mk : ∀ {R : Type u_1} {Γ : Type u_2} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ] {v : Valuation R Γ}
  [inst_2 : ValuativeRel R], (∀ (x y : R), x ≤ᵥ y ↔ v x ≤ v y) → v.Compatible
-- Init.Data.Vector.Lemmas
Vector.append_assoc : ∀ {α : Type u_1} {n m k : ℕ} {xs : Vector α n} {ys : Vector α m} {zs : Vector α k},
  xs ++ ys ++ zs = Vector.cast ⋯ (xs ++ (ys ++ zs))
-- Init.Data.Order.Lemmas
Std.lt_of_le_of_ne : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Std.Antisymm fun x1 x2 => x1 ≤ x2] [Std.LawfulOrderLT α] {a b : α},
  a ≤ b → a ≠ b → a < b
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- If a point is in the affine span of a set, adding it to that set does not change the vector
span.  -/
vectorSpan_insert_eq_vectorSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p : P} {ps : Set P}, p ∈ affineSpan k ps → vectorSpan k (insert p ps) = vectorSpan k ps
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddLocalization.addEquivOfQuotient_mk' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  {f : S.LocalizationMap N} (x : M) (y : ↥S),
  (AddLocalization.addEquivOfQuotient f) ((AddLocalization.addMonoidOf S).mk' x y) = f.mk' x y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_insertMany!_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α},
      compare k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
          k ∈ List.map Sigma.fst l → (↑(t.insertMany! l)).getKey! k' = k
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_linearCombination : ∀ {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_9}
  {β : Type u_10} (A : α → M) (B : β → α →₀ R) (f : β →₀ R),
  (Finsupp.linearCombination R A) ((Finsupp.linearCombination R B) f) =
    (Finsupp.linearCombination R fun b => (Finsupp.linearCombination R A) (B b)) f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negAddY_of_Z_eq_zero_left : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.negAddY P Q = P 1 ^ 2 * Q 2 * W'.negY Q
-- Mathlib.Algebra.Group.Subgroup.Map
/-- The preimage of a subgroup along a monoid homomorphism is a subgroup.  -/
Subgroup.comap : {G : Type u_1} → [inst : Group G] → {N : Type u_7} → [inst_1 : Group N] → (G →* N) → Subgroup N → Subgroup G
-- Lean.Elab.Tactic.Induction
/-- Given a goal `... targets ... |- C[targets, complexArgs]` associated with `mvarId`,
where `complexArgs` are the complex (i.e. non-target) arguments to the motive in the conclusion
of the eliminator, construct `motiveArg := fun targets rs => C[targets, rs]`

This checks if the type of the complex arguments match what's expected by the motive, and
ignores them otherwise. This limits the ability of `cases` to use unfolding function
principles with dependent types, because after generalization of the targets, the types do
no longer match. This can likely be improved.
 -/
Lean.Elab.Tactic.ElimApp.setMotiveArg : Lean.MVarId → Lean.MVarId → Array Lean.FVarId → optParam (Array Lean.Expr) #[] → Lean.MetaM Unit
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.semilinearEquivOfRingEquiv.congr_simp : ∀ {A : Type u_8} {B : Type u_9} (K : Type u_10) (L : Type u_11) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : CommRing K] [inst_3 : CommRing L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K]
  [inst_6 : Algebra B L] [inst_7 : IsFractionRing B L] (f : A ≃+* B),
  IsFractionRing.semilinearEquivOfRingEquiv K L f = IsFractionRing.semilinearEquivOfRingEquiv K L f
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
FirstOrder.Language.Theory.ACF.eq_1 : ∀ (p : ℕ),
  FirstOrder.Language.Theory.ACF p =
    FirstOrder.Language.Theory.fieldOfChar p ∪ FirstOrder.Field.genericMonicPolyHasRoot '' {n | 0 < n}
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_smulRight : ∀ {E : Type u_2} {F : Type u_3} [inst : AddCommMonoid E] [inst_1 : StarAddMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : StarAddMonoid F] {S : Type u_5} [inst_4 : Semiring S] [inst_5 : StarAddMonoid S] [inst_6 : StarModule S S]
  [inst_7 : Module S E] [inst_8 : StarModule S E] [inst_9 : Module S F] [inst_10 : StarModule S F]
  (f : WithConv (E →ₗ[S] S)) (x : F),
  star (WithConv.toConv (f.ofConv.smulRight x)) = WithConv.toConv ((star f).ofConv.smulRight (star x))
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.mk.injEq : ∀ (perm : Mathlib.Tactic.Translate.Permutation) (argReorders : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder))
  (perm_1 : Mathlib.Tactic.Translate.Permutation) (argReorders_1 : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder)),
  ({ perm := perm, argReorders := argReorders } = { perm := perm_1, argReorders := argReorders_1 }) =
    (perm = perm_1 ∧ argReorders = argReorders_1)
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.map.eq_1 : ∀ {m : Type w → Type w'} [inst : Functor m] {α : Type u} {β : Type v} (f : α → β) (x : Std.Iterators.HetT m α),
  Std.Iterators.HetT.map f x = x.pmap fun a x => f a
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkInductiveAux₁.eq_def : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1) (one : P.X 1 ⟶ Q.X 2)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1))
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X (n + 1)) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                  CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
              CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2)))
  (x : ℕ),
  Homotopy.mkInductiveAux₁ e zero one comm_one succ x =
    match x with
    | 0 => ⟨zero, ⟨one, comm_one⟩⟩
    | 1 => ⟨one, ⟨(succ 0 ⟨zero, ⟨one, comm_one⟩⟩).fst, ⋯⟩⟩
    | n.succ.succ =>
      ⟨(Homotopy.mkInductiveAux₁ e zero one comm_one succ (n + 1)).snd.fst,
        ⟨(succ (n + 1) (Homotopy.mkInductiveAux₁ e zero one comm_one succ (n + 1))).fst, ⋯⟩⟩
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClopen_basicOpen_of_mul_add : ∀ {R : Type u} [inst : CommSemiring R] (e f : R), e * f = 0 → e + f = 1 → IsClopen ↑(PrimeSpectrum.basicOpen e)
-- Mathlib.Data.List.Palindrome
List.Palindrome.iff_reverse_eq : ∀ {α : Type u_1} {l : List α}, l.Palindrome ↔ l.reverse = l
-- Std.Http.Data.Method
Std.Http.Method.instEncodeV11 : Std.Http.Internal.Encode Std.Http.Version.v11 Std.Http.Method
-- Lean.Server.RequestCancellation
Lean.Server.instMonadCancellableOfMonadLift : (m : Type → Type u_1) →
  (n : Type → Type u_2) → [MonadLift m n] → [Lean.Server.MonadCancellable m] → Lean.Server.MonadCancellable n
-- Mathlib.Algebra.Module.RingHom
RingHom.smulOneHom_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : NonAssocSemiring S] [inst_2 : Module R S]
  [inst_3 : IsScalarTower R S S] (x : R), RingHom.smulOneHom x = x • 1
-- Lean.Elab.AutoBound
/-- Tracks a working set of variables that the auto-binding process currently
anticipates adding implicit binding for.
 -/
Lean.Elab.AutoBoundImplicitContext.boundVariables : Lean.Elab.AutoBoundImplicitContext → Lean.PArray Lean.Expr
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit
/-- If `X : SSet`, then `X` is the colimit of its monogenous subcomplexes.
(Note: a monogenous subcomplex of `X` is generated by a unique nondegenerate
simplex `x : X.N`.)  -/
SSet.isColimitCoconeN : (X : SSet) → CategoryTheory.Limits.IsColimit X.coconeN
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A fixed block is a block.  -/
MulAction.IsFixedBlock.isBlock : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] {B : Set X}, MulAction.IsFixedBlock G B → MulAction.IsBlock G B
-- Mathlib.CategoryTheory.IsConnected
/-- Another induction principle for `IsPreconnected J`:
given a type family `Z : J → Sort*` and
a rule for transporting in *both* directions along a morphism in `J`,
we can transport an `x : Z j₀` to a point in `Z j` for any `j`.
 -/
CategoryTheory.isPreconnected_induction : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected J] (Z : J → Sort u_1)
  (h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂) (h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁) {j₀ : J} (x : Z j₀) (j : J),
  Nonempty (Z j)
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.IntegrableOn.union : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} {s t : Set X},
  MeasurableSet s → MeasurableSet t → μ.IntegrableOn f s → μ.IntegrableOn f t → μ.IntegrableOn f (s ∪ t)
-- Mathlib.Data.Matrix.Composition
Matrix.compRingEquiv_symm_apply : ∀ (I : Type u_1) (J : Type u_2) (R : Type u_5) [inst : AddCommMonoid R] [inst_1 : Mul R] [inst_2 : Fintype I]
  [inst_3 : Fintype J] (M : Matrix (I × J) (I × J) R),
  (Matrix.compRingEquiv I J R).symm M = (Matrix.comp I I J J R).symm M
-- Mathlib.Analysis.Calculus.FDeriv.Linear
ContinuousLinearMap.differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E →L[𝕜] F) {s : Set E}, DifferentiableOn 𝕜 (⇑f) s
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τl : ∀ (x : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ),
  (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapId x).inv.τl =
    CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pullbackId (Opposite.unop x.as)).inv
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fintypeEdgeSetSup : {V : Type u} →
  (G₁ G₂ : SimpleGraph V) → [DecidableEq V] → [Fintype ↑G₁.edgeSet] → [Fintype ↑G₂.edgeSet] → Fintype ↑(G₁ ⊔ G₂).edgeSet
-- Mathlib.Data.Matrix.Reflection
Matrix.mulVecᵣ.eq_1 : ∀ {l m : ℕ} {α : Type u_1} [inst : Mul α] [inst_1 : Add α] [inst_2 : Zero α] (A : Matrix (Fin l) (Fin m) α)
  (v : Fin m → α), A.mulVecᵣ v = FinVec.map (fun a => Matrix.dotProductᵣ a v) A
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.singleton_union : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α) (s : Finset α), {x} ∪ s = insert x s
-- Std.Data.HashSet.Lemmas
Std.HashSet.equiv_emptyWithCapacity_iff_isEmpty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {c : ℕ},
  m.Equiv (Std.HashSet.emptyWithCapacity c) ↔ m.isEmpty = true
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.all_filterM : ∀ {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_2 : MonadLiftT m n] [inst_3 : Std.IteratorLoop α m m] [inst_4 : Monad m] [LawfulMonad m] [inst_6 : Monad n]
  [inst_7 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n]
  [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {f : β → n (ULift.{w, 0} Bool)} {p : β → Bool},
  Std.IterM.all p (Std.IterM.filterM f it) =
    Std.IterM.allM
      (fun x => do
        let __do_lift ← f x
        if __do_lift.down = true then pure { down := p x } else pure { down := true })
      (Std.IterM.mapM pure it)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- Given a map `f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G` and an estimate
`H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖`, construct a continuous linear
map from `F` to `E [⋀^ι]→L[𝕜] G`.

In order to lift, e.g., a map `f : (E [⋀^ι]→ₗ[𝕜] F) →ₗ[𝕜] E' [⋀^ι]→ₗ[𝕜] G`
to a map `(E [⋀^ι]→L[𝕜] F) →L[𝕜] E' [⋀^ι]→L[𝕜] G`,
one can apply this construction to `f.comp ContinuousAlternatingMap.toAlternatingMapLinear`
which is a linear map from `E [⋀^ι]→L[𝕜] F` to `E' [⋀^ι]→ₗ[𝕜] G`.  -/
AlternatingMap.mkContinuousLinear : {𝕜 : Type u} →
  {E : Type wE} →
    {F : Type wF} →
      {G : Type wG} →
        {ι : Type v} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : SeminormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : SeminormedAddCommGroup G] →
                      [inst_6 : NormedSpace 𝕜 G] →
                        [inst_7 : Fintype ι] →
                          (f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G) →
                            (C : ℝ) → (∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) → F →L[𝕜] E [⋀^ι]→L[𝕜] G
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.inlX_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder] (i j : ι)
  (hij : c.Rel j i),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inlX K i j hij)
      ((HomologicalComplex.cylinder.π K).f j) =
    0
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.ext_iff : ∀ {A : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} A} {B : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} B} {T : Type u_3} {inst_2 : CategoryTheory.Category.{v_3, u_3} T}
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} {x y : X.Hom Y}, x = y ↔ x.left = y.left ∧ x.right = y.right
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.lsum_symm_apply : ∀ {ι : Type u_1} {R : Type u_3} (S : Type u_4) {M : ι → Type u_5} {N : Type u_6} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
  [inst_4 : Module R N] [inst_5 : DecidableEq ι] [inst_6 : Semiring S] [inst_7 : Module S N]
  [inst_8 : SMulCommClass R S N] (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι),
  (DFinsupp.lsum S).symm F i = F ∘ₗ DFinsupp.lsingle i
-- Lean.Expr
Lean.Expr.instBEq : BEq Lean.Expr
-- Mathlib.Order.Heyting.Boundary
Coheyting.boundary_le : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a : α}, Coheyting.boundary a ≤ a
-- Mathlib.RingTheory.Polynomial.Wronskian
Polynomial.wronskian_eq_of_sum_zero : ∀ {R : Type u_1} [inst : CommRing R] {a b c : Polynomial R}, a + b + c = 0 → a.wronskian b = b.wronskian c
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- For any element `m : M` and any set `B i` in the submodule basis on `M`,
there is a `U` in the ring filter basis on `R` such that `U * m` is in `B i`.  -/
RingFilterBasis.SubmodulesBasis.smul : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {BR : RingFilterBasis R} {B : ι → Submodule R M},
  BR.SubmodulesBasis B → ∀ (m : M) (i : ι), ∃ U ∈ BR, U ⊆ (fun x => x • m) ⁻¹' ↑(B i)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.iUnion_incidenceSet : ∀ {V : Type u} (G : SimpleGraph V), ⋃ v, G.incidenceSet v = G.edgeSet
-- Lean.DocString.Types
/-- An item in a description list.  -/
Lean.Doc.DescItem : Type u → Type v → Type (max u v)
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fundamentalSequence.match_1.eq_5 : ∀ (motive : Option ONote ⊕ (ℕ → ONote) → ℕ → Sort u_1) (f : ℕ → ONote) (h_1 : Unit → motive (Sum.inl none) 0)
  (h_2 : (m : ℕ) → motive (Sum.inl none) m.succ) (h_3 : (a' : ONote) → motive (Sum.inl (some a')) 0)
  (h_4 : (a' : ONote) → (m : ℕ) → motive (Sum.inl (some a')) m.succ) (h_5 : (f : ℕ → ONote) → motive (Sum.inr f) 0)
  (h_6 : (f : ℕ → ONote) → (m : ℕ) → motive (Sum.inr f) m.succ),
  (match Sum.inr f, 0 with
    | Sum.inl none, 0 => h_1 ()
    | Sum.inl none, m.succ => h_2 m
    | Sum.inl (some a'), 0 => h_3 a'
    | Sum.inl (some a'), m.succ => h_4 a' m
    | Sum.inr f, 0 => h_5 f
    | Sum.inr f, m.succ => h_6 f m) =
    h_5 f
-- Mathlib.Algebra.Category.Grp.Biproducts
/-- Construct limit data for a product in `AddCommGrpCat`, using
`AddCommGrpCat.of (∀ j, F.obj j)`.
 -/
AddCommGrpCat.HasLimit.productLimitCone : {J : Type w} → (f : J → AddCommGrpCat) → CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor f)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₂ → (m₁ ∩ m₂).getKey? k = none
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.tendsto_defaultRatCDF_atTop : Filter.Tendsto ProbabilityTheory.defaultRatCDF Filter.atTop (nhds 1)
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `setOfPred_gauge_lt_one_subset_self`. -/
setOf_gauge_lt_one_subset_self : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  Convex ℝ s → 0 ∈ s → Absorbent ℝ s → {x | gauge s x < 1} ⊆ s
-- Mathlib.Data.Nat.Log
Nat.log_le_clog : ∀ (b n : ℕ), Nat.log b n ≤ Nat.clog b n
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.instAddCommGroupHomComma : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    [inst_1 : CategoryTheory.Preadditive A] →
      {B : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_3 : CategoryTheory.Preadditive B] →
            {T : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} T] →
                [inst_5 : CategoryTheory.Preadditive T] →
                  (L : CategoryTheory.Functor A T) →
                    [L.Additive] →
                      (R : CategoryTheory.Functor B T) →
                        [R.Additive] → {u v : CategoryTheory.Comma L R} → AddCommGroup (u ⟶ v)