mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The equivalence between `Hom (F X) Y` and `Hom X (G Y)`  -/
CategoryTheory.Adjunction.CoreHomEquiv.homEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            CategoryTheory.Adjunction.CoreHomEquiv F G → (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.nnnorm_def : ∀ {R : Type u_3} {M : Type u_4} [inst : SeminormedRing R] [inst_1 : SeminormedAddCommGroup M] (x : TrivSqZeroExt R M),
  ‖x‖₊ = ‖x.fst‖₊ + ‖x.snd‖₊
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExSumNat.add.sizeOf_spec : ∀ {a b : Q(ℕ)} (a_1 : Mathlib.Tactic.Ring.Common.ExProdNat a) (a_2 : Mathlib.Tactic.Ring.Common.ExSumNat b),
  sizeOf (Mathlib.Tactic.Ring.Common.ExSumNat.add a_1 a_2) = 1 + sizeOf a + sizeOf b + sizeOf a_1 + sizeOf a_2
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
BoundedVariationOn.vectorMeasure_univ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f : α → E}
  (hf : BoundedVariationOn f Set.univ), hf.vectorMeasure Set.univ = Filter.atTop.limUnder f - Filter.atBot.limUnder f
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.isClosed_closedCell`. -/
Topology.CWComplex.isClosed_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] [T2Space X] {n : ℕ}
  {i : Topology.RelCWComplex.cell C n}, IsClosed (Topology.RelCWComplex.closedCell n i)
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- Another characterization lemma for the addition on the Ore localization delivering
Ore witnesses and conditions bundled in a sigma type.  -/
AddOreLocalization.oreSubAddChar' : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [inst_1 : AddOreLocalization.AddOreSet S] →
        (r₁ r₂ : R) →
          (s₁ s₂ : ↥S) → (r' : R) ×' (s' : ↥S) ×' ↑s' + r₁ = r' + ↑s₂ ∧ r₁ -ₒ s₁ + (r₂ -ₒ s₂) = r' + r₂ -ₒ (s' + s₁)
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.iff_of_equiv : ∀ {R : Type u} {A : Type v} {B : Type u_1} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] (e : A ≃ₐ[R] B), Algebra.FormallyEtale R A ↔ Algebra.FormallyEtale R B
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.EqResult.eq.inj : ∀ {x y p x_1 y_1 p_1 : Lean.Expr}, Nat.EqResult.eq✝ x y p = Nat.EqResult.eq✝ x_1 y_1 p_1 → x = x_1 ∧ y = y_1 ∧ p = p_1
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS₂_three : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), complEDS₂ b c d 3 = preNormEDS (b ^ 4) c d 5 * b - d ^ 2 * b
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.testAgainstNN_one : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω),
  μ.testAgainstNN 1 = μ.mass
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.image : ∀ {R : Type u_3} {X : Type u_5} {Y : Type u_6} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y] {f : X → Y}
  {s : Set X}, Convexity.IsAffineMap R f → Convexity.IsConvexSet R s → Convexity.IsConvexSet R (f '' s)
-- Mathlib.NumberTheory.ModularForms.Discriminant
ModularForm.tendsto_atImInfty_tprod_one_sub_eta_q_pow : Filter.Tendsto (fun x => ∏' (n : ℕ), (1 - ModularForm.eta_q n ↑x) ^ 24) UpperHalfPlane.atImInfty (nhds 1)
-- Lean.Syntax
/-- List of `Syntax` nodes in which each succeeding element is the parent of
the current. The associated index is the index of the preceding element in the
list of children of the current element.  -/
Lean.Syntax.Stack : Type
-- Mathlib.CategoryTheory.Comma.Over.OverClass
/-- `OverClass X S` is the typeclass containing the data of a structure morphism `X ↘ S : X ⟶ S`.
 -/
CategoryTheory.OverClass : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → C → Type v
-- Mathlib.Algebra.Lie.Basic
LieEquiv.refl_apply : ∀ {R : Type u} {L₁ : Type v} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁] (x : L₁),
  LieEquiv.refl x = x
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.injective_iff_periodicPts_eq_univ : ∀ {α : Type u_1} {f : α → α} [Finite α], Function.Injective f ↔ Function.periodicPts f = Set.univ
-- Mathlib.Order.Bounds.Basic
isLUB_pair : ∀ {γ : Type u_3} [inst : SemilatticeSup γ] {a b : γ}, IsLUB {a, b} (a ⊔ b)
-- Mathlib.Data.Finset.Option
Finset.eraseNone.eq_1 : ∀ {α : Type u_1},
  Finset.eraseNone =
    (Finset.mapEmbedding (Equiv.optionIsSomeEquiv α).toEmbedding).toOrderHom.comp
      { toFun := Finset.subtype fun x => x.isSome = true, monotone' := ⋯ }
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
/-- **Double counting** argument.

Considering `r` as a bipartite graph, the LHS is a lower bound on the number of edges while the RHS
is an upper bound.  -/
Finset.card_nsmul_le_card_nsmul : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β} [inst : Semiring R]
  [inst_1 : PartialOrder R] [IsOrderedRing R] {m n : R} [inst_3 : (a : α) → (b : β) → Decidable (r a b)],
  (∀ a ∈ s, m ≤ ↑(Finset.bipartiteAbove r t a).card) →
    (∀ b ∈ t, ↑(Finset.bipartiteBelow r s b).card ≤ n) → s.card • m ≤ t.card • n
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isRat_eq_true : ∀ {α : Type u} [inst : Ring α] {a b : α} {n : ℤ} {d : ℕ},
  Mathlib.Meta.NormNum.IsRat a n d → Mathlib.Meta.NormNum.IsRat b n d → a = b
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasProdLocallyUniformlyOn f g s ↔ TendstoLocallyUniformlyOn (fun x1 x2 => ∏ i ∈ x1, f i x2) g Filter.atTop s
-- Init.Data.List.Sort.Lemmas
List.MergeSort.Internal.splitInTwo_cons_cons_zipIdx_snd : ∀ {α : Type u_1} {a b : α} (i : ℕ) (l : List α),
  ↑(List.MergeSort.Internal.splitInTwo ⟨(a, i) :: (b, i + 1) :: l.zipIdx (i + 2), ⋯⟩).2 =
    (↑(List.MergeSort.Internal.splitInTwo ⟨a :: b :: l, ⋯⟩).2).zipIdx (i + (l.length + 3) / 2)
-- Mathlib.Analysis.Normed.Affine.AddTorsor
DilationEquiv.smulTorsor_ratio : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : NormSMulClass 𝕜 E] {P : Type u_3} [inst_4 : PseudoMetricSpace P] [inst_5 : NormedAddTorsor E P] {c : P}
  {k : 𝕜} (hk : k ≠ 0) {x y : E}, dist x y ≠ 0 → Dilation.ratio (DilationEquiv.smulTorsor c hk) = ‖k‖₊
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k a : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.getKey! a =
    if compare k a = Ordering.eq ∧ k ∉ t then k else t.getKey! a
-- Lean.Meta.Eqns
/-- Returns `true` if `s` is of the form `eq_<idx>`  -/
Lean.Meta.isEqnReservedNameSuffix : String → Bool
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.step_iterFromIdxM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} {xs : Vector β n} {pos : ℕ},
  (xs.iterFromIdxM m pos).step =
    pure
      (Std.Shrink.deflate
        (if h : pos < n then Std.PlausibleIterStep.yield (xs.iterFromIdxM m (pos + 1)) xs[pos] ⋯
        else Std.PlausibleIterStep.done ⋯))
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {km : α}, t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
/-- The constant sheaf functor commutes up to isomorphism the inverse equivalence of sheaf categories
induced by a dense subsite.
 -/
CategoryTheory.equivCommuteConstant' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type u_2) →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.HasWeakSheafify J D] →
            {C' : Type u_3} →
              [inst_3 : CategoryTheory.Category.{v_3, u_3} C'] →
                (K : CategoryTheory.GrothendieckTopology C') →
                  [inst_4 : CategoryTheory.HasWeakSheafify K D] →
                    (G : CategoryTheory.Functor C C') →
                      [inst_5 :
                          ∀ (X : C'ᵒᵖ),
                            CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) D] →
                        [inst_6 : CategoryTheory.Functor.IsDenseSubsite J K G] →
                          {T : C} →
                            CategoryTheory.Limits.IsTerminal T →
                              CategoryTheory.Limits.IsTerminal (G.obj T) →
                                (CategoryTheory.constantSheaf J D ≅
                                  (CategoryTheory.constantSheaf K D).comp
                                    (CategoryTheory.Functor.IsDenseSubsite.sheafEquiv J K G D).inverse)
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.funUnique.eq_1 : ∀ (α : Type u_2) (M : Type u_4) [inst : Add M] [inst_1 : Unique α],
  AddEquiv.funUnique α M = { toEquiv := Equiv.funUnique α M, map_add' := ⋯ }
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsAEKolmogorovProcess.kolmogorovCondition : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E},
  ProbabilityTheory.IsAEKolmogorovProcess X P p q M →
    ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q
-- Mathlib.CategoryTheory.Square
/-- the bottom morphism  -/
CategoryTheory.Square.f₃₄ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (self : CategoryTheory.Square C) → self.X₃ ⟶ self.X₄
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.pairingIn_same : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [FaithfulSMul S R] [inst_8 : P.IsValuedIn S] (i : ι),
  P.pairingIn S i i = 2
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
InformationTheory.isMinOn_klFun : IsMinOn InformationTheory.klFun (Set.Ici 0) 1
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntFinCoOfNatIntCast : {n : ℕ} → Lean.Grind.ToInt (Fin n) (Lean.Grind.IntInterval.co 0 ↑n)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RccSlice.instToIterator : {α : Type u_1} →
  [inst : Ord α] →
    Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Unit.RccSliceData α)) Id
      (Std.Iterators.Types.Map (Std.DTreeMap.Internal.RxcIterator α fun x => Unit) Id Id (fun ⦃x⦄ => monadLift) fun b =>
        pure b.fst)
      α
-- Std.Async.System
Std.Async.System.instOrdUserId : Ord Std.Async.System.UserId
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.instInhabitedWalkingParallelFamily.default : {J : Type w} → CategoryTheory.Limits.WalkingParallelFamily J
-- Init.Omega.Constraint
/-- An upper bound.  -/
Lean.Omega.Constraint.upperBound : Lean.Omega.Constraint → Lean.Omega.UpperBound
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.lt_map_of_nat_lt_translationNumber : ∀ (f : CircleDeg1Lift) {n : ℕ}, ↑n < f.translationNumber → ∀ (x : ℝ), x + ↑n < f x
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.sub : ∀ {𝕜 : 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'] {z : M} {f g : M → E'}, MDiffAt f z → MDiffAt g z → MDiffAt (f - g) z
-- Mathlib.Algebra.Group.Equiv.Defs
Monoid.End.equiv.eq_1 : ∀ (M : Type u_9) [inst : MulOne M], Monoid.End.equiv M = { toFun := id, invFun := id, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Order.Compare
Ordering.Compares.cmp_eq : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} {o : Ordering}, o.Compares a b → cmp a b = o
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.comap_range_self : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), AddSubgroup.comap f f.range = ⊤
-- Mathlib.Order.Filter.Map
Filter.map_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {m : α → β} {f : ι → Filter α},
  Filter.map m (⨆ i, f i) = ⨆ i, Filter.map m (f i)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_comp_C_mul_X_add_C : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R) (a b : R),
  IsUnit a →
    (p.comp (Polynomial.C a * Polynomial.X + Polynomial.C b)).roots =
      Multiset.map (fun x => Ring.inverse a * (x - b)) p.roots
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_unitIso_inv_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) (X : CategoryTheory.MorphismProperty.Comma L₁ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).unitIso.inv.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Init.Data.Option.Lemmas
Option.toList_some : ∀ {α : Type u_1} (a : α), (some a).toList = [a]
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.preComp.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasImage g]
  [inst_2 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)],
  CategoryTheory.Limits.image.preComp f g =
    CategoryTheory.Limits.image.lift
      { I := CategoryTheory.Limits.image g, m := CategoryTheory.Limits.image.ι g, m_mono := ⋯,
        e := CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.factorThruImage g), fac := ⋯ }
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.comp_apply : ∀ {R S T : CommSemiRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : ↑R),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) r =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) r)
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- Over a noetherian ring the infimum of a finite family of CoFG submodules is CoFG.  -/
Submodule.CoFG.sInf_of_finite : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherianRing R]
  {s : Set (Submodule R M)}, s.Finite → (∀ S ∈ s, S.CoFG) → (sInf s).CoFG
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_erase_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α}, (m.erase k)[k]! = default
-- Mathlib.MeasureTheory.Function.LpOrder
MeasureTheory.Lp.coeFn_nonneg : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  [inst : NormedAddCommGroup E] [inst_1 : PartialOrder E] (f : ↥(MeasureTheory.Lp E p μ)), 0 ≤ᵐ[μ] ↑↑f ↔ 0 ≤ f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false ↔ ∃ a, a ∈ t
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haarMeasure.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G),
  MeasureTheory.Measure.haarMeasure K₀ =
    ((MeasureTheory.Measure.haar.haarContent K₀).measure ↑K₀)⁻¹ • (MeasureTheory.Measure.haar.haarContent K₀).measure
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryExtensive.isPullback_initial_to_sigma_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.FinitaryExtensive C] {ι : Type u_1}
  [inst_2 : Finite ι] (X : ι → C) (i j : ι),
  i ≠ j →
    CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j))
      (CategoryTheory.Limits.Sigma.ι X i) (CategoryTheory.Limits.Sigma.ι X j)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_3_comp_chainsIso₃_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {Z : ModuleCat k}
  (h : ModuleCat.of k (H × H × H →₀ ↑B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((groupHomology.chainsMap f φ).f 3)
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₃ B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₃ A).hom
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap₃ f φ) h)
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtrOn.inter : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsLocalExtrOn f s a → ∀ (t : Set α), IsLocalExtrOn f (s ∩ t) a
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- With Mathlib's particular conventions, we have `ζ 1 ≠ 0`.  -/
riemannZeta_one_ne_zero : riemannZeta 1 ≠ 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.map_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type w'} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp}
  {f : α → β → γ} {g : α → γ → δ},
  Std.ExtTreeMap.map g (Std.ExtTreeMap.map f t) = Std.ExtTreeMap.map (fun k v => g k (f k v)) t
-- Mathlib.CategoryTheory.Category.Cat
/-- The equivalence between the type of functors between two categories and
the type of 1-morphisms in Cat between the objects corresponding to those categories.
 -/
CategoryTheory.Functor.equivCatHom : (C D : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Category.{v, u} D] →
      CategoryTheory.Functor C D ≃ (CategoryTheory.Cat.of C ⟶ CategoryTheory.Cat.of D)
-- Lean.Meta.Iterator
/-- Map and filter results of iterator and returning only those values returned
by `f`.
 -/
Lean.Meta.Iterator.filterMapM : {α β : Type} → (α → Lean.MetaM (Option β)) → Lean.Meta.Iterator α → Lean.Meta.Iterator β
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- Given a sheaf of `R`-modules `M` and a `Presentation M`, there is two morphism of
sheaves of `R`-modules `f : free ι ⟶ free σ` and `g : free σ ⟶ M` satisfying `H : f ≫ g = 0`
and `IsColimit (CokernelCofork.ofπ g H)`.  -/
SheafOfModules.Presentation.isColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} →
              (P : M.Presentation) →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ P.generators.π ⋯)
-- Mathlib.Topology.Semicontinuity.Defs
hasOpenLowerSections_restrict_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {s : Set α},
  HasOpenLowerSections (s.domRestrict f) ↔ HasOpenLowerSectionsOn f s
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_eq_getKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α} {h' : a ∈ t}, t.getKey a h' = t.getKey! a
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] (X Y : C),
  CategoryTheory.CategoryStruct.comp
      (e.counitIso.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y)))
      (e.functor.map (CategoryTheory.Functor.OplaxMonoidal.δ e.inverse (e.functor.obj X) (e.functor.obj Y))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ e.functor X Y)
      (e.functor.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y)))
-- Mathlib.Topology.UniformSpace.Closeds
hausdorffEntourage_mono : ∀ {α : Type u_1} {U V : SetRel α α}, U ⊆ V → hausdorffEntourage U ⊆ hausdorffEntourage V
-- Std.Http.Data.URI.Basic
/-- Authority port representation, preserving the distinction between:
* no port separator (`example.com`)
* empty port (`example.com:`)
* numeric port (`example.com:443`)
 -/
Std.Http.URI.Port : Type
-- Mathlib.Analysis.BoundedVariation
LocallyBoundedVariationOn.smul : ∀ {α : Type u_2} [inst : LinearOrder α] {F : Type u_4} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {𝕜 : Type u_6} {f : α → 𝕜} {g : α → F} [inst_3 : NormedRing 𝕜] [inst_4 : NormedAlgebra ℝ 𝕜] [inst_5 : Module 𝕜 F]
  [NormSMulClass 𝕜 F] [IsScalarTower ℝ 𝕜 F] {s : Set α},
  LocallyBoundedVariationOn f s → LocallyBoundedVariationOn g s → LocallyBoundedVariationOn (f • g) s
-- Mathlib.Analysis.Normed.Group.Basic
norm_one' : ∀ {E : Type u_5} [inst : SeminormedGroup E], ‖1‖ = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.differentiable_cosh : Differentiable ℝ Real.cosh
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- Coercion to a function as a `AddMonoidHom`. Similar to `AddMonoidHom.coeFn`.  -/
CompactlySupportedContinuousMap.coeFnMonoidHom : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddMonoid β] → [inst_3 : ContinuousAdd β] → CompactlySupportedContinuousMap α β →+ α → β
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nonneg_cases : ∀ {d : ℕ} {a : ℤ√↑d},
  a.Nonneg → ∃ x y, a = { re := ↑x, im := ↑y } ∨ a = { re := ↑x, im := -↑y } ∨ a = { re := -↑x, im := ↑y }
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.const.injEq : ∀ (a : Lean.Name) (a_1 : ℕ) (a_2 : Lean.Name) (a_3 : ℕ),
  (Lean.Meta.DiscrTree.Key.const a a_1 = Lean.Meta.DiscrTree.Key.const a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
/-- The inertia degree of `w` over `v`.  -/
NumberField.InfinitePlace.inertiaDeg : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] → [Algebra K L] → NumberField.InfinitePlace K → NumberField.InfinitePlace L → ℕ
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.convexHull_subset_space : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s : Finset E}, s ∈ K.faces → (convexHull 𝕜) ↑s ⊆ K.space
-- Mathlib.Algebra.Group.ULift
ULift.commSemigroup : {α : Type u} → [CommSemigroup α] → CommSemigroup (ULift.{u_1, u} α)