mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.coe_map_neg : ∀ {M : Type u} {N : Type v} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N) (u : AddUnits M),
  ↑(-(AddUnits.map f) u) = f ↑(-u)
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.inv_denom_smul_num : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] (A : Matrix m n ℚ),
  (↑A.den)⁻¹ • A.num.map Int.cast = A
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_mul : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] (s : Set α) (f g : α → M),
  (s.mulIndicator fun a => f a * g a) = fun a => s.mulIndicator f a * s.mulIndicator g a
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.disjoint_closedEBall_of_lt_infEDist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α} {r : ENNReal},
  r < Metric.infEDist x s → Disjoint (Metric.closedEBall x r) s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- The square
```
  Y --inr--> X ⊞ Y
  |            |
  0           fst
  |            |
  v            v
  0 ---0-----> X
```
is a pushout square.
 -/
CategoryTheory.IsPushout.inr_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.IsPushout CategoryTheory.Limits.biprod.inr 0 CategoryTheory.Limits.biprod.fst 0
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k k' fallback : α}, (k == k') = true → m.getD k fallback = m.getD k' fallback
-- Mathlib.LinearAlgebra.Dual.Lemmas
FiniteDimensional.mem_span_of_iInf_ker_le_ker : ∀ {ι : Type u_3} {𝕜 : Type u_4} {E : Type u_5} [inst : Field 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [FiniteDimensional 𝕜 E] {L : ι → E →ₗ[𝕜] 𝕜} {K : E →ₗ[𝕜] 𝕜},
  ⨅ i, (L i).ker ≤ K.ker → K ∈ Submodule.span 𝕜 (Set.range L)
-- Mathlib.Data.ENNReal.Inv
ENNReal.mulRightOrderIso_symm_apply : ∀ (a : ENNReal) (ha : IsUnit a) (x : ENNReal), (RelIso.symm (a.mulRightOrderIso ha)) x = x * ↑ha.unit⁻¹
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeEquiv_trans : ∀ {α : Sort u_1} {β : Sort u_4} {γ : Sort u_7} {p : α → Prop} {q : β → Prop} {r : γ → Prop} (e : α ≃ β) (f : β ≃ γ)
  (h : ∀ (a : α), p a ↔ q (e a)) (h' : ∀ (b : β), q b ↔ r (f b)),
  (e.subtypeEquiv h).trans (f.subtypeEquiv h') = (e.trans f).subtypeEquiv ⋯
-- Mathlib.Data.Multiset.Bind
Multiset.bind_map : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : β → Multiset γ) (f : α → β),
  (Multiset.map f m).bind n = m.bind fun a => n (f a)
-- Mathlib.Algebra.Order.Monovary
Antivary.mul_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : CommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedMonoid β] {f : ι → α} {g₁ g₂ : ι → β}, Antivary f g₁ → Antivary f g₂ → Antivary f (g₁ * g₂)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepSet_iff_condIndepSets_singleton : ∀ {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
  {s t : Set Ω},
  MeasurableSet s →
    MeasurableSet t →
      ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
        ProbabilityTheory.CondIndepSet m' hm' s t μ ↔ ProbabilityTheory.CondIndepSets m' hm' {s} {t} μ
-- Init.Data.UInt.Lemmas
UInt64.toNat_ofNatClamp_of_lt : ∀ {n : ℕ}, n < UInt64.size → (UInt64.ofNatClamp n).toNat = n
-- Mathlib.Topology.Instances.Rat
Rat.totallyBounded_Icc : ∀ (a b : ℚ), TotallyBounded (Set.Icc a b)
-- Mathlib.GroupTheory.Coxeter.Matrix
CoxeterMatrix.mk.sizeOf_spec : ∀ {B : Type u_1} [inst : SizeOf B] (M : Matrix B B ℕ) (isSymm : autoParam M.IsSymm CoxeterMatrix.isSymm._autoParam)
  (diagonal : autoParam (∀ (i : B), M i i = 1) CoxeterMatrix.diagonal._autoParam)
  (off_diagonal : autoParam (∀ (i i' : B), i ≠ i' → M i i' ≠ 1) CoxeterMatrix.off_diagonal._autoParam),
  sizeOf { M := M, isSymm := isSymm, diagonal := diagonal, off_diagonal := off_diagonal } = 1 + sizeOf isSymm
-- Mathlib.RingTheory.Invariant.Basic
IsFractionRing.stabilizerQuotientInertiaEquiv_mk : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [inst_3 : Group G] [inst_4 : Finite G] [inst_5 : MulSemiringAction G B] [inst_6 : SMulCommClass G A B] (P : Ideal A)
  (Q : Ideal B) [inst_7 : Q.IsPrime] [inst_8 : Q.LiesOver P] (K : Type u_4) (L : Type u_5) [inst_9 : Field K]
  [inst_10 : Field L] [inst_11 : Algebra (A ⧸ P) K] [inst_12 : Algebra (B ⧸ Q) L] [inst_13 : Algebra (A ⧸ P) L]
  [inst_14 : IsScalarTower (A ⧸ P) (B ⧸ Q) L] [inst_15 : Algebra K L] [inst_16 : IsScalarTower (A ⧸ P) K L]
  [inst_17 : Algebra.IsInvariant A B G] [inst_18 : IsFractionRing (A ⧸ P) K] [inst_19 : IsFractionRing (B ⧸ Q) L]
  (g : ↥(MulAction.stabilizer G Q)),
  (IsFractionRing.stabilizerQuotientInertiaEquiv G P Q K L) ↑g = (IsFractionRing.stabilizerHom G P Q K L) g
-- Mathlib.Analysis.Asymptotics.LinearGrowth
Frequently.linearGrowthInf_le : ∀ {u : ℕ → EReal} {a : EReal}, (∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ a * ↑n) → LinearGrowth.linearGrowthInf u ≤ a
-- Mathlib.Analysis.Convex.Function
convexOn_iff_div : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [inst_6 : SMul 𝕜 E]
  [inst_7 : SMul 𝕜 β] {s : Set E} {f : E → β},
  ConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s →
          ∀ ⦃y : E⦄,
            y ∈ s →
              ∀ ⦃a b : 𝕜⦄,
                0 ≤ a →
                  0 ≤ b →
                    0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y
-- Lean.Meta.Match.MatcherApp.Transform
/-- Fvars/exprs introduced in the telescope of a matcher alternative during `transform`.

* `args` are the values passed to `instantiateLambda` on the original alt. They usually
  coincide with `fields`, but may include non-fvar values (e.g. `Unit.unit` for thunked alts).
* `fields` are the constructor-field fvars (proper fvar subset of `args`).
* `overlaps` are overlap-parameter fvars (splitter path only, for non-`casesOn` splitters).
* `discrEqs` are discriminant-equation fvars from the matcher's own type (`numDiscrEqs`).
* `extraEqs` are equation fvars added by the `addEqualities` flag.

**Example.** `transform` with `addEqualities := true` on a `Nat.casesOn` application
`Nat.casesOn (motive := …) n alt₀ alt₁` opens alt telescopes:
```
Alt 0 (zero):  (heq : n = Nat.zero) → motive Nat.zero
  ⟹ { args := #[], fields := #[], extraEqs := #[heq] }

Alt 1 (succ):  (k : Nat) → (heq : n = Nat.succ k) → motive (Nat.succ k)
  ⟹ { args := #[k], fields := #[k], extraEqs := #[heq] }
```
 -/
Lean.Meta.MatcherApp.TransformAltFVars : Type
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.binomial_singleton : ∀ (n k : ℕ) (p : ↑unitInterval),
  (ProbabilityTheory.binomial n p) {k} = ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k))
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.coe_trans : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (e₁ : M ≃* N)
  (e₂ : N ≃* P), ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
-- Mathlib.Topology.UniformSpace.Closeds
mem_hausdorffEntourage : ∀ {α : Type u_1} (U : SetRel α α) (s t : Set α), (s, t) ∈ hausdorffEntourage U ↔ s ⊆ U.preimage t ∧ t ⊆ U.image s
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.lo? : Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval → Option Lean.Meta.Grind.Arith.Cutsat.SymbolicBound
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.skeleton_succ : ∀ (X : SSet) (n : ℕ), X.skeleton (n + 1) = X.skeleton n ⊔ ⨆ x, SSet.Subcomplex.ofSimplex ↑x
-- Mathlib.Topology.AlexandrovDiscrete
nhdsKer_singleton_subset_iff_mem_nhds : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {t : Set α} {a : α}, nhdsKer {a} ⊆ t ↔ t ∈ nhds a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- If `terminalComparison F` is an Iso, then `F` preserves terminal objects.  -/
CategoryTheory.CartesianMonoidalCategory.preservesLimit_empty_of_isIso_terminalComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D)
  [CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.terminalComparison F)],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.toLinearMap_inj : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] {f g : E₁ →ₚ[R] E₂}, f.toLinearMap = g.toLinearMap ↔ f = g
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainGoal.mk.inj : ∀ {rendered : String} {goals : Array String} {rendered_1 : String} {goals_1 : Array String},
  { rendered := rendered, goals := goals } = { rendered := rendered_1, goals := goals_1 } →
    rendered = rendered_1 ∧ goals = goals_1
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrable_finsetSum' : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] {μ : MeasureTheory.Measure X}
  {ε''' : Type u_9} [inst_2 : TopologicalSpace ε'''] [inst_3 : ESeminormedAddCommMonoid ε'''] [ContinuousAdd ε''']
  {ι : Type u_10} (s : Finset ι) {f : ι → X → ε'''},
  (∀ i ∈ s, MeasureTheory.LocallyIntegrable (f i) μ) → MeasureTheory.LocallyIntegrable (∑ i ∈ s, f i) μ
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- a morphism from the (pre)cylinder object to the target  -/
HomotopicalAlgebra.Precylinder.LeftHomotopy.h : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {P : HomotopicalAlgebra.Precylinder X} → {Y : C} → {f g : X ⟶ Y} → P.LeftHomotopy f g → (P.I ⟶ Y)
-- Mathlib.LinearAlgebra.Projectivization.Collinear
Projectivization.line_unique : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {x y : Projectivization K V},
  x ≠ y →
    ∀ (p q : Submodule K V),
      Module.finrank K ↥p = 2 →
        Module.finrank K ↥q = 2 →
          x ∈ Submodule.projectivization p →
            y ∈ Submodule.projectivization p →
              x ∈ Submodule.projectivization q → y ∈ Submodule.projectivization q → p = q
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.instIsIsoFunctorSheafOfModulesCounitSheafificationAdjunction : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat],
  CategoryTheory.IsIso (PresheafOfModules.sheafificationAdjunction α).counit
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.hasDerivWithinAt_arcsin_Ici : ∀ {x : ℝ}, x ≠ -1 → HasDerivWithinAt Real.arcsin (1 / √(1 - x ^ 2)) (Set.Ici x) x
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
writtenInExtChartAt_extChartAt_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x : M} {y : E},
  y ∈ (extChartAt I x).target →
    writtenInExtChartAt (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x) x) (↑(extChartAt I x).symm) y = y
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.ext : ∀ {α : Sort u_1} {β : Sort u_2} {f g : α ↪ β}, (∀ (x : α), f x = g x) → f = g
-- Batteries.Data.Fin.Coding
Fin.decodeOrdering_encodeOrdering : ∀ (x : Ordering), Fin.decodeOrdering (Fin.encodeOrdering x) = x
-- Aesop.Rule.Name
Aesop.BuilderName.forward.sizeOf_spec : sizeOf Aesop.BuilderName.forward = 1
-- Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal
/-- The orthogonal complement of a submodule `N` with respect to some bilinear map is the set of
elements `x` which are orthogonal to all elements of `N`; i.e., for all `y` in `N`, `B x y = 0`.

Note that for general (neither symmetric nor antisymmetric) bilinear maps this definition has a
chirality; in addition to this "left" orthogonal complement one could define a "right" orthogonal
complement for which, for all `y` in `N`, `B y x = 0`.  This variant definition is not currently
provided in mathlib.  -/
Submodule.orthogonalBilin : {R : Type u_1} →
  {R₁ : Type u_2} →
    {R₂ : Type u_3} →
      {M : Type u_4} →
        {M₁ : Type u_5} →
          {M₂ : Type u_6} →
            [inst : CommSemiring R] →
              [inst_1 : CommSemiring R₁] →
                [inst_2 : CommSemiring R₂] →
                  [inst_3 : AddCommMonoid M] →
                    [inst_4 : Module R M] →
                      [inst_5 : AddCommMonoid M₁] →
                        [inst_6 : Module R₁ M₁] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R₂ M₂] →
                              {I₁ : R₁ →+* R} →
                                {I₂ : R₂ →+* R} → (M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) → Submodule R₁ M₁ → Submodule R₂ M₂
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
/-- The isomorphism `(Γ₀.splitting K).nondegComplex ≅ K` for all `K : ChainComplex C ℕ`.  -/
AlgebraicTopology.DoldKan.Γ₀NondegComplexIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        (K : ChainComplex C ℕ) → (AlgebraicTopology.DoldKan.Γ₀.splitting K).nondegComplex ≅ K
-- Mathlib.Data.Set.Lattice
Set.biUnion_ge_eq_iUnion : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {s : α → Set β}, ⋃ n, ⋃ m, ⋃ (_ : m ≥ n), s m = ⋃ n, s n
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.interior_setOfPred_le_re`. -/
Complex.interior_setOf_le_re : ∀ (a : ℝ), interior {z | a ≤ z.re} = {z | a < z.re}
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Trie.brecOn_1.go : {α : Type} →
  {motive_1 : Lean.Meta.DiscrTree.Trie α → Sort u} →
    {motive_2 : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u} →
      {motive_3 : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u} →
        {motive_4 : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α → Sort u} →
          (t : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) →
            ((t : Lean.Meta.DiscrTree.Trie α) → t.below → motive_1 t) →
              ((t : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) →
                  Lean.Meta.DiscrTree.Trie.below_1 t → motive_2 t) →
                ((t : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) →
                    Lean.Meta.DiscrTree.Trie.below_2 t → motive_3 t) →
                  ((t : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) →
                      Lean.Meta.DiscrTree.Trie.below_3 t → motive_4 t) →
                    motive_2 t ×' Lean.Meta.DiscrTree.Trie.below_1 t
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- An open subset of a scheme is affine if the open subscheme is affine.  -/
AlgebraicGeometry.IsAffineOpen : {X : AlgebraicGeometry.Scheme} → X.Opens → Prop
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_piecewise_of_subset_left : ∀ {ι : Type u_1} {π : ι → Sort u_2} {s t : Finset ι} [inst : (i : ι) → Decidable (i ∈ s)]
  [inst_1 : (i : ι) → Decidable (i ∈ t)],
  s ⊆ t → ∀ (f₁ f₂ g : (a : ι) → π a), s.piecewise (t.piecewise f₁ f₂) g = s.piecewise f₁ g
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.toDual_apply_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {x y : E}, ((InnerProductSpace.toDual 𝕜 E) x) y = inner 𝕜 x y
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isIso_homologyπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι),
  c.prev j = i → K.d i j = 0 → ∀ [inst_2 : K.HasHomology j], CategoryTheory.IsIso (K.homologyπ j)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.Meq.mk_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD] {X : C}
  {P : CategoryTheory.Functor Cᵒᵖ D} (S : J.Cover X) (x : CategoryTheory.ToType (P.obj (Opposite.op X))) (I : S.Arrow),
  ↑(CategoryTheory.Meq.mk S x) I = (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) x
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {X : C} {ringObj : CategoryTheory.RingObj X} {X_1 : C}
  {ringObj_1 : CategoryTheory.RingObj X_1},
  { X := X, ringObj := ringObj } = { X := X_1, ringObj := ringObj_1 } → X = X_1 ∧ ringObj ≍ ringObj_1
-- Mathlib.Logic.Equiv.Defs
Equiv.permCongr_def : ∀ {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p : Equiv.Perm α'), e.permCongr p = (e.symm.trans p).trans e
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.copy_eq : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] (C : ConvexCone R M) (s : Set M) (hs : s = ↑C), C.copy s hs = C
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- Limit induction on ordinals: if one can prove a property by induction at successor ordinals and
at limit ordinals, then it holds for all ordinals.

Note that this is just a special (though sometimes convenient) case of the more general
well-founded recursion `WellFoundedLT.fix`.  -/
Ordinal.limitRecOn : {motive : Ordinal.{u_5} → Sort u_4} →
  (o : Ordinal.{u_5}) →
    motive 0 →
      ((o : Ordinal.{u_5}) → motive o → motive (o + 1)) →
        ((o : Ordinal.{u_5}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_5}) → o' < o → motive o') → motive o) → motive o
-- Aesop.Search.Expansion.Norm
Aesop.NormM.Context.mk.sizeOf_spec : ∀ (options : Aesop.Options') (ruleSet : Aesop.LocalRuleSet) (normSimpContext : Aesop.NormSimpContext),
  sizeOf { options := options, ruleSet := ruleSet, normSimpContext := normSimpContext } =
    1 + sizeOf options + sizeOf ruleSet + sizeOf normSimpContext
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [Countable ι] (hτ : MeasureTheory.IsStoppingTime f τ) (i : ι), MeasurableSet {ω | τ ω = ↑i}
-- Mathlib.Data.List.Permutation
_private.Mathlib.Data.List.Permutation.0.List.permutationsAux.rec.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (t : α) (ts is : List α) (h_1 : (is : List α) → motive [] is)
  (h_2 : (t : α) → (ts is : List α) → motive (t :: ts) is),
  (match t :: ts, is with
    | [], is => h_1 is
    | t :: ts, is => h_2 t ts is) =
    h_2 t ts is
-- Mathlib.Topology.EMetricSpace.Basic
/-- Expressing locally uniform convergence using `edist`.  -/
EMetric.tendstoLocallyUniformly_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] {ι : Type u_2} [inst_1 : TopologicalSpace β] {F : ι → β → α}
  {f : β → α} {p : Filter ι},
  TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.EqnInfo.mk.inj : ∀ {declName : Lean.Name} {levelParams : List Lean.Name} {type value : Lean.Expr} {declNames : Array Lean.Name}
  {declNameNonRec : Lean.Name} {argsPacker : Lean.Meta.ArgsPacker} {fixedParamPerms : Lean.Elab.FixedParamPerms}
  {declName_1 : Lean.Name} {levelParams_1 : List Lean.Name} {type_1 value_1 : Lean.Expr} {declNames_1 : Array Lean.Name}
  {declNameNonRec_1 : Lean.Name} {argsPacker_1 : Lean.Meta.ArgsPacker} {fixedParamPerms_1 : Lean.Elab.FixedParamPerms},
  { declName := declName, levelParams := levelParams, type := type, value := value, declNames := declNames,
        declNameNonRec := declNameNonRec, argsPacker := argsPacker, fixedParamPerms := fixedParamPerms } =
      { declName := declName_1, levelParams := levelParams_1, type := type_1, value := value_1,
        declNames := declNames_1, declNameNonRec := declNameNonRec_1, argsPacker := argsPacker_1,
        fixedParamPerms := fixedParamPerms_1 } →
    declName = declName_1 ∧
      levelParams = levelParams_1 ∧
        type = type_1 ∧
          value = value_1 ∧
            declNames = declNames_1 ∧
              declNameNonRec = declNameNonRec_1 ∧ argsPacker = argsPacker_1 ∧ fixedParamPerms = fixedParamPerms_1
-- Mathlib.Data.Finset.Defs
Finset.mk : {α : Type u_4} → (val : Multiset α) → val.Nodup → Finset α
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.mulEquivHaarChar_symm : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalGroup G] [inst_5 : LocallyCompactSpace G] {φ : G ≃ₜ* G},
  MeasureTheory.mulEquivHaarChar φ.symm = (MeasureTheory.mulEquivHaarChar φ)⁻¹
-- Mathlib.GroupTheory.Index
/-- The index of a subgroup as a natural number. Returns `0` if the index is infinite. 

[Wikidata Q1464168](https://www.wikidata.org/wiki/Q1464168) -/
Subgroup.index : {G : Type u_1} → [inst : Group G] → Subgroup G → ℕ
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- An inner product with a sum on the left.  -/
sum_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} (s : Finset ι) (f : ι → E) (x : E), inner 𝕜 (∑ i ∈ s, f i) x = ∑ i ∈ s, inner 𝕜 (f i) x
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex : {n : ℕ} → Affine.Simplex.PointsWithCircumcenterIndex n
-- Lean.Compiler.IR.Basic
Lean.IR.CtorInfo.type : Lean.IR.CtorInfo → Lean.IR.IRType
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_eq_of_le : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {t : Subsemiring R},
  s ⊆ ↑t → t ≤ Subsemiring.closure s → Subsemiring.closure s = t
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.ext : ∀ {A : Type u} {inst : Ring A} {relations : Module.Relations A} {M : Type v} {inst_1 : AddCommGroup M}
  {inst_2 : Module A M} {x y : relations.Solution M}, x.var = y.var → x = y
-- Mathlib.Algebra.BigOperators.Finprod
finprod_prod_comm : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] (s : Finset β) (f : α → β → M),
  (∀ b ∈ s, Function.HasFiniteMulSupport fun a => f a b) → ∏ᶠ (a : α), ∏ b ∈ s, f a b = ∏ b ∈ s, ∏ᶠ (a : α), f a b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
/-- For a polynomial `P` and coefficient function `c`, `sumNodes n c P` is a linear combination
of `P` evaluated at the `n`'th order Chebyshev nodes, with coefficients taken from `c`.  -/
Polynomial.Chebyshev.sumNodes : ℕ → (ℕ → ℝ) → Polynomial ℝ → ℝ
-- Mathlib.SetTheory.ZFC.Class
Class.classToCong.eq_1 : ∀ (x : Class.{u}), x.classToCong = {y | y ∈ x}
-- Init.Data.Range.Polymorphic.PRange
/-- The intersection operator.  -/
Std.Ric.HasRcoIntersection.intersection : {α : Type w} → [self : Std.Ric.HasRcoIntersection α] → Std.Ric α → Std.Rco α → Std.Rco α
-- Mathlib.GroupTheory.Index
Subgroup.isFiniteRelIndex_of_finiteIndex : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [h : H.FiniteIndex], H.IsFiniteRelIndex K