mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_f_desc_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain F K (-1)) (β : G ⟶ K)
  (eq :
    CochainComplex.HomComplex.δ (-1) 0 α =
      CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
  (p : ℤ) {Z : C} (h : K.X p ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.desc φ α β eq).f p) h) =
    CategoryTheory.CategoryStruct.comp (β.f p) h
-- Init.Data.BitVec.Lemmas
/-- If the current width `w` is smaller than the extended width `v`,
then the value when interpreted as an integer does not change.
 -/
BitVec.toInt_signExtend_of_le : ∀ {w v : ℕ} {x : BitVec w}, w ≤ v → (BitVec.signExtend v x).toInt = x.toInt
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.Hom.match_1.eq_1 : ∀ {C : Type u_1} (motive : CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → Sort u_2) (X Y : C)
  (h_1 : (X Y : C) → motive (CategoryTheory.WithInitial.of X) (CategoryTheory.WithInitial.of Y))
  (h_2 : (a : C) → (x : CategoryTheory.WithInitial C) → motive (CategoryTheory.WithInitial.of a) x)
  (h_3 : (x : CategoryTheory.WithInitial C) → motive CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.of X, CategoryTheory.WithInitial.of Y with
    | CategoryTheory.WithInitial.of X, CategoryTheory.WithInitial.of Y => h_1 X Y
    | CategoryTheory.WithInitial.of a, x => h_2 a x
    | CategoryTheory.WithInitial.star, x => h_3 x) =
    h_1 X Y
-- Mathlib.Analysis.Normed.Operator.NNNorm
/-- If one controls the norm of every `A x`, `‖x‖₊ ≠ 0`, then one controls the norm of `A`.  -/
ContinuousLinearMap.opNNNorm_le_bound' : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F) (M : NNReal), (∀ (x : E), ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊) → ‖f‖₊ ≤ M
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- Every function is Lipschitz on the empty set (with any Lipschitz constant).  -/
lipschitzOnWith_empty : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (K : NNReal) (f : α → β),
  LipschitzOnWith K f ∅
-- Mathlib.Tactic.Sat.FromLRAT
/-- If `f` subsumes `c` (i.e. `c ∈ f`), then `f.proof c`.  -/
Sat.Fmla.proof_of_subsumes : ∀ {f : Sat.Fmla} {c : Sat.Clause}, f.subsumes (Sat.Fmla.one c) → f.proof c
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y : C) (U : CategoryTheory.Over X),
  (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)).counit.app
      U =
    CategoryTheory.Over.homMk (CategoryTheory.SemiCartesianMonoidalCategory.fst U.left Y) ⋯
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.gi.eq_1 : ∀ (M : Type u_1) [inst : AddZeroClass M],
  AddSubmonoid.gi M = { choice := fun s x => AddSubmonoid.closure s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
/-- The (curried version of the) external product bifunctor: given diagrams
`K₁ : J₁ ⥤ C` and `K₂ : J₂ ⥤ C`, this is the bifunctor `j₁ ↦ j₂ ↦ K₁ j₁ ⊗ K₂ j₂`.  -/
CategoryTheory.MonoidalCategory.externalProductBifunctorCurried : (J₁ : Type u₁) →
  (J₂ : Type u₂) →
    (C : Type u₃) →
      [inst : CategoryTheory.Category.{v₁, u₁} J₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            [CategoryTheory.MonoidalCategory C] →
              CategoryTheory.Functor (CategoryTheory.Functor J₁ C)
                (CategoryTheory.Functor (CategoryTheory.Functor J₂ C)
                  (CategoryTheory.Functor J₁ (CategoryTheory.Functor J₂ C)))
-- Mathlib.Algebra.Lie.Normalizer
LieSubalgebra.normalizer_eq_self_iff : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L), H.normalizer = H ↔ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule) = ⊥
-- Std.Time.Zoned.TimeZone
/-- The `Offset` of the date time.
 -/
Std.Time.TimeZone.offset : Std.Time.TimeZone → Std.Time.TimeZone.Offset
-- Mathlib.NumberTheory.Ostrowski
/-- **Ostrowski's Theorem**: every absolute value (with values in `ℝ`) on `ℚ` is equivalent
to either the standard absolute value or a `p`-adic absolute value for a prime `p`.  -/
Rat.AbsoluteValue.equiv_real_or_padic : ∀ (f : AbsoluteValue ℚ ℝ),
  f.IsNontrivial → f ≈ Rat.AbsoluteValue.real ∨ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ Rat.AbsoluteValue.padic p
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.le_of_mem : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), J ∈ π → J ≤ I
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.addCayley_empty : ∀ {M : Type u_1} [inst : Add M], SimpleGraph.addCayley ∅ = ⊥
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- Any two algebras whose quadratic forms differ by a bilinear form are isomorphic as modules.

This is $\bar \lambda_B$ from [bourbaki2007] §9 Proposition 3.  -/
CliffordAlgebra.changeFormEquiv : {R : Type u1} →
  [inst : CommRing R] →
    {M : Type u2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {Q Q' : QuadraticForm R M} →
            {B : LinearMap.BilinForm R M} →
              LinearMap.BilinMap.toQuadraticMap B = Q' - Q → CliffordAlgebra Q ≃ₗ[R] CliffordAlgebra Q'
-- Mathlib.MeasureTheory.Order.Lattice
/-- We say that a type has `MeasurableSup` if `(c ⊔ ·)` and `(· ⊔ c)` are measurable functions.
For a typeclass assuming measurability of `uncurry (· ⊔ ·)` see `MeasurableSup₂`.  -/
MeasurableSup : (M : Type u_1) → [MeasurableSpace M] → [Max M] → Prop
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.mul_of_commute : ∀ {S : Type u_3} [inst : Semigroup S] {a b : S},
  Commute a b → IsIdempotentElem a → IsIdempotentElem b → IsIdempotentElem (a * b)
-- Lean.Elab.DocString
Lean.Doc.SuggestionMode.noConfusionType : Sort v✝ → Lean.Doc.SuggestionMode → Lean.Doc.SuggestionMode → Sort v✝
-- Init.Data.Array.Lex.Lemmas
Array.instDecidableLTOfDecidableEq : {α : Type u_1} → [DecidableEq α] → [inst : LT α] → [DecidableLT α] → DecidableLT (Array α)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lt_sub : ∀ {a b c : Ordinal.{u_4}}, a < b - c ↔ c + a < b
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RcoSliceData.mk.injEq : ∀ {α : Type u} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit) (range : Std.Rco α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit) (range_1 : Std.Rco α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.trinomial_monic : ∀ {R : Type u_1} [inst : Semiring R] {k m n : ℕ} {u v : R}, k < m → m < n → (Polynomial.trinomial k m n u v 1).Monic
-- Mathlib.Computability.Partrec
Computable.partrec : ∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → σ}, Computable f → Partrec ↑f
-- Mathlib.CategoryTheory.Functor.Hom
CategoryTheory.Functor.hom_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : Cᵒᵖ × C} (f : X ⟶ Y),
  (CategoryTheory.Functor.hom C).map f =
    TypeCat.ofHom fun h => CategoryTheory.CategoryStruct.comp f.1.unop (CategoryTheory.CategoryStruct.comp h f.2)
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.hom_comp : ∀ {X Y T : GrpCat} (f : X ⟶ Y) (g : Y ⟶ T),
  GrpCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (GrpCat.Hom.hom g).comp (GrpCat.Hom.hom f)
-- Mathlib.Tactic.Determinant.Bird.Meta
Mathlib.Tactic.Determinant.ReifiedBirdDet.mk.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} (rα : Q(CommRing «$α»)) (ctx : Mathlib.Tactic.Determinant.Ctx rα),
  sizeOf { u := u, α := α, rα := rα, ctx := ctx } = 1 + sizeOf u + sizeOf α + sizeOf rα + sizeOf ctx
-- Mathlib.CategoryTheory.Monad.Types
CategoryTheory.kleisliCatEquivKleisli_functor_obj_of : ∀ (m : Type u → Type u) [inst : Monad m] [inst_1 : LawfulMonad m] (X : CategoryTheory.KleisliCat m),
  ((CategoryTheory.kleisliCatEquivKleisli m).functor.obj X).of = X
-- Mathlib.Geometry.Euclidean.MongePoint
/-- **Sylvester's theorem**, specialized to triangles.  -/
Affine.Triangle.orthocenter_vsub_circumcenter_eq_sum_vsub : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P),
  t.orthocenter -ᵥ Affine.Simplex.circumcenter t = ∑ i, (t.points i -ᵥ Affine.Simplex.circumcenter t)
-- Mathlib.Analysis.Convex.Combination
convexHull_sum : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] {ι : Type u_8} (s : Finset ι) (t : ι → Set E),
  (convexHull R) (∑ i ∈ s, t i) = ∑ i ∈ s, (convexHull R) (t i)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.find?_toArray_eq_some_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {v : β k},
  Array.find? (fun x => cmp x.fst k == Ordering.eq) t.toArray = some ⟨k, v⟩ ↔ t.get? k = some v
-- Mathlib.Probability.Distributions.TwoValued
/-- If a random variable is ae equal to `0` or `1`, then its variance is the product of
the probabilities that it's equal to `0` and that it's equal to `1`.  -/
ProbabilityTheory.variance_of_ae_eq_zero_or_one : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsZeroOrProbabilityMeasure μ],
  AEMeasurable X μ →
    (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → ProbabilityTheory.variance X μ = μ.real {ω | X ω = 0} * μ.real {ω | X ω = 1}
-- Lean.Server.FileWorker.Utils
/-- Returns all current diagnostics (sticky ++ doc).  -/
Lean.Server.FileWorker.EditableDocumentCore.collectCurrentDiagnostics : Lean.Server.FileWorker.EditableDocumentCore → BaseIO (Lean.PersistentArray Lean.Widget.InteractiveDiagnostic)
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.support_abs : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [IsOrderedAddMonoid R] (x : Lex (HahnSeries Γ R)), (ofLex |x|).support = (ofLex x).support
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.GrindM : Type → Type
-- Mathlib.Analysis.Normed.Group.Basic
nndist_eq_nnnorm_sub : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E), nndist a b = ‖a - b‖₊
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.primesOver_bot : ∀ (A : Type u_1) [inst : CommRing A] (B : Type u_2) [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Algebra.IsIntegral A B] [Module.IsTorsionFree A B] [IsDomain A] [IsDomain B], ⊥.primesOver B = {⊥}
-- Lean.Server.Rpc.Basic
Lean.Lsp.instBEqRpcRef : BEq Lean.Lsp.RpcRef
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.toGrothendieck_bot : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C], ⊥.toGrothendieck = ⊥
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.toEquivalence_counitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [inst_2 : ∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)]
  [inst_3 : ∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] (X : D),
  adj.toEquivalence.counitIso.inv.app X = CategoryTheory.inv (adj.counit.app X)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Noncomputably make a limit cone from the existence of unique factorizations.  -/
CategoryTheory.Limits.Fork.IsLimit.ofExistsUnique : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {t : CategoryTheory.Limits.Fork f g} →
          (∀ (s : CategoryTheory.Limits.Fork f g), ∃! l, CategoryTheory.CategoryStruct.comp l t.ι = s.ι) →
            CategoryTheory.Limits.IsLimit t
-- Mathlib.Data.List.Basic
List.map_subset_iff : ∀ {α : Type u} {β : Type v} {l₁ l₂ : List α} (f : α → β),
  Function.Injective f → (List.map f l₁ ⊆ List.map f l₂ ↔ l₁ ⊆ l₂)
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projection_apply`. -/
Submodule.IsCompl.projection_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : E), (p.projection q hpq) x = ↑((p.projectionOnto q hpq) x)
-- Mathlib.CategoryTheory.Category.Preorder
OrderIso.equivalence_unitIso : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (e : X ≃o Y),
  e.equivalence.unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
-- Init.Data.Range.Polymorphic.Basic
Std.Roo.lt_upper_of_mem : ∀ {α : Type u} {r : Std.Roo α} {a : α} [inst : LT α], a ∈ r → a < r.upper
-- Init.Data.UInt.Lemmas
UInt8.sub_def : ∀ (a b : UInt8), a - b = { toBitVec := a.toBitVec - b.toBitVec }
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.instEnrichedCategoryCat : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] →
      CategoryTheory.EnrichedCategory CategoryTheory.Cat (CategoryTheory.CatEnrichedOrdinary C)
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `α` is a type, then `FreeGroup α` is the free group generated by `α`.
This is a group equipped with a function `FreeGroup.of : α → FreeGroup α` which has
the following universal property: if `G` is any group, and `f : α → G` is any function,
then this function is the composite of `FreeGroup.of` and a unique group homomorphism
`FreeGroup.lift f : FreeGroup α →* G`.

A typical element of `FreeGroup α` is a formal product of
elements of `α` and their formal inverses, quotient by reduction.
For example if `x` and `y` are terms of type `α` then `x⁻¹ * y * y * x * y⁻¹` is a
"typical" element of `FreeGroup α`. In particular if `α` is empty
then `FreeGroup α` is isomorphic to the trivial group, and if `α` has one term
then `FreeGroup α` is isomorphic to `Multiplicative ℤ`.
If `α` has two or more terms then `FreeGroup α` is not commutative.


[Wikidata Q431078](https://www.wikidata.org/wiki/Q431078) -/
FreeGroup : Type u → Type u
-- Mathlib.Logic.Function.DependsOn
Set.dependsOn_domRestrict : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Set ι), DependsOn s.domRestrict s
-- Lean.Meta.Tactic.Grind.EMatchAction
/-- Creates an `instantiate` tactic that takes the `usedThms` as parameters.
 -/
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.mkInstantiateTactic : Lean.Meta.Grind.Goal → Array Lean.Meta.Grind.EMatchTheorem → Bool → Lean.Meta.Grind.GrindM Lean.Meta.Grind.TGrind
-- Init.Data.List.Sublist
List.suffix_append : ∀ {α : Type u_1} (l₁ l₂ : List α), l₂ <:+ l₁ ++ l₂
-- Mathlib.Topology.Compactness.LocallyCompact
Function.locallyCompactSpace_of_finite : ∀ {Y : Type u_2} {ι : Type u_3} [inst : TopologicalSpace Y] [Finite ι] [LocallyCompactSpace Y],
  LocallyCompactSpace (ι → Y)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (t.alter k f).minKey? = some k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β}, (t.insertIfNew k v)[a]? = if cmp k a = Ordering.eq ∧ k ∉ t then some v else t[a]?
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.vadd_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {𝕜 : Type u_5} [inst_1 : TopologicalSpace 𝕜] [inst_2 : VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α → 𝕜},
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (c : β), MeasureTheory.AEStronglyMeasurable (fun x => f x +ᵥ c) μ
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.IsSymm.exp : ∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommRing 𝔸]
  [inst_3 : TopologicalSpace 𝔸] [inst_4 : IsTopologicalRing 𝔸] [Algebra ℚ 𝔸] [T2Space 𝔸] {A : Matrix m m 𝔸},
  A.IsSymm → (NormedSpace.exp A).IsSymm
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.instGroupSubtypeMemSubmonoid.eq_1 : ∀ {M : Type u_1} [inst : Monoid M],
  Submonoid.instGroupSubtypeMemSubmonoid =
    { toMonoid := inferInstance, inv := fun x => ⟨↑(IsUnit.unit ⋯)⁻¹, ⋯⟩, div := DivInvMonoid.div', zpow := zpowRec,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.instRing : {R : Type u_1} →
  {N₁ : Type u_8} → [inst : Semiring R] → [inst_1 : AddCommGroup N₁] → [inst_2 : Module R N₁] → Ring (Module.End R N₁)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.SubobjectRepresentableBy.uniq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {U X : C} {m : U ⟶ X} [inst_2 : CategoryTheory.Mono m] {χ' : X ⟶ Ω}
  {π : U ⟶ CategoryTheory.Subobject.underlying.obj h.Ω₀}, CategoryTheory.IsPullback m π χ' h.Ω₀.arrow → χ' = h.χ m
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.lcoeFun_apply : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : α →₀ M), Finsupp.lcoeFun f = ⇑f
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_zero : ∀ {R : Type u} {M : Type v} [inst : Zero R] [inst_1 : Zero M], TrivSqZeroExt.fst 0 = 0
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.inf : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SemilatticeInf β] {f g : α → β} {a : α} {s : Set α},
  IsLocalMinOn f s a → IsLocalMinOn g s a → IsLocalMinOn (fun x => f x ⊓ g x) s a
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.unopSymm_X : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex Vᵒᵖ c.symm) (i : ι),
  X.unopSymm.X i = Opposite.unop (X.X i)
-- Mathlib.Data.Fin.SuccPredOrder
Fin.orderPred_apply : ∀ {n : ℕ} (i : Fin (n + 1)), Order.pred i = Fin.cases 0 Fin.castSucc i
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.getStackEntries.loop.reduce : Array Lean.Expr →
  Lean.Expr →
    ℕ →
      ℕ →
        (ℕ → Lean.Expr → Lean.Expr → Lean.BinderInfo → Lean.MetaM (List Lean.Meta.RefinedDiscrTree.StackEntry)) →
          Lean.MetaM (List Lean.Meta.RefinedDiscrTree.StackEntry)
-- Std.Http.Protocol.H1.Parser
/-- Result of parsing partial or complete information.
 -/
Std.Http.Protocol.H1.TakeResult : Type
-- Mathlib.Data.Nat.Choose.Lucas
/-- For primes `p` and positive integer `n`, assume that for all `i ∈ Icc 1 (n - 1)`,
`choose n i` congruent to `0` module `p`, then `n = p ^ multiplicity p n`.
Also see `eq_pow_multiplicity_of_choose_modEq_zero` for the version with `ZMOD`.  -/
Choose.eq_pow_multiplicity_of_choose_modEq_zero_nat : ∀ {n p : ℕ} [Fact (Nat.Prime p)],
  0 < n → (∀ i ∈ Finset.Icc 1 (n - 1), n.choose i ≡ 0 [MOD p]) → n = p ^ multiplicity p n
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_filterMap : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] [inst_3 : Inhabited α] {f : (a : α) → β a → Option (γ a)} {k : α}
  (h : (↑m).WF),
  (Std.DHashMap.Internal.Raw₀.filterMap f m).getKey! k =
    ((m.getKey? k).pfilter fun x h' => (f x (m.get x ⋯)).isSome).get!
-- Mathlib.Order.Restriction
Preorder.frestrictLe₂_comp_frestrictLe₂ : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} [inst_1 : LocallyFiniteOrderBot α] {a b c : α} (hab : a ≤ b)
  (hbc : b ≤ c), Preorder.frestrictLe₂ hab ∘ Preorder.frestrictLe₂ hbc = Preorder.frestrictLe₂ ⋯
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.lpMeasToLpTrim_smul : ∀ {α : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {p : ENNReal} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (c : 𝕜)
  (f : ↥(MeasureTheory.lpMeas F 𝕜 m p μ)),
  MeasureTheory.lpMeasToLpTrim F 𝕜 p μ hm (c • f) = c • MeasureTheory.lpMeasToLpTrim F 𝕜 p μ hm f
-- Mathlib.Algebra.Group.ForwardDiff
/-- Linear-endomorphism version of the shift-by-1 operator.  -/
fwdDiff_aux.shiftₗ : (M : Type u_1) → (G : Type u_2) → [AddCommMonoid M] → [inst : AddCommGroup G] → M → Module.End ℤ (M → G)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.instSemilatticeSup : {α : Type u_1} → [inst : TopologicalSpace α] → SemilatticeSup (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
/-- A left Kan lift `t` of the identity along `u` that commutes with `u`, in the sense that
`t.whisker u` is a left Kan lift, is a left adjoint to `u`. The unit of this adjoint is given by
the unit of the Kan lift.  -/
CategoryTheory.Bicategory.LeftLift.IsKan.adjunction : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {u : b ⟶ a} →
        {t : CategoryTheory.Bicategory.LeftLift u (CategoryTheory.CategoryStruct.id a)} →
          t.IsKan → (t.whisker u).IsKan → CategoryTheory.Bicategory.Adjunction t.lift u
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
/-- For type-valued presheaves, the sheaf condition in terms of unique gluings is equivalent to the
usual sheaf condition.
 -/
TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_types : ∀ {X : TopCat} (F : TopCat.Presheaf (Type u_4) X), F.IsSheaf ↔ F.IsSheafUniqueGluing
-- Mathlib.Algebra.RingQuot
RingQuot.toQuot : {R : Type uR} → [inst : Semiring R] → {r : R → R → Prop} → RingQuot r → Quot (RingQuot.Rel r)
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (fiber : CategoryTheory.Functor C (Type w)) →
        autoParam (CategoryTheory.IsCofiltered fiber.Elements)
            CategoryTheory.GrothendieckTopology.Point.isCofiltered._autoParam →
          autoParam (CategoryTheory.InitiallySmall fiber.Elements)
              CategoryTheory.GrothendieckTopology.Point.initiallySmall._autoParam →
            (∀ {X : C},
                ∀ R ∈ J X,
                  ∀ (x : fiber.obj X),
                    ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (CategoryTheory.ConcreteCategory.hom (fiber.map f)) y = x) →
              J.Point
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn.isCompatible_iff : ∀ {n : ℕ} {X : SSet} {i : Fin (n + 3)} (f : (j : Fin (n + 3)) → j ≠ i → (SSet.stdSimplex.obj { len := n + 1 } ⟶ X)),
  SSet.horn.IsCompatible f ↔
    ∀ (j k : Fin (n + 3)) (hj : j ≠ i) (hk : k ≠ i) (hjk : j < k),
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ (k.pred ⋯)) (f j hj) =
        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ (j.castPred ⋯)) (f k hk)
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.Measure.toFinite.eq_1 : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SFinite μ],
  μ.toFinite = μ.toFiniteAux[|Set.univ]