mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
/-- An element of the character space of a unital algebra, as an algebra homomorphism.  -/
WeakDual.CharacterSpace.toAlgHom : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing 𝕜] →
      [NoZeroDivisors 𝕜] →
        [inst_2 : TopologicalSpace 𝕜] →
          [inst_3 : ContinuousAdd 𝕜] →
            [inst_4 : ContinuousConstSMul 𝕜 𝕜] →
              [inst_5 : TopologicalSpace A] →
                [inst_6 : Semiring A] → [inst_7 : Algebra 𝕜 A] → ↑(WeakDual.characterSpace 𝕜 A) → A →ₐ[𝕜] 𝕜
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.eq_of_bisim : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {x y : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  (motive :
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl → Prop),
  motive x y →
    (∀ (x y : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
        motive x y →
          x = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil ∧
              y = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil ∨
            ∃ exp coef x' y',
              x = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef x' ∧
                y = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef y' ∧ motive x' y') →
      x = y
-- Init.Data.List.Lemmas
List.tail_eq_tailD : ∀ {α : Type u_1} {l : List α}, l.tail = l.tailD []
-- Init.Data.UInt.Lemmas
UInt64.le_or_lt : ∀ (a b : UInt64), a ≤ b ∨ b < a
-- Std.Data.HashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.HashMap.getKey? : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → Option α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_eq_some_minKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.minKey? = some t.minKey!
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.isConnected_op_iff_isConnected : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J],
  CategoryTheory.IsConnected Jᵒᵖ ↔ CategoryTheory.IsConnected J
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.hasNoLoop_up : ∀ {α : Type u_2} [inst : AddZeroClass α] [inst_1 : IsRightCancelAdd α] [IsLeftCancelAdd α] [inst_3 : One α],
  1 ≠ 0 → (ComplexShape.up α).HasNoLoop
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α}, (Std.DHashMap.filter f m).get? k = Option.filter (f k) (m.get? k)
-- Mathlib.Analysis.Real.Sqrt
Real.comap_sqrt_atTop : Filter.comap (fun x => √x) Filter.atTop = Filter.atTop
-- Lean.Elab.Tactic.Omega.OmegaM
/-- Retrieve the list of atoms.  -/
Lean.Elab.Tactic.Omega.atoms : Lean.Elab.Tactic.Omega.OmegaM (Array Lean.Expr)
-- Mathlib.Data.Multiset.ZeroCons
/-- `cons a s` is the multiset which contains `s` plus one more instance of `a`.  -/
Multiset.«term_::ₘ_» : Lean.TrailingParserDescr
-- Init.Data.Nat.Basic
Nat.sub.elim : ∀ {motive : ℕ → Prop} (x y : ℕ), (y ≤ x → ∀ (k : ℕ), x = y + k → motive k) → (x < y → motive 0) → motive (x - y)
-- Batteries.Data.Stream
Std.Stream.fst_take_zero : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ), (Std.Stream.take s 0).1 = []
-- Mathlib.Topology.Metrizable.ContinuousMap
ContinuousMap.instPseudoMetrizableSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X]
  [inst_3 : TopologicalSpace Y] [TopologicalSpace.PseudoMetrizableSpace Y],
  TopologicalSpace.PseudoMetrizableSpace C(X, Y)
-- Mathlib.Tactic.CrossRefAttribute
/-- `lmfdbId` is the node kind of LMFDB identifiers: lower case words with `.` in between.
The words can also contain underscores and digits.  -/
Mathlib.CrossRef.lmfdbIdKind : Lean.SyntaxNodeKind
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instReprCompletionItemTag : Repr Lean.Lsp.CompletionItemTag
-- Mathlib.Data.Set.Card
Set.ncard_compl_of_ncard_eq_add : ∀ {α : Type u_1} [Finite α] (s : Set α) {n : ℕ}, Nat.card α = n + s.ncard → sᶜ.ncard = n
-- Batteries.Data.Nat.Lemmas
Nat.ofBits_succ : ∀ {n : ℕ} (f : Fin (n + 1) → Bool), Nat.ofBits f = 2 * Nat.ofBits (f ∘ Fin.succ) + (f 0).toNat
-- Lean.Parser.Command
/-- `#check_assertions` reports whether all `assert_not_exists` and `assert_not_imported`
assertions in the current file and its imports have been satisfied.
Use `#check_assertions!` to only show unsatisfied assertions.
 -/
Lean.Parser.Command.checkAssertions : Lean.Parser.Parser
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_mul : ∀ {p q : ℝ}, 0 ≤ p → ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ),
  ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₃ =
    n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom
-- Std.Http.Data.Chunk
/-- A validated chunk extension name that ensures all characters conform to HTTP standards
per RFC 9112 §7.1.1. Extension names appear in chunked transfer encoding as key-value metadata.

Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension
 -/
Std.Http.Chunk.ExtensionName : Type
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
AntitoneOn.neg : ∀ {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftMono α] [AddRightMono α]
  [inst_4 : Preorder β] {f : β → α} {s : Set β}, AntitoneOn f s → MonotoneOn (fun x => -f x) s
-- Mathlib.RingTheory.WittVector.Defs
WittVector.instOne : {p : ℕ} → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [CommRing R] → One (WittVector p R)
-- Mathlib.Topology.Compactness.Lindelof
/-- A σ-compact set `s` is Lindelöf  -/
IsSigmaCompact.isLindelof : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsSigmaCompact s → IsLindelof s
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.initial_of_final_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.op.Final], F.Initial
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- A cases eliminator that makes `cases z` use `UnitClosedDisc.mk` instead of `Subtype.mk`.  -/
Complex.UnitClosedDisc.casesOn : {motive : Complex.UnitClosedDisc → Sort u_1} →
  ((z : ℂ) → (hz : ‖z‖ ≤ 1) → motive (Complex.UnitClosedDisc.mk z hz)) → (z : Complex.UnitClosedDisc) → motive z
-- Mathlib.Data.Set.Lattice
Set.iInter_subset_iUnion : ∀ {α : Type u_1} {ι : Sort u_5} [Nonempty ι] {s : ι → Set α}, ⋂ i, s i ⊆ ⋃ i, s i
-- Mathlib.Algebra.Ring.Defs
/-- A not-necessarily-unital, not-necessarily-associative, but commutative semiring.  -/
NonUnitalNonAssocCommSemiring : Type u → Type u
-- Mathlib.Order.Cofinal
IsCofinal.singleton_top : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderTop α], IsCofinal {⊤}
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubsetResult.strict.sizeOf_spec : ∀ (s : Lean.Grind.AC.Seq), sizeOf (Lean.Grind.AC.SubsetResult.strict s) = 1 + sizeOf s
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- **Alias** of `Convexity.convexCombPair_zero`.

---

A binary convex combination with weight 0 on the first point returns the second point.  -/
Convexity.convexComboPair_zero : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] {x y : M}, Convexity.convexCombPair 0 1 ⋯ ⋯ ⋯ x y = y
-- Mathlib.Algebra.Group.Graph
/-- **Vertical line test** for group homomorphisms.

Let `G ≤ H × I` be a subgroup of a product of monoids. Assume that `G` maps bijectively to the
first factor. Then `G` is the graph of some monoid homomorphism `f : H → I`.  -/
Subgroup.exists_eq_graph : ∀ {H : Type u_2} {I : Type u_3} [inst : Group H] [inst_1 : Group I] {G : Subgroup (H × I)},
  Function.Bijective (Prod.fst ∘ ⇑G.subtype) → ∃ f, G = f.graph
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.StructuredArrow.hasLimitsOfShape : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T}
  [CategoryTheory.Limits.HasLimitsOfShape J A] [CategoryTheory.Limits.PreservesLimitsOfShape J G],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.StructuredArrow X G)
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.vertices_toPath_tail : ∀ {V : Type u_1} [inst : Quiver V] {i j : V} (e : i ⟶ j), e.toPath.vertices.tail = [j]
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_mul_omega0 : Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) Ordinal.omega0
-- Lean.Linter.UnusedVariables
Lean.Linter.UnusedVariables.References.mk.inj : ∀ {constDecls : Std.HashSet Lean.Syntax.Range}
  {fvarDefs : Std.HashMap Lean.Syntax.Range Lean.Linter.UnusedVariables.FVarDefinition}
  {fvarUses : Std.HashSet Lean.FVarId} {fvarAliases : Std.HashMap Lean.FVarId Lean.FVarId}
  {assignments : Array (Lean.PersistentHashMap Lean.MVarId Lean.Expr)} {constDecls_1 : Std.HashSet Lean.Syntax.Range}
  {fvarDefs_1 : Std.HashMap Lean.Syntax.Range Lean.Linter.UnusedVariables.FVarDefinition}
  {fvarUses_1 : Std.HashSet Lean.FVarId} {fvarAliases_1 : Std.HashMap Lean.FVarId Lean.FVarId}
  {assignments_1 : Array (Lean.PersistentHashMap Lean.MVarId Lean.Expr)},
  { constDecls := constDecls, fvarDefs := fvarDefs, fvarUses := fvarUses, fvarAliases := fvarAliases,
        assignments := assignments } =
      { constDecls := constDecls_1, fvarDefs := fvarDefs_1, fvarUses := fvarUses_1, fvarAliases := fvarAliases_1,
        assignments := assignments_1 } →
    constDecls = constDecls_1 ∧
      fvarDefs = fvarDefs_1 ∧ fvarUses = fvarUses_1 ∧ fvarAliases = fvarAliases_1 ∧ assignments = assignments_1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instHashablePurity : Hashable Lean.Compiler.LCNF.Purity
-- Mathlib.GroupTheory.OrderOfElement
Prod.addOrderOf_mk : ∀ {α : Type u_4} {β : Type u_5} [inst : AddMonoid α] [inst_1 : AddMonoid β] {a : α} {b : β},
  addOrderOf (a, b) = (addOrderOf a).lcm (addOrderOf b)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.expPartialHomeomorph_source : Real.expPartialHomeomorph.source = Set.univ
-- Init.Data.Rat.Lemmas
Rat.neg_add : ∀ {a b : ℚ}, -(a + b) = -a + -b
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.modify' : (Lean.Meta.Grind.Arith.Linear.State → Lean.Meta.Grind.Arith.Linear.State) → Lean.Meta.Grind.GoalM Unit
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
Ideal.stabilizerEquiv.congr_simp : ∀ {M : Type u_1} {R : Type u_3} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {N : Type u_4}
  [inst_3 : Group N] [inst_4 : MulSemiringAction N R] (I : Ideal R) (e e_1 : M ≃* N) (e_e : e = e_1)
  (he : ∀ (m : M) (x : R), e m • x = m • x), I.stabilizerEquiv e he = I.stabilizerEquiv e_1 ⋯
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Tensoring on the left with a fixed object, as a functor.  -/
CategoryTheory.MonoidalCategory.tensorLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → C → CategoryTheory.Functor C C
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.ev_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} (f : I ⟶ J)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f],
  CategoryTheory.ExponentiableMorphism.ev f = (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj f).counit
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- A semilinear isometric equivalence between two normed vector spaces,
denoted as `f : E ≃ₛₗᵢ[σ₁₂] E₂`.  -/
«term_≃ₛₗᵢ[_]_» : Lean.TrailingParserDescr
-- Init.Data.UInt.Lemmas
UInt32.toNat_lt : ∀ (n : UInt32), n.toNat < 2 ^ 32
-- Mathlib.Analysis.Real.Sqrt
Real.sq_sqrt : ∀ {x : ℝ}, 0 ≤ x → √x ^ 2 = x
-- Mathlib.Data.Sym.Sym2
_private.Mathlib.Data.Sym.Sym2.0.Sym2.fromVector.match_1.splitter : {α : Type u_1} →
  (motive : List.Vector α 2 → Sort u_2) →
    (x : List.Vector α 2) → ((a b : α) → (property : [a, b].length = 2) → motive ⟨[a, b], property⟩) → motive x
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_lt_add_one_iff`. -/
ENat.coe_lt_add_one_iff : ∀ {m : ℕ} {n : ℕ∞}, ↑m < n + 1 ↔ ↑m ≤ n
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
/-- Given a t-structure `t` on a triangulated category `C`, this is the functor
`ComposableArrows EInt 1 ⥤ C ⥤ C` which sends an arrows `a ⟶ b` in `EInt`
to the functor `t.eTruncLT.obj b ⋙ t.eTruncGE.obj a`.  -/
CategoryTheory.Triangulated.TStructure.ω₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C →
                CategoryTheory.Functor (CategoryTheory.ComposableArrows EInt 1) (CategoryTheory.Functor C C)
-- Lean.DocString.Markdown
Lean.Doc.instInhabitedMdRendererState.default : Lean.Doc.MdRendererState
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.subtype_injective : ∀ {M : Type u_4} [inst : AddZeroClass M] (s : AddSubmonoid M), Function.Injective ⇑s.subtype
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.δ_map_of_gt_assoc : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  (self : f.MulStruct g fg i) (j : Fin (n + 2)),
  i.succ.succ < j →
    ∀ {Z : SSet} (h : X ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp self.map h) =
        CategoryTheory.CategoryStruct.comp (SSet.const x) h
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceL.match_7.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (r : Std.DTreeMap.Internal.Impl α β) →
      r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size → Sort u_3)
  (rs : ℕ) (k : α) (v : β k) (l_1 r : Std.DTreeMap.Internal.Impl α β)
  (hrb : (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).size)
  (h_1 :
    (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size Std.DTreeMap.Internal.Impl.leaf.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hrb hlr)
  (h_2 :
    (rs : ℕ) →
      (k : α) →
        (v : β k) →
          (l_2 r : Std.DTreeMap.Internal.Impl α β) →
            (hrb : (Std.DTreeMap.Internal.Impl.inner rs k v l_2 r).Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size
                    (Std.DTreeMap.Internal.Impl.inner rs k v l_2 r).size) →
                motive (Std.DTreeMap.Internal.Impl.inner rs k v l_2 r) hrb hlr),
  (match Std.DTreeMap.Internal.Impl.inner rs k v l_1 r, hrb, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hrb, hlr => h_1 hrb hlr
    | Std.DTreeMap.Internal.Impl.inner rs k v l_2 r, hrb, hlr => h_2 rs k v l_2 r hrb hlr) =
    h_2 rs k v l_1 r hrb hlr
-- Mathlib.Analysis.Calculus.ImplicitContDiff
IsContDiffImplicitAt.hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  {E₂ : Type u_3} [inst_3 : NormedAddCommGroup E₂] [inst_4 : NormedSpace 𝕜 E₂] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : E₁ × E₂ → F} {f' : E₁ × E₂ →L[𝕜] F}
  {u : E₁ × E₂}, IsContDiffImplicitAt n f f' u → HasFDerivAt f f' u
-- Lean.Server.References
_private.Lean.Server.References.0.Lean.Server.combineIdents.buildIdMap : Array Lean.Elab.InfoTree →
  Array Lean.Server.Reference →
    Std.HashMap Lean.Lsp.Range Lean.Lsp.RefIdent → Std.HashMap Lean.Lsp.RefIdent Lean.Lsp.RefIdent
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.TriggerCondition.continue.inj : ∀ {ctx : Type u_1} {context context_1 : ctx},
  Mathlib.TacticAnalysis.TriggerCondition.continue context =
      Mathlib.TacticAnalysis.TriggerCondition.continue context_1 →
    context = context_1
-- Init.Data.String.Defs
String.instDecidableIsAtEnd : {s : String} → {pos : s.Pos} → Decidable pos.IsAtEnd
-- Mathlib.Analysis.Normed.Operator.Extend
LinearMap.extendOfNorm.congr_simp : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [inst : NormedDivisionRing 𝕜]
  [inst_1 : NormedDivisionRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : AddCommGroup E] [inst_3 : SeminormedAddCommGroup Eₗ]
  [inst_4 : NormedAddCommGroup F] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ F] [inst_7 : IsBoundedSMul 𝕜₂ F]
  [inst_8 : Module 𝕜 Eₗ] [inst_9 : IsBoundedSMul 𝕜 Eₗ] [inst_10 : CompleteSpace F] (f f_1 : E →ₛₗ[σ₁₂] F),
  f = f_1 → ∀ (e e_1 : E →ₗ[𝕜] Eₗ), e = e_1 → f.extendOfNorm e = f_1.extendOfNorm e_1
-- Mathlib.Data.Multiset.AddSub
Multiset.mem_sub : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s t : Multiset α}, a ∈ s - t ↔ Multiset.count a t < Multiset.count a s
-- Mathlib.Topology.Baire.BaireMeasurable
BaireMeasurableSet.sUnion : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set (Set α)},
  s.Countable → (∀ t ∈ s, BaireMeasurableSet t) → BaireMeasurableSet (⋃₀ s)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
/-- If `ω` is a closed `1`-form on a convex set `s`,
then the function given by `F b = ∫ᶜ x in Path.segment a b, ω x` is a primitive of `ω` on `s`,
i.e., `dF = ω`.
 -/
Convex.hasFDerivWithinAt_curveIntegral_segment_of_hasFDerivWithinAt_symmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  [inst_6 : NormedSpace ℝ F] {a b : E} {s : Set E} {ω : E → E →L[𝕜] F} {dω : E → E →L[ℝ] E →L[𝕜] F} [CompleteSpace F],
  Convex ℝ s →
    (∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x) →
      (∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x) →
        a ∈ s → b ∈ s → HasFDerivWithinAt (fun x => ∫ᶜ (x : E) in Path.segment a x, ω x) (ω b) s b
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CongrTheoremCacheKey.numArgs : Lean.Meta.Grind.CongrTheoremCacheKey → ℕ
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.instIsIsoAppUnitReflectorAdjunctionObjEssImage : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i] (X : i.EssImageSubcategory),
  CategoryTheory.IsIso ((CategoryTheory.reflectorAdjunction i).unit.app X.obj)
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- Given `f : X ⟶ Y`, this is the class of `f` in the quotient `LeftHomotopyClass X Y`.  -/
HomotopicalAlgebra.LeftHomotopyClass.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] → (X ⟶ Y) → HomotopicalAlgebra.LeftHomotopyClass X Y
-- Lean.Level
/-- Universe level metavariable Id    -/
Lean.LevelMVarId : Type
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a fallback : α}, t.contains a = false → t.getKeyD a fallback = fallback
-- Mathlib.Logic.Equiv.Prod
/-- Any family of `Unique` types is a right identity for dependent type product up to
equivalence.  -/
Equiv.sigmaUnique : (α : Type u_10) → (β : α → Type u_9) → [(a : α) → Unique (β a)] → (a : α) × β a ≃ α
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverse_involute : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (a : CliffordAlgebra Q),
  CliffordAlgebra.reverse (CliffordAlgebra.involute a) = CliffordAlgebra.involute (CliffordAlgebra.reverse a)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_roo : ∀ {m n i : ℕ}, (m<...n).toList[i]! = if i < n - (m + 1) then m + 1 + i else 0
-- Mathlib.RingTheory.Trace.Basic
Algebra.traceForm_toMatrix_powerBasis : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (h : PowerBasis R S),
  (LinearMap.BilinForm.toMatrix h.basis) (Algebra.traceForm R S) =
    Matrix.of fun i j => (Algebra.trace R S) (h.gen ^ (↑i + ↑j))
-- Batteries.Data.PairingHeap
/-- `O(n)`. Fold a function over the tree structure to accumulate a value.  -/
Batteries.PairingHeapImp.Heap.foldTree : {β : Type u_1} → {α : Type u_2} → β → (α → β → β → β) → Batteries.PairingHeapImp.Heap α → β
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.evalComp_cons : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g h i j : a ⟶ b} (α : f ≅ g) (η : g ⟶ h) {ηs : h ⟶ i}
  {θ : i ⟶ j} {ι : h ⟶ j},
  CategoryTheory.CategoryStruct.comp ηs θ = ι →
    CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) θ =
      CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ι)
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_Ioi' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Ici a) → Filter.Tendsto f Filter.atTop Filter.atBot → Set.Iio (f a) ⊆ f '' Set.Ioi a
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.incidenceSet_inter_incidenceSet_subset : ∀ {V : Type u} (G : SimpleGraph V) {a b : V}, a ≠ b → G.incidenceSet a ∩ G.incidenceSet b ⊆ {s(a, b)}
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetFilterResult.filter : BigOperators.FinsetFilterResult✝ → Option Lean.Term
-- Mathlib.GroupTheory.OrderOfElement
orderOf_pow_of_dvd : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ}, n ≠ 0 → n ∣ orderOf x → orderOf (x ^ n) = orderOf x / n
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.ofNatCode.match_3.eq_4 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : Unit → motive 3) (h_5 : (n : ℕ) → motive n.succ.succ.succ.succ),
  (match 3 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()
    | 3 => h_4 ()
    | n.succ.succ.succ.succ => h_5 n) =
    h_4 ()
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearEquiv.symm_conjContinuousAlgEquiv_apply_apply : ∀ {𝕜 : Type u_1} {G : Type u_4} {H : Type u_5} [inst : AddCommGroup G] [inst_1 : AddCommGroup H]
  [inst_2 : NormedField 𝕜] [inst_3 : Module 𝕜 G] [inst_4 : Module 𝕜 H] [inst_5 : TopologicalSpace G]
  [inst_6 : TopologicalSpace H] [inst_7 : IsTopologicalAddGroup G] [inst_8 : IsTopologicalAddGroup H]
  [inst_9 : ContinuousConstSMul 𝕜 G] [inst_10 : ContinuousConstSMul 𝕜 H] (e : G ≃L[𝕜] H) (f : H →L[𝕜] H) (x : G),
  (e.conjContinuousAlgEquiv.symm f) x = e.symm (f (e x))