mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.trivial.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Mon.trivial C =
    { X := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, mon := CategoryTheory.MonObj.instTensorUnit }
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivWithinAt.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_14} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_15}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {s : Set (M × M')} {p : M × M'} {f : M → N} {g : M' → N'}
  {df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)},
  HasMFDerivAt[Prod.fst '' s] f p.1 df →
    ∀ {dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)},
      HasMFDerivAt[Prod.snd '' s] g p.2 dg → HasMFDerivAt[s] (Prod.map f g) p (df.prodMap dg)
-- Std.Data.ExtDHashMap.Lemmas
Quotient.lift.congr_simp : ∀ {α : Sort u} {β : Sort v} {s : Setoid α} (f f_1 : α → β) (e_f : f = f_1) (a : ∀ (a b : α), a ≈ b → f a = f b)
  (a_1 a_2 : Quotient s), a_1 = a_2 → Quotient.lift f a a_1 = Quotient.lift f_1 ⋯ a_2
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.op_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) {X Y : C}
  {f : X ⟶ Y} (hf : W₁.MapFactorizationData W₂ f),
  (CategoryTheory.MorphismProperty.MapFactorizationData.op W₁ W₂ hf).p = hf.i.op
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.of_nonneg_disjoint_union_eq_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : MeasureTheory.SignedMeasure α} {A B : Set α},
  Disjoint A B → MeasurableSet A → MeasurableSet B → 0 ≤ s A → 0 ≤ s B → s (A ∪ B) = 0 → s A = 0
-- Mathlib.Algebra.Algebra.Basic
/-- Explicit characterization of the submonoid map in the case of an algebra.
`S` is made explicit to help with type inference  -/
Algebra.algebraMapSubmonoid : {R : Type u_1} →
  [inst : CommSemiring R] → (S : Type u_4) → [inst_1 : Semiring S] → [Algebra R S] → Submonoid R → Submonoid S
-- Mathlib.Algebra.Field.Basic
one_div_add_one_div : ∀ {K : Type u_1} [inst : Semifield K] {a b : K}, a ≠ 0 → b ≠ 0 → 1 / a + 1 / b = (a + b) / (a * b)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
differentiableWithinAt_inverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_5} [inst_1 : NormedRing R] [HasSummableGeomSeries R]
  [inst_3 : NormedAlgebra 𝕜 R] {x : R}, IsUnit x → ∀ (s : Set R), DifferentiableWithinAt 𝕜 Ring.inverse s x
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.instInhabitedLoogleResult.default : LeanSearchClient.LoogleResult
-- Mathlib.Data.Ordmap.Ordset
Ordnode.eraseMin.valid : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α}, t.Valid → t.eraseMin.Valid
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- `ℓ²(ι, E)` is the space of square-summable functions `ι → E`. When `E := 𝕜`, with `RCLike 𝕜`,
this is a Hilbert space.  -/
lp.«termℓ²(_,_)» : Lean.ParserDescr
-- Mathlib.CategoryTheory.GradedObject
/-- The natural isomorphism comparing between
pulling back along two propositionally equal functions.
 -/
CategoryTheory.GradedObject.comapEq : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {β γ : Type w} →
      {f g : β → γ} → f = g → (CategoryTheory.GradedObject.comap C f ≅ CategoryTheory.GradedObject.comap C g)
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.toBialgHom_id : ∀ {R : Type u} [inst : CommRing R] {M : BialgCat R},
  BialgCat.Hom.toBialgHom (CategoryTheory.CategoryStruct.id M) = BialgHom.id R M.carrier
-- Mathlib.Data.Set.Image
Set.rangeSplitting_injective : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.Injective (Set.rangeSplitting f)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.smul_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β] {R : Type u_2}
  [inst_3 : Zero R] [inst_4 : SMulWithZero R β] [inst_5 : ContinuousConstSMul R β] (r : R)
  (f : ZeroAtInftyContinuousMap α β) (x : α), (r • f) x = r • f x
-- Mathlib.Data.Nat.Bits
Nat.div2_zero : Nat.div2 0 = 0
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- If `L` has well-defined support, then so does its map along an embedding.  -/
SummationFilter.instHasSupportMap : ∀ {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) [L.HasSupport] (f : β ↪ γ), (L.map f).HasSupport
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_sub_cbm : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B C : E →L[ℝ] F →L[ℝ] G},
  μ.Integrable f → ∫ᵛ (x : X), f x ∂[B - C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]
-- Init.Data.UInt.Lemmas
UInt8.ne_iff_toBitVec_ne : ∀ {a b : UInt8}, a ≠ b ↔ a.toBitVec ≠ b.toBitVec
-- Mathlib.Topology.Algebra.Field
affineHomeomorph.congr_simp : ∀ {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : IsTopologicalRing 𝕜] (a a_1 : 𝕜)
  (e_a : a = a_1) (b b_1 : 𝕜), b = b_1 → ∀ (h : a ≠ 0), affineHomeomorph a b h = affineHomeomorph a_1 b_1 ⋯
-- Mathlib.Combinatorics.Matroid.Basic
/-- `M` has a predicate `Indep` defining its independent sets.  -/
Matroid.Indep : {α : Type u_1} → Matroid α → Set α → Prop
-- Mathlib.Order.WithBot
WithBot.unbotA.congr_simp : ∀ {α : Type u_1} [inst : Nonempty α] (a a_1 : WithBot α), a = a_1 → a.unbotA = a_1.unbotA
-- Init.Data.UInt.Bitwise
UInt16.toBitVec_or : ∀ (a b : UInt16), (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- Constructor for morphisms for `E^{n₁}(f₁, f₂, f₃)`.  -/
CategoryTheory.Abelian.SpectralObject.descE : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (f₁₂ : i ⟶ k) →
                      (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) →
                        (n₀ n₁ n₂ : ℤ) →
                          {A : C} →
                            (x : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁₂) ⟶ A) →
                              CategoryTheory.CategoryStruct.comp
                                    ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) x =
                                  0 →
                                (hn₁ : n₀ + 1 = n₁) →
                                  CategoryTheory.CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) x = 0 →
                                    (hn₂ :
                                        autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.descE._auto_1) →
                                      X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ A
-- Lean.Data.NameTrie
Lean.instInhabitedNameTrie : {β : Type u_1} → Inhabited (Lean.NameTrie β)
-- Mathlib.Data.Finset.Max
Finset.max_of_nonempty : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α}, s.Nonempty → ∃ a, s.max = ↑a
-- Mathlib.Analysis.Normed.Group.Continuity
Continuous.norm : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E},
  Continuous f → Continuous fun x => ‖f x‖
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.coe_comp : ∀ {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X}
  (f' : G' ↪g G'') (f : G ↪g G'), ⇑(f'.comp f) = ⇑f' ∘ ⇑f
-- Mathlib.Data.Set.Sups
Set.image_sup_prod : ∀ {α : Type u_2} [inst : SemilatticeSup α] (s t : Set α), Set.image2 (fun x1 x2 => x1 ⊔ x2) s t = s ⊻ t
-- Mathlib.Data.Set.Basic
Set.subset_def : ∀ {α : Type u} {s t : Set α}, (s ⊆ t) = ∀ x ∈ s, x ∈ t
-- Mathlib.Logic.Equiv.Defs
Equiv.conj_refl : ∀ {α : Sort u}, (Equiv.refl α).conj = Equiv.refl (α → α)
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor.mk.injEq : ∀ (toPreprocessorBase : Mathlib.Tactic.Linarith.PreprocessorBase)
  (transform : Lean.MVarId → List Lean.Expr → Lean.MetaM (List Mathlib.Tactic.Linarith.Branch))
  (toPreprocessorBase_1 : Mathlib.Tactic.Linarith.PreprocessorBase)
  (transform_1 : Lean.MVarId → List Lean.Expr → Lean.MetaM (List Mathlib.Tactic.Linarith.Branch)),
  ({ toPreprocessorBase := toPreprocessorBase, transform := transform } =
      { toPreprocessorBase := toPreprocessorBase_1, transform := transform_1 }) =
    (toPreprocessorBase = toPreprocessorBase_1 ∧ transform = transform_1)
-- Aesop.RuleTac.Basic
Aesop.instInhabitedRuleTac : Inhabited Aesop.RuleTac
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.ofSubsingleton_apply : ∀ {R : Type u_1} (M : Type u_5) (M₂ : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] [inst_5 : Subsingleton M]
  [inst_6 : Subsingleton M₂] (x : M), (LinearEquiv.ofSubsingleton M M₂) x = 0
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkspaceEdit.mk.injEq : ∀ (changes? : Option (Std.TreeMap Lean.Lsp.DocumentUri Lean.Lsp.TextEditBatch compare))
  (documentChanges? : Option (Array Lean.Lsp.DocumentChange))
  (changeAnnotations? : Option (Std.TreeMap String Lean.Lsp.ChangeAnnotation compare))
  (changes?_1 : Option (Std.TreeMap Lean.Lsp.DocumentUri Lean.Lsp.TextEditBatch compare))
  (documentChanges?_1 : Option (Array Lean.Lsp.DocumentChange))
  (changeAnnotations?_1 : Option (Std.TreeMap String Lean.Lsp.ChangeAnnotation compare)),
  ({ changes? := changes?, documentChanges? := documentChanges?, changeAnnotations? := changeAnnotations? } =
      { changes? := changes?_1, documentChanges? := documentChanges?_1, changeAnnotations? := changeAnnotations?_1 }) =
    (changes? = changes?_1 ∧ documentChanges? = documentChanges?_1 ∧ changeAnnotations? = changeAnnotations?_1)
-- Mathlib.AlgebraicTopology.DoldKan.Equivalence
CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  (X : CategoryTheory.SimplicialObject A) (i : ℕ),
  (CategoryTheory.Abelian.DoldKan.comparisonN.inv.app X).f i =
    CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex A ℕ)).inverse.map
            ((AlgebraicTopology.DoldKan.N₁_iso_normalizedMooreComplex_comp_toKaroubi A).hom.app X)).f
        i)
      (((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex A ℕ)).unitIso.inv.app
            (CategoryTheory.Abelian.DoldKan.N.obj X)).f
        i)
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₃_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) (X X_1 X_2 : C),
  (((CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₃ F).app X).app X_1).app X_2 =
    (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj X_1) (F.obj X_2)).hom
-- Init.Data.Bool
Bool.toNat_le : ∀ (c : Bool), c.toNat ≤ 1
-- Mathlib.Condensed.Discrete.Colimit
Condensed.lanPresheafIso_hom : ∀ {S : Profinite} {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))}
  (hF : CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)),
  (Condensed.lanPresheafIso hF).hom =
    CategoryTheory.Limits.colimit.desc
      ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op (Opposite.op S)).comp
        (FintypeCat.toProfinite.op.comp F))
      (Profinite.Extend.cocone F S)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
notMem_of_csSup_lt : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {x : α} {s : Set α}, sSup s < x → BddAbove s → x ∉ s
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The Fourier coefficients of a function on `UnitAddTorus d` can be computed as integrals
over `∏ i, (aᵢ, aᵢ + 1]`, for any `a : d → ℝ`.  -/
UnitAddTorus.mFourierCoeff_eq_integral : ∀ {d : Type u_1} [inst : Fintype d] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℂ E]
  (f : UnitAddTorus d → E) (n : d → ℤ) (a : d → ℝ),
  UnitAddTorus.mFourierCoeff f n =
    ∫ (x : d → ℝ) in {x | ∀ (i : d), x i ∈ Set.Ioc (a i) (a i + 1)},
      ((UnitAddTorus.mFourier (-n)) fun i => ↑(x i)) • f fun i => ↑(x i)
-- Lean.Meta.Sym.Pattern
/-- Creates a `Pattern` from an equational theorem, using the left-hand side of the equation.
It also returns the right-hand side of the equation

Like `mkPatternFromDecl`, this strips all leading universal quantifiers, recording variable
types and instance status. However, instead of using the entire resulting type as the pattern,
it extracts just the LHS of the equation.

For a theorem `∀ x₁ ... xₙ, lhs = rhs`, returns a pattern matching `lhs` with `n` pattern variables.
Throws an error if the theorem's conclusion is not an equality.
 -/
Lean.Meta.Sym.mkEqPatternFromDecl : Lean.Name → Lean.MetaM (Lean.Meta.Sym.Pattern × Lean.Expr)
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of the forward direction of `le_one_iff_eq_one`. -/
eq_one_of_le_one : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : One α] [IsBotOneClass α], a ≤ 1 → a = 1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.insert.go.eq_def : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (a : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.insert.go k m a =
    match a with
    | Lean.Grind.CommRing.Poly.num k' => Lean.Grind.CommRing.Poly.add k m (Lean.Grind.CommRing.Poly.num k')
    | Lean.Grind.CommRing.Poly.add k' m' p =>
      match m.grevlex m' with
      | Ordering.eq =>
        have k := k + k';
        bif k == 0 then p else Lean.Grind.CommRing.Poly.add k m p
      | Ordering.gt => Lean.Grind.CommRing.Poly.add k m (Lean.Grind.CommRing.Poly.add k' m' p)
      | Ordering.lt => Lean.Grind.CommRing.Poly.add k' m' (Lean.Grind.CommRing.Poly.insert.go k m p)
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.ext : ∀ {X Y : TopPair} {f g : X ⟶ Y} {x y : TopPair.Homotopy f g}, x.fst = y.fst → x.snd = y.snd → x = y
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl) The natural transformation used to define the new cone  -/
CategoryTheory.Monad.ForgetCreatesLimits.γ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {J : Type u} →
        [inst_1 : CategoryTheory.Category.{v, u} J] →
          (D : CategoryTheory.Functor J T.Algebra) → D.comp (T.forget.comp T.toFunctor) ⟶ D.comp T.forget
-- Mathlib.Data.Vector.Snoc
List.Vector.reverse_cons : ∀ {α : Type u_1} {n : ℕ} {x : α} (xs : List.Vector α n), (x ::ᵥ xs).reverse = xs.reverse.snoc x
-- Init.Data.Int.Order
Int.add_lt_add_iff_left : ∀ {b c : ℤ} (a : ℤ), a + b < a + c ↔ b < c
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst.eq_4 : ∀ (n k : ℕ), n.succ.stirlingFirst k.succ = n * n.stirlingFirst (k + 1) + n.stirlingFirst k
-- Mathlib.NumberTheory.SiegelsLemma
_private.Mathlib.NumberTheory.SiegelsLemma.0.Int.Matrix.termS : Lean.ParserDescr
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.SL_slash_def : ∀ {k : ℤ} (f : UpperHalfPlane → ℂ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ),
  SlashAction.map k γ f = fun τ =>
    f (γ • τ) *
      UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ ^
        (-k)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instAddCommSemigroupQuotient : {R : Type u_1} → [inst : AddCommSemigroup R] → [inst_1 : Mul R] → (c : RingCon R) → AddCommSemigroup c.Quotient
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, k ∈ m.alter k f ↔ (f (m.get? k)).isSome = true
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.biUnion_le_iff : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} {π' : BoxIntegral.Prepartition I},
  π.biUnion πi ≤ π' ↔ ∀ J ∈ π, πi J ≤ π'.restrict J
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : (Fin 0 → H) → ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₀ B).hom)
      ((CategoryTheory.ConcreteCategory.hom ((groupCohomology.cochainsMap f φ).f 0)) x) =
    (Rep.Hom.hom φ) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₀ A).hom) x)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- `VectorMeasure.map` as an additive monoid homomorphism.  -/
MeasureTheory.VectorMeasure.mapGm : {β : Type u_2} →
  [inst : MeasurableSpace β] →
    {M : Type u_3} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] →
          [inst_3 : ContinuousAdd M] →
            {α : Type u_4} →
              [inst_4 : MeasurableSpace α] →
                (α → β) → MeasureTheory.VectorMeasure α M →+ MeasureTheory.VectorMeasure β M
-- Mathlib.CategoryTheory.EquivalenceRelation
TypeCat.jointlyMono₂ : ∀ {X : Type w} (φ : X → X → Prop), CategoryTheory.JointlyMono₂ (TypeCat.p₁OfRel φ) (TypeCat.p₂OfRel φ)
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_inf_mul_relrank_of_le : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  (C : IntermediateField F E), A ≤ B → A.relrank (B ⊓ C) * B.relrank C = A.relrank C
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.map_smul : ∀ {R : Type u_1} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : SeminormedAddCommGroup E₂] [inst_3 : Module R E] [inst_4 : Module R E₂] (f : E →ₗᵢ[R] E₂) (c : R) (x : E),
  f (c • x) = c • f x
-- Mathlib.Combinatorics.Colex
/-- For finsets of naturals, the colexicographic order is equivalent to the order induced by the
`n`-ary expansion.  -/
Finset.geomSum_le_geomSum_iff_toColex_le_toColex : ∀ {s t : Finset ℕ} {n : ℕ}, 2 ≤ n → (∑ k ∈ s, n ^ k ≤ ∑ k ∈ t, n ^ k ↔ toColex s ≤ toColex t)
-- Mathlib.Algebra.Category.MonCat.Basic
AddEquiv.toAddMonCatIso_hom : ∀ {X Y : Type u} [inst : AddMonoid X] [inst_1 : AddMonoid Y] (e : X ≃+ Y),
  e.toAddMonCatIso.hom = AddMonCat.ofHom e.toAddMonoidHom
-- Mathlib.Order.BooleanAlgebra.Set
Set.notMem_of_mem_compl : ∀ {α : Type u_1} {s : Set α} {x : α}, x ∈ sᶜ → x ∉ s
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.unitGroup_injective : ∀ {K : Type u} [inst : Field K], Function.Injective ValuationSubring.unitGroup
-- Init.PropLemmas
Decidable.not_imp_not : ∀ {a b : Prop} [Decidable a], ¬a → ¬b ↔ b → a
-- Lean.Elab.PreDefinition.WF.Fix
Lean.Elab.WF.isNatLtWF : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeGPFree.smul_set : ∀ {α : Type u_2} [inst : CommMonoid α] [IsCancelMul α] {s : Set α} {a : α}, ThreeGPFree s → ThreeGPFree (a • s)
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.PollSources.response : {α β : Type} →
  Std.Http.Server.Connection.PollSources✝ α β → Option (Std.Channel (Except IO.Error (Std.Http.Response β)))
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.InducedCategory.concreteCategory : {C : Type u} →
  {D : Type u'} →
    [inst : CategoryTheory.Category.{v', u'} D] →
      {FD : D → D → Type u_2} →
        {CD : D → Type w} →
          [inst_1 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
            [CategoryTheory.ConcreteCategory D FD] →
              (f : C → D) →
                CategoryTheory.ConcreteCategory (CategoryTheory.InducedCategory D f) fun X Y => FD (f X) (f Y)
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDecl.lt : Lean.Meta.Simp.SimprocDecl → Lean.Meta.Simp.SimprocDecl → Bool
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.id_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V] {π₁ : ContRepresentation R G V}
  (v : V), ContIntertwiningMap.id v = v
-- Mathlib.Topology.VectorBundle.Basic
/-- The space `Bundle.TotalSpace F E` (for `E : B → Type*` such that each `E x` is a topological
vector space) has a topological vector space structure with fiber `F` (denoted with
`VectorBundle R F E`) if around every point there is a fiber bundle trivialization which is linear
in the fibers.  -/
VectorBundle : (R : Type u_1) →
  {B : Type u_2} →
    (F : Type u_3) →
      (E : B → Type u_4) →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [(x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [NormedSpace R F] →
                  [inst : TopologicalSpace B] →
                    [inst_4 : TopologicalSpace (Bundle.TotalSpace F E)] →
                      [inst_5 : (x : B) → TopologicalSpace (E x)] → [FiberBundle F E] → Prop
-- Mathlib.Tactic.CongrExclamation
/-- Does `Lean.MVarId.intros` but then cleans up the introduced hypotheses, removing anything
that is trivial. If there are any patterns in the current `CongrMetaM` state then instead
of `Lean.MVarId.intros` it does `Lean.Elab..Tactic.RCases.rintro`.

Cleaning up includes:
- deleting hypotheses of the form `x ≍ x`, `x = x`, and `x ↔ x`.
- deleting Prop hypotheses that are already in the local context.
- converting `x ≍ y` to `x = y` if possible.
- converting `x = y` to `x ↔ y` if possible.
 -/
Lean.MVarId.introsClean : Lean.MVarId → CongrMetaM (List Lean.MVarId)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.dirac_withDensity : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [MeasurableSingletonClass α] (f : α → ENNReal) (a : α),
  (MeasureTheory.Measure.dirac a).withDensity f = f a • MeasureTheory.Measure.dirac a
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.valuedCompletion_apply : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
  (x : K), Valued.v ↑x = Valued.v x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.lift_comp_algebraMap : ∀ (K : Type u_1) [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K]
  [inst_3 : Algebra.IsAlgebraic k K] (φ : k →+* ℂ), (NumberField.ComplexEmbedding.lift K φ).comp (algebraMap k K) = φ
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.RightHomologyData),
  CategoryTheory.CategoryStruct.comp h.homologyIso.hom h.ι =
    CategoryTheory.CategoryStruct.comp S.homologyι h.opcyclesIso.hom