mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivAt.comp_hasMFDerivWithinAt : ∀ {𝕜 : 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'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {s : Set M} {g : M' → M''} {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}
  {g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))},
  HasMFDerivAt% g (f x) g' → HasMFDerivAt[s] f x f' → HasMFDerivAt[s] (g ∘ f) x (g' ∘SL f')
-- Init.Data.Int.Lemmas
Int.subNatNat.eq_1 : ∀ (m n : ℕ),
  Int.subNatNat m n =
    match n - m with
    | 0 => Int.ofNat (m - n)
    | k.succ => Int.negSucc k
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceL!.match_5.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (l : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((ls : ℕ) →
              (lk : α) →
                (lv : β lk) →
                  (ll lr : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)) →
            motive l
-- Mathlib.Topology.Category.CompactlyGenerated
/-- The underlying topological space is compactly generated.  -/
CompactlyGenerated.is_compactly_generated : ∀ (self : CompactlyGenerated), UCompactlyGeneratedSpace ↑self.toTop
-- Mathlib.Topology.Category.Stonean.Basic
/-- The morphism from `presentation X` to `X` is an epimorphism.  -/
CompHaus.presentation.epi_π : ∀ (X : CompHaus), CategoryTheory.Epi (CompHaus.presentation.π X)
-- Mathlib.Data.ENat.Defs
/-- **Alias** of `ENat.recTopCoe_natCast`. -/
ENat.recTopCoe_coe : ∀ {C : ℕ∞ → Sort u_1} (d : C ⊤) (f : (a : ℕ) → C ↑a) (x : ℕ), ENat.recTopCoe d f ↑x = f x
-- Mathlib.Analysis.Normed.MulAction
dist_smul_le : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedAddGroup α] [inst_1 : SeminormedAddGroup β]
  [inst_2 : SMulZeroClass α β] [IsBoundedSMul α β] (s : α) (x y : β), dist (s • x) (s • y) ≤ ‖s‖ * dist x y
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.relations.comp : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Localization.Construction.relations W
    (CategoryTheory.Localization.Construction.ψ₁ W (CategoryTheory.CategoryStruct.comp f g))
    (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Construction.ψ₁ W f)
      (CategoryTheory.Localization.Construction.ψ₁ W g))
-- Init.Data.Prod
Prod.map_id : ∀ {α : Type u_1} {β : Type u_2}, Prod.map id id = id
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.vonNeumann_add_one : ∀ (o : Ordinal.{u_1}), ZFSet.vonNeumann (o + 1) = (ZFSet.vonNeumann o).powerset
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.derivCLM_apply : ∀ (𝕜 : Type u_2) {F : Type u_8} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [inst_2 : RCLike 𝕜]
  [inst_3 : NormedSpace 𝕜 F] (f : SchwartzMap ℝ F) (x : ℝ), ((SchwartzMap.derivCLM 𝕜 F) f) x = deriv (⇑f) x
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquiv_inverse_obj : ∀ (A : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} A] (A' : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] (B : Type u) [inst_2 : CategoryTheory.Category.{v, u} B]
  (F : CategoryTheory.Functor A B × CategoryTheory.Functor A' B),
  (CategoryTheory.Sum.functorEquiv A A' B).inverse.obj F = F.1.sum' F.2
-- Mathlib.Algebra.Order.Ring.Idempotent
instLatticeSubtypeIsIdempotentElem : {R : Type u_1} → [inst : CommRing R] → Lattice { a // IsIdempotentElem a }
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivWithinAt.congr_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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s t : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)},
  HasMFDerivAt[s] f x f' → (∀ x ∈ t, f₁ x = f x) → f₁ x = f x → t ⊆ s → HasMFDerivAt[t] f₁ x f'
-- Mathlib.Data.LawfulXor.Basic
xor_left_eq_self_iff : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] {a b : α}, a ^^^ b = a ↔ b = 0
-- Mathlib.Tactic.WLOG
/-- The `FVarId` of the hypothesis `h` in `hypothesisGoal`  -/
Mathlib.Tactic.WLOGResult.hypothesisFVarId : Mathlib.Tactic.WLOGResult → Lean.FVarId
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.mapIso_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (i : X ≅ Y), F.mapIso i.symm = (F.mapIso i).symm
-- Mathlib.Order.LatticeIntervals
Set.Icc.disjoint_iff : ∀ {α : Type u_1} {a b : α} [inst : SemilatticeInf α] [inst_1 : Fact (a ≤ b)] {x y : ↑(Set.Icc a b)},
  Disjoint x y ↔ ↑x ⊓ ↑y = a
-- Mathlib.Order.SuccPred.Basic
PredOrder.mk : {α : Type u_3} →
  [inst : Preorder α] →
    (pred : α → α) →
      (∀ (a : α), pred a ≤ a) → (∀ {a : α}, a ≤ pred a → IsMin a) → (∀ {a b : α}, a < b → a ≤ pred b) → PredOrder α
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : (Fin 1 → H) → ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₁ B).hom)
      ((CategoryTheory.ConcreteCategory.hom ((groupCohomology.cochainsMap f φ).f 1)) x) =
    ((Rep.Hom.hom φ).compLeft G)
      ((LinearMap.funLeft k ↑A ⇑f) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₁ A).hom) x))
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.monotone_comap : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Monotone (FirstOrder.Language.Substructure.comap f)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Bitwise xor.
 -/
Std.Tactic.BVDecide.BVBinOp.xor : Std.Tactic.BVDecide.BVBinOp
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
SubMulAction.ofStabilizer.isMultiplyPretransitive_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [MulAction.IsPretransitive G α] {n : ℕ}
  {a b : α},
  MulAction.IsMultiplyPretransitive (↥(MulAction.stabilizer G a)) (↥(SubMulAction.ofStabilizer G a)) n ↔
    MulAction.IsMultiplyPretransitive (↥(MulAction.stabilizer G b)) (↥(SubMulAction.ofStabilizer G b)) n
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.checkUnsafe : Array Lean.Elab.Command.PreElabHeaderResult → Lean.Elab.TermElabM Unit
-- Mathlib.RingTheory.Valuation.Quotient
Valuation.onQuot_comap_eq : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : CommRing R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {J : Ideal R} (hJ : J ≤ v.supp), Valuation.comap (Ideal.Quotient.mk J) (v.onQuot hJ) = v
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
CategoryTheory.instInhabitedIsSplitCoequalizerId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      Inhabited
        (CategoryTheory.IsSplitCoequalizer (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)
          (CategoryTheory.CategoryStruct.id X))
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
/-- Isomorphism expressing a compatibility of the equivalence `triangleOpEquivalence C`
with the rotation of triangles.  -/
CategoryTheory.Pretriangulated.Opposite.rotateTriangleOpEquivalenceInverseObjRotateUnopIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
          (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) →
            (Opposite.unop ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse.obj T.rotate)).rotate ≅
              Opposite.unop ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse.obj T)
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
WeakDual.gelfandTransform_apply_apply : ∀ (𝕜 : Type u_1) (A : Type u_2) [inst : CommRing 𝕜] [inst_1 : NoZeroDivisors 𝕜] [inst_2 : TopologicalSpace 𝕜]
  [inst_3 : IsTopologicalRing 𝕜] [inst_4 : TopologicalSpace A] [inst_5 : Semiring A] [inst_6 : Algebra 𝕜 A] (a : A)
  (φ : ↑(WeakDual.characterSpace 𝕜 A)), ((WeakDual.gelfandTransform 𝕜 A) a) φ = φ a
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
/-- An `n`-simplex of a simplicial set `X` is degenerate if it is in the range
of `X.map f.op` for some morphism `f : [n] ⟶ [m]` with `m < n`.  -/
SSet.degenerate : (X : SSet) → (n : ℕ) → Set (X.obj (Opposite.op { len := n }))
-- Init.Data.Format.Basic
Std.Format.FlattenAllowability.disallow.sizeOf_spec : sizeOf Std.Format.FlattenAllowability.disallow = 1
-- Mathlib.Algebra.Polynomial.Eval.Coeff
/-- **Alias** of the forward direction of `Polynomial.zero_isRoot_iff_coeff_zero_eq_zero`. -/
Polynomial.coeff_zero_eq_zero_of_zero_isRoot : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.IsRoot 0 → p.coeff 0 = 0
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
/-- A ring with finite quotients has only finitely many nonzero prime ideals of bounded norm.  -/
Ring.HasFiniteQuotients.finite_absNorm_heightOneSpectrum_le : ∀ {R : Type u_1} [inst : CommRing R] [Ring.HasFiniteQuotients R] [inst_2 : IsDedekindDomain R]
  [inst_3 : Module.Free ℤ R] (B : ℕ), {p | Ideal.absNorm p.asIdeal ≤ B}.Finite
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_congr : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' fallback : α}, (k == k') = true → m.getKeyD k fallback = m.getKeyD k' fallback
-- Plausible.Sampleable
Plausible.instSampleableExtSigma : {α : Type u_1} →
  {β : Type u_2} → [Plausible.SampleableExt α] → [Plausible.SampleableExt β] → Plausible.SampleableExt ((_ : α) × β)
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.Limplies.eq_1 : ∀ (α : Type u) {σ1 : Type v} {σ2 : Type w} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2),
  Std.Tactic.BVDecide.LRAT.Internal.Limplies α f1 f2 =
    ∀ (a : α → Bool),
      Std.Tactic.BVDecide.LRAT.Internal.Entails.eval a f1 → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval a f2
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Multiset.aestronglyMeasurable_sum : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [ContinuousAdd M] (l : Multiset (α → M)),
  (∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) → MeasureTheory.AEStronglyMeasurable l.sum μ
-- Mathlib.Algebra.GCDMonoid.Basic
Prime.dvd_or_dvd_of_dvd_lcm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b p : α}, Prime p → p ∣ lcm a b → p ∣ a ∨ p ∣ b
-- Aesop.Forward.SlotIndex
Aesop.SlotIndex.mk.inj : ∀ {toNat toNat_1 : ℕ}, { toNat := toNat } = { toNat := toNat_1 } → toNat = toNat_1
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.llr_self : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ],
  MeasureTheory.llr μ μ =ᵐ[μ] 0
-- Mathlib.Algebra.Ring.WithZero
WithZero.instRightDistribClass : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Add α] [RightDistribClass α], RightDistribClass (WithZero α)
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.stronglyMeasurable : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {m : MeasurableSpace E} [OpensMeasurableSpace E]
  (f : TestFunction Ω F n), MeasureTheory.StronglyMeasurable ⇑f
-- Mathlib.CategoryTheory.Sites.Limits
/-- Construct a cocone by sheafifying a cocone point of a cocone `E` of presheaves
over a functor which factors through sheaves.
In `isColimitSheafifyCocone`, we show that this is a colimit cocone when `E` is a colimit.  -/
CategoryTheory.Sheaf.sheafifyCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {K : Type z} →
            [inst_2 : CategoryTheory.Category.{z', z} K] →
              [CategoryTheory.HasWeakSheafify J D] →
                {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)} →
                  CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf J D)) →
                    CategoryTheory.Limits.Cocone F
-- Mathlib.Analysis.Complex.Periodic
/-- If `f` is periodic, and holomorphic and bounded at `I∞`, then it has the form (constant) +
(exponentially decaying term) as `z → I∞`.
 -/
Function.Periodic.exp_decay_sub_of_bounded_at_inf : ∀ {h : ℝ} {f : ℂ → ℂ},
  0 < h →
    Function.Periodic f ↑h →
      (∀ᶠ (z : ℂ) in Filter.comap Complex.im Filter.atTop, DifferentiableAt ℂ f z) →
        (Filter.comap Complex.im Filter.atTop).BoundedAtFilter f →
          (fun z => f z - Function.Periodic.cuspFunction h f 0) =O[Filter.comap Complex.im Filter.atTop] fun z =>
            Real.exp (-2 * Real.pi * z.im / h)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
/-- Morphisms of Day functors are natural transformations of the underlying
functors.  -/
CategoryTheory.MonoidalCategory.DayFunctor.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            CategoryTheory.MonoidalCategory.DayFunctor C V →
              CategoryTheory.MonoidalCategory.DayFunctor C V → Type (max u₁ v₂)
-- Mathlib.Algebra.Group.Defs
instIsDedekindFiniteAddMonoidOfIsLeftCancelAdd : ∀ (M : Type u_2) [inst : AddMonoid M] [IsLeftCancelAdd M], IsDedekindFiniteAddMonoid M
-- Lean.Parser.Module
Lean.Parser.testParseModuleAux : Lean.Environment →
  Lean.Parser.InputContext →
    Lean.Parser.ModuleParserState → Lean.MessageLog → Array Lean.Syntax → IO (Array Lean.Syntax)
-- Lean.Data.SMap
/-- Similar to `find?`, but searches for result in the hashmap first.
So, the result is correct only if we never "overwrite" `map₁` entries using `map₂`.  -/
Lean.SMap.find?' : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SMap α β → α → Option β
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.mem_minimalPrimes : ∀ {R : Type u_1} [inst : CommRing R] [IsArtinianRing R] {I p : Ideal R} [hp : p.IsPrime], I ≤ p → p ∈ I.minimalPrimes
-- Init.Data.List.Find
List.idxOf?_eq_some_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α} {i : ℕ},
  List.idxOf? a l = some i ↔ ∃ (h : i < l.length), l[i] = a ∧ ∀ (j : ℕ) (x : j < i), ¬l[j] = a
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instIsCofilteredElementsFiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] [CategoryTheory.IsCofiltered N],
  CategoryTheory.IsCofiltered (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber p).Elements
-- Batteries.Data.Fin.Fold
Fin.dfoldrM_succ : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Fin (n + 1 + 1) → Type u_1} [inst : Monad m] [LawfulMonad m]
  (f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)) (x : α (Fin.last (n + 1))),
  Fin.dfoldrM (n + 1) α f x = Fin.dfoldrM n (α ∘ Fin.succ) (fun x => f x.succ) x >>= f 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqLetDecl : {pu : Lean.Compiler.LCNF.Purity} → BEq (Lean.Compiler.LCNF.LetDecl pu)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.continuous_precomp : ∀ {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [inst : NormedField 𝕜₁]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  [inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_4 : AddCommGroup E] [inst_5 : TopologicalSpace E]
  [inst_6 : Module 𝕜₁ E] [inst_7 : AddCommGroup F] [inst_8 : TopologicalSpace F] [inst_9 : Module 𝕜₂ F]
  [inst_10 : AddCommGroup G] [inst_11 : TopologicalSpace G] [inst_12 : Module 𝕜₃ G] [inst_13 : IsTopologicalAddGroup G]
  [inst_14 : ContinuousConstSMul 𝕜₃ G] (f : E →SWOT[σ₁₂] F), Continuous fun g => g.comp f
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientQuotientEquivQuotientAux.congr_simp : ∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M),
  QuotientGroup.quotientQuotientEquivQuotientAux N M h = QuotientGroup.quotientQuotientEquivQuotientAux N M h
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.StructuredArrow.isCoseparating_inverseImage_proj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (S : D) (T : CategoryTheory.Functor C D) {P : CategoryTheory.ObjectProperty C},
  P.IsCoseparating → (P.inverseImage (CategoryTheory.StructuredArrow.proj S T)).IsCoseparating
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.prodPUnit_apply : ∀ (X : Type u) [inst : TopologicalSpace X], ⇑(Homeomorph.prodPUnit X) = fun p => p.1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∩ t₂).getKey? k = none
-- Lean.Parser.Command
Lean.Parser.Command.eval.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Syntax
Lean.Syntax.Traverser.fromSyntax : Lean.Syntax → Lean.Syntax.Traverser
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapComp_naturality_left : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (self.mapComp f g) (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g))
      (self.mapComp f' g)
-- Mathlib.Algebra.Order.Floor.Defs
/-- Construct a `FloorRing` instance noncomputably, from the hypothesis that every element is
bounded above by a natural number.  -/
FloorRing.ofBounded : (α : Type u_4) →
  [inst : Ring α] →
    [inst_1 : LinearOrder α] → [IsOrderedRing α] → [Nontrivial α] → (∀ (x : α), ∃ n, x ≤ ↑n) → FloorRing α
-- Mathlib.Data.Option.Basic
Option.casesOn'_coe : ∀ {α : Type u_1} {β : Type u_2} (x : β) (f : α → β) (a : α), (some a).casesOn' x f = f a
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
/-- A linear independent set of `finrank K V`-many vectors forms a basis.  -/
setBasisOfLinearIndependentOfCardEqFinrank : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {s : Set V} →
            [Nonempty ↑s] →
              [inst_4 : Fintype ↑s] →
                LinearIndependent K Subtype.val → s.toFinset.card = Module.finrank K V → Module.Basis (↑s) K V
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Iic_castAdd : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a : Fin n),
  ∏ i ≤ Fin.castAdd m a, f i = ∏ i ≤ a, f (Fin.castAdd m i)
-- Mathlib.Data.Opposite
Opposite.op.injEq : ∀ {α : Sort u} (unop unop_1 : α), (Opposite.op unop = Opposite.op unop_1) = (unop = unop_1)
-- Mathlib.CategoryTheory.FinCategory.Basic
CategoryTheory.FinCategory.fintypeHom : {J : Type v} →
  {inst : CategoryTheory.SmallCategory J} → [self : CategoryTheory.FinCategory J] → (j j' : J) → Fintype (j ⟶ j')
-- Mathlib.Algebra.Order.Module.Basic
sup_eq_half_smul_add_add_abs_sub' : ∀ (𝕜 : Type u_1) {M : Type u_3} [inst : DivisionSemiring 𝕜] [NeZero 2] [inst_2 : Lattice M] [inst_3 : AddCommGroup M]
  [inst_4 : Module 𝕜 M] [IsOrderedAddMonoid M] (x y : M), x ⊔ y = 2⁻¹ • (x + y + |y - x|)
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- The defining property of an adic Cauchy sequence unwrapped.  -/
AdicCompletion.AdicCauchySequence.mk_eq_mk : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {m n : ℕ},
  m ≤ n → ∀ (f : AdicCompletion.AdicCauchySequence I M), Submodule.Quotient.mk (↑f n) = Submodule.Quotient.mk (↑f m)
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.of_ker_isNilpotent_of_isMulCentral : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {I : Type u_3} {e : I → R}
  [inst_2 : Fintype I],
  (∀ x ∈ RingHom.ker f, IsNilpotent x) →
    (∀ (i : I), IsIdempotentElem (e i)) →
      (∀ (i : I), IsMulCentral (e i)) → CompleteOrthogonalIdempotents (⇑f ∘ e) → CompleteOrthogonalIdempotents e
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
`m + 1 ≤ n` is `C^m`.
Version within a set at a point.  -/
ContMDiffWithinAt.mpullbackWithin_vectorField_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} {t : Set M'} [CompleteSpace E] [inst_12 : IsManifold I 1 M]
  [inst_13 : IsManifold I' 1 M'],
  ContMDiffWithinAt I' I'.tangent m (fun x => ⟨x, V x⟩) t (f x₀) →
    ContMDiffWithinAt I I' n f s x₀ →
      (mfderiv[s] f x₀).IsInvertible →
        x₀ ∈ s →
          UniqueMDiff[s] →
            m + 1 ≤ n →
              ContMDiffWithinAt I I.tangent m (fun x => ⟨x, VectorField.mpullbackWithin I I' f V s x⟩) (s ∩ f ⁻¹' t) x₀
-- Mathlib.Data.ENNReal.Basic
ENNReal.one_ne_top : 1 ≠ ⊤
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.not_infinite_zero : ¬Hyperreal.Infinite 0
-- Mathlib.Algebra.CharP.Basic
CharP.intCast_injOn_Ico : ∀ (R : Type u_1) [inst : AddGroupWithOne R] (p : ℕ) [CharP R p] [IsRightCancelAdd R], Set.InjOn Int.cast (Set.Ico 0 ↑p)