mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.ofList_eq_insertMany_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)}, Std.ExtDHashMap.Const.ofList l = Std.ExtDHashMap.Const.insertMany ∅ l
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.elim.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr), sizeOf (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.elim c) = 1 + sizeOf c
-- Mathlib.Order.SuccPred.Basic
SuccOrder.ofSuccLeIff.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (succ : α → α) (hsucc_le_iff : ∀ {a b : α}, succ a ≤ b ↔ a < b),
  SuccOrder.ofSuccLeIff succ hsucc_le_iff = { succ := succ, le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- The level for 1-morphisms.  -/
Mathlib.Tactic.Bicategory.Context.level₁ : Mathlib.Tactic.Bicategory.Context → Lean.Level
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.isoMk_inv_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S}
  (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i))
  (w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreZeroHypercover.isoMk._auto_1)
  (a : F.I₀), (CategoryTheory.PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ a = s₀.symm a
-- Mathlib.Order.Lattice
toDual_min : ∀ {α : Type u} [inst : LinearOrder α] (a b : α),
  OrderDual.toDual (min a b) = max (OrderDual.toDual a) (OrderDual.toDual b)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.comp_eq_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A₀ A₁ A₂ : CategoryTheory.Endofunctor.Algebra F} (f : A₀ ⟶ A₁) (g : A₁ ⟶ A₂),
  CategoryTheory.Endofunctor.Algebra.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ofList_eq_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α},
  Std.ExtTreeSet.ofList l cmp = List.foldl (fun acc a => acc.insert a) ∅ l
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_braiding_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.CategoryStruct.comp (β_ Y X).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g f) h
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_neg_cancel_right : ∀ {α : Type u} [inst : SubtractionMonoid α] {b : α}, IsAddUnit b → ∀ (a : α), a + b + -b = a
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The naturality condition.  -/
CategoryTheory.Oplax.LaxTrans.Modification.naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (self : CategoryTheory.Oplax.LaxTrans.Modification η θ)
  {a b : B} (f : a ⟶ b),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.app a) (G.map f)) (θ.naturality f) =
    CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.app b))
-- Mathlib.Topology.Sheaves.Skyscraper
/-- The counit in `Presheaf.stalkFunctor ⊣ skyscraperPresheafFunctor`
 -/
StalkSkyscraperPresheafAdjunctionAuxs.counit : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          [inst_2 : CategoryTheory.Limits.HasTerminal C] →
            [inst_3 : CategoryTheory.Limits.HasColimits C] →
              (skyscraperPresheafFunctor p₀).comp (TopCat.Presheaf.stalkFunctor C p₀) ⟶ CategoryTheory.Functor.id C
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_div_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} (d : 𝕜'), deriv (fun x => c x / d) x = deriv c x / d
-- Mathlib.Order.KonigLemma
/-- A version of Kőnig's lemma where the sequence starts at the minimum of an infinite order.  -/
exists_orderEmbedding_covby_of_forall_covby_finite_of_bot : ∀ {α : Type u_1} [inst : PartialOrder α] [IsStronglyAtomic α] [inst_2 : OrderBot α] [Infinite α],
  (∀ (a : α), {x | a ⋖ x}.Finite) → ∃ f, f 0 = ⊥ ∧ ∀ (i : ℕ), f i ⋖ f (i + 1)
-- Batteries.Data.List.Basic
/-- Optimized version of `sections`.  -/
List.sectionsTR : {α : Type u_1} → List (List α) → List (List α)
-- Mathlib.Data.EReal.Basic
/-- The canonical map from nonnegative extended reals to extended reals.  -/
ENNReal.toEReal : ENNReal → EReal
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.preLeft_obj_hom : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma (F.comp L) R),
  ((CategoryTheory.Comma.preLeft F L R).obj X).hom = X.hom
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.addCommGroup : {α : Type u} → [CommGroup α] → AddCommGroup (Additive α)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.Adj.left_triangle_components_assoc : ∀ {C₁ C₂ : CategoryTheory.Bicategory.Adj CategoryTheory.Cat} (α : C₁ ⟶ C₂) (X : ↑C₁.obj) {Z : ↑C₂.obj}
  (h : (CategoryTheory.CategoryStruct.id C₂.obj).toFunctor.obj (α.l.toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.l.toFunctor.map (α.adj.unit.toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp (α.adj.counit.toNatTrans.app (α.l.toFunctor.obj X)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (α.l.toFunctor.obj X)) h
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- An embedding into a normed division ring defines a place of `K`  -/
NumberField.place : {K : Type u_1} → [inst : Field K] → {A : Type u_2} → [inst_1 : NormedDivisionRing A] → (K →+* A) → AbsoluteValue K ℝ
-- Mathlib.Analysis.Fourier.AddCircle
/-- **Parseval's identity**: for a function `f` which is square integrable on `(a,b]`,
the sum of the squared norms of the Fourier coefficients equals the `L²` norm of `f`.  -/
hasSum_sq_fourierCoeffOn : ∀ {a b : ℝ} {f : ℝ → ℂ} (hab : a < b),
  MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Set.Ioc a b)) →
    HasSum (fun i => ‖fourierCoeffOn hab f i‖ ^ 2) ((b - a)⁻¹ • ∫ (x : ℝ) in a..b, ‖f x‖ ^ 2)
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If `g` and `h` commute, then `g` fixes `h +ᵥ x` iff `g` fixes `x`.
This is equivalent to say that the set `fixedBy α g` is fixed by `h`.  -/
AddAction.fixedBy_mem_fixedBy_of_addCommute : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g h : G},
  AddCommute g h → AddAction.fixedBy α g ∈ AddAction.fixedBy (Set α) h
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.HoRel₂.of_compStruct : ∀ {V : SSet.Truncated 2}
  {x₀ x₁ x₂ : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
  (h : e₀₁.CompStruct e₁₂ e₀₂),
  SSet.OneTruncation₂.HoRel₂ V
    ((CategoryTheory.Cat.FreeRefl.quotientFunctor (SSet.OneTruncation₂ V)).map
      (CategoryTheory.CategoryStruct.comp (Quiver.Hom.toPath e₀₁) (Quiver.Hom.toPath e₁₂)))
    ((CategoryTheory.Cat.FreeRefl.quotientFunctor (SSet.OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₂))
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.filter.pi.match_1.eq_1 : ∀ {n : ℕ} {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj] {r t t' : ℕ} (K : G.CompleteEquipartiteSubgraph r t')
  (motive : ↥(SimpleGraph.ErdosStone.filter✝ K t) → Sort u_1) (val : Fin n)
  (h : val ∈ SimpleGraph.ErdosStone.filter✝ K t)
  (h_1 : (val : Fin n) → (h : val ∈ SimpleGraph.ErdosStone.filter✝ K t) → motive ⟨val, h⟩),
  (match ⟨val, h⟩ with
    | ⟨val, h⟩ => h_1 val h) =
    h_1 val h
-- Mathlib.Topology.LocallyClosed
coborder.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), coborder s = (closure s \ s)ᶜ
-- Mathlib.Order.Partition.Finpartition
/-- We say that `P ≤ Q` if `P` refines `Q`: each part of `P` is less than some part of `Q`.  -/
Finpartition.instLE : {α : Type u_1} → [inst : Lattice α] → [inst_1 : OrderBot α] → {a : α} → LE (Finpartition a)
-- Mathlib.Data.Set.Lattice
/-- **Alias** of `Set.iInter_ofPred`. -/
Set.iInter_setOf : ∀ {α : Type u_1} {ι : Sort u_5} (P : ι → α → Prop), ⋂ i, {x | P i x} = {x | ∀ (i : ι), P i x}
-- Init.Data.Array.Monadic
/-- Variant of `filterM_toArray` with a side condition for the stop position.  -/
List.filterM_toArray' : ∀ {m : Type → Type u_1} {α : Type} {stop : ℕ} [inst : Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool},
  stop = l.length → Array.filterM p l.toArray 0 stop = List.toArray <$> List.filterM p l
-- Mathlib.Logic.Relation
Std.Symm.iff : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r] (x y : α), r x y ↔ r y x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.toList_keysArray_eq_keys : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β), (↑m).keysArray.toList = (↑m).keys
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.hasBasis_totalLengthFilter : ∀ {X : Type u_1} [inst : PseudoMetricSpace X],
  AbsolutelyContinuousOnInterval.totalLengthFilter.HasBasis (fun ε => 0 < ε) fun ε =>
    {E | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε}
-- Lean.Elab.Match
Lean.Elab.Term.instInhabitedDiscr.default : Lean.Elab.Term.Discr
-- Mathlib.Algebra.BigOperators.Fin
/-- Let `(g₀, g₁, ..., gₙ)` be a tuple of elements in `Gⁿ⁺¹`.
Then if `k < j`, this says `(g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ = gₖ`.
If `k = j`, it says `(g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ₊₁ = gₖgₖ₊₁`.
If `k > j`, it says `(g₀g₁...gₖ)⁻¹ * g₀g₁...gₖ₊₁ = gₖ₊₁.`
Useful for defining group cohomology.  -/
Fin.inv_partialProd_mul_eq_contractNth : ∀ {n : ℕ} {G : Type u_3} [inst : Group G] (g : Fin (n + 1) → G) (j : Fin (n + 1)) (k : Fin n),
  (Fin.partialProd g (j.succ.succAbove k.castSucc))⁻¹ * Fin.partialProd g (j.succAbove k).succ =
    j.contractNth (fun x1 x2 => x1 * x2) g k
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.isoOfEq_inv_ι : ∀ (X : AlgebraicGeometry.Scheme) {U V : X.Opens} (e : U = V),
  CategoryTheory.CategoryStruct.comp (X.isoOfEq e).inv U.ι = V.ι
-- Lean.Elab.Tactic.Omega.Frontend
_private.Lean.Elab.Tactic.Omega.Frontend.0.Lean.Elab.Tactic.Omega.formatErrorMessage.varNameOf : ℕ → String
-- Mathlib.Logic.Function.Basic
Function.sometimes_spec : ∀ {p : Prop} {α : Sort u_1} [inst : Nonempty α] (P : α → Prop) (f : p → α) (a : p), P (f a) → P (Function.sometimes f)
-- Mathlib.RingTheory.FractionalIdeal.Operations
IsFractional.map : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] (g : P →ₐ[R] P') {I : Submodule R P},
  IsFractional S I → IsFractional S (Submodule.map g.toLinearMap I)
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.ofComposition_parts : ∀ (n : ℕ) (c : Composition n), (Nat.Partition.ofComposition n c).parts = ↑c.blocks
-- Init.Conv
/-- Performs one step of "congruence", which takes a term and produces
subgoals for all the function arguments. For example, if the target is `f x y` then
`congr` produces two subgoals, one for `x` and one for `y`.  -/
Lean.Parser.Tactic.Conv.congr : Lean.ParserDescr
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.ClientInfo.mk.sizeOf_spec : ∀ (name : String) (version? : Option String),
  sizeOf { name := name, version? := version? } = 1 + sizeOf name + sizeOf version?
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
/-- The AM–GM inequality for two `NNReal`s, with means in canonical form.  -/
NNReal.sqrt_mul_le_half_add : ∀ (x y : NNReal), NNReal.sqrt (x * y) ≤ (x + y) / 2
-- Mathlib.LinearAlgebra.Determinant
LinearEquiv.ofIsUnitDet.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] {ι : Type u_4} {inst_5 : DecidableEq ι} [inst_6 : DecidableEq ι]
  [inst_7 : Fintype ι] {f f_1 : M →ₗ[R] M'} (e_f : f = f_1) {v v_1 : Module.Basis ι R M} (e_v : v = v_1)
  {v' v'_1 : Module.Basis ι R M'} (e_v' : v' = v'_1) (h : IsUnit ((LinearMap.toMatrix v v') f).det),
  LinearEquiv.ofIsUnitDet h = LinearEquiv.ofIsUnitDet ⋯
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.mul_iUnion : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Mul α] (s : Set α) (t : ι → Set α), s * ⋃ i, t i = ⋃ i, s * t i
-- Mathlib.Data.Finset.Empty
Finset.instEmptyCollection : {α : Type u_1} → EmptyCollection (Finset α)
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextEdit.mk.injEq : ∀ (range : Lean.Lsp.Range) (newText : String) (leanExtSnippet? : Option Lean.Lsp.SnippetString)
  (annotationId? : Option String) (range_1 : Lean.Lsp.Range) (newText_1 : String)
  (leanExtSnippet?_1 : Option Lean.Lsp.SnippetString) (annotationId?_1 : Option String),
  ({ range := range, newText := newText, leanExtSnippet? := leanExtSnippet?, annotationId? := annotationId? } =
      { range := range_1, newText := newText_1, leanExtSnippet? := leanExtSnippet?_1,
        annotationId? := annotationId?_1 }) =
    (range = range_1 ∧ newText = newText_1 ∧ leanExtSnippet? = leanExtSnippet?_1 ∧ annotationId? = annotationId?_1)
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearEquiv.map_eq_of_mem_fixingSubgroup : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_3} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] (e : V ≃ₗ[R] V)
  (W : Submodule R V), e ∈ fixingSubgroup (V ≃ₗ[R] V) W.carrier → Submodule.map (↑e) W = W
-- Mathlib.Algebra.Group.Nat.Hom
MonoidHom.ext_mnat_iff : ∀ {M : Type u_1} [inst : Monoid M] {f g : Multiplicative ℕ →* M},
  f = g ↔ f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.equiv_apply : ∀ (X : Type u_3) (x : FundamentalGroupoid X), (FundamentalGroupoid.equiv X) x = x.as
-- Init.Grind.Ring.Field
Lean.Grind.Field.noNatZeroDivisors.ofIsCharPZero : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0], Lean.Grind.NoNatZeroDivisors α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKey ⋯ =
    t.minKey?.elim k fun k' => if compare k k' = Ordering.lt then k else k'
-- Mathlib.Logic.Equiv.Fin.Basic
Fin.succFunEquiv_symm_apply : ∀ (α : Type u_1) (n : ℕ) (a : (Fin n → α) × α) (a_1 : Fin (n + 1)),
  (Fin.succFunEquiv α n).symm a a_1 = Fin.append a.1 (uniqueElim a.2) a_1
-- Mathlib.Order.Disjointed
disjointed_le : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : Preorder ι]
  [inst_2 : LocallyFiniteOrderBot ι] (f : ι → α), disjointed f ≤ f
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₁₂Functor_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)),
  CategoryTheory.bifunctorComp₁₂Functor.obj F₁₂ = CategoryTheory.bifunctorComp₁₂FunctorObj F₁₂
-- Mathlib.Data.ENNReal.Basic
ENNReal.iInf_coe_eq_top : ∀ {ι : Sort u_2} {f : ι → NNReal}, ⨅ i, ↑(f i) = ⊤ ↔ IsEmpty ι
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_union' : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  Disjoint s₁ s₂ →
    MeasurableSet s₁ →
      autoParam (μ s₁ ≠ ⊤) MeasureTheory.measureReal_union'._auto_1 →
        autoParam (μ s₂ ≠ ⊤) MeasureTheory.measureReal_union'._auto_3 → μ.real (s₁ ∪ s₂) = μ.real s₁ + μ.real s₂
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.baseAction : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} → MulAction H (Monoid.PushoutI.NormalWord d)
-- Mathlib.Data.Matrix.Basic
Matrix.diag_list_sum : ∀ {n : Type u_3} {α : Type u_11} [inst : AddMonoid α] (l : List (Matrix n n α)),
  l.sum.diag = (List.map Matrix.diag l).sum
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.coe_pow : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] (x : ↑(Set.Icc 0 1)) (n : ℕ),
  ↑(x ^ n) = ↑x ^ n
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.shortExact_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂), S₁.ShortExact → S₂.ShortExact
-- Mathlib.Data.SetLike.Basic
/-- membership is inherited from `Set X`  -/
SetLike.instSubtypeSet : {X : Type u_3} → {p : Set X → Prop} → SetLike { s // p s } X
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.anyM_filterMapM : ∀ {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : MonadLiftT m n] [inst_3 : Monad m] [LawfulMonad m] [inst_5 : Monad n]
  [inst_6 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] {it : Std.IterM m β} {f : β → n (Option β')}
  {p : β' → n (ULift.{w, 0} Bool)},
  Std.IterM.anyM p (Std.IterM.filterMapM f it) =
    Std.IterM.anyM
      (fun x => do
        let __do_lift ← f x
        match __do_lift with
          | some fx => p fx
          | none => pure { down := false })
      (Std.IterM.mapM pure it)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.associativity_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C))
  (m₁ m₂ m₃ : M) (X : C) [inst_3 : F.LaxMonoidal] {Z : C}
  (h :
    (F.obj
            (CategoryTheory.MonoidalCategoryStruct.tensorObj m₁
              (CategoryTheory.MonoidalCategoryStruct.tensorObj m₂ m₃))).obj
        X ⟶
      Z),
  CategoryTheory.CategoryStruct.comp ((F.obj m₃).map ((CategoryTheory.Functor.LaxMonoidal.μ F m₁ m₂).app X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X)
        (CategoryTheory.CategoryStruct.comp
          ((F.map (CategoryTheory.MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X) h)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.LaxMonoidal.μ F m₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj m₂ m₃)).app X) h)
-- Std.Do.SPred.Notation
/-- Unexpander that reconstructs `spred(... ↔ ...)⌝` syntax from applications of `SPred.iff`, lifting
nested applications of `spred(...)` from the arguments.
 -/
Std.Do.SPred.Notation.unexpandIff : Lean.PrettyPrinter.Unexpander
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.algebraLeft : {S : Type u_2} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {R : Type u_3} →
        (T : Type u_4) →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring T] → [Algebra R T] → (v : AbsoluteValue R S) → Algebra (WithAbs v) T
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R], MonoidAlgebra.coeff 0 = 0
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The family of arrows of the image of a subgroupoid under a functor injective on objects  -/
CategoryTheory.Subgroupoid.Map.Arrows : {C : Type u} →
  [inst : CategoryTheory.Groupoid C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Groupoid D] →
        (φ : CategoryTheory.Functor C D) →
          Function.Injective φ.obj → CategoryTheory.Subgroupoid C → (c d : D) → (c ⟶ d) → Prop
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRic.decEq : {α : Type u_1} → [DecidableEq α] → (x x_1 : Std.Ric α) → Decidable (x = x_1)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeProd.match_1.eq_1 : ∀ {m n : ℕ} (motive : Fin m × Fin n → Sort u_1) (i : Fin m) (j : Fin n)
  (h_1 : (i : Fin m) → (j : Fin n) → motive (i, j)),
  (match (i, j) with
    | (i, j) => h_1 i j) =
    h_1 i j
-- Mathlib.Topology.Category.Locale
topToLocale_map : ∀ {X Y : TopCat} (f : X ⟶ Y), topToLocale.map f = (Frm.ofHom (TopologicalSpace.Opens.comap (TopCat.Hom.hom f))).op
-- Mathlib.Logic.Equiv.Fin.Basic
/-- `Fin (n + 1) → α` and `(Fin n → α) × α` are equivalent.  -/
Fin.succFunEquiv : (α : Type u_1) → (n : ℕ) → (Fin (n + 1) → α) ≃ (Fin n → α) × α
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indepSet_self' : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μα : MeasureTheory.Measure α},
  (∀ᵐ (a : α) ∂μα, MeasureTheory.IsFiniteMeasure (κ a)) →
    ∀ {t : Set Ω}, ProbabilityTheory.Kernel.IndepSet t t κ μα → ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- Two non-unital subrings are equal if they have the same elements.  -/
NonUnitalSubring.ext : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {S T : NonUnitalSubring R}, (∀ (x : R), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.mulAntidiagonal.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s t : Set α}
  (hs : s.IsPWO) (ht : t.IsPWO) (a : α), Finset.mulAntidiagonal hs ht a = ⋯.toFinset
-- Mathlib.Topology.Order
gc_coinduced_induced : ∀ {α : Type u_1} {β : Type u_2} (f : α → β),
  GaloisConnection (TopologicalSpace.coinduced f) (TopologicalSpace.induced f)
-- Mathlib.Logic.Equiv.Defs
Equiv.coe_fn_mk : ∀ {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : Function.LeftInverse g f) (r : Function.RightInverse g f),
  ⇑{ toFun := f, invFun := g, left_inv := l, right_inv := r } = f
-- Mathlib.Analysis.Meromorphic.Divisor
/-- The divisor of a constant function is `0`.
 -/
MeromorphicOn.divisor_natCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} (n : ℕ), MeromorphicOn.divisor (↑n) U = 0
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.op_iSup : ∀ {ι : Sort u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : ι → Subalgebra R A), (iSup S).op = ⨆ i, (S i).op
-- Init.Data.Bool
Bool.or' : Bool → Bool → Bool
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsReflection.isLeftInversion_mul_right_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W},
  cs.IsReflection t → ∀ {w : W}, cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t