mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_iff_forall_eventually_mem : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β},
  Filter.Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, ∀ᶠ (x : α) in l₁, f x ∈ s
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.nu_lt_one_of_dvd_prodPrimes : ∀ {s : BoundingSieve} {d : ℕ}, d ∣ s.prodPrimes → d ≠ 1 → s.nu d < 1
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.altitudeFoot_mem_altitude : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.altitudeFoot i ∈ s.altitude i
-- Mathlib.LinearAlgebra.Matrix.Ideal
Ideal.matrix_top : ∀ {R : Type u_1} [inst : Semiring R] (n : Type u_2) [inst_1 : Fintype n] [inst_2 : DecidableEq n], Ideal.matrix n ⊤ = ⊤
-- Init.Data.BitVec.Lemmas
BitVec.rotateRight.eq_1 : ∀ {w : ℕ} (x : BitVec w) (n : ℕ), x.rotateRight n = x.rotateRightAux (n % w)
-- Mathlib.Algebra.Regular.Basic
/-- A unit in a monoid is regular.  -/
IsUnit.isRegular : ∀ {R : Type u_1} [inst : Monoid R] {a : R}, IsUnit a → IsRegular a
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.instInhabitedLoogleMatch : Inhabited LeanSearchClient.LoogleMatch
-- Mathlib.Order.SuccPred.CompleteLinearOrder
IsGLB.exists_of_nonempty_of_not_isPredLimit : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α} {x : α},
  IsGLB (Set.range f) x → ¬Order.IsPredLimit x → ∃ i, f i = x
-- Mathlib.Geometry.Euclidean.Volume.Measure
Submodule.measurableEquivProd.congr_simp : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MetricSpace P]
  [inst_6 : MeasurableSpace P] [inst_7 : BorelSpace P] [inst_8 : NormedAddTorsor V P] (s : Submodule ℝ V) (p p_1 : P),
  p = p_1 → s.measurableEquivProd p = s.measurableEquivProd p_1
-- Mathlib.MeasureTheory.Integral.Indicator
/-- If `μ` is a finite measure and the indicators of measurable sets `Aᵢ` tend pointwise
almost everywhere to the indicator of a measurable set `A`, then the measures `μ Aᵢ` tend to
the measure `μ A`.  -/
MeasureTheory.tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] {A : Set α} {ι : Type u_2} (L : Filter ι) [L.IsCountablyGenerated]
  {As : ι → Set α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ],
  MeasurableSet A →
    (∀ (i : ι), MeasurableSet (As i)) →
      (∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) → Filter.Tendsto (fun i => μ (As i)) L (nhds (μ A))
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instMulOneClass : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [MulOneClass M] → MulOneClass (l.Germ M)
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.quotDualCoannihilatorToDual_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (W : Submodule R (Module.Dual R M)), Function.Injective ⇑W.quotDualCoannihilatorToDual
-- Mathlib.Logic.Relation
Relation.EqvGen.below : {α : Type u_1} →
  {r : α → α → Prop} →
    {motive : (a a_1 : α) → Relation.EqvGen r a a_1 → Prop} → {a a_1 : α} → Relation.EqvGen r a a_1 → Prop
-- Mathlib.Data.Complex.Basic
Complex.instInv : Inv ℂ
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.div_eq_one_iff_eq : ∀ {α : Type u} [inst : DivisionMonoid α] {a b : α}, IsUnit b → (a / b = 1 ↔ a = b)
-- Std.Http.Data.URI.Basic
/-- Extracts the authority component from a request target, if available.
 -/
Std.Http.RequestTarget.authority? : Std.Http.RequestTarget → Option Std.Http.URI.Authority
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.center_le_centralizer : ∀ {R : Type u_1} [inst : Ring R] (s : Set R), Subring.center R ≤ Subring.centralizer s
-- Init.Control.Lawful.Instances
instLawfulMonadExcept : ∀ {ε : Type u_1}, LawfulMonad (Except ε)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.tprod_finset_bUnion_disjoint : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [T2Space α]
  [ContinuousMul α] {ι : Type u_4} {s : Finset ι} {t : ι → Set β},
  (↑s).Pairwise (Function.onFun Disjoint t) →
    (∀ i ∈ s, Multipliable (f ∘ Subtype.val)) → ∏' (x : ↑(⋃ i ∈ s, t i)), f ↑x = ∏ i ∈ s, ∏' (x : ↑(t i)), f ↑x
-- Mathlib.Topology.Connected.LocallyPathConnected
coe_connectedComponentsEquivZerothHomotopy_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LocallyPathConnectedSpace X],
  ⇑connectedComponentsEquivZerothHomotopy.symm = ZerothHomotopy.toConnectedComponents
-- Mathlib.Order.Hom.Lattice
InfHom.comp.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Min α] [inst_1 : Min β] [inst_2 : Min γ] (f : InfHom β γ)
  (g : InfHom α β), f.comp g = { toFun := ⇑f ∘ ⇑g, map_inf' := ⋯ }
-- Init.Data.SInt.IntToBitVec
ISize.eq_iff_toBitVec64_eq : ∀ {a b : ISize} (h : System.Platform.numBits = 64), a = b ↔ a.toBitVec64 h = b.toBitVec64 h
-- Init.Prelude
/-- Congruence in both function and argument. If `f₁ = f₂` and `a₁ = a₂` then
`f₁ a₁ = f₂ a₂`. This only works for nondependent functions; the theorem
statement is more complex in the dependent case.

For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
congr : ∀ {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α}, f₁ = f₂ → a₁ = a₂ → f₁ a₁ = f₂ a₂
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
/-- If `F` preserves the initial object and binary coproducts, then it preserves products indexed by
`Fin n` for any `n`.
 -/
CategoryTheory.preserves_fin_of_preserves_binary_and_initial : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F]
  [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) (f : Fin n → C),
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) F
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Mathlib.Tactic.Bicategory.of_normalize_eq : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g f' : a ⟶ b} {η θ : f ≅ g}
  (η_f : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ≅ f')
  (η_g : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g ≅ f'),
  CategoryTheory.Bicategory.whiskerLeftIso (CategoryTheory.CategoryStruct.id a) η ≪≫ η_g = η_f →
    CategoryTheory.Bicategory.whiskerLeftIso (CategoryTheory.CategoryStruct.id a) θ ≪≫ η_g = η_f → η = θ
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of types,
where `G` is locally-full and cover-dense, and `ℱ, ℱ'` are sheaves,
we may obtain a natural isomorphism between presheaves.
 -/
CategoryTheory.Functor.IsCoverDense.Types.presheafIso : {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] →
        {K : CategoryTheory.GrothendieckTopology D} →
          {G : CategoryTheory.Functor C D} →
            [G.IsCoverDense K] →
              [G.IsLocallyFull K] →
                {ℱ ℱ' : CategoryTheory.Sheaf K (Type v)} → (G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) → (ℱ.obj ≅ ℱ'.obj)
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Meta.Grind.Params.eraseEMatchCore : Lean.Meta.Grind.Params → Lean.Name → Lean.Meta.Grind.Params
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RiiSliceData : Type u → Type u
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instNeg : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Ring R] →
          [inst_1 : (i : ι) → AddCommGroup (M₁ i)] →
            [inst_2 : AddCommGroup M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] → [IsTopologicalAddGroup M₂] → Neg (ContinuousMultilinearMap R M₁ M₂)
-- Mathlib.Order.InitialSeg
InitialSeg.subsingleton_of_trichotomous_of_irrefl : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Trichotomous s] [Std.Irrefl s]
  [IsWellFounded α r], Subsingleton (InitialSeg r s)
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The Fourier transform from `L1` functions to bounded continuous functions.  -/
Real.Lp.fourierTransform : {V : Type u_1} →
  {E : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℂ E] →
        [inst_2 : NormedAddCommGroup V] →
          [inst_3 : InnerProductSpace ℝ V] →
            [inst_4 : MeasurableSpace V] →
              [inst_5 : BorelSpace V] →
                [inst_6 : FiniteDimensional ℝ V] →
                  ↥(MeasureTheory.Lp E 1 MeasureTheory.volume) → BoundedContinuousFunction V E
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofHasKernel_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [inst_2 : CategoryTheory.Limits.HasKernel S.g],
  (CategoryTheory.ShortComplex.HomologyData.ofHasKernel S hf).iso =
    CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernel S hf).H
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.isInvertible_fderiv_prodFun : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  (fderiv 𝕜 φ.prodFun φ.pt).IsInvertible
-- Std.Internal.UV.System
Std.Internal.UV.System.GroupInfo.mk.inj : ∀ {groupname : String} {gid : UInt64} {members : Array String} {groupname_1 : String} {gid_1 : UInt64}
  {members_1 : Array String},
  { groupname := groupname, gid := gid, members := members } =
      { groupname := groupname_1, gid := gid_1, members := members_1 } →
    groupname = groupname_1 ∧ gid = gid_1 ∧ members = members_1
-- Lean.Server.ServerTask
Lean.Server.ServerTask.EIO.asTask : {ε α : Type} → EIO ε α → BaseIO (Lean.Server.ServerTask (Except ε α))
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_inv_comp_d_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₁ : ι}
  (h : p₂ = p₁) (p₃ : ι) {Z : V} (h_1 : K.X p₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv (CategoryTheory.CategoryStruct.comp (K.d p₂ p₃) h_1) =
    CategoryTheory.CategoryStruct.comp (K.d p₁ p₃) h_1
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.uliftNatTransOfLe_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S T : CategoryTheory.Sieve X} (h : S ≤ T),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.uliftNatTransOfLe h) T.uliftFunctorInclusion =
    S.uliftFunctorInclusion
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.generateFrom_iInter_toPlots : ∀ {X : Type u_1} {ι : Type u_2} (D : ι → DiffeologicalSpace X),
  DiffeologicalSpace.generateFrom (⋂ i, (D i).toPlots) = ⨅ i, D i
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_one_fst_sub_single_one_fst_mem_boundaries₂ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g h : G) (a : ↑A),
  ((fun₀ | (1, g * h) => a) - fun₀ | (1, g) => a) ∈ groupHomology.boundaries₂ A
-- Lean.Util.InstantiateLevelParams
/-- Instantiate universe level parameters names `paramNames` with `lvls` in `e`.
If the two lists have different length, the smallest one is used.
(Does not preserve expression sharing.)
 -/
Lean.Expr.instantiateLevelParamsNoCache : Lean.Expr → List Lean.Name → List Lean.Level → Lean.Expr
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_div_comm : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] (a b : α), |a / b|ₘ = |b / a|ₘ
-- Std.Data.HashMap.Lemmas
Std.HashMap.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, List.find? (fun x_2 => x_2.1 == k) m.toList = none ↔ k ∉ m
-- Mathlib.Order.Comparable
CompRel.refl : ∀ {α : Type u_1} (r : α → α → Prop) [Std.Refl r] (a : α), CompRel r a a
-- Mathlib.CategoryTheory.SmallObject.Basic
CategoryTheory.MorphismProperty.smallObjectκ_isRegular : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C)
  [inst_1 : I.HasSmallObjectArgument], Fact I.smallObjectκ.IsRegular
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_iUnion_congr : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i) ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.mapA.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₁_id_comp_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C)
  (x : ↥(groupHomology.cycles₁ A)),
  (CategoryTheory.ConcreteCategory.hom
        (groupHomology.mapCycles₁ (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ)))
      x =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₁ (MonoidHom.id G) ψ))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₁ (MonoidHom.id G) φ)) x)
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.matches'.match_1.splitter : {α : Type u_1} →
  (motive : RegularExpression α → Sort u_2) →
    (x : RegularExpression α) →
      (Unit → motive RegularExpression.zero) →
        (Unit → motive RegularExpression.epsilon) →
          ((a : α) → motive (RegularExpression.char a)) →
            ((P Q : RegularExpression α) → motive (P.plus Q)) →
              ((P Q : RegularExpression α) → motive (P.comp Q)) → ((P : RegularExpression α) → motive P.star) → motive x
-- Lean.Util.ReplaceLevel
Lean.Expr.ReplaceLevelImpl.State.results : Lean.Expr.ReplaceLevelImpl.State → Array Lean.Expr
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
/-- **Alias** of the reverse direction of `Set.finite_inv`. -/
Set.Finite.inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α}, s.Finite → s⁻¹.Finite
-- Mathlib.Order.Closure
ClosureOperator.IsClosed.closure_eq : ∀ {α : Type u_1} [inst : Preorder α] {c : ClosureOperator α} {x : α}, c.IsClosed x → c x = x
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instOrdDiagnosticTag : Ord Lean.Lsp.DiagnosticTag
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- The isomorphism giving rise to the oplax functoriality constraint  -/
CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F : CategoryTheory.OplaxFunctor B C} →
          F.PseudoCore →
            {a b c : B} →
              (f : a ⟶ b) →
                (g : b ⟶ c) →
                  F.map (CategoryTheory.CategoryStruct.comp f g) ≅
                    CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)
-- Mathlib.Algebra.DirectSum.Basic
/-- A direct sum over an empty type is trivial.  -/
DirectSum.uniqueOfIsEmpty : {ι : Type v} →
  {β : ι → Type w} → [inst : (i : ι) → AddCommMonoid (β i)] → [IsEmpty ι] → Unique (DirectSum ι fun i => β i)
-- Batteries.Data.List.Lemmas
List.getElem_swap_left : ∀ {α : Type u_1} {xs : List α} {i j : ℕ} (hi : i < (xs.swap i j).length),
  (xs.swap i j)[i] = if hj : j < xs.length then xs[j] else xs[i]
-- Mathlib.Analysis.Normed.Affine.AsymptoticCone
/-- In a finite dimensional normed affine space over `ℝ`, a set is bounded if and only if its
asymptotic cone is trivial.  -/
isBounded_iff_asymptoticCone_subset_singleton : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [FiniteDimensional ℝ V] {s : Set P}, Bornology.IsBounded s ↔ asymptoticCone ℝ s ⊆ {0}
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.sqFrom_id : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C₁ : HomologicalComplex V c) (i : ι),
  HomologicalComplex.Hom.sqFrom (CategoryTheory.CategoryStruct.id C₁) i =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk (C₁.dFrom i))
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.mem_disjUnion : ∀ {α : Type u_1} {n m : ℕ} {s : ↑(Set.powersetCard α m)} {t : ↑(Set.powersetCard α n)} {hst : Disjoint ↑s ↑t} {a : α},
  a ∈ Set.powersetCard.disjUnion hst ↔ a ∈ s ∨ a ∈ t
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.mkHom.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g}
  (k k_1 : s.pt ⟶ t.pt) (e_k : k = k_1) (w : CategoryTheory.CategoryStruct.comp k t.ι = s.ι),
  CategoryTheory.Limits.Fork.mkHom k w = CategoryTheory.Limits.Fork.mkHom k_1 ⋯
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.monadMap_ReaderT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ρ : Type u} [Monad m] [inst : Std.Do.WP m ps]
  (f : {β : Type u} → m β → m β) {α : Type u} (x : ReaderT ρ m α) (Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ ps)),
  ⦃fun s => (Std.Do.wp (f (x.run s))).apply (fun a => Q.1 a s, Q.2)⦄ MonadFunctor.monadMap (fun {β} => f) x ⦃Q⦄
-- Mathlib.CategoryTheory.Monad.Algebra
/-- Composition of Eilenberg–Moore algebra homomorphisms.  -/
CategoryTheory.Monad.Algebra.Hom.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} → {P Q R : T.Algebra} → P.Hom Q → Q.Hom R → P.Hom R
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.iteratedDeriv_even_sin : ∀ (n : ℕ), iteratedDeriv (2 * n) Complex.sin = (-1) ^ n * Complex.sin
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.functorToCore_comp_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : Type u₂} [inst_1 : CategoryTheory.Groupoid G]
  {C' : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} C'] (H : CategoryTheory.Functor G C)
  (F : CategoryTheory.Functor C C'),
  CategoryTheory.Core.functorToCore (H.comp F) = (CategoryTheory.Core.functorToCore H).comp F.core
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_neg : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] (m : M) (r : R),
  AddMonoidAlgebra.single m (-r) = -AddMonoidAlgebra.single m r
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.prod_eq_one_iff : ∀ {α : Type u_2} [inst : CommMonoid α] {m : Multiset α} [inst_1 : PartialOrder α] [CanonicallyOrderedMul α]
  [IsOrderedMonoid α], m.prod = 1 ↔ ∀ x ∈ m, x = 1
-- Lean.Meta.Tactic.Grind.EMatchTheoremPtr
Lean.Meta.Grind.EMatchTheoremPtr.thm : Lean.Meta.Grind.EMatchTheoremPtr → Lean.Meta.Grind.EMatchTheorem
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.assignments : {numVarsSucc : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula numVarsSucc → Array Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Batteries.Recycling.RBTree.Basic
/-- A `RBNode.Path α` is a "cursor" into an `RBNode` which represents the path
from the root to a subtree. Note that the path goes from the target subtree
up to the root, which is reversed from the normal way data is stored in the tree.
See [Zipper](https://en.wikipedia.org/wiki/Zipper_(data_structure)) for more information.
 -/
RBTree.RBNode.Path : Type u → Type u
-- Mathlib.Topology.Bases
/-- A countable topological basis of `α`.  -/
TopologicalSpace.countableBasis : (α : Type u) → [t : TopologicalSpace α] → [SecondCountableTopology α] → Set (Set α)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.abs_floor_sub_le : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R] {a : R},
  0 ≤ a → |↑⌊a⌋₊ - a| ≤ 1
-- Mathlib.Data.Fintype.Basic
Fin.univ_image_def : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (f : Fin n → α), Finset.image f Finset.univ = (List.ofFn f).toFinset
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- The isomorphism between the coproduct of `X.toFun` and the object `X` itself.  -/
CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X : CategoryTheory.Limits.FormalCoproduct C) → ∐ X.toFun ≅ X
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.coe_injective : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S},
  Function.Injective DFunLike.coe
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_inv_natCast_pow : ∀ {x : ℝ} {n : ℕ}, 0 ≤ x → n ≠ 0 → (x ^ (↑n)⁻¹) ^ n = x
-- Mathlib.Data.NNReal.Basic
NNReal.toReal_ne : ∀ (a b : NNReal), a ≠ b ↔ ↑a ≠ ↑b
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.liftAux.smul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {f : M →ₗ[R] N →ₗ[R] P} (r : R) (x : TensorProduct R M N),
  (TensorProduct.liftAux f) (r • x) = r • (TensorProduct.liftAux f) x
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.mk.congr_simp : ∀ {α : Type u_5} {β : Type u_6} (toFun toFun_1 : α → β) (e_toFun : toFun = toFun_1) (invFun invFun_1 : β → α)
  (e_invFun : invFun = invFun_1) (source source_1 : Set α) (e_source : source = source_1) (target target_1 : Set β)
  (e_target : target = target_1) (map_source' : ∀ ⦃x : α⦄, x ∈ source → toFun x ∈ target)
  (map_target' : ∀ ⦃x : β⦄, x ∈ target → invFun x ∈ source) (left_inv' : ∀ ⦃x : α⦄, x ∈ source → invFun (toFun x) = x)
  (right_inv' : ∀ ⦃x : β⦄, x ∈ target → toFun (invFun x) = x),
  { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
      map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' } =
    { toFun := toFun_1, invFun := invFun_1, source := source_1, target := target_1, map_source' := ⋯, map_target' := ⋯,
      left_inv' := ⋯, right_inv' := ⋯ }
-- Mathlib.Algebra.Module.ZMod
AddMonoidHom.toZModLinearMap_injective : ∀ (n : ℕ) {M : Type u_1} {M₁ : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₁] [inst_2 : Module (ZMod n) M]
  [inst_3 : Module (ZMod n) M₁], Function.Injective (AddMonoidHom.toZModLinearMap n)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.mk.inj : ∀ {ι : 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 φ} {toWord : Monoid.CoprodI.Word G} {head : H}
  {normalized : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ toWord.toList → g ∈ d.set i} {toWord_1 : Monoid.CoprodI.Word G}
  {head_1 : H} {normalized_1 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ toWord_1.toList → g ∈ d.set i},
  { toWord := toWord, head := head, normalized := normalized } =
      { toWord := toWord_1, head := head_1, normalized := normalized_1 } →
    toWord = toWord_1 ∧ head = head_1