mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiffOn.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} {n : WithTop ℕ∞}, ContDiffOn ℝ n f s → (∀ x ∈ s, f x ≠ 0) → ContDiffOn ℝ n (fun y => ‖f y‖) s
-- Mathlib.Tactic.Translate.ToDual
/-- An attribute that tells that certain arguments of this definition are not
involved when translating.
This helps the translation heuristic by also transforming definitions if `ℕ` or another
fixed type occurs as one of these arguments.  -/
Mathlib.Tactic.ToDual.ignoreArgsAttr : Lean.NameMapExtension (List ℕ)
-- Lean.Meta.Tactic.Grind.Types
/-- Executes `f` to each term in the equivalence class containing `e`  -/
Lean.Meta.Grind.traverseEqc : Lean.Expr → (Lean.Meta.Grind.ENode → Lean.Meta.Grind.GoalM Unit) → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flipping_unitIso_hom_app_app_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X_1 : C) (X_2 : D),
  ((CategoryTheory.Functor.flipping.unitIso.hom.app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.id ((X.obj X_1).obj X_2)
-- Mathlib.Tactic.TacticAnalysis
/-- `skip` means that the current tactic and the ones before it will be discarded.  -/
Mathlib.TacticAnalysis.TriggerCondition.skip : {ctx : Type u_1} → Mathlib.TacticAnalysis.TriggerCondition ctx
-- Mathlib.CategoryTheory.Abelian.Exact
/-- In an abelian category, a short complex `S` is exact
iff `imageSubobject S.f = kernelSubobject S.g`.
 -/
CategoryTheory.ShortComplex.exact_iff_image_eq_kernel : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  S.Exact ↔ CategoryTheory.Limits.imageSubobject S.f = CategoryTheory.Limits.kernelSubobject S.g
-- Mathlib.Data.Nat.Choose.Bounds
Nat.pow_le_choose : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (r n : ℕ),
  ↑(n + 1 - r) ^ r / ↑r.factorial ≤ ↑(n.choose r)
-- Init.Data.List.Attach
List.mem_pmap_of_mem : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {H : ∀ a ∈ l, p a} {a : α}
  (h : a ∈ l), f a ⋯ ∈ List.pmap f l H
-- Init.Data.Array.Erase
Array.mem_eraseIdx_iff_getElem : ∀ {α : Type u_1} {x : α} {xs : Array α} {k : ℕ} {h : k < xs.size},
  x ∈ xs.eraseIdx k h ↔ ∃ i, ∃ (w : i < xs.size), i ≠ k ∧ xs[i] = x
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Compatibility of `Adjunction.Commshift` with the composition of adjunctions.
 -/
CategoryTheory.Adjunction.CommShift.instComp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) (A : Type u_3) [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] {E : Type u_4}
  [inst_7 : CategoryTheory.Category.{v_3, u_4} E] {F' : CategoryTheory.Functor D E} {G' : CategoryTheory.Functor E D}
  (adj' : F' ⊣ G') [inst_8 : CategoryTheory.HasShift E A] [inst_9 : F'.CommShift A] [inst_10 : G'.CommShift A]
  [adj.CommShift A] [adj'.CommShift A], (adj.comp adj').CommShift A
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.limitIsoOfIsRightKanExtension.congr_simp : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α α_1 : L.comp F' ⟶ F) (e_α : α = α_1) [inst_3 : F'.IsRightKanExtension α]
  [inst_4 : CategoryTheory.Limits.HasLimit F] [inst_5 : CategoryTheory.Limits.HasLimit F'],
  F'.limitIsoOfIsRightKanExtension α = F'.limitIsoOfIsRightKanExtension α_1
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- An additive group homomorphism (a bundled morphism of a type that implements
`AddMonoidHomClass`) between two uniform additive groups is uniformly continuous provided that it
is continuous at zero. See also `continuous_of_continuousAt_zero`.  -/
uniformContinuous_of_continuousAt_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {hom : Type u_3}
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [IsUniformAddGroup β] [inst_6 : FunLike hom α β]
  [AddMonoidHomClass hom α β] (f : hom), ContinuousAt (⇑f) 0 → UniformContinuous ⇑f
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A partial diffeomorphism on `s` is a function `f : M → N` such that `f` restricts to a
diffeomorphism `s → t` between open subsets of `M` and `N`, respectively.
This is an auxiliary definition and should not be used outside of this file.  -/
PartialDiffeomorph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        ModelWithCorners 𝕜 E H₁ →
                          ModelWithCorners 𝕜 F H₂ →
                            (M : Type u_8) →
                              [inst : TopologicalSpace M] →
                                [ChartedSpace H₁ M] →
                                  (N : Type u_9) →
                                    [inst : TopologicalSpace N] → [ChartedSpace H₂ N] → WithTop ℕ∞ → Type (max u_8 u_9)
-- Mathlib.CategoryTheory.ComposableArrows.Three
CategoryTheory.ComposableArrows.threeδ₃Toδ₂_app_two : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {i j k l : C} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l)
  (f₂₃ : j ⟶ l) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃),
  (CategoryTheory.ComposableArrows.threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 2 = f₃
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `Semiring` across an `Equiv`  -/
Equiv.semiring : {α : Type u_1} → {β : Type u_2} → α ≃ β → [Semiring β] → Semiring α
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewFact.fact : Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Grind.NewFact
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The opposite category of `WithTerminal C` is equivalent to `WithInitial Cᵒᵖ`.  -/
CategoryTheory.WithTerminal.opEquiv : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → (CategoryTheory.WithTerminal C)ᵒᵖ ≌ CategoryTheory.WithInitial Cᵒᵖ
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_sInf_dom : ∀ {α : Type ua} {β : Type ub} {f : α → β} {u₁ : Set (UniformSpace α)} {u₂ : UniformSpace β} {u : UniformSpace α},
  u ∈ u₁ → UniformContinuous f → UniformContinuous f
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- Continuous algebra homomorphisms from `C(s, ℝ)` into an `ℝ`-algebra `A` which agree
at `X : 𝕜[X]` (interpreted as a continuous map) are, in fact, equal.  -/
ContinuousMap.algHom_ext_map_X : ∀ {A : Type u_1} [inst : Semiring A] [inst_1 : Algebra ℝ A] [inst_2 : TopologicalSpace A] [T2Space A] {s : Set ℝ}
  [CompactSpace ↑s] {φ ψ : C(↑s, ℝ) →ₐ[ℝ] A},
  Continuous ⇑φ →
    Continuous ⇑ψ →
      φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) =
          ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) →
        φ = ψ
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- If `M` is finite free over a PID `R`, then for any submodule `N` of the same rank,
we can find basis for `M` and `N` with the same indexing such that the inclusion map
is a square diagonal matrix; these are the entries of the diagonal matrix. See:
* `Submodule.smithNormalFormTopBasis` for the basis on `M`,
* `Submodule.smithNormalFormBotBasis` for the basis on `N`,
* `Submodule.smithNormalFormBotBasis_def` for the proof that the inclusion map
  forms a square diagonal matrix.
 -/
Submodule.smithNormalFormCoeffs : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {M : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [IsDomain R] →
              [IsPrincipalIdealRing R] →
                {N : Submodule R M} → [Finite ι] → Module.Basis ι R M → Module.finrank R ↥N = Module.finrank R M → ι → R
-- Mathlib.Algebra.Regular.Pow
IsRightRegular.prod : ∀ {ι : Type u_2} {R : Type u_3} [inst : CommMonoid R] {s : Finset ι} {f : ι → R},
  (∀ i ∈ s, IsRightRegular (f i)) → IsRightRegular (∏ i ∈ s, f i)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {f : β → β}, (m.modify k f)[k']? = if (k == k') = true then Option.map f m[k]? else m[k']?
-- Init.Data.List.Sublist
List.suffix_append_inj_of_length_eq : ∀ {α : Type u_1} {l₁ l₂ s₁ s₂ : List α}, s₁.length = s₂.length → (l₁ ++ s₁ <:+ l₂ ++ s₂ ↔ l₁ <:+ l₂ ∧ s₁ = s₂)
-- Mathlib.Data.Sum.Order
Sum.Lex.inl_le_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (a : α) (b : β), toLex (Sum.inl a) ≤ toLex (Sum.inr b)
-- Mathlib.Order.Lex
ofLex_symm_eq : ∀ {α : Type u_1}, ofLex.symm = toLex
-- Aesop.Util.UnionFind
Aesop.UnionFind.find? : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → α → Aesop.UnionFind α → Option USize × Aesop.UnionFind α
-- Mathlib.Topology.Filter
Filter.tendsto_nhds_atTop_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder β] {l : Filter α} {f : α → Filter β},
  Filter.Tendsto f l (nhds Filter.atTop) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Set.Ici y ∈ f a
-- Mathlib.RingTheory.Radical.NatInt
Nat.self_lt_radical_iff : ∀ {n : ℕ}, n < UniqueFactorizationMonoid.radical n ↔ n = 0
-- Init.Data.UInt.Lemmas
USize.ofBitVec_uInt64ToBitVec : ∀ (n : UInt64), { toBitVec := BitVec.setWidth System.Platform.numBits n.toBitVec } = n.toUSize
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.le_log_iff_exp_le : ∀ {x y : ℝ}, 0 < y → (x ≤ Real.log y ↔ Real.exp x ≤ y)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- The covariant derivative as a function.  -/
CovariantDerivative.toFun : {𝕜 : 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] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [inst_14 : FiberBundle F V] →
                                            CovariantDerivative I F V →
                                              ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
-- Init.Data.Nat.MinMax
Nat.min_eq_right : ∀ {a b : ℕ}, b ≤ a → min a b = b
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_rcc : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : LE α] [inst_3 : DecidableLE α] [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.Rxc.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] [inst_7 : Std.PRange.LawfulUpwardEnumerableLE α] {xs : Std.Rcc α}
  {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.Precoverage.instContainsIdentitiesMorphismPropertyOfHasIsos : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Precoverage C} [K.HasIsos],
  K.morphismProperty.ContainsIdentities
-- Std.Http.Data.URI.Basic
/-- Optional query string as key-value pairs.
 -/
Std.Http.URI.query : Std.Http.URI → Std.Http.URI.Query
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.ext : ∀ {x y : UpperHalfPlane}, ↑x = ↑y → x = y
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.Away.val_mk : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {f : A} {d : ι} (n : ℕ) (hf : f ∈ 𝒜 d) (x : A) (hx : x ∈ 𝒜 (n • d)),
  HomogeneousLocalization.val (HomogeneousLocalization.Away.mk 𝒜 hf n x hx) = Localization.mk x ⟨f ^ n, ⋯⟩
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainLength_neg : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  LieAlgebra.IsKilling.chainLength (-α) β = LieAlgebra.IsKilling.chainLength α β
-- Mathlib.Algebra.Order.Group.CompleteLattice
mul_ciSup : ∀ {ι : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
  [MulLeftMono G], BddAbove (Set.range f) → ∀ (a : G), a * ⨆ i, f i = ⨆ i, a * f i
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Iso.sumBoxProdDistrib_toEquiv : ∀ {V₁ : Type u_5} {V₂ : Type u_6} {W : Type u_7} (G₁ : SimpleGraph V₁) (G₂ : SimpleGraph V₂) (H : SimpleGraph W),
  (SimpleGraph.Iso.sumBoxProdDistrib G₁ G₂ H).toEquiv = Equiv.sumProdDistrib V₁ V₂ W
-- Lean.Data.KVMap
/-- Update a `Nat` entry based on its current value.  -/
Lean.KVMap.updateNat : Lean.KVMap → Lean.Name → (ℕ → ℕ) → Lean.KVMap
-- Mathlib.Algebra.Notation.Pi.Defs
Function.const_sub : ∀ {ι : Type u_1} {G : Type u_7} [inst : Sub G] (a b : G),
  Function.const ι a - Function.const ι b = Function.const ι (a - b)
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_pos_real : ∀ {x : ENNReal}, x ≠ 0 → x ≠ ⊤ → x.log = ↑(Real.log x.toReal)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.foldRevM_eq_foldrM_toArray : ∀ {α : Type u} {δ : Type w} {m' : Type w → Type w'} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst : Monad m'] [LawfulMonad m'] {f : δ → α → β → m' δ} {init : δ},
  Std.DHashMap.Raw.Internal.foldRevM f init ↑m =
    Array.foldrM (fun a b => f b a.1 a.2) init (Std.DHashMap.Raw.Const.toArray ↑m)
-- Mathlib.Util.Export
Lean.Export.OfState.modify : {α : Type} →
  {inst : BEq α} →
    {inst_1 : Hashable α} →
      [self : Lean.Export.OfState α] →
        (Lean.Export.Alloc α → Lean.Export.Alloc α) → Lean.Export.State → Lean.Export.State
-- Mathlib.Algebra.GroupWithZero.Action.ConjAct
ConjAct.mulAction₀ : {G₀ : Type u_2} → [inst : GroupWithZero G₀] → MulAction (ConjAct G₀) G₀
-- Lean.Server.Requests
/-- Finds the command syntax and info tree of the first snapshot task containing `pos`, asynchronously.
The info tree may be from a nested snapshot, such as a single tactic.

See `SnapshotTree.findInfoTreeAtPos` for details on how the search is done.
 -/
Lean.Server.RequestM.findCmdDataAtPos : Lean.Server.FileWorker.EditableDocument →
  String.Pos.Raw → Bool → Lean.Server.ServerTask (Option (Lean.Syntax × Lean.Elab.InfoTree))
-- Mathlib.Data.Ordering.Lemmas
Ordering.ite_eq_lt_distrib : ∀ (c : Prop) [inst : Decidable c] (a b : Ordering),
  ((if c then a else b) = Ordering.lt) = if c then a = Ordering.lt else b = Ordering.lt
-- Init.Data.Int.Order
Int.neg_of_mul_neg_right : ∀ {a b : ℤ}, a * b < 0 → 0 < a → b < 0
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.structureMapCLM_zero_injective : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E},
  Function.Injective ⇑(ContDiffMapSupportedIn.structureMapCLM 𝕜 n 0)
-- Init.Data.List.Nat.Basic
List.intersperse.induct_unfolding : ∀ {α : Type u} (sep : α) (motive : List α → List α → Prop),
  motive [] [] →
    (∀ (head : α), motive [head] [head]) →
      (∀ (a : α) (as : List α),
          (as = [] → False) →
            motive as (List.intersperse sep as) → motive (a :: as) (a :: sep :: List.intersperse sep as)) →
        ∀ (l : List α), motive l (List.intersperse sep l)
-- Mathlib.Topology.Algebra.Monoid
tendsto_list_prod : ∀ {ι : Type u_1} {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [ContinuousMul M]
  {f : ι → α → M} {x : Filter α} {a : ι → M} (l : List ι),
  (∀ i ∈ l, Filter.Tendsto (f i) x (nhds (a i))) →
    Filter.Tendsto (fun b => (List.map (fun c => f c b) l).prod) x (nhds (List.map a l).prod)
-- Mathlib.Data.ENat.Basic
ENat.add_one_le_natCast_iff : ∀ {m : ℕ∞} {n : ℕ}, m + 1 ≤ ↑n ↔ m < ↑n
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousSemilinearMapClass.mk : ∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} [inst : Semiring R] [inst_1 : Semiring S]
  {σ : outParam (R →+* S)} {M : outParam (Type u_4)} [inst_2 : TopologicalSpace M] [inst_3 : AddCommMonoid M]
  {M₂ : outParam (Type u_5)} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M]
  [inst_7 : Module S M₂] [inst_8 : FunLike F M M₂] [toSemilinearMapClass : SemilinearMapClass F σ M M₂]
  [toContinuousMapClass : ContinuousMapClass F M M₂], ContinuousSemilinearMapClass F σ M M₂
-- Init.Data.BitVec.Bitblast
BitVec.toInt_umod_neg_add : ∀ {w : ℕ} {x y : BitVec w},
  y.msb = true → x.msb = false → ¬y.toInt ∣ x.toInt → (x % -y + y).toInt = x.toInt % y.toInt + y.toInt
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_finset_iff : ∀ {α : Type u_1} (S : Set (Finset α)), MeasurableSet S ↔ ∃ S', MeasurableSet S' ∧ {s | ↑s ∈ S'} = S
-- Mathlib.Topology.Sheaves.Flasque
CategoryTheory.StructuredArrow.hcongr_6 : ∀ (C C' : Type u₁),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v₁, u₁} C) (inst' : CategoryTheory.Category.{v₁, u₁} C'),
      inst ≍ inst' →
        ∀ (D D' : Type u₂),
          D = D' →
            ∀ (inst_1 : CategoryTheory.Category.{v₂, u₂} D) (inst'_1 : CategoryTheory.Category.{v₂, u₂} D'),
              inst_1 ≍ inst'_1 →
                ∀ (S : D) (S' : D'),
                  S ≍ S' →
                    ∀ (T : CategoryTheory.Functor C D) (T' : CategoryTheory.Functor C' D'),
                      T ≍ T' → CategoryTheory.StructuredArrow S T ≍ CategoryTheory.StructuredArrow S' T'
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalHorizontalComp_nil_nil : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g h i : C}
  (α : f ≅ g) (β : h ≅ i),
  (CategoryTheory.MonoidalCategory.tensorIso α β).hom = (CategoryTheory.MonoidalCategory.tensorIso α β).hom
-- Init.Data.Int.Basic
/-- `x ≤ y` for kernel reduction.  -/
Int.ble' : ℤ → ℤ → Bool
-- Lean.Elab.Attributes
Lean.Elab.Attribute.mk.sizeOf_spec : ∀ (kind : Lean.AttributeKind) (name : Lean.Name) (stx : Lean.Syntax),
  sizeOf { kind := kind, name := name, stx := stx } = 1 + sizeOf kind + sizeOf name + sizeOf stx
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- Eta-expanded form of `iteratedDeriv_add` -/
iteratedDeriv_fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f g : 𝕜 → F},
  ContDiffAt 𝕜 (↑n) f x →
    ContDiffAt 𝕜 (↑n) g x → iteratedDeriv n (fun i => f i + g i) x = iteratedDeriv n f x + iteratedDeriv n g x
-- Mathlib.Analysis.Complex.Exponential
Real.exp_approx_succ : ∀ {n : ℕ} {x a₁ b₁ : ℝ} (m : ℕ),
  n + 1 = m →
    ∀ (a₂ b₂ : ℝ),
      |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂ →
        |Real.exp x - Real.expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂ →
          |Real.exp x - Real.expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivary_inv_left`. -/
Antivary.of_inv_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Antivary f⁻¹ g → Monovary f g
-- Mathlib.Topology.Maps.Strict.Group
/-- The isomorphism of topological additive groups `G ⧸ f.ker ≃ f.range` given by a
strict additive group homomorphism `f`. This is an avatar of the first isomorphism theorem.  -/
ContinuousAddEquiv.quotientKerEquivRange : {G : Type u_1} →
  {H : Type u_2} →
    [inst : AddGroup G] →
      [inst_1 : AddGroup H] →
        {f : G →+ H} →
          [inst_2 : TopologicalSpace G] →
            [inst_3 : TopologicalSpace H] → Topology.IsStrictMap ⇑f → G ⧸ f.ker ≃ₜ+ ↥f.range
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum_map_zero : ∀ {ι : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {m : Multiset ι}, (Multiset.map (fun x => 0) m).sum = 0
-- Mathlib.Algebra.Order.Ring.Canonical
AddLECancellable.mul_tsub : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [inst_3 : Sub R]
  [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] {a b c : R}, AddLECancellable (a * c) → a * (b - c) = a * b - a * c
-- Mathlib.Order.WithBot
WithBot.map_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ},
  g₁ ∘ f₁ = g₂ ∘ f₂ → ∀ (a : α), WithBot.map g₁ (WithBot.map f₁ ↑a) = WithBot.map g₂ (WithBot.map f₂ ↑a)
-- Lean.Elab.Match
/-- `some h` if discriminant is annotated with the `h : ` notation.  -/
Lean.Elab.Term.Discr.h? : Lean.Elab.Term.Discr → Option Lean.Syntax
-- Mathlib.RingTheory.ChainOfDivisors
DivisorChain.isPrimePow_of_has_chain : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [UniqueFactorizationMonoid M] {q : Associates M} {n : ℕ},
  n ≠ 0 →
    ∀ {c : Fin (n + 1) → Associates M},
      StrictMono c → (∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i) → q ≠ 0 → IsPrimePow q
-- Mathlib.RingTheory.Congruence.Defs
RingCon.trans : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) {x y z : R}, c x y → c y z → c x z