mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.match_3.eq_4 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l' : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l'))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  (match Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit with
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l' => h_3 l'
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) =
    h_4 ()
-- Init.Data.Array.Lemmas
Array.getElem_swap_of_ne : ∀ {α : Type u_1} {k : ℕ} {xs : Array α} {i j : ℕ} {hi : i < xs.size} {hj : j < xs.size}
  {h : k < (xs.swap i j hi hj).size}, k ≠ i → k ≠ j → (xs.swap i j hi hj)[k] = xs[k]
-- Mathlib.Order.SupIndep
iSupIndep.injective : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {t : ι → α},
  iSupIndep t → (∀ (i : ι), t i ≠ ⊥) → Function.Injective t
-- Mathlib.Data.EReal.Basic
instSupSetEReal : SupSet EReal
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.symm_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.symm.unit = e.counitInv
-- Mathlib.Data.Fin.Basic
Fin.val_pos_iff : ∀ {n : ℕ} [inst : NeZero n] {a : Fin n}, 0 < ↑a ↔ 0 < a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.contains_insertMany_emptyWithCapacity_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α},
  (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).contains k =
    (List.map Prod.fst l).contains k
-- Mathlib.MeasureTheory.VectorMeasure.Prod
MeasureTheory.VectorMeasure.prod_eq_zero_of_not_hasProd : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {μ : MeasureTheory.VectorMeasure X E} {ν : MeasureTheory.VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G},
  ¬μ.HasProd ν B → μ.prod ν B = 0
-- Mathlib.Data.Prod.Basic
Prod.mk_inj : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
-- Mathlib.Data.Set.Basic
Set.subset_union_right : ∀ {α : Type u} {s t : Set α}, t ⊆ s ∪ t
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.re_ofNat : ∀ {R : Type u_1} {a b : R} [inst : AddCommMonoidWithOne R] (n : ℕ) [inst_1 : n.AtLeastTwo],
  (OfNat.ofNat n).re = OfNat.ofNat n
-- Lean.Data.Json.Basic
/-- Attempts to convert a float to a JsonNumber, if the number isn't finite returns
the appropriate string from "NaN", "Infinity", "-Infinity".  -/
Lean.JsonNumber.fromFloat? : Float → String ⊕ Lean.JsonNumber
-- Mathlib.NumberTheory.Bernoulli
/-- Alternate form of **Faulhaber's theorem**, relating the sum of p-th powers to the Bernoulli
numbers:
$$\sum_{k=1}^{n} k^p = \sum_{i=0}^p (-1)^iB_i\binom{p+1}{i}\frac{n^{p+1-i}}{p+1}.$$
Deduced from `sum_range_pow`.  -/
sum_Ico_pow : ∀ (n p : ℕ),
  ∑ k ∈ Finset.Ico 1 (n + 1), ↑k ^ p =
    ∑ i ∈ Finset.range (p + 1), bernoulli' i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.colimitAuxiliaryCocone_pt : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))),
  (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂).pt = R.obj c₂.pt
-- Mathlib.CategoryTheory.Thin
/-- If `C` is a thin category, then `D ⥤ C` is a thin category.  -/
CategoryTheory.functor_thin : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [Quiver.IsThin C], Quiver.IsThin (CategoryTheory.Functor D C)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache : Std.Sat.AIG Std.Tactic.BVDecide.BVBit → Type
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.lift_lt_ofENat : ∀ {x : Cardinal.{v}} {m : ℕ∞}, Cardinal.lift.{u, v} x < ↑m ↔ x < ↑m
-- Mathlib.Algebra.Homology.TotalComplexShift
/-- The compatibility isomorphisms of the total complex with the shifts
in both variables "commute" only up to a sign `(x * y).negOnePow`.  -/
HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ)
  [inst_2 : K.HasTotal (ComplexShape.up ℤ)],
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).totalShift₁Iso x).hom
      ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map (K.totalShift₂Iso y).hom) =
    (x * y).negOnePow •
      CategoryTheory.CategoryStruct.comp
        (HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₁₂CommIso C x y).hom.app K)
          (ComplexShape.up ℤ))
        (CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map (K.totalShift₁Iso x).hom)
            ((CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (ComplexShape.up ℤ)))))
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.replaceFun_toFun : ∀ {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)}
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)) (f : ℝ → ℝ), (ms.replaceFun f).toFun = f
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.instCreatesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfCreatesColimitOfIsSplitPair : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {F : CategoryTheory.Functor C D} →
            (adj : F ⊣ G) →
              [CategoryTheory.Monad.CreatesColimitOfIsSplitPair G] →
                (A : adj.toMonad.Algebra) →
                  CategoryTheory.CreatesColimit
                    (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_erase!_eq_iff_not_compare_minKey!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).isEmpty = false →
        ((Std.DTreeMap.Internal.Impl.erase! k t).minKey! = t.minKey! ↔ ¬compare k t.minKey! = Ordering.eq)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∈ t₂ → (t₁ \ t₂).getKeyD k fallback = fallback
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.length_toList : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.HasSize α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_6 : Std.Rxo.IsAlwaysFinite α] [Std.Rxo.LawfulHasSize α], r.toList.length = r.size
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.IsLeftAdjoint.mk' : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {left : a ⟶ b},
  Nonempty (CategoryTheory.Bicategory.RightAdjoint left) → CategoryTheory.Bicategory.IsLeftAdjoint left
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.foldl_filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precomposeEquivalence_functor : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G),
  (CategoryTheory.Limits.Cocone.precomposeEquivalence α).functor = CategoryTheory.Limits.Cocone.precompose α.inv
-- Mathlib.Algebra.Group.TypeTags.Hom
AddMonoidHom.toMultiplicative_symm_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : AddZeroClass β]
  (f : Multiplicative α →* Multiplicative β) (a : α),
  (AddMonoidHom.toMultiplicative.symm f) a = Multiplicative.toAdd (f (Multiplicative.ofAdd a))
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_div_const : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] (a : α), UniformContinuous fun b => b / a
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace β] [inst_3 : Preorder β] [inst_4 : TopologicalSpace γ] [inst_5 : Preorder γ]
  (g : EsakiaHom β γ) (f : EsakiaHom α β) (a : α), (g.comp f) a = g (f a)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.degreeOf : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Var → ℕ
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.insert : ∀ {α : Type u} (a : α) {s : Set α}, s.Finite → (insert a s).Finite
-- Mathlib.Algebra.Regular.Opposite
/-- **Alias** of the reverse direction of `isAddRightRegular_unop`. -/
IsAddRightRegular.unop : ∀ {R : Type u_1} [inst : Add R] {a : Rᵃᵒᵖ}, IsAddLeftRegular a → IsAddRightRegular (AddOpposite.unop a)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_one : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : One β], ⇑1 = 1
-- Qq.Match
Qq.Impl.PatternVar.mk.injEq : ∀ (name : Lean.Name) (arity : ℕ) (mvar : Lean.Expr) (stx : Lean.Term) (name_1 : Lean.Name) (arity_1 : ℕ)
  (mvar_1 : Lean.Expr) (stx_1 : Lean.Term),
  ({ name := name, arity := arity, mvar := mvar, stx := stx } =
      { name := name_1, arity := arity_1, mvar := mvar_1, stx := stx_1 }) =
    (name = name_1 ∧ arity = arity_1 ∧ mvar = mvar_1 ∧ stx = stx_1)
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.leval_eq_smeval.linearMap : ∀ {R : Type u_3} [inst : Semiring R] (r : R), Polynomial.leval r = Polynomial.smeval.linearMap R r
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.contains a = m_1.contains a_1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.beq'_eq : ∀ (m₁ m₂ : Lean.Grind.CommRing.Mon), (m₁.beq' m₂ = true) = (m₁ = m₂)
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ_assoc : ∀ (X : TopCat) {Z : SSet} (h : TopCat.toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X TopCat.I) ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.ι₁
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (TopCat.toSSet.obj X) SSet.stdSimplex.toSSetObjI)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I) h)) =
    CategoryTheory.CategoryStruct.comp (TopCat.toSSet.map TopCat.ι₁) h
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
HomogeneousSubmodule.isHomogeneous : ∀ {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A]
  [inst_1 : AddCommMonoid M] [inst_2 : Module A M] {𝒜 : ιA → σA} {ℳ : ιM → σM} [inst_3 : DecidableEq ιA]
  [inst_4 : AddMonoid ιA] [inst_5 : SetLike σA A] [inst_6 : AddSubmonoidClass σA A] [inst_7 : GradedRing 𝒜]
  [inst_8 : DecidableEq ιM] [inst_9 : SetLike σM M] [inst_10 : AddSubmonoidClass σM M]
  [inst_11 : DirectSum.Decomposition ℳ] [inst_12 : VAdd ιA ιM] [inst_13 : SetLike.GradedSMul 𝒜 ℳ]
  (p : HomogeneousSubmodule 𝒜 ℳ), p.IsHomogeneous ℳ
-- Init.Meta.Defs
Lean.TSyntax.instCoeNameLitTerm : Coe Lean.NameLit Lean.Term
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃_map_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X₁ Y₁ : C}
  (φ : X₁ ⟶ Y₁) (X₂ X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃ C).map φ).app X₂).app X₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ X₁ X₃).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂ (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ X₃))
        (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₁ X₃).inv)
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `upperSemiContinuous_neg_iff`. -/
LowerSemicontinuous.neg : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β], LowerSemicontinuous f → UpperSemicontinuous (-f)
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_Ioc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (a b : α i),
  Pi.single i '' Set.Ioc a b = Set.Ioc (Pi.single i a) (Pi.single i b)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_toNonUnitalSubring : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing A] [inst_2 : Module R A]
  (S : NonUnitalSubalgebra R A), ↑S.toNonUnitalSubring = ↑S
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.containsThenInsert : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → Bool × Std.TreeSet.Raw α cmp
-- Mathlib.LinearAlgebra.Complex.Module
Complex.coe_smul : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℂ E] (x : ℝ) (y : E), ↑x • y = x • y
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.fvar.inj : ∀ {a : Lean.FVarId} {a_1 : ℕ} {a_2 : Lean.FVarId} {a_3 : ℕ},
  Lean.Meta.LazyDiscrTree.Key.fvar a a_1 = Lean.Meta.LazyDiscrTree.Key.fvar a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Data.PNat.Basic
/-- The order isomorphism between ℕ and ℕ+ given by `succ`.  -/
OrderIso.pnatIsoNat : ℕ+ ≃o ℕ
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Transport evidence that a cocone is a colimit cocone across an isomorphism of cocones.  -/
CategoryTheory.Limits.IsColimit.ofIsoColimit : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {r t : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit r → (r ≅ t) → CategoryTheory.Limits.IsColimit t
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- A field `𝕜` satisfying `RCLike` is itself a `𝕜`-inner product space.  -/
RCLike.innerProductSpace : {𝕜 : Type u_1} → [inst : RCLike 𝕜] → InnerProductSpace 𝕜 𝕜
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.sigmaCurry_apply : ∀ {ι : Type v} [inst : DecidableEq ι] {α : ι → Type u} {δ : (i : ι) → α i → Type w}
  [inst_1 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] (f : DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd)
  (i : ι) (j : α i), ((DirectSum.sigmaCurry f) i) j = f ⟨i, j⟩
-- Init.Data.Option.Lemmas
Option.eq_none_iff_forall_some_ne : ∀ {α : Type u_1} {o : Option α}, o = none ↔ ∀ (a : α), some a ≠ o
-- Init.Data.Fin.OverflowAware
_private.Init.Data.Fin.OverflowAware.0.Fin.addNat?.eq_1 : ∀ {n : ℕ} (i : Fin n) (m : ℕ), i.addNat? m = if h : ↑i + m < n then some ⟨↑i + m, h⟩ else none
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- There exists `π : R` with `v`-adic valuation `WithZero.exp (-1)`.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
  ∃ π, v.intValuation π = WithZero.exp (-1)
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDate.instHSubDuration : HSub Std.Time.PlainDate Std.Time.PlainDate Std.Time.Duration
-- Std.Time.Date.Unit.Month
Std.Time.Month.instDecidableLtOffset : {x y : Std.Time.Month.Offset} → Decidable (x < y)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.epi_τ₂_of_exact_of_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Balanced C] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  S₂.Exact →
    ∀ [CategoryTheory.Epi S₁.g] [CategoryTheory.Epi S₂.g] [CategoryTheory.Epi φ.τ₁] [CategoryTheory.Epi φ.τ₃],
      CategoryTheory.Epi φ.τ₂
-- Mathlib.RingTheory.WittVector.Defs
WittVector.hasIntScalar : {p : ℕ} → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [CommRing R] → SMul ℤ (WittVector p R)
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.mul_leftInvEquiv_symm : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S),
  ↑x * ↑((S.leftInvEquiv hS).symm x) = 1
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- A finite-dimensional space has zero `finrank` iff it is a subsingleton.
This is the `finrank` version of `rank_zero_iff`.  -/
Module.finrank_zero_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] [IsDomain R] [Module.IsTorsionFree R M], Module.finrank R M = 0 ↔ Subsingleton M
-- Mathlib.CategoryTheory.Category.Preorder
OrderHom.equivalenceFunctor_inverse_obj : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (F : CategoryTheory.Functor X Y),
  OrderHom.equivalenceFunctor.inverse.obj F = F.toOrderHom
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.HeadCheck.shape.sizeOf_spec : ∀ (k : List Lean.SyntaxNodeKind) (arity : Option ℕ),
  sizeOf (Lean.Elab.Term.Quotation.HeadCheck.shape k arity) = 1 + sizeOf k + sizeOf arity
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.tensorHom_tmul : ∀ {R : Type u} [inst : CommRing R] {K L M N : ModuleCat R} (f : K ⟶ L) (g : M ⟶ N) (k : ↑K) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) (k ⊗ₜ[R] m) =
    (CategoryTheory.ConcreteCategory.hom f) k ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom g) m
-- Mathlib.Data.ENNReal.Holder
/-- A class stating that `p q r : ℝ≥0∞` satisfy `p⁻¹ + q⁻¹ = r⁻¹`.
This is exactly the condition for which **Hölder's inequality** is valid
(see `MeasureTheory.MemLp.smul`).

When `r := 1`, one generally says that `p q` are **Hölder conjugate**.

This class exists so that we can define a heterogeneous scalar multiplication
on `MeasureTheory.Lp`, and this is why `r` must be marked as a
`semiOutParam`. We don't mark it as an `outParam` because this would
prevent Lean from using `HolderTriple p q r` and `HolderTriple p q r'`
within a single proof, as may be occasionally convenient.  -/
ENNReal.HolderTriple : ENNReal → ENNReal → semiOutParam ENNReal → Prop
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsNClique.erase_of_sup_edge_of_mem : ∀ {α : Type u_1} {G : SimpleGraph α} [inst : DecidableEq α] {v w : α} {s : Finset α} {n : ℕ},
  (G ⊔ SimpleGraph.edge v w).IsNClique n s → v ∈ s → G.IsNClique (n - 1) (s.erase v)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instNatCast : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                {𝒜 : ι → σ} → [GradedRing 𝒜] → {x : Submonoid A} → NatCast (HomogeneousLocalization 𝒜 x)
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PrepathObject.RightHomotopy.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} {P : HomotopicalAlgebra.PrepathObject Y} {X : C}
  {f g : X ⟶ Y} [inst_1 : SizeOf C] (h : X ⟶ P.P)
  (h₀ :
    autoParam (CategoryTheory.CategoryStruct.comp h P.p₀ = f)
      HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀._autoParam)
  (h₁ :
    autoParam (CategoryTheory.CategoryStruct.comp h P.p₁ = g)
      HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁._autoParam),
  sizeOf { h := h, h₀ := h₀, h₁ := h₁ } = 1 + sizeOf h + sizeOf h₀ + sizeOf h₁
-- Mathlib.Topology.Algebra.Group.Basic
/-- A subgroup `S` of a topological group `G` acts on `G` properly discontinuously on the left, if
it is discrete in the sense that `S ∩ K` is finite for all compact `K`. (See also
`DiscreteTopology`.)  -/
Subgroup.properlyDiscontinuousSMul_of_tendsto_cofinite : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (S : Subgroup G),
  Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G) → ProperlyDiscontinuousSMul (↥S) G
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
instPolynormableSpaceForall : ∀ {𝕜 : Type u_2} {ι : Type u_9} [inst : NormedField 𝕜] {E : ι → Type u_11} [inst_1 : (i : ι) → AddCommGroup (E i)]
  [inst_2 : (i : ι) → Module 𝕜 (E i)] [inst_3 : (i : ι) → TopologicalSpace (E i)]
  [∀ (i : ι), PolynormableSpace 𝕜 (E i)], PolynormableSpace 𝕜 ((i : ι) → E i)
-- Aesop.Percent
Aesop.Percent.instToString : ToString Aesop.Percent
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.isSome_get?_eq_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α}, (Std.ExtDTreeMap.Const.get? t a).isSome = t.contains a
-- Init.Data.List.Lemmas
List.foldr_eq_apply_foldl : ∀ {α : Type u_1} {init x : α} {xs : List α} {f : α → α → α} [Std.Associative f] [Std.LawfulLeftIdentity f init],
  List.foldr f x xs = f (List.foldl f init xs) x
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.integralAgainstBilinCLM_eq_integral : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_6} {F₂ : Type u_7} {F₃ : Type u_8} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : Algebra ℝ 𝕜] [inst_12 : IsScalarTower ℝ 𝕜 F₁]
  [inst_13 : NormedSpace ℝ F₃] [inst_14 : IsScalarTower ℝ 𝕜 F₃] {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} {μ : MeasureTheory.Measure E}
  {φ : E → F₂},
  MeasureTheory.LocallyIntegrableOn φ (↑Ω) μ →
    ∀ {f : TestFunction Ω F₁ n}, (TestFunction.integralAgainstBilinCLM B μ φ) f = ∫ (x : E), (B (f x)) (φ x) ∂μ