mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Function
Set.InjOn.imageFactorization_injective : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s → Function.Injective (Set.imageFactorization f s)
-- Std.Data.Iterators.Producers.Monadic.Empty
Std.Iterators.Types.Empty.instIteratorLoop : {m : Type w → Type w'} →
  {β : Type w} →
    {n : Type x → Type x'} → [inst : Monad m] → [Monad n] → Std.IteratorLoop (Std.Iterators.Types.Empty m β) m n
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.awayToAwayRight.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (x x_1 : R) (e_x : x = x_1) [inst_4 : IsLocalization.Away x S] (y y_1 : R) (e_y : y = y_1)
  [inst_5 : Algebra R P] [inst_6 : IsLocalization.Away (x * y) P],
  IsLocalization.Away.awayToAwayRight x y = IsLocalization.Away.awayToAwayRight x_1 y_1
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_sub_Ioi : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => a - x) '' Set.Ioi b = Set.Iio (a - b)
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The second of the two parallel morphisms of the fork diagram, induced by the second projection in
each pullback.
 -/
CategoryTheory.Equalizer.Presieve.Arrows.secondMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type w)) →
      {B : C} →
        {I : Type t} →
          [inst_1 : Small.{w, t} I] →
            (X : I → C) →
              (π : (i : I) → X i ⟶ B) →
                [inst_2 : (CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks] →
                  CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X ⟶
                    CategoryTheory.Equalizer.Presieve.Arrows.SecondObj P X π
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.rnDeriv_add : ∀ {α : Type u_1} {m : MeasurableSpace α} (s t : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α)
  [s.HaveLebesgueDecomposition μ] [t.HaveLebesgueDecomposition μ] [(s + t).HaveLebesgueDecomposition μ],
  (s + t).rnDeriv μ =ᵐ[μ] s.rnDeriv μ + t.rnDeriv μ
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [inst_2 : AddZeroClass α] →
          [inst_3 : AddZeroClass β] → (toAddMonoidHom : α →+ β) → Monotone (↑toAddMonoidHom).toFun → α →+o β
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.admissible_E8 : ADEInequality.Admissible ADEInequality.E8
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.arrowMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] {j : J}
  (F : CategoryTheory.Functor (↑(Set.Iic j)) C) (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ j),
  CategoryTheory.SmallObject.SuccStruct.arrowMap F i₁ i₂ h₁₂ h₂ =
    CategoryTheory.Arrow.mk (F.map (CategoryTheory.homOfLE h₁₂))
-- Mathlib.Data.Finmap
Finmap.erase.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : Finmap β),
  Finmap.erase a s = s.liftOn (fun t => (AList.erase a t).toFinmap) ⋯
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- A simpler inductive constructor for `ℕ`-indexed chain complexes.

You provide explicitly the first differential,
then a function which takes a differential,
and returns the next object, its differential, and the fact it composes appropriately to zero.
 -/
ChainComplex.mk' : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (X₀ X₁ : V) →
        (X₁ ⟶ X₀) →
          ({X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0) →
            ChainComplex V ℕ
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemKind.arrayElem : Lean.Json.CompressWorkItemKind✝
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.weightedSMul.eq_1 : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (s : Set α), MeasureTheory.weightedSMul μ s = μ.real s • ContinuousLinearMap.id ℝ F
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaAddMon_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : CategoryTheory.AddMon C), CategoryTheory.yonedaAddMon.obj M = CategoryTheory.yonedaAddMonObj M.X
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.coe_mk : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {f : A →ₗ[R] B} (h : CoalgebraStruct.counit ∘ₗ f = CoalgebraStruct.counit)
  (h₁ : TensorProduct.map f f ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ f),
  ⇑{ toLinearMap := f, counit_comp := h, map_comp_comul := h₁ } = ⇑f
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.mk''_eq_mk : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁), Quotient.mk'' p = Path.Homotopic.Quotient.mk p
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- Sum of a list of elements in an `AddSubmonoid` is in the `AddSubmonoid`.  -/
list_sum_mem : ∀ {M : Type u_1} {B : Type u_3} [inst : AddMonoid M] [inst_1 : SetLike B M] [AddSubmonoidClass B M] {S : B}
  {l : List M}, (∀ x ∈ l, x ∈ S) → l.sum ∈ S
-- Mathlib.Algebra.Group.Basic
inv_eq_iff_mul_eq_one : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a⁻¹ = b ↔ a * b = 1
-- Mathlib.Analysis.Polynomial.CauchyBound
Polynomial.cauchyBound.eq_1 : ∀ {K : Type u_1} [inst : NormedDivisionRing K] (p : Polynomial K),
  p.cauchyBound = ((Finset.range p.natDegree).sup fun x => ‖p.coeff x‖₊) / ‖p.leadingCoeff‖₊ + 1
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_units_coe_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (u : αˣ) (a : α),
  lcm (↑u) a = normalize a
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The coproduct of a finite family of objects in `CompHaus`, constructed as the disjoint
union with its usual topology.
 -/
CompHausLike.finiteCoproduct : {P : TopCat → Prop} →
  {α : Type w} → [Finite α] → (X : α → CompHausLike P) → [CompHausLike.HasExplicitFiniteCoproduct X] → CompHausLike P
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- `MultilinearMap.domDomCongr` as an equivalence.

This is declared separately because it does not work with dot notation.  -/
MultilinearMap.domDomCongrEquiv : {R : Type uR} →
  {M₂ : Type v₂} →
    {M₃ : Type v₃} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M₂] →
          [inst_2 : AddCommMonoid M₃] →
            [inst_3 : Module R M₂] →
              [inst_4 : Module R M₃] →
                {ι₁ : Type u_1} →
                  {ι₂ : Type u_2} → ι₁ ≃ ι₂ → MultilinearMap R (fun x => M₂) M₃ ≃+ MultilinearMap R (fun x => M₂) M₃
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- This is `Quot.recOn` specialized to connected components.
For convenience, it strengthens the assumptions in the hypothesis
to provide a path between the vertices.  -/
SimpleGraph.ConnectedComponent.recOn : {V : Type u} →
  {G : SimpleGraph V} →
    {motive : G.ConnectedComponent → Sort u_1} →
      (c : G.ConnectedComponent) →
        (f : (v : V) → motive (G.connectedComponentMk v)) →
          (∀ (u v : V) (p : G.Walk u v), p.IsPath → ⋯ ▸ f u = f v) → motive c
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} {d e : CategoryTheory.Factorisation f}
  {x y : d.Hom e}, x = y ↔ x.h = y.h
-- Mathlib.Topology.CompactOpen
ContinuousMap.instContinuousEvalConst : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  ContinuousEvalConst C(X, Y) X Y
-- Mathlib.Data.Sym.Basic
Sym.exists_mem : ∀ {α : Type u_1} {n : ℕ} (s : Sym α n.succ), ∃ a, a ∈ s
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.cond_univ : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ],
  μ[|Set.univ] = μ
-- Mathlib.RingTheory.Algebraic.Basic
IsLocalization.isAlgebraic : ∀ {R : Type u} (S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Nontrivial R]
  (M : Submonoid R) [IsLocalization M S], Algebra.IsAlgebraic R S
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
ConditionallyCompleteLinearOrderBot.toOrderBot : {α : Type u_5} → [self : ConditionallyCompleteLinearOrderBot α] → OrderBot α
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_sub : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Sub β]
  [inst_3 : ContinuousSub β] (f g : C(α, β)), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.pow_of_le_right : ∀ {α : Type u_1} {l : Filter α} {f : α → ℝ}, 1 ≤ᶠ[l] f → ∀ {m n : ℕ}, n ≤ m → (f ^ n) =O[l] (f ^ m)
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedCommGroup.genLTOne_eq_of_top : ∀ (G : Type u_1) [inst : CommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedMonoid G] [inst_3 : Nontrivial G]
  [inst_4 : IsCyclic G], LinearOrderedCommGroup.genLTOne G = LinearOrderedCommGroup.Subgroup.genLTOne ⊤
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquivClass.toMulEquiv.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : Mul α] [inst_2 : Mul β]
  [inst_3 : MulEquivClass F α β] (f : F), ↑f = { toEquiv := ↑f, map_mul' := ⋯ }
-- Mathlib.Topology.CantorBendixson
/-- The perfect kernel of a set, defined as the intersection of all iterated derived sets. It is
the largest perfect subset of the original set.  -/
CantorBendixson.perfectKernel : {X : Type u} → [TopologicalSpace X] → Set X → Set X
-- Mathlib.Data.Option.Defs
Option.elim'_eq_elim : ∀ {α : Type u_3} {β : Type u_4} (b : β) (f : α → β) (a : Option α), Option.elim' b f a = a.elim b f
-- Mathlib.Geometry.Manifold.WhitneyEmbedding
_private.Mathlib.Geometry.Manifold.WhitneyEmbedding.0.SmoothBumpCovering.embeddingPiTangent_injOn : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {H : Type uH} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_4 : TopologicalSpace M]
  [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I (↑⊤) M] [inst_7 : T2Space M] [inst_8 : Fintype ι] {s : Set M}
  (f : SmoothBumpCovering ι I M s), Set.InjOn (⇑(SmoothBumpCovering.embeddingPiTangent✝ f)) s
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_zsmul' : ∀ {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : SubNegMonoid G]
  [inst_2 : SubNegMonoid H] [AddMonoidHomClass F G H] (f : F),
  (∀ (x : G), f (-x) = -f x) → ∀ (g : ι → G) (n : ℤ), ⇑f ∘ (n • g) = n • ⇑f ∘ g
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularCompactLTTop.instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [BorelSpace α]
  [R1Space α] [h : μ.InnerRegularCompactLTTop] [MeasureTheory.IsFiniteMeasure μ], μ.Regular
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.term? : Aesop.Frontend.RuleConfig → Option Lean.Term
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.coeSubmodule_mono : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {I J : Ideal R}, I ≤ J → IsLocalization.coeSubmodule S I ≤ IsLocalization.coeSubmodule S J
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- Subgroups of a group `G` are isomorphic to additive subgroups of `Additive G`.  -/
Subgroup.toAddSubgroup : {G : Type u_1} → [inst : Group G] → Subgroup G ≃o AddSubgroup (Additive G)
-- Std.Http.Data.URI.Basic
Std.Http.URI.instReprUserInfo : Repr Std.Http.URI.UserInfo
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
Std.IterM.step_empty : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m],
  (Std.IterM.empty m β).step = pure (Std.Shrink.deflate ⟨Std.IterStep.done, ⋯⟩)
-- Lean.Meta.Tactic.Grind.AC.Types
/-- If `recheck` is `true`, then new equalities have been added to the basis since we checked
disequalities and implied equalities.
 -/
Lean.Meta.Grind.AC.Struct.recheck : Lean.Meta.Grind.AC.Struct → Bool
-- Mathlib.Computability.Primrec.List
Primrec.list_rec : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → List β} {g : α → σ} {h : α → β × List β × σ → σ},
  Primrec f → Primrec g → Primrec₂ h → Primrec fun a => List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_getEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α}
  (hl : Std.Internal.List.containsKey k l = true), Std.Internal.List.getEntry k l hl ∈ l
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, k ∈ t₂ → (t₁ \ t₂).get! k = default
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_insertManyIfNewUnit_emptyWithCapacity_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  Std.DHashMap.Internal.Raw₀.Const.get?
      (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k =
    if l.contains k = true then some () else none
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.rank_lt_iff_mem : ∀ {x y : ZFSet.{u_1}}, x.IsOrdinal → y.IsOrdinal → (x.rank < y.rank ↔ x ∈ y)
-- Mathlib.Algebra.Group.Commute.Basic
Commute.inv_mul_cancel : ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → a⁻¹ * b * a = b
-- Init.Data.Nat.Lemmas
/-- Shift left on successor with multiple moved inside.  -/
Nat.shiftLeft_succ_inside : ∀ (m n : ℕ), m <<< (n + 1) = (2 * m) <<< n
-- Mathlib.RingTheory.Algebraic.Basic
/-- **Alias** of `isAlgebraic_natCast`. -/
isAlgebraic_nat : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Nontrivial R] (n : ℕ),
  IsAlgebraic R ↑n
-- Mathlib.Data.Set.Lattice
iInf_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : CompleteLattice β] (s : ι → Set α) (f : α → β),
  ⨅ a ∈ ⋃ i, s i, f a = ⨅ i, ⨅ a ∈ s i, f a
-- Mathlib.Algebra.BigOperators.Balance
Fintype.balance_apply : ∀ {ι : Type u_1} {G : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup G] [inst_2 : Module ℚ≥0 G] (f : ι → G)
  (x : ι), Fintype.balance f x = f x - Finset.univ.expect fun y => f y
-- Mathlib.Algebra.Group.Defs
AddLeftCancelSemigroup.toAddSemigroup : {G : Type u} → [self : AddLeftCancelSemigroup G] → AddSemigroup G
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.IsRepresentedBy.iff_natIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {x : F.obj (Opposite.op X)} {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (e : F ≅ F'),
  F'.IsRepresentedBy ((CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op X))) x) ↔ F.IsRepresentedBy x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.refl : ∀ {V : Type u} {G : SimpleGraph V} (u : V), G.Reachable u u
-- Init.Data.Array.Lemmas
/-- Variant of `anyM_toArray` with a side condition on `stop`.  -/
List.anyM_toArray' : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α} {stop : ℕ},
  stop = l.toArray.size → Array.anyM p l.toArray 0 stop = List.anyM p l
-- Mathlib.Algebra.Category.Grp.Limits
/-- The flat sections of a functor into `GrpCat` form a subgroup of all sections.  -/
GrpCat.sectionsSubgroup : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] → (F : CategoryTheory.Functor J GrpCat) → Subgroup ((j : J) → ↑(F.obj j))
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendMap_f : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c')
  {i : ι} {i' : ι'} (h : e.f i = i'),
  (HomologicalComplex.extendMap φ e).f i' =
    CategoryTheory.CategoryStruct.comp (K.extendXIso e h).hom
      (CategoryTheory.CategoryStruct.comp (φ.f i) (L.extendXIso e h).inv)
-- Init.Grind.Ring.Field
/-- The inverse of zero is zero. This is a "junk value" convention.  -/
Lean.Grind.Field.inv_zero : ∀ {α : Type u} [self : Lean.Grind.Field α], 0⁻¹ = 0
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.sup_disjoint : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) (K₁ K₂ : TopologicalSpace.Compacts G),
  Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → μ (K₁ ⊔ K₂) = μ K₁ + μ K₂
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.eq_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α)
  {a b : α}, a ≤ b → variationOnFromTo f s a b = (eVariationOn f (s ∩ Set.Icc a b)).toReal
-- Mathlib.GroupTheory.OrderOfElement
finEquivZPowers.congr_simp : ∀ {G : Type u_1} [inst : Group G] {x : G} (hx : IsOfFinOrder x), finEquivZPowers hx = finEquivZPowers hx
-- Mathlib.Order.SymmDiff
sdiff_symmDiff : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b c : α), c \ symmDiff a b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.instIsHomologicalHomologyFunctor : ∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_3, u_2} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (n : ℤ), (DerivedCategory.Plus.homologyFunctor C n).IsHomological
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
/-- A function `f` is integrable with respect to a countable sum of measures `Measure.sum μ`
if and only if `f` is integrable with respect to each `μ i` and
the sequence `fun i ↦ ∫ x, ‖f x‖ ∂μ i` is summable.  -/
MeasureTheory.integrable_sum_measure_iff : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} [Countable ι] {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  {μ : ι → MeasureTheory.Measure X} {f : X → E},
  MeasureTheory.Integrable f (MeasureTheory.Measure.sum μ) ↔
    (∀ (i : ι), MeasureTheory.Integrable f (μ i)) ∧ Summable fun i => ∫ (x : X), ‖f x‖ ∂μ i
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.divRight.congr_simp : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] (x x_1 : G),
  x = x_1 → Homeomorph.divRight x = Homeomorph.divRight x_1
-- Mathlib.Data.Finset.NAry
Finset.image₂_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
  Finset.image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅
-- Lean.Meta.Tactic.Grind.Action
_private.Lean.Meta.Tactic.Grind.Action.0.Lean.Meta.Grind.Action.loop.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive n
-- Mathlib.Data.W.Basic
_private.Mathlib.Data.W.Basic.0.WType.encodable_succ : {α : Type u_1} →
  {β : α → Type u_2} →
    [inst : (a : α) → Fintype (β a)] →
      [(a : α) → Encodable (β a)] →
        [Encodable α] → (n : ℕ) → Encodable (WType.WType'✝ β n) → Encodable (WType.WType'✝ β (n + 1))
-- Mathlib.Analysis.MeanInequalities
Real.geom_mean_lt_arith_mean2_weighted_iff_of_nonneg : ∀ {w₁ w₂ p₁ p₂ : ℝ},
  0 ≤ w₁ → 0 ≤ w₂ → 0 ≤ p₁ → 0 ≤ p₂ → w₁ + w₂ = 1 → (p₁ ^ w₁ * p₂ ^ w₂ < w₁ * p₁ + w₂ * p₂ ↔ w₁ ≠ 0 ∧ w₂ ≠ 0 ∧ p₁ ≠ p₂)
-- Mathlib.Topology.Spectral.Hom
/-- proof that `toFun` is a spectral map  -/
SpectralMap.spectral' : ∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (self : SpectralMap α β),
  IsSpectralMap self.toFun
-- Mathlib.Data.Finsupp.Fin
Finsupp.cons_ne_zero_of_left : ∀ {n : ℕ} {M : Type u_1} [inst : Zero M] {y : M} {s : Fin n →₀ M}, y ≠ 0 → Finsupp.cons y s ≠ 0
-- Mathlib.Dynamics.BirkhoffSum.NormedSpace
dist_birkhoffSum_apply_birkhoffSum : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] (f : α → α) (g : α → E) (n : ℕ) (x : α),
  dist (birkhoffSum f g n (f x)) (birkhoffSum f g n x) = dist (g (f^[n] x)) (g x)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_inv_naturality : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {d₁ d₂ : D} {c₁ c₂ c₃ c₄ : C} (f : d₁ ⟶ d₂)
  (g : c₁ ⟶ c₂) (h : c₃ ⟶ c₄),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g) h)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d₂ c₂ c₄).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d₁ c₁ c₃).inv
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f
        (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.countablePartition.eq_1 : ∀ (α : Type u_3) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α],
  MeasurableSpace.countablePartition α = memPartition (Set.enumerateCountable ⋯ ∅)
-- Mathlib.Algebra.BigOperators.Pi
Pi.multiset_sum_apply : ∀ {α : Type u_7} {M : α → Type u_8} [inst : (a : α) → AddCommMonoid (M a)] (a : α) (s : Multiset ((a : α) → M a)),
  s.sum a = (Multiset.map (fun f => f a) s).sum
-- Init.Data.List.Lemmas
List.getElem?_concat_length : ∀ {α : Type u_1} {l : List α} {a : α}, (l ++ [a])[l.length]? = some a
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.bot_F : ∀ {α : Type u_1} (u : Unit), Filter.Realizer.bot.F.f u = ∅
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPullback.iso_inv_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G]
  [inst_3 : CategoryTheory.Limits.HasPullback f g] [inst_4 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
  {Z_1 : D} (h : G.obj X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).inv
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.fst f g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (G.map f) (G.map g)) h
-- Mathlib.RingTheory.Valuation.Basic
Valuation.ne_zero_iff : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀]
  (v : Valuation K Γ₀) {x : K}, v x ≠ 0 ↔ x ≠ 0
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_closure : ∀ {M : Type u_2} [inst : MulOneClass M] (s : Set Mᵐᵒᵖ),
  (Submonoid.closure s).unop = Submonoid.closure (MulOpposite.op ⁻¹' s)
-- Mathlib.Algebra.Group.Action.Sum
Sum.instSMulCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst_1 : SMul M β] [inst_2 : SMul N α]
  [inst_3 : SMul N β] [SMulCommClass M N α] [SMulCommClass M N β], SMulCommClass M N (α ⊕ β)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsClosedSubgraph.closed : ∀ {α : Type u_1} {β : Type u_2} {H G : Graph α β},
  H.IsClosedSubgraph G → ∀ ⦃e : β⦄ ⦃x : α⦄, G.Inc e x → x ∈ H.vertexSet → e ∈ H.edgeSet
-- Mathlib.Topology.Category.FinTopCat
/-- The forgetful functor to `FintypeCat`.  -/
FinTopCat.instHasForget₂ContinuousMapCarrierToTopFintypeCatFunObjFinite : CategoryTheory.HasForget₂ FinTopCat FintypeCat