mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.fderivCLM_eq_of_scalars : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n k : ℕ∞} {K : TopologicalSpace.Compacts E} (𝕜' : Type u_5)
  [inst_7 : NontriviallyNormedField 𝕜'] [inst_8 : NormedSpace 𝕜' F] [inst_9 : SMulCommClass ℝ 𝕜' F],
  ⇑(ContDiffMapSupportedIn.fderivCLM 𝕜 n k) = ⇑(ContDiffMapSupportedIn.fderivCLM 𝕜' n k)
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_add_right_closedBall : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoMetricSpace G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) (r : ℝ),
  (fun x => x + a) ⁻¹' Metric.closedBall b r = Metric.closedBall (b - a) r
-- Lean.Elab.MutualDef
Lean.Elab.Term.AsyncBodyInfo.mk : Lean.Elab.Term.AsyncBodyInfo
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.isPartial : Lean.Elab.Modifiers → Bool
-- Mathlib.MeasureTheory.Measure.Prod
AEMeasurable.lintegral_prod_left : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {f : α → β → ENNReal},
  AEMeasurable (Function.uncurry f) (μ.prod ν) → AEMeasurable (fun y => ∫⁻ (x : α), f x y ∂μ) ν
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Re-index the components of the tensor power by `e`.  -/
PiTensorProduct.reindex : {ι : Type u_1} →
  {ι₂ : Type u_2} →
    (R : Type u_4) →
      [inst : CommSemiring R] →
        (s : ι → Type u_7) →
          [inst_1 : (i : ι) → AddCommMonoid (s i)] →
            [inst_2 : (i : ι) → Module R (s i)] →
              (e : ι ≃ ι₂) → (PiTensorProduct R fun i => s i) ≃ₗ[R] PiTensorProduct R fun i => s (e.symm i)
-- Mathlib.Analysis.RCLike.Inner
RCLike.norm_wInner_le : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : Fintype ι] [inst_1 : RCLike 𝕜] {w : ι → ℝ} {f g : ι → 𝕜},
  0 ≤ w → ‖⟪f, g⟫_[𝕜, w]‖ ≤ ⟪fun i => ‖f i‖, fun i => ‖g i‖⟫_[ℝ, w]
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.sSup_of_not_bddAbove : ∀ {α : Type u_1} [inst : LE α] [inst_1 : SupSet α] {s : Set (WithBot α)}, ¬BddAbove s → sSup s = ⊥
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_eq_mul : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] {s : Finset ι} {f : ι → M} (a b : ι),
  a ≠ b → (∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) → (a ∉ s → f a = 1) → (b ∉ s → f b = 1) → ∏ x ∈ s, f x = f a * f b
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RioSliceData.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Rio α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β) (range_1 : Std.Rio α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.Algebra.Group.Shrink
equivShrink_symm_one : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : One α], (equivShrink α).symm 1 = 1
-- Mathlib.Data.Seq.Computation
Computation.map_comp : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (s : Computation α),
  Computation.map (g ∘ f) s = Computation.map g (Computation.map f s)
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModuleHierarchyImportsParams.mk.sizeOf_spec : ∀ (module : Lean.Lsp.LeanModule), sizeOf { module := module } = 1 + sizeOf module
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The basic open set of a section `f` on an affine open as an `X.affineOpens`.  -/
AlgebraicGeometry.Scheme.affineBasicOpen : (X : AlgebraicGeometry.Scheme) → {U : ↑X.affineOpens} → ↑(X.presheaf.obj (Opposite.op ↑U)) → ↑X.affineOpens
-- Init.System.Promise
/-- Like `Promise.result`, but resolves to `dflt` if the promise is dropped without ever being resolved.
 -/
IO.Promise.resultD : {α : Type} → IO.Promise α → α → Task α
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.hom_inv_s₁_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  {i j : E.I₀} (k : E.I₁ i j), e.inv.s₁ (e.hom.s₁ k) = (CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) k
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- This instance asserts that if `G` has a right-cancellative addition, a linear order,
and addition is strictly monotone w.r.t. the second argument, then `G` has `TwoUniqueSums`.  -/
TwoUniqueSums.of_covariant_right : ∀ {G : Type u} [inst : Add G] [IsRightCancelAdd G] [inst_2 : LinearOrder G] [AddLeftStrictMono G], TwoUniqueSums G
-- Mathlib.Algebra.Group.Action.Pretransitive
/-- The left regular action of a group on itself is transitive.  -/
MulAction.Regular.isPretransitive : ∀ {G : Type u_2} [inst : Group G], MulAction.IsPretransitive G G
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.isoMk_hom : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} {x : CommRing X} {x_1 : CommRing Y} {x_2 : HopfAlgebra R X}
  {x_3 : HopfAlgebra R Y} (e : X ≃ₐc[R] Y), (CommHopfAlgCat.isoMk e).hom = CommHopfAlgCat.ofHom ↑e
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_diff_le_size_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (m₁ \ m₂).size ≤ m₁.size
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n),
  ‖OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c‖ ≤ 1
-- Mathlib.Order.JordanHolder
JordanHolderLattice.sup_eq_of_isMaximal : ∀ {X : Type u} {inst : Lattice X} [self : JordanHolderLattice X] {x y z : X},
  JordanHolderLattice.IsMaximal x z → JordanHolderLattice.IsMaximal y z → x ≠ y → x ⊔ y = z
-- Init.Data.SInt.Basic
instReprAtomISize : ReprAtom ISize
-- Mathlib.Data.PNat.Find
PNat.find_spec : ∀ {p : ℕ+ → Prop} [inst : DecidablePred p] (h : ∃ n, p n), p (PNat.find h)
-- Mathlib.Algebra.Group.Prod
/-- The additive monoid equivalence between additive units of a product
of two additive monoids, and the product of the additive units of each additive monoid.  -/
AddEquiv.prodAddUnits : {M : Type u_3} →
  {N : Type u_4} → [inst : AddMonoid M] → [inst_1 : AddMonoid N] → AddUnits (M × N) ≃+ AddUnits M × AddUnits N
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- Auxiliary definition for `SSet.Truncated.liftOfStrictSegal`.  -/
SSet.Truncated.liftOfStrictSegal.f₂ : {X Y : SSet.Truncated 2} →
  (f₀ :
      X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
        Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })) →
    (f₁ :
        X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
          Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })) →
      (∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
          f₀
              ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op))
                x) =
            (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op))
              (f₁ x)) →
        (∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
            f₀
                ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op))
                  x) =
              (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op))
                (f₁ x)) →
          Y.StrictSegal →
            X.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ }) →
              Y.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ })
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.map_id : ∀ {α : Type u_1} [inst : Preorder α], Topology.WithLowerSet.map OrderHom.id = ContinuousMap.id (Topology.WithLowerSet α)
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_splits_map : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : CommRing S] [inst_2 : IsDomain S] {f : Polynomial R}
  (i : R →+* S), (Polynomial.map i f).Splits → (∀ a ∈ (Polynomial.map i f).roots, a ∈ i.range) → f.Splits
-- Mathlib.Logic.Function.Defs
/-- Compose a binary function `f` with a pair of unary functions `g` and `h`.
If both arguments of `f` have the same type and `g = h`, then `bicompl f g g = f on g`.  -/
Function.bicompl : {α : Sort u_1} →
  {β : Sort u_2} → {γ : Sort u_3} → {δ : Sort u_4} → {ε : Sort u_5} → (γ → δ → ε) → (α → γ) → (β → δ) → α → β → ε
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstLVal.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.NumberTheory.ADEInequality
/-- `E' r := {2,3,r}` is a `Multiset ℕ+`.
For `r ∈ {3,4,5}` is a solution to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`.

These solutions are related to the Dynkin diagrams $E_{r+3}$.  -/
ADEInequality.E' : ℕ+ → Multiset ℕ+
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ},
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) ↔ ∃ x ∈ t, x.1 = a ∧ x.2.2 = c
-- Mathlib.CategoryTheory.SmallObject.Basic
/-- When `I : MorphismProperty C` permits the small object argument,
this is a cardinal `κ` such that `IsCardinalForSmallObjectArgument I κ` holds.  -/
CategoryTheory.MorphismProperty.smallObjectκ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) → [I.HasSmallObjectArgument] → Cardinal.{w}
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normalClosure_le_iff_of_normal : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] [Normal F L]
  {K₁ K₂ : IntermediateField F L} [Normal F ↥K₂], IntermediateField.normalClosure F (↥K₁) L ≤ K₂ ↔ K₁ ≤ K₂
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.inl_biprodXIso_inv_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) {Z : C} (h : (K ⊞ L).X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (CategoryTheory.CategoryStruct.comp (K.biprodXIso L i).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) h
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.mk₀_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y : C} [inst_3 : CategoryTheory.Preadditive C] (m₀ : M) (hm₀ : m₀ = 0)
  (f g : X ⟶ Y),
  CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ (f + g) =
    CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ f + CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ g
-- Mathlib.Order.Cover
/-- **Alias** of the forward direction of `wcovBy_iff_covBy_or_eq`. -/
WCovBy.covBy_or_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⩿ b → a ⋖ b ∨ a = b
-- Mathlib.Topology.UniformSpace.Ultra.Basic
IsUltraUniformity.mem_nhds_iff_symm_trans : ∀ {X : Type u_1} [inst : UniformSpace X] [IsUltraUniformity X] {x : X} {s : Set X},
  s ∈ nhds x ↔ ∃ V ∈ uniformity X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ UniformSpace.ball x V ⊆ s
-- Mathlib.Dynamics.Transitive
/-- An action of a monoid `M` on `α` that is continuous in the second argument is topologically
transitive if and only if any nonempty open subset `U` of `α` with `(m • ·) ⁻¹' U ⊆ U` for all
`m : M` is dense in `α`.  -/
MulAction.isTopologicallyTransitive_iff_dense_of_preimage_invariant : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Monoid M] [inst_2 : MulAction M α]
  [h : ContinuousConstSMul M α],
  MulAction.IsTopologicallyTransitive M α ↔
    ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun x => m • x) ⁻¹' U ⊆ U) → Dense U
-- Init.Data.UInt.Lemmas
UInt32.neg_mul_comm : ∀ (a b : UInt32), -a * b = a * -b
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.hasBasis_nhds_one_of_basis : ∀ {α : Type u_1} {G : Type u_2} {ι : Type u_3} [inst : Group G] [inst_1 : UniformSpace G] [IsUniformGroup G]
  {p : ι → Prop} {b : ι → Set G},
  (nhds 1).HasBasis p b → (nhds 1).HasBasis p fun i => {f | ∀ (x : α), UniformFun.toFun f x ∈ b i}
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
/-- Exactness of `Hᵢ(G, X₁) ⟶ Hᵢ(G, X₂) ⟶ Hᵢ(G, X₃)`.  -/
groupHomology.mapShortComplex₂_exact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)},
  X.ShortExact → ∀ (i : ℕ), (groupHomology.mapShortComplex₂ X i).Exact
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.NatTrans.prod_app_snd : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {F G : CategoryTheory.Functor A B} {H I : CategoryTheory.Functor C D}
  (α : F ⟶ G) (β : H ⟶ I) (X : A × C), ((CategoryTheory.NatTrans.prod α β).app X).2 = β.app X.2
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
SimplexCategoryGenRel.instIsSplitEpiσ : ∀ {n : ℕ} {i : Fin (n + 1)}, CategoryTheory.IsSplitEpi (SimplexCategoryGenRel.σ i)
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.augmentedCechNerve_obj_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (f : CategoryTheory.Arrow C) (x : SimplexCategoryᵒᵖ),
  (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).hom.app x =
    CategoryTheory.Limits.WidePullback.base fun x => f.hom
-- Mathlib.Data.Finset.NAry
Finset.forall_mem_image₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  {p : γ → Prop}, (∀ z ∈ Finset.image₂ f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)
-- Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Module.Free.linearMap : ∀ (R : Type u) (S : Type u') (M : Type v) (N : Type w) [inst : Ring R] [inst_1 : Ring S] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.Free R M] [Module.Finite R M] [inst_6 : AddCommGroup N] [inst_7 : Module R N]
  [inst_8 : Module S N] [inst_9 : SMulCommClass R S N] [Module.Free S N], Module.Free S (M →ₗ[R] N)
-- Mathlib.Data.Fin.Tuple.Take
/-- `Fin.take` intertwines with `List.take` via `List.ofFn`.  -/
Fin.ofFn_take_eq_take_ofFn : ∀ {n : ℕ} {α : Type u_2} {m : ℕ} (h : m ≤ n) (v : Fin n → α), List.ofFn (Fin.take m h v) = List.take m (List.ofFn v)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.edist_snd_le : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] (x y : WithLp p (α × β)), edist x.snd y.snd ≤ edist x y
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.run_eq_map : ∀ {m : Type w → Type w'} [inst : Monad m] {α : Type w} {x : Std.Iterators.PostconditionT m α},
  x.run = Subtype.val <$> x.operation
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.conjugateEquiv_leftAdjointCompIso_inv : ∀ {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₁] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₂]
  {F₀₁ : CategoryTheory.Functor C₀ C₁} {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₀₂ : CategoryTheory.Functor C₀ C₂}
  {G₁₀ : CategoryTheory.Functor C₁ C₀} {G₂₁ : CategoryTheory.Functor C₂ C₁} {G₂₀ : CategoryTheory.Functor C₂ C₀}
  (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₀₂ : F₀₂ ⊣ G₂₀) (e₀₁₂ : G₂₁.comp G₁₀ ≅ G₂₀),
  (CategoryTheory.conjugateEquiv (adj₀₁.comp adj₁₂) adj₀₂) (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂).inv = e₀₁₂.hom
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.isLimitWhiskerEquiv.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.Cone G),
  CategoryTheory.Functor.Initial.isLimitWhiskerEquiv F t = CategoryTheory.Functor.Initial.isLimitWhiskerEquiv F t
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.coe_toLieModuleHom : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N), ⇑e.toLieModuleHom = ⇑e
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The variant of `is_left_invariant_chaar` for `haarContent`  -/
MeasureTheory.Measure.haar.is_left_invariant_haarContent : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} (g : G) (K : TopologicalSpace.Compacts G),
  (MeasureTheory.Measure.haar.haarContent K₀) (TopologicalSpace.Compacts.map (fun x => g * x) ⋯ K) =
    (MeasureTheory.Measure.haar.haarContent K₀) K
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.termη : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.mk : Int.Internal.Linear.Poly → Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof → Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.
 -/
MeasureTheory.Measure : (α : Type u_6) → [MeasurableSpace α] → Type u_6
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_inv_fac_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesLeftKanExtension F L] [inst_5 : L.HasLeftKanExtension F]
  {Z : CategoryTheory.Functor A D} (h : L.comp ((L.leftKanExtension F).comp G) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.leftKanExtensionUnit (F.comp G))
      (CategoryTheory.CategoryStruct.comp (L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).inv) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L.leftKanExtensionUnit F) G)
      (CategoryTheory.CategoryStruct.comp (L.associator (L.leftKanExtension F) G).hom h)
-- Mathlib.Algebra.Star.Basic
/-- A non-unital non-associative ring endowed with `star` is a star ring if it admits an injective
map that preserves `star`, `*` and `+` to a star ring. See note [reducible non-instances].  -/
Function.Injective.starRing : {R : Type u} →
  {S : Type v} →
    (f : R → S) →
      [inst : Star R] →
        [inst_1 : NonUnitalNonAssocSemiring R] →
          [inst_2 : NonUnitalNonAssocSemiring S] →
            [inst_3 : StarRing S] →
              Function.Injective f →
                (∀ (x : R), f (star x) = star (f x)) →
                  (∀ (x y : R), f (x + y) = f x + f y) → (∀ (x y : R), f (x * y) = f x * f y) → StarRing R
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` preserves limits of shape `Jᵒᵖ`, then `F : Cᵒᵖ ⥤ D` preserves colimits
of shape `J`.  -/
CategoryTheory.Limits.preservesColimitsOfShape_of_rightOp : ∀ {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] (F : CategoryTheory.Functor Cᵒᵖ D)
  [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F.rightOp], CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Mathlib.CategoryTheory.Category.Quiv
/-- Naturality of `pathComposition`, which defines a natural transformation
`Quiv.forget ⋙ Cat.free ⟶ 𝟭 _`.  -/
CategoryTheory.Quiv.pathComposition_naturality : ∀ {C : Type u} {D : Type u₁} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (F : CategoryTheory.Functor C D),
  (CategoryTheory.Cat.freeMap F.toPrefunctor).comp (CategoryTheory.pathComposition D) =
    (CategoryTheory.pathComposition C).comp F
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.StructuredArrow.functor_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (T : CategoryTheory.Functor C D) {X Y : Dᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.StructuredArrow.functor T).map f = (CategoryTheory.StructuredArrow.map f.unop).toCatHom
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The structure of two-sided continuous isomorphisms between additive groups.
Note that both the map and its inverse have to be continuous.  -/
ContinuousAddEquiv : (G : Type u) → [TopologicalSpace G] → (H : Type v) → [TopologicalSpace H] → [Add G] → [Add H] → Type (max u v)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.values_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.values = t₂.values
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.instInhabited : {μ : YoungDiagram} → Inhabited (SemistandardYoungTableau μ)
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
/-- `R` is integrally closed in `A` if all integral elements of `A` are also elements of `R`.
 -/
IsIntegrallyClosedIn : (R : Type u_1) → (A : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Prop
-- Init.Data.SInt.Bitwise
Int8.and_zero : ∀ {a : Int8}, a &&& 0 = 0
-- Mathlib.Algebra.Order.SuccPred.WithBot
WithBot.one_le_iff_pos : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero 1] [SuccAddOrder α]
  (a : WithBot α), 1 ≤ a ↔ 0 < a
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.coe_divXPowOrderHom : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : NoZeroDivisors R] [inst_2 : Nontrivial R],
  ⇑PowerSeries.divXPowOrderHom = PowerSeries.divXPowOrder
-- Mathlib.Algebra.Group.Hom.Basic
/-- A homomorphism from an additive group to an additive monoid is injective iff its
kernel is trivial, stated as an iff on the triviality of the kernel. For the implication, see
`injective_iff_map_eq_zero`.  -/
injective_iff_map_eq_zero' : ∀ {F : Type u_7} {G : Type u_8} {H : Type u_9} [inst : AddGroup G] [inst_1 : AddZeroClass H] [inst_2 : FunLike F G H]
  [AddMonoidHomClass F G H] (f : F), Function.Injective ⇑f ↔ ∀ (a : G), f a = 0 ↔ a = 0
-- Mathlib.Algebra.Group.Action.End
/-- **Alias** of `AddAut.apply_faithfulVAdd`.

---

`AddAut.applyAddDistribAddAction` is faithful.  -/
AddAut.apply_faithfulSMul : ∀ {M : Type u_2} [inst : AddMonoid M], FaithfulVAdd (AddAut M) M
-- Mathlib.Algebra.Order.Group.PosPart
negPart_nonpos : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], a⁻ ≤ 0 ↔ 0 ≤ a