mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.CoconeMorphism.ext_iff : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F} {f g : c' ⟶ c}, f = g ↔ f.hom = g.hom
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If `t : Cone F` is a limit cone, then `t.op : Cocone F.op` is a colimit cocone.
 -/
CategoryTheory.Limits.IsLimit.op : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} → CategoryTheory.Limits.IsLimit t → CategoryTheory.Limits.IsColimit t.op
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.haarScalarFactor_map : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsHaarMeasure]
  [inst_6 : μ'.IsHaarMeasure] (φ : G ≃ₜ* G),
  (MeasureTheory.Measure.map (⇑φ) μ').haarScalarFactor (MeasureTheory.Measure.map (⇑φ) μ) = μ'.haarScalarFactor μ
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- The bijection `((free R).obj X ⟶ M) ≃ (X → M)` when `X` is a type and `M` a module.  -/
ModuleCat.freeHomEquiv : {R : Type u} → [inst : Ring R] → {X : Type u} → {M : ModuleCat R} → ((ModuleCat.free R).obj X ⟶ M) ≃ (X ⟶ ↑M)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_minKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKey?.isSome = true
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.instMulQ : {α : Type u} →
  [inst : Lean.Grind.CommSemiring α] →
    [Lean.Grind.CommRing (Lean.Grind.Ring.OfSemiring.Q α)] → Mul (Lean.Grind.Ring.OfSemiring.Q α)
-- Mathlib.Combinatorics.Matroid.Minor.Delete
/-- `M ＼ D` refers to the deletion of a set `D` from the matroid `M`.  -/
Matroid.«term_＼_» : Lean.TrailingParserDescr
-- Mathlib.Tactic.Basic
_private.Mathlib.Tactic.Basic.0.Mathlib.Tactic.evalIntrov.intro1PStep : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.LinearAlgebra.Complex.Module
Complex.equivRealProdLm_symm_apply_re : ∀ (a : ℝ × ℝ), (Complex.equivRealProdLm.symm a).re = a.1
-- Lean.SubExpr
Lean.SubExpr.bindingDomain! : Lean.SubExpr → Lean.SubExpr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minView_k_eq_minView! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hl : l.Balanced}
  {hr : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size},
  (Std.DTreeMap.Internal.Impl.minView k v l r hl hr hlr).k = (Std.DTreeMap.Internal.Impl.minView! k v l r).k
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnriched.hComp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b c d : CategoryTheory.CatEnriched C}
  {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f') (θ : g ⟶ g') (κ : h ⟶ h'),
  CategoryTheory.CatEnriched.hComp (CategoryTheory.CatEnriched.hComp η θ) κ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatEnriched.hComp η (CategoryTheory.CatEnriched.hComp θ κ))
        (CategoryTheory.eqToHom ⋯))
-- Init.Data.List.MapIdx
List.head?_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : ℕ → α → β}, (List.mapIdx f l).head? = Option.map (f 0) l.head?
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.ofDarts_cons_cons : ∀ {V : Type u} {G : SimpleGraph V} {d₁ d₂ : G.Dart} {l : List G.Dart} (hchain : List.IsChain G.DartAdj (d₁ :: d₂ :: l)),
  SimpleGraph.Walk.ofDarts (d₁ :: d₂ :: l) ⋯ hchain = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.ofDarts (d₂ :: l) ⋯ ⋯)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.instCoeOut : {X : AlgebraicGeometry.Scheme} → CoeOut X.Opens AlgebraicGeometry.Scheme
-- Mathlib.RingTheory.Invariant.Profinite
instNonemptyObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {G : Type u}
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [inst_5 : SMulCommClass G A B] [inst_6 : TopologicalSpace G]
  [CompactSpace G] [IsTopologicalGroup G] (P : Ideal A) (Q : Ideal B) [Q.IsPrime] [inst_10 : Q.LiesOver P]
  [Algebra.IsInvariant A B G] (σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) (N : OpenNormalSubgroup G),
  Nonempty ((Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor P Q σ).obj N)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.pre_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)),
  ((CategoryTheory.StructuredArrow.pre S F G).obj X).right = F.obj X.right
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.up_length_toList_eq_count : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  (fun x => { down := x.length }) <$> it.toList = it.length
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.hadamard_assoc : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B C : Matrix m n α) [inst : Semigroup α],
  (A.hadamard B).hadamard C = A.hadamard (B.hadamard C)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.smul_trans : ∀ {S : Type u_14} {R : Type u_15} {V : Type u_16} {W : Type u_17} {G : Type u_18} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid V] [inst_3 : Module R V] [inst_4 : Module S V]
  [inst_5 : AddCommMonoid W] [inst_6 : Module R W] [inst_7 : Module S W] [inst_8 : AddCommMonoid G]
  [inst_9 : Module R G] [inst_10 : Module S G] [inst_11 : SMulCommClass R S W] [inst_12 : SMul S R]
  [inst_13 : IsScalarTower S R V] [inst_14 : IsScalarTower S R W] [inst_15 : SMulCommClass R S V]
  [inst_16 : IsScalarTower S R G] (α : Sˣ) (e : G ≃ₗ[R] V) (f : V ≃ₗ[R] W), (α • e) ≪≫ₗ f = α • e ≪≫ₗ f
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendHomologyIso_hom_homologyι : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'],
  CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').hom (K.homologyι j) =
    CategoryTheory.CategoryStruct.comp ((K.extend e).homologyι j') (K.extendOpcyclesIso e hj').hom
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- Additive subgroups of an additive group `Additive G` are isomorphic to subgroups of `G`.  -/
AddSubgroup.toSubgroup' : {G : Type u_1} → [inst : Group G] → AddSubgroup (Additive G) ≃o Subgroup G
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.singleTriangle.mor₁ = (DerivedCategory.singleFunctor C 0).map S.f
-- Init.Data.Range.Polymorphic.Map
Std.Rxo.IsAlwaysFinite.ofMap : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : LT α] [inst_3 : LT β] [Std.Rxo.IsAlwaysFinite β] (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesLT],
  Std.Rxo.IsAlwaysFinite α
-- Init.Data.String.Defs
/-- The end position of a slice, as a `Pos.Raw`.  -/
String.Slice.rawEndPos : String.Slice → String.Pos.Raw
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_withDensity_iff_integrable_coe_smul₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → NNReal},
  AEMeasurable f μ →
    ∀ {g : α → E},
      MeasureTheory.Integrable g (μ.withDensity fun x => ↑(f x)) ↔ MeasureTheory.Integrable (fun x => ↑(f x) • g x) μ
-- Lean.Util.ParamMinimizer
Lean.Util.ParamMinimizer.Status.missing.sizeOf_spec : sizeOf Lean.Util.ParamMinimizer.Status.missing = 1
-- Mathlib.Order.Types.Defs
OrderType.instOrderBot : OrderBot OrderType.{u_1}
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.max'_zero : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : LinearOrder α], Finset.max' 0 ⋯ = 0
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- A rational map restricts to a map from `Spec K(X)`.  -/
AlgebraicGeometry.Scheme.RationalMap.fromFunctionField : {X Y : AlgebraicGeometry.Scheme} →
  [inst : IrreducibleSpace ↥X] → X.RationalMap Y → (AlgebraicGeometry.Spec X.functionField ⟶ Y)
-- Std.Data.ExtDTreeMap.Basic
/-- Implementation detail of the tree map  -/
Std.ExtDTreeMap.mk : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → Std.ExtDTreeMap α β cmp
-- Mathlib.Topology.MetricSpace.Congruence
Congruent.symm : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂], Congruent v₁ v₂ → Congruent v₂ v₁
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.ReflectsFiniteProducts.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ (n : ℕ), CategoryTheory.Limits.ReflectsLimitsOfShape (CategoryTheory.Discrete (Fin n)) F) →
    CategoryTheory.Limits.ReflectsFiniteProducts F
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.BlockMem.instBoundedOrder.eq_1 : ∀ (G : Type u_1) [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] (a : X),
  MulAction.BlockMem.instBoundedOrder G a = { top := ⟨Set.univ, ⋯⟩, le_top := ⋯, bot := ⟨{a}, ⋯⟩, bot_le := ⋯ }
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.uliftFunctor.eq_1 : AddGrpCat.uliftFunctor =
  { obj := fun X => AddGrpCat.of (ULift.{u, v} ↑X),
    map := fun {x x_1} f =>
      AddGrpCat.ofHom
        (AddEquiv.ulift.symm.toAddMonoidHom.comp ((AddGrpCat.Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom)),
    map_id := ⋯, map_comp := ⋯ }
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_lt_one_mul : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℤ_[p]}, ‖z2‖ < 1 → ‖z1 * z2‖ < 1
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.ContainsIdentities.unop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ)
  [W.ContainsIdentities], W.unop.ContainsIdentities
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.concatCM_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {a b c : α}
  [inst_3 : Fact (a ≤ b)] [inst_4 : Fact (b ≤ c)] {E : Type u_2} [inst_5 : TopologicalSpace E] {x : ↑(Set.Icc a c)}
  (hx : ↑x ≤ b) {fg : { fg // fg.1 ⊤ = fg.2 ⊥ }}, (ContinuousMap.concatCM fg) x = (↑fg).1 ⟨↑x, ⋯⟩
-- Mathlib.GroupTheory.Congruence.Hom
/-- The diagram described by the universal property for quotients
of `AddMonoid`s, when the additive congruence relation is the kernel of the homomorphism,
commutes.  -/
AddCon.kerLift_mk : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {f : M →+ P} (x : M),
  (AddCon.kerLift f) ↑x = f x
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.not_rankPos_iff : ∀ {α : Type u_1} {M : Matroid α}, ¬M.RankPos ↔ M = Matroid.loopyOn M.E
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.preservesColimit_comp_of_createsColimit : ∀ {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} {E : Type u₃}
  [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  [CategoryTheory.CreatesColimit K F] [CategoryTheory.Limits.PreservesColimit K (F.comp G)],
  CategoryTheory.Limits.PreservesColimit (K.comp F) G
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle_inv : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Group (G i)] [inst_3 : ∀ (i : ι), SubgroupClass (S i) (G i)] (i : ι)
  (r : G i), RestrictedProduct.mulSingle A i r⁻¹ = (RestrictedProduct.mulSingle A i r)⁻¹
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- `addHaar` is some choice of a Haar measure, on a locally compact additive group.  -/
MeasureTheory.Measure.addHaar : {G : Type u_1} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalAddGroup G] →
        [inst : MeasurableSpace G] → [BorelSpace G] → [LocallyCompactSpace G] → MeasureTheory.Measure G
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.ofHom_apply : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : CommRing X] [inst_2 : Algebra R X] [inst_3 : CommRing Y]
  [inst_4 : Algebra R Y] (f : X →ₐ[R] Y) (x : X), (CategoryTheory.ConcreteCategory.hom (CommAlgCat.ofHom f)) x = f x
-- Mathlib.RingTheory.AdicCompletion.RingHom
IsAdicComplete.of_liftRingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S)
  [inst_2 : IsAdicComplete I S] (f : (n : ℕ) → R →+* S ⧸ I ^ n)
  (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) (x : R),
  (AdicCompletion.of I S) ((IsAdicComplete.liftRingHom I f ⋯) x) = (AdicCompletion.liftRingHom I f ⋯) x
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
instIsFiniteRelIndexGeneralLinearGroupAdjoinNegOne : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : Ring R] (𝒢 : Subgroup (GL n R)),
  𝒢.IsFiniteRelIndex 𝒢.adjoinNegOne
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.map_baseChange : ∀ {R : Type u} [inst : CommRing R] (C : WeierstrassCurve.VariableChange R) {S : Type s} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {A : Type v} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [IsScalarTower R S A] {B : Type w} [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B]
  [IsScalarTower R S B] (ψ : A →ₐ[S] B), (C.baseChange A).map ↑ψ = C.baseChange B
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The orthogonal complement of any submodule `K` is closed.  -/
Submodule.isClosed_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E), IsClosed ↑Kᗮ
-- Mathlib.RingTheory.Ideal.Colon
Submodule.mem_colon_singleton : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  {x : M} {r : R}, r ∈ N.colon {x} ↔ r • x ∈ N
-- Mathlib.Data.Multiset.Count
Multiset.countP_zero : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p], Multiset.countP p 0 = 0
-- Mathlib.Analysis.LocallyConvex.Montel
/-- The linear equivalence that sends a continuous linear map to the type copy endowed with the
topology of compact convergence.

This definition is only used to prove the continuous linear equivalence.  -/
_private.Mathlib.Analysis.LocallyConvex.Montel.0.LinearEquiv.toCompactConvergenceCLM : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          (E : Type u_3) →
            (F : Type u_4) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module 𝕜₁ E] →
                  [inst_4 : TopologicalSpace E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : Module 𝕜₂ F] →
                        [inst_7 : TopologicalSpace F] →
                          [inst_8 : IsTopologicalAddGroup F] →
                            [inst_9 : ContinuousSMul 𝕜₂ F] → (E →SL[σ] F) ≃ₗ[𝕜₂] CompactConvergenceCLM σ E F
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.real_smul_negPart_neg : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α),
  ∀ r < 0, (r • j).negPart = (-r).toNNReal • j.posPart
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Linear map version of the map `toAlternatingMap`
associating to a continuous alternating map the corresponding alternating map.  -/
ContinuousAlternatingMap.toAlternatingMapLinear : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        {ι : Type u_5} →
          [inst : Semiring R] →
            [inst_1 : Semiring A] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid N] →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : TopologicalSpace N] →
                      [inst_6 : ContinuousAdd N] →
                        [inst_7 : Module A M] →
                          [inst_8 : Module A N] →
                            [inst_9 : Module R N] →
                              [inst_10 : ContinuousConstSMul R N] →
                                [inst_11 : SMulCommClass A R N] → M [⋀^ι]→L[A] N →ₗ[R] M [⋀^ι]→ₗ[A] N
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k a : α},
      Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.erase! k t) = true →
        Std.DTreeMap.Internal.Impl.contains a t = true
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF →
    ∀ {k : α} {f : β → β},
      Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.Const.modify t k f) k =
        Option.map f (Std.DTreeMap.Raw.Const.get? t k)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_filter_key_eq_size_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → Bool},
  (Std.ExtDHashMap.filter (fun k x => f k) m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) = true
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsAlt.eq_of_add_add_eq_zero : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁]
  {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M},
  B.IsAlt → ∀ [IsCancelAdd M] {a b c : M₁}, a + b + c = 0 → (B a) b = (B b) c
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.instHasHomotopyCofiberOppositeMapSymmOpFunctorOp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} {F G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyFiber φ],
  HomologicalComplex.HasHomotopyCofiber ((HomologicalComplex.opFunctor C c).map φ.op)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- A group admitting a free group basis is a free group.  -/
FreeGroupBasis.isFreeGroup : ∀ {ι : Type u_1} {G : Type u_3} [inst : Group G] (b : FreeGroupBasis ι G), IsFreeGroup G
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.fundCocircuit_isCocircuit : ∀ {α : Type u_1} {M : Matroid α} {e : α} {B : Set α}, e ∈ B → M.IsBase B → M.IsCocircuit (M.fundCocircuit e B)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice},
  String.Slice.Pattern.ForwardPattern.skipPrefix? p s =
    String.Slice.Pattern.ForwardPattern.skipPrefix? (fun x => decide (p x)) s
-- Mathlib.Analysis.Normed.Field.Lemmas
Filter.inv_cobounded₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α], (Bornology.cobounded α)⁻¹ = nhdsWithin 0 {0}ᶜ
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preserves : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h₁ : S.LeftHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S], h₁.IsPreservedBy F
-- Init.Data.UInt.Bitwise
UInt64.or_zero : ∀ {a : UInt64}, a ||| 0 = a
-- Mathlib.Topology.Algebra.Group.Basic
map_add_right_nhds_zero : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (x : G),
  Filter.map (fun x_1 => x_1 + x) (nhds 0) = nhds x
-- Mathlib.GroupTheory.OrderOfElement
mod_natCard_nsmul : ∀ {G : Type u_6} [inst : AddGroup G] (a : G) (n : ℕ), (n % Nat.card G) • a = n • a
-- Mathlib.Topology.Order.Compact
/-- A continuous function with compact support has a global maximum.  -/
Continuous.exists_forall_ge_of_hasCompactMulSupport : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIciTopology α] [Nonempty β] [inst_5 : One α] {f : β → α},
  Continuous f → HasCompactMulSupport f → ∃ x, ∀ (y : β), f y ≤ f x
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instDistribLattice : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [DistribLattice β] → DistribLattice (l.Germ β)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.sum_strictMono : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : PartialOrder M]
  [IsOrderedCancelAddMonoid M], StrictMono fun f => ∑ x, f x
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.comp_toRingHom : ∀ {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : CommSemiring A] [inst_1 : CommSemiring B]
  [inst_2 : CommSemiring C] {I : Ideal A} {J : Ideal B} {K : Ideal C} {hI : DividedPowers I} {hJ : DividedPowers J}
  {hK : DividedPowers K} (g : hJ.DPMorphism hK) (f : hI.DPMorphism hJ), (g.comp f).toRingHom = g.comp f.toRingHom
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.postcomp_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  {W' : CategoryTheory.MorphismProperty C} [W.RespectsRight W'] [W.HasOfPostcompProperty W'] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), W' g → (W (CategoryTheory.CategoryStruct.comp f g) ↔ W f)
-- Mathlib.Data.Nat.Count
Nat.count_false : ∀ (n : ℕ), Nat.count (fun x => False) n = 0
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_iff_disjoint : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {v : ι → M},
  LinearIndepOn R v s ↔ Disjoint (Finsupp.supported R R s) (Finsupp.linearCombination R v).ker
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.map_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
  (f : W ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) CategoryTheory.Limits.prod.snd =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g
-- Mathlib.Data.List.Sym
List.sym.eq_1 : ∀ {α : Type u_1} (x : List α), List.sym 0 x = [Sym.nil]