mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Adding a point to a collinear set produces a coplanar set.  -/
Collinear.coplanar_insert : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P}, Collinear k s → ∀ (p : P), Coplanar k (insert p s)
-- Mathlib.Topology.MetricSpace.Isometry
Fin.appendIsometry_apply : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (m n : ℕ) (fg : (Fin m → α) × (Fin n → α)) (a : Fin (m + n)),
  (Fin.appendIsometry m n) fg a = Fin.append fg.1 fg.2 a
-- Init.Data.Vector.Lemmas
Vector.any_toArray : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.toArray.any p = xs.any p
-- Mathlib.CategoryTheory.EssentiallySmall
/-- Help the typechecker by explicitly translating from `ShrinkHoms C` to `C`.  -/
CategoryTheory.ShrinkHoms.fromShrinkHoms : {C' : Type u_2} → CategoryTheory.ShrinkHoms.{u_2} C' → C'
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.acyclic_op_iff : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c), K.op.Acyclic ↔ K.Acyclic
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
_private.Mathlib.NumberTheory.EllipticDivisibilitySequence.0.preNormEDS'.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : Unit → motive 3) (h_5 : Unit → motive 4) (h_6 : (n : ℕ) → motive n.succ.succ.succ.succ.succ),
  (match 2 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()
    | 3 => h_4 ()
    | 4 => h_5 ()
    | n.succ.succ.succ.succ.succ => h_6 n) =
    h_3 ()
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.evalEquiv.congr_simp : ∀ (S : CategoryTheory.Functor Type uᵒᵖ (Type u))
  (hs : CategoryTheory.Presheaf.IsSheaf CategoryTheory.typesGrothendieckTopology S) (α : Type u),
  CategoryTheory.evalEquiv S hs α = CategoryTheory.evalEquiv S hs α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₃_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C}
  (h_1 : X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p₁₃ (CategoryTheory.CategoryStruct.comp h₁₃.p₂ h_1) =
    CategoryTheory.CategoryStruct.comp h.p₃ h_1
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.Measure.tilted.eq_1 : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ℝ),
  μ.tilted f = μ.withDensity fun x => ENNReal.ofReal (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ)
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.id_eq_id : ∀ (X : CategoryTheory.ReflQuiv), CategoryTheory.CategoryStruct.id X = 𝟭rq ↑X
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_of_contains_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α}, (m.erase k).contains a = true → m.contains a = true
-- Mathlib.Order.Bounds.Basic
bddBelow_iff_subset_Ici : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddBelow s ↔ ∃ a, s ⊆ Set.Ici a
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- The two step comparison map
  `image (f ≫ (g ≫ h)) ⟶ image (g ≫ h) ⟶ image h`
agrees with the one step comparison map
  `image (f ≫ (g ≫ h)) ≅ image ((f ≫ g) ≫ h) ⟶ image h`.
 -/
CategoryTheory.Limits.image.preComp_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) {W : C} (h : Z ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp g h)]
  [inst_2 :
    CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))]
  [inst_3 : CategoryTheory.Limits.HasImage h]
  [inst_4 :
    CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.preComp f (CategoryTheory.CategoryStruct.comp g h))
      (CategoryTheory.Limits.image.preComp g h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.eqToHom ⋯)
      (CategoryTheory.Limits.image.preComp (CategoryTheory.CategoryStruct.comp f g) h)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- **Alias** of `CategoryTheory.Limits.cokernelIsoOfEq`.

---

If two morphisms are known to be equal, then their cokernels are isomorphic.  -/
CategoryTheory.Limits.cokernel.congr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f g : X ⟶ Y} →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            [inst_3 : CategoryTheory.Limits.HasCokernel g] →
              f = g → (CategoryTheory.Limits.cokernel f ≅ CategoryTheory.Limits.cokernel g)
-- Mathlib.LinearAlgebra.FreeModule.Finite.Basic
Module.Free.ChooseBasisIndex.eq_1 : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M], Module.Free.ChooseBasisIndex R M = ↑⋯.choose
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.response : {β : Type} → Except IO.Error (Std.Http.Response β) → Std.Http.Server.Connection.Recv✝ β
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertMany_append : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l₁ l₂ : List (α × β)},
  Std.ExtDHashMap.Const.insertMany m (l₁ ++ l₂) =
    Std.ExtDHashMap.Const.insertMany (Std.ExtDHashMap.Const.insertMany m l₁) l₂
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The adjoint is unique: a map `A` is the adjoint of `B` iff it satisfies `⟪A x, y⟫ = ⟪x, B y⟫`
for all `x` and `y`.  -/
LinearMap.eq_adjoint_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E),
  A = LinearMap.adjoint B ↔ ∀ (x : E) (y : F), inner 𝕜 (A x) y = inner 𝕜 x (B y)
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ y * x` is quasi-measure-preserving.  -/
MeasureTheory.quasiMeasurePreserving_mul_swap : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [μ.IsMulLeftInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving (fun p => p.2 * p.1) (μ.prod ν) μ
-- Mathlib.Algebra.Algebra.Basic
/-- If `E` is an `F`-algebra, and there exists a surjective `F`-linear map from `F` to `E`,
then the algebra map from `F` to `E` is also surjective.  -/
surjective_algebraMap_of_linearMap : ∀ {F : Type u_1} {E : Type u_2} [inst : CommSemiring F] [inst_1 : Semiring E] [inst_2 : Algebra F E] (b : F →ₗ[F] E),
  Function.Surjective ⇑b → Function.Surjective ⇑(algebraMap F E)
-- Mathlib.Topology.EMetricSpace.Basic
/-- The triangle (polygon) inequality for sequences of points; `Finset.Ico` version.  -/
edist_le_Ico_sum_edist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (f : ℕ → α) {m n : ℕ},
  m ≤ n → edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
-- Mathlib.Order.Interval.Basic
NonemptyInterval.toDualProd_strictMono : ∀ {α : Type u_1} [inst : Preorder α], StrictMono NonemptyInterval.toDualProd
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.map_eq_iff_postcomp : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f₁ f₂ : X ⟶ Y),
  L.map f₁ = L.map f₂ ↔
    ∃ Z s, ∃ (_ : W s), CategoryTheory.CategoryStruct.comp f₁ s = CategoryTheory.CategoryStruct.comp f₂ s
-- Mathlib.Order.RelIso.Basic
/-- A relation homomorphism with respect to a given pair of relations `r` and `s`
is a function `f : α → β` such that `r a b → s (f a) (f b)`.  -/
RelHom : {α : Type u_5} → {β : Type u_6} → (α → α → Prop) → (β → β → Prop) → Type (max u_5 u_6)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff_coeff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (x : AddMonoidAlgebra R M), AddMonoidAlgebra.ofCoeff x.coeff = x
-- Lean.Parser.Term
Lean.Parser.Term.unsafe.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.HashMap.Raw
/-- Updates the values of the hash map by applying the given function to all mappings.  -/
Std.HashMap.Raw.map : {α : Type u} → {β : Type v} → {γ : Type w} → (α → β → γ) → Std.HashMap.Raw α β → Std.HashMap.Raw α γ
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.inv_toLeftFun_mul_mem : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G} (hS : Subgroup.IsComplement S ↑H) (g : G),
  (↑(hS.toLeftFun g))⁻¹ * g ∈ H
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.diag2.congr_simp : ∀ {F : Type u_1} [inst : Field F] (a a_1 : F) (e_a : a = a_1) (ha : a ≠ 0),
  Matrix.SpecialLinearGroup.diag2 a ha = Matrix.SpecialLinearGroup.diag2 a_1 ⋯
-- Lean.Meta.ExprLens
_private.Lean.Meta.ExprLens.0.Lean.Meta.lensAux : {M : Type → Type} →
  [Monad M] →
    [MonadLiftT Lean.MetaM M] →
      [MonadControlT Lean.MetaM M] → [Lean.MonadError M] → (Lean.Expr → M Lean.Expr) → List ℕ → Lean.Expr → M Lean.Expr
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.StateStack.mk : {α β σ : Type} →
  List (Lean.ScopedEnvExtension.State σ) →
    Lean.ScopedEnvExtension.ScopedEntries β →
      List (Lean.ScopedEnvExtension.Entry α) → Lean.ScopedEnvExtension.StateStack α β σ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getThenInsertIfNew?_fst : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (Std.DTreeMap.Raw.Const.getThenInsertIfNew? t k v).1 = Std.DTreeMap.Raw.Const.get? t k
-- Mathlib.Data.Rat.Init
/-- The denominator of a nonnegative rational.  -/
NNRat.den : ℚ≥0 → ℕ
-- Mathlib.Topology.ContinuousMap.Algebra
/-- The subgroup of continuous maps `α → β`.  -/
continuousSubgroup : (α : Type u_1) →
  (β : Type u_2) →
    [TopologicalSpace α] → [inst : TopologicalSpace β] → [inst_1 : Group β] → [IsTopologicalGroup β] → Subgroup (α → β)
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.mul_right_not_lt : ∀ {R : Type u} [inst : EuclideanDomain R] {a : R} (b : R), a ≠ 0 → ¬EuclideanDomain.r (a * b) b
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
/-- A (functorial) factorization of any morphisms in a Grothendieck abelian category
as a monomorphism followed by a morphism which has the right lifting property
with respect to all monomorphisms.  -/
CategoryTheory.IsGrothendieckAbelian.monoMapFactorizationDataRlp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] →
        {X Y : C} →
          (f : X ⟶ Y) →
            (CategoryTheory.MorphismProperty.monomorphisms C).MapFactorizationData
              (CategoryTheory.MorphismProperty.monomorphisms C).rlp f
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_pos_of_neg_of_neg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] [ExistsAddOfLE R] [MulPosStrictMono R]
  [AddRightStrictMono R] [AddRightReflectLT R] {a b : R}, a < 0 → b < 0 → 0 < a * b
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.map₂Left'.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (a : α) (as : List α) (b : β) (bs : List β)
  (h_1 : (bs : List β) → motive [] bs) (h_2 : (a : α) → (as : List α) → motive (a :: as) [])
  (h_3 : (a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs)),
  (match a :: as, b :: bs with
    | [], bs => h_1 bs
    | a :: as, [] => h_2 a as
    | a :: as, b :: bs => h_3 a as b bs) =
    h_3 a as b bs
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.lipschitzWith_restrict : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : PseudoEMetricSpace β] [inst_1 : Finite ↑𝔖],
  ∀ s ∈ 𝔖, LipschitzWith 1 (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖))
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Origin.fvar.sizeOf_spec : ∀ (fvarId : Lean.FVarId), sizeOf (Lean.Meta.Grind.Origin.fvar fvarId) = 1 + sizeOf fvarId
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
/-- The congruence relation induced by this ideal.  -/
TwoSidedIdeal.ringCon : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → TwoSidedIdeal R → RingCon R
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- An integer exponent `l` such that `(1 + ‖x‖) ^ (-l)` is integrable if `μ` has
temperate growth.  -/
MeasureTheory.Measure.integrablePower : {E : Type u_5} → [NormedAddCommGroup E] → [inst : MeasurableSpace E] → MeasureTheory.Measure E → ℕ
-- Mathlib.Data.Semiquot
/-- Convert a `Semiquot α` to a `Trunc α`.  -/
Semiquot.toTrunc : {α : Type u_1} → Semiquot α → Trunc α
-- Init.Data.Int.DivMod.Lemmas
Int.add_emod_left : ∀ (a b : ℤ), (a + b) % a = b % a
-- Lean.Server.Utils
/-- Version number of the document. Incremented whenever the document is edited.  -/
Lean.Server.DocumentMeta.version : Lean.Server.DocumentMeta → ℕ
-- Mathlib.Topology.UniformSpace.Defs
/-- Notation for uniform continuity with respect to non-standard `UniformSpace` instances.  -/
Uniformity.«termUniformContinuous[_,_]» : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.IsIndContained.refl : ∀ {V : Type u_1} (G : SimpleGraph V), G.IsIndContained G
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsFiniteKernel.swapLeft : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsFiniteKernel κ.swapLeft
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The Gaussian pdf is nonnegative.  -/
ProbabilityTheory.gaussianPDFReal_nonneg : ∀ (μ : ℝ) (v : NNReal) (x : ℝ), 0 ≤ ProbabilityTheory.gaussianPDFReal μ v x
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_braiding : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X Y : Rep.{u, u, v} k G},
  Rep.Hom.hom (β_ X Y).hom = ↑(Representation.TensorProduct.comm X.ρ Y.ρ)
-- Mathlib.Lean.Meta.CongrTheorems
/-- Process the congruence theorem by trying to pre-prove arguments using `prove`.

- `cthm` is the original `CongrTheorem`, modified only after visiting every argument.
- `type` is type of the congruence theorem, after all the parameters so far have been applied.
- `argKinds` is the list of `CongrArgKind`s, which this function recurses on.
- `argKinds'` is the accumulated array of `CongrArgKind`s, which is the original array but
  with some kinds replaced by `.subsingletonInst`.
- `params` is the *new* list of parameters, as fvars that need to be abstracted at the end.
- `args` is the list of arguments (fvars) to supply to `cthm.proof` before abstracting `params`.
- `letArgs` records `(fvar, expr)` assignments for each `fvar` that was solved for by `prove`.
 -/
_private.Mathlib.Lean.Meta.CongrTheorems.0.Lean.Meta.mkHCongrWithArity'.process : Lean.Meta.CongrTheorem →
  Lean.Expr →
    List Lean.Meta.CongrArgKind →
      Array Lean.Meta.CongrArgKind →
        Array Lean.Expr → Array Lean.Expr → Array (Lean.Expr × Lean.Expr) → Lean.MetaM Lean.Meta.CongrTheorem
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.zero_oreDiv : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddMonoid X] [inst_3 : DistribMulAction R X] (s : ↥S), 0 /ₒ s = 0
-- Lean.Elab.DefView
/-- Snapshot for incremental processing of this definition.

Invariant: If the bundle's `old?` is set, then elaboration of the header is guaranteed to result
in the same elaboration result and state, i.e. reuse is possible.
 -/
Lean.Elab.DefView.headerSnap? : Lean.Elab.DefView → Option (Lean.Language.SnapshotBundle (Option Lean.Elab.HeaderProcessedSnapshot))
-- Init.Data.SInt.Lemmas
Int8.sub_left_inj : ∀ {a b : Int8} (c : Int8), a - c = b - c ↔ a = b
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.left_of_comp : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ} {g : α → α},
  Function.Commute f g → Function.IsPeriodicPt (f ∘ g) n x → Function.IsPeriodicPt g n x → Function.IsPeriodicPt f n x
-- Mathlib.Data.Finset.Card
/-- **Alias** of the forward direction of `Finset.card_filter_eq_iff`. -/
Finset.filter_card_eq : ∀ {α : Type u_1} {s : Finset α} {p : α → Prop} [inst : DecidablePred p],
  (Finset.filter p s).card = s.card → ∀ x ∈ s, p x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.length_keys : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.keys.length = m.size
-- Mathlib.Algebra.Module.NatInt
Int.smul_one_eq_cast : ∀ {R : Type u_5} [inst : NonAssocRing R] (m : ℤ), m • 1 = ↑m
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.coe_iInf : ∀ {ι : Sort u_1} {α : Type u_2} [inst : BooleanAlgebra α] (f : ι → BooleanSubalgebra α), ↑(⨅ i, f i) = ⋂ i, ↑(f i)
-- Init.ShareCommon
ShareCommon.Object.ptrHash : ShareCommon.Object → UInt64
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.valuation_coe : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]), (↑x).valuation = ↑x.valuation
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Module.lift_comp_of : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Semiring R]
  [inst_5 : (i : ι) → AddCommMonoid (G i)] [inst_6 : (i : ι) → Module R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] {P : Type u_7}
  [inst_9 : AddCommMonoid P] [inst_10 : Module R P] (g : (i : ι) → G i →ₗ[R] P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) {i : ι},
  DirectLimit.Module.lift R ι G f g Hg ∘ₗ DirectLimit.Module.of R ι G f i = g i
-- Mathlib.Topology.Semicontinuity.Defs
Semicontinuous.semicontinuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop},
  Semicontinuous r → ∀ (x : α), SemicontinuousAt r x
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
RingOfIntegers.not_dvd_exponent_iff : ∀ {K : Type u_1} [inst : Field K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [Fact (Nat.Prime p)],
  ¬p ∣ RingOfIntegers.exponent θ ↔
    Codisjoint (Ideal.comap (algebraMap ℤ (NumberField.RingOfIntegers K)) (conductor ℤ θ)) (Ideal.span {↑p})
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearMap.smul_compMultilinearMap : ∀ {R : Type uR} {S : Type uS} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃] [inst_7 : Monoid S]
  [inst_8 : DistribMulAction S M₃] [inst_9 : SMulCommClass R S M₃] (g : M₂ →ₗ[R] M₃) (s : S)
  (f : MultilinearMap R M₁ M₂), (s • g).compMultilinearMap f = s • g.compMultilinearMap f
-- Mathlib.Order.RelClasses
Order.Preimage.instIrrefl : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Irrefl r] {f : β → α}, Std.Irrefl (f ⁻¹'o r)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_add_size_eq_size_union!_add_size_inter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₁.size + m₂.size = (m₁.union! m₂).size + (m₁.inter! m₂).size
-- Mathlib.Order.TypeTags
WithBot.recBotCoe_bot : ∀ {α : Type u_1} {C : WithBot α → Sort u_2} (d : C ⊥) (f : (a : α) → C ↑a), WithBot.recBotCoe d f ⊥ = d
-- Mathlib.Data.Quot
Quot.hrecOn.congr_simp : ∀ {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (q : Quot r) (f f_1 : (a : α) → motive (Quot.mk r a))
  (e_f : f = f_1) (c : ∀ (a b : α), r a b → f a ≍ f b), Quot.hrecOn q f c = Quot.hrecOn q f_1 ⋯
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_eq_one_iff : ∀ {x : ENNReal}, x.log = 0 ↔ x = 1
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.Regular.instIsRegularEpiFrobeniusMorphism : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Regular C] {A B : C} (f : A ⟶ B)
  (A' : CategoryTheory.Subobject A) (B' : CategoryTheory.Subobject B),
  CategoryTheory.IsRegularEpi (CategoryTheory.Regular.frobeniusMorphism f A' B')
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.direction_orthRadius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p : P),
  (s.orthRadius p).direction = (ℝ ∙ (p -ᵥ s.center))ᗮ
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedComm.eq_1 : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)],
  TensorProduct.gradedComm R 𝒜 ℬ =
    ((TensorProduct.directSum R R 𝒜 ℬ).trans
          (LinearEquiv.ofLinearMap (TensorProduct.gradedCommAux R 𝒜 ℬ) (TensorProduct.gradedCommAux R ℬ 𝒜) ⋯ ⋯)).trans
      (TensorProduct.directSum R R ℬ 𝒜).symm
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_eq_X_mul_U_sub_U : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.T R (n + 2) = Polynomial.X * Polynomial.Chebyshev.U R (n + 1) - Polynomial.Chebyshev.U R n
-- Mathlib.GroupTheory.Coxeter.Basic
/-- If two Coxeter systems on the same group `W` have the same Coxeter matrix `M : Matrix B B ℕ`
and the same simple reflection map `B → W`, then they are identical.  -/
CoxeterSystem.simple_determines_coxeterSystem : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B}, Function.Injective CoxeterSystem.simple
-- Lean.Elab.Do.Basic
/-- The mutable variables in declaration order. Kept in sync with `mutVarDefs`; insertions go
through `declareMutVar` / `declareMutVars` only.
 -/
Lean.Elab.Do.Context.mutVars : Lean.Elab.Do.Context → Array Lean.Elab.Do.MutVar
-- Mathlib.RepresentationTheory.Continuous.TopRep
_private.Mathlib.RepresentationTheory.Continuous.TopRep.0.TopRep.Hom.mk.sizeOf_spec : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] {A : TopRep k G}
  {B : TopRep k G} [inst_3 : SizeOf k] [inst_4 : SizeOf G] (hom' : ContIntertwiningMap A.ρ B.ρ),
  sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Order.RelIso.Set
RelHomClass.directedOn : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_3} [inst : FunLike F α β]
  [RelHomClass F r s] {f : F} {t : Set α}, DirectedOn r t → DirectedOn s (⇑f '' t)
-- Mathlib.Order.RelIso.Set
/-- If a proposition holds for all elements, then the `Subrel` is equivalent to the original
relation.  -/
RelIso.subrelUnivIso : {α : Type u_1} → {r : α → α → Prop} → {p : α → Prop} → (∀ (x : α), p x) → Subrel r p ≃r r