mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Lp.WithLp
/-- Lift a (semi)linear equivalence to `WithLp`.  -/
LinearEquiv.withLpCongr : (p : ENNReal) →
  {K : Type u_1} →
    {K' : Type u_2} →
      {V : Type u_4} →
        {V' : Type u_5} →
          [inst : Semiring K] →
            [inst_1 : Semiring K'] →
              {σ : K →+* K'} →
                {σ' : K' →+* K} →
                  [inst_2 : RingHomInvPair σ σ'] →
                    [inst_3 : RingHomInvPair σ' σ] →
                      [inst_4 : AddCommGroup V] →
                        [inst_5 : Module K V] →
                          [inst_6 : AddCommGroup V'] →
                            [inst_7 : Module K' V'] → (V ≃ₛₗ[σ] V') → WithLp p V ≃ₛₗ[σ] WithLp p V'
-- Mathlib.Topology.Algebra.Module.LocallyConvex
/-- In a locally convex space, every point `x` and closed convex set `s ∌ x` admit disjoint convex
open neighborhoods.  -/
exists_open_convex_of_notMem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [ZeroLEOneClass 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] [inst_5 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
  [LocallyConvexSpace 𝕜 E] {s : Set E} {x : E},
  x ∉ s → Convex 𝕜 s → IsClosed s → ∃ U V, IsOpen U ∧ IsOpen V ∧ Convex 𝕜 U ∧ Convex 𝕜 V ∧ x ∈ U ∧ s ⊆ V ∧ Disjoint U V
-- Init.Data.BitVec.Basic
BitVec.xor_eq : ∀ {w : ℕ} (x y : BitVec w), x.xor y = x ^^^ y
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.app_ε_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Comonad C}
  (self : CategoryTheory.ComonadHom M N) (X : C) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (N.ε.app X) h) =
    CategoryTheory.CategoryStruct.comp (M.ε.app X) h
-- Batteries.Data.Char.Basic
Char.any.eq_1 : ∀ (p : Char → Bool),
  Char.any p =
    ((Char.minSurrogate.any fun c h₁ => p (Char.ofNatAux c ⋯)) ||
      (Char.max - Char.maxSurrogate).any fun c h₂ => p (Char.ofNatAux (c + Char.maxSurrogate + 1) ⋯))
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.instFunLike : {R : Type u_1} →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] →
      [inst_2 : IsStrictOrderedRing R] →
        {X : Type u_2} →
          {Y : Type u_3} →
            [inst_3 : Convexity.ConvexSpace R X] →
              [inst_4 : Convexity.ConvexSpace R Y] → FunLike (Convexity.ConvexSpace.AffineMap R X Y) X Y
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getEntryD.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (fallback : (a : α) × β a) (a_1 : α) (b : β a_1)
  (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getEntryD a fallback (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    if (a_1 == a) = true then ⟨a_1, b⟩ else Std.DHashMap.Internal.AssocList.getEntryD a fallback es
-- Mathlib.RingTheory.PowerSeries.Exp
PowerSeries.map_exp : ∀ {A : Type u_1} {A' : Type u_2} [inst : Ring A] [inst_1 : Ring A'] [inst_2 : Algebra ℚ A] [inst_3 : Algebra ℚ A']
  (f : A →+* A'), (PowerSeries.map f) (PowerSeries.exp A) = PowerSeries.exp A'
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.isClosedEmbedding_singleton : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T0Space α], Topology.IsClosedEmbedding fun x => {x}
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_of_notMem : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {a : α}, a ∉ s → ∀ (f : α → M), s.indicator f a = 0
-- Mathlib.Analysis.Normed.Group.Constructions
MulOpposite.instSeminormedAddCommGroup : {E : Type u_2} → [SeminormedAddCommGroup E] → SeminormedAddCommGroup Eᵐᵒᵖ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get?_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ \ m₂).get? k = none
-- Lean.Elab.Tactic.Conv.Pattern
Lean.Elab.Tactic.Conv.PatternMatchState.occs.injEq : ∀ (subgoals : Array (ℕ × Lean.MVarId)) (idx : ℕ) (remaining : List (ℕ × ℕ)) (subgoals_1 : Array (ℕ × Lean.MVarId))
  (idx_1 : ℕ) (remaining_1 : List (ℕ × ℕ)),
  (Lean.Elab.Tactic.Conv.PatternMatchState.occs subgoals idx remaining =
      Lean.Elab.Tactic.Conv.PatternMatchState.occs subgoals_1 idx_1 remaining_1) =
    (subgoals = subgoals_1 ∧ idx = idx_1 ∧ remaining = remaining_1)
-- Std.Data.ExtTreeMap.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.ExtTreeMap.ofArray : {α : Type u} →
  {β : Type v} →
    Array (α × β) → (cmp : autoParam (α → α → Ordering) Std.ExtTreeMap.ofArray._auto_1) → Std.ExtTreeMap α β cmp
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypePreimage_symm_apply_coe_neg : ∀ {α : Sort u_1} {β : Sort u_4} (p : α → Prop) [inst : DecidablePred p] (x₀ : { a // p a } → β) (x : { a // ¬p a } → β)
  (a : α) (h : ¬p a), ↑((Equiv.subtypePreimage p x₀).symm x) a = x ⟨a, h⟩
-- Aesop.EMap
Aesop.EMap.mapM : {m : Type → Type u_1} → [Monad m] → {α β : Type} → (Lean.Expr → α → m β) → Aesop.EMap α → m (Aesop.EMap β)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- Coercion to a function as an `AddMonoidHom`.
Similar to `AddMonoidHom.coeFn`.  -/
ContMDiffMap.coeFnAddMonoidHom : {𝕜 : 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 ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : AddMonoid G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [inst_12 : ContMDiffAdd I' n G] → ContMDiffMap I I' N G n →+ N → G
-- Mathlib.LinearAlgebra.Quotient.Basic
/-- The ordering on submodules of the quotient of `M` by `p` embeds into the ordering on submodules
of `M`.  -/
Submodule.comapMkQOrderEmbedding : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (p : Submodule R M) → Submodule R (M ⧸ p) ↪o Submodule R M
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.dropn_congr : ∀ {α : Type u} {s t : Stream'.WSeq α}, s ~ʷ t → ∀ (n : ℕ), s.drop n ~ʷ t.drop n
-- Init.Data.List.TakeDrop
List.rotateRight_zero : ∀ {α : Type u_1} {l : List α}, l.rotateRight 0 = l
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 0th object in the complex of inhomogeneous chains of `A : Rep k G` is isomorphic
to `A` as a `k`-module.  -/
groupHomology.chainsIso₀ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → (groupHomology.inhomogeneousChains A).X 0 ≅ ModuleCat.of k ↑A
-- Init.Data.Fin.Bitwise
Fin.xor_val : ∀ {n : ℕ} (a b : Fin n), ↑(a ^^^ b) = (↑a ^^^ ↑b) % n
-- Mathlib.Analysis.InnerProductSpace.LaxMilgram
_private.Mathlib.Analysis.InnerProductSpace.LaxMilgram.0.IsCoercive.«term_♯» : Lean.TrailingParserDescr
-- Lean.Server.Utils
Lean.Server.DocumentMeta.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri) (mod : Lean.Name) (version : ℕ) (text : Lean.FileMap)
  (dependencyBuildMode : Lean.Lsp.DependencyBuildMode),
  sizeOf { uri := uri, mod := mod, version := version, text := text, dependencyBuildMode := dependencyBuildMode } =
    1 + sizeOf uri + sizeOf mod + sizeOf version + sizeOf text + sizeOf dependencyBuildMode
-- Mathlib.Topology.UniformSpace.Equiv
/-- A uniform isomorphism as a homeomorphism.  -/
UniformEquiv.toHomeomorph : {α : Type u} → {β : Type u_1} → [inst : UniformSpace α] → [inst_1 : UniformSpace β] → α ≃ᵤ β → α ≃ₜ β
-- Mathlib.Topology.Category.Stonean.Basic
/-- If `X` is profinite, `presentation X` is a Stonean space equipped with an epimorphism down to
`X` (see `Profinite.presentation.π` and `Profinite.presentation.epi_π`).  -/
Profinite.presentation : Profinite → Stonean
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.hom_ext : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  {f g : S ⟶ S'}, f.fst = g.fst → f.snd = g.snd → f = g
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.instHasOfPostcompPropertySchemeUniversallyClosedIsSeparated : CategoryTheory.MorphismProperty.HasOfPostcompProperty @AlgebraicGeometry.UniversallyClosed
  @AlgebraicGeometry.IsSeparated
-- Lean.Elab.DocString
/-- Adds a builtin documentation code suggestion provider.

Should be run during initialization.
 -/
Lean.Doc.addBuiltinCodeBlockSuggestion : Lean.Name → Lean.Doc.CodeBlockSuggester → IO Unit
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The monoidal product is a measurable function from the product of finite measures over
`α` and `β` into the type of finite measures over `α × β`.  -/
MeasureTheory.FiniteMeasure.measurable_fun_prod : ∀ {α : Type u_3} {β : Type u_4} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β],
  Measurable fun μ => (↑μ.1).prod ↑μ.2
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instReprAltParamInfo : Repr Lean.Meta.Match.AltParamInfo
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableOn.neg : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {f : M → E'} {s : Set M}, MDiff[s] f → MDiff[s] (-f)
-- Mathlib.NumberTheory.FLT.Three
/-- Given any `S : Solution`, there is another `S₁ : Solution` such that
`S₁.multiplicity < S.multiplicity`  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.exists_Solution_multiplicity_lt : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  ∃ S₁, FermatLastTheoremForThreeGen.Solution.multiplicity✝ S₁ < FermatLastTheoremForThreeGen.Solution.multiplicity✝ S
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- If a word reduces to another word, then they have a common maximal reduction.  -/
FreeAddGroup.reduce.eq_of_red : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.Red L₁ L₂ → FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂
-- Std.Time.Time.Unit.Second
Std.Time.Second.instReprOffset : Repr Std.Time.Second.Offset
-- Mathlib.LinearAlgebra.TensorPower.Pairing
TensorPower.pairingDual_tprod_tprod : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (f : Fin n → Module.Dual R M) (v : Fin n → M),
  ((TensorPower.pairingDual R M n) ((PiTensorProduct.tprod R) f)) ((PiTensorProduct.tprod R) v) = ∏ i, (f i) (v i)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.extend_apply_of_mem_I : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁) {t : ℝ} (ht : t ∈ unitInterval) (x : X), (F.extend t) x = F (⟨t, ht⟩, x)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.ofFn.go.eq_1 : ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (acc : Array α) (i_1 : ℕ) (h : i_1 + 1 ≤ n),
  Array.ofFn.go✝ f acc i_1.succ h = Array.ofFn.go✝ f (acc.push (f ⟨n - i_1 - 1, ⋯⟩)) i_1 ⋯
-- Mathlib.Algebra.Group.Hom.Basic
ZeroHom.coe_add : ∀ {M : Type u_8} {N : Type u_9} [inst : Zero M] [inst_1 : AddZeroClass N] (f g : ZeroHom M N), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Order.BoundedOrder.Basic
Subtype.coe_top : ∀ {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : OrderTop (Subtype p)],
  p ⊤ → ↑⊤ = ⊤
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.isSymm_conjTranspose_iff : ∀ {α : Type u_1} {n : Type u_3} [inst : InvolutiveStar α] {A : Matrix n n α}, A.conjTranspose.IsSymm ↔ A.IsSymm
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.r.sizeOf_spec : ∀ {n : ℕ} (a : ZMod n), sizeOf (DihedralGroup.r a) = 1 + sizeOf a
-- Mathlib.CategoryTheory.Limits.Creates
/-- any limit cocone can be lifted to a cocone above  -/
CategoryTheory.CreatesColimit.lifts : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        {J : Type w} →
          {inst_2 : CategoryTheory.Category.{w', w} J} →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [self : CategoryTheory.CreatesColimit K F] →
                  (c : CategoryTheory.Limits.Cocone (K.comp F)) →
                    CategoryTheory.Limits.IsColimit c → CategoryTheory.LiftableCocone K F c
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_sSup_of_directedOn : ∀ {G : Type u_1} [inst : Group G] {K : Set (Subgroup G)},
  K.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) K → ∀ {x : G}, x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.instInhabitedExtensionState.default : {γ : Type} → Lean.KeyedDeclsAttribute.ExtensionState γ
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.Error.headersTooLarge.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Error.headersTooLarge = 1
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_re_ax : ∀ {K : semiOutParam (Type u_1)} [self : RCLike K] (z : K), RCLike.re ((starRingEnd K) z) = RCLike.re z
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.trans_F : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {F' : Type u_6} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace 𝕜 F'] [inst_9 : TopologicalSpace H]
  [inst_10 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11}
  {N : Type u_13} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H M] [inst_13 : TopologicalSpace N]
  [inst_14 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M},
  Manifold.IsSubmersionAtOfComplement F I J n f x → ∀ (e : F ≃L[𝕜] F'), Manifold.IsSubmersionAtOfComplement F' I J n f x
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The name of the lemma  -/
Mathlib.Tactic.LibraryRewrite.RewriteLemma.name : Mathlib.Tactic.LibraryRewrite.RewriteLemma → Lean.Name
-- Mathlib.Topology.Algebra.Order.Field
tendsto_const_mul_zpow_atTop_nhds_iff : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {n : ℤ} {c d : 𝕜},
  c ≠ 0 → (Filter.Tendsto (fun x => c * x ^ n) Filter.atTop (nhds d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0)
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- Maps `P₁ → P₂` and `P₂ → P₁` between extensions
induce an isomorphism between `H¹(L_P₁)` and `H¹(L_P₂)`.  -/
Algebra.Extension.H1Cotangent.equiv : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P₁ : Algebra.Extension R S} →
            {P₂ : Algebra.Extension R S} → P₁.Hom P₂ → P₂.Hom P₁ → P₁.H1Cotangent ≃ₗ[S] P₂.H1Cotangent
-- Std.Time.DateTime
/-- Determines the week of the year for the given `DateTime`, using `firstDay` as the start of the week
and `minDays` as the minimum number of days a week must have in the new year to count as week 1.
 -/
Std.Time.DateTime.weekOfYear : Std.Time.DateTime →
  optParam Std.Time.Weekday Std.Time.Weekday.monday →
    optParam (Std.Time.Internal.Bounded.LE 0 6)
        (Std.Time.Internal.Bounded.LE.mk 4 Std.Time.DateTime.weekOfYear._proof_1) →
      Std.Time.Week.OfYear.Ordinal
-- Mathlib.Topology.Connected.TotallyDisconnected
Topology.IsCoinducing.connectedComponentsMap : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Topology.IsCoinducing f), Topology.IsCoinducing ⋯.connectedComponentsMap
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearEquiv.mdifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E ≃L[𝕜] E') {x : E}, MDiffAt ⇑f x
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_mul_nat : ∀ {n : ℕ}, n ≠ 0 → Cardinal.continuum * ↑n = Cardinal.continuum
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.symm_mapDomainRingEquiv : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  (e : M ≃+ N), (AddMonoidAlgebra.mapDomainRingEquiv R e).symm = AddMonoidAlgebra.mapDomainRingEquiv R e.symm
-- Plausible.DeriveArbitrary
/-- Deriving handler which produces an instance of the `ArbitraryFueled` typeclass for
each type specified in `declNames`  -/
_private.Plausible.DeriveArbitrary.0.Plausible.mkArbitraryInstanceHandler : Array Lean.Name → Lean.Elab.Command.CommandElabM Bool
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.iterated_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} [CompleteSpace E] {n : ℕ}, Meromorphic f → Meromorphic (deriv^[n] f)
-- Mathlib.Data.Finset.Dedup
List.toFinset_toList : ∀ {α : Type u_1} [inst : DecidableEq α] {s : List α}, s.Nodup → s.toFinset.toList.Perm s
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.structureSheafInType.smul_apply : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)} (r : R)
  (s : (AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op U)) (x : ↥U), ↑(r • s) x = r • ↑s x
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.LinearMap.dp_zero : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : CommSemiring S] {N : Type u_5} [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : Module S N]
  (f : M →ₗ[R] N) {a : M}, DividedPowerAlgebra.dp S 0 (f a) = 1
-- Mathlib.Algebra.Star.Basic
MulOpposite.instStarModule : ∀ {R : Type u} {M : Type u_1} [inst : Star R] [inst_1 : Star M] [inst_2 : SMul R M] [StarModule R M], StarModule R Mᵐᵒᵖ
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.eq_or_isStrictRestriction : ∀ {α : Type u_1} {M N : Matroid α}, N.IsRestriction M → N = M ∨ N.IsStrictRestriction M
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.sub_left_inj_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a b c : α}, a ≠ ⊤ → (b - a = c - a ↔ b = c)
-- Mathlib.Data.Complex.Basic
/-- The coercion `ℝ → ℂ` as a `RingHom`.  -/
Complex.ofRealHom : ℝ →+* ℂ
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.trans_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) (a : α), (ab.trans bc) a = bc (ab a)
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of the sum of two formal power series
is the minimum of their orders if their orders differ.  -/
PowerSeries.order_add_of_order_ne : ∀ {R : Type u_1} [inst : Semiring R] (φ ψ : PowerSeries R), φ.order ≠ ψ.order → (φ + ψ).order = min φ.order ψ.order
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
/-- The integral representation of the function `x ↦ x ^ p` (where `p ∈ (1, 2)`).  -/
CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₁₂ : ∀ (A : Type u_1) [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : SMulCommClass ℝ A A] [inst_4 : IsScalarTower ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [CompleteSpace A] {p : NNReal},
  p ∈ Set.Ioo 1 2 →
    ∃ μ,
      ∀ a ∈ Set.Ici 0,
        MeasureTheory.IntegrableOn (fun t => cfcₙ ((↑p).rpowIntegrand₁₂ t) a) (Set.Ioi 0) μ ∧
          a ^ p = ∫ (t : ℝ) in Set.Ioi 0, cfcₙ ((↑p).rpowIntegrand₁₂ t) a ∂μ
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- The property of reflecting terminal objects expressed in terms of `IsTerminal`.  -/
CategoryTheory.Limits.IsTerminal.isTerminalOfObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          (X : C) →
            [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty C) G] →
              CategoryTheory.Limits.IsTerminal (G.obj X) → CategoryTheory.Limits.IsTerminal X
-- Lean.Elab.Tactic.Omega.Core
/-- A `Justification` bundled together with its parameters.  -/
Lean.Elab.Tactic.Omega.Fact : Type
-- Mathlib.Data.Matrix.Mul
Matrix.mul_mul_apply : ∀ {n : Type u_3} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype n] (A B C : Matrix n n α) (i j : n),
  (A * B * C) i j = A i ⬝ᵥ B.mulVec (C.transpose j)
-- Init.Data.Vector.Basic
/-- Maps corresponding elements of two vectors of equal size using the function `f`.  -/
Vector.zipWith : {α : Type u_1} → {β : Type u_2} → {φ : Type u_3} → {n : ℕ} → (α → β → φ) → Vector α n → Vector β n → Vector φ n
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.isLocallyInjective_toSheafify' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} (J : CategoryTheory.GrothendieckTopology C) {CD : D → Type (max u v)}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  (P : CategoryTheory.Functor Cᵒᵖ D) [inst_4 : CategoryTheory.HasWeakSheafify J D]
  [J.HasSheafCompose (CategoryTheory.forget D)] [J.PreservesSheafification (CategoryTheory.forget D)],
  CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.norm_apply : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : Group G] [inst_2 : Fintype G] (A : Rep.{w, u, v} k G)
  {x : ↑A}, (Rep.Hom.hom A.norm) x = A.ρ.norm x