mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.IterM.step_intermediateDropWhileWithPostcondition.match_1.splitter : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} →
      (out : β) →
        (motive : Subtype (P out).Property → Sort u_3) →
          (__do_lift : Subtype (P out).Property) →
            ((h'' : (P out).Property { down := true }) → motive ⟨{ down := true }, h''⟩) →
              ((h'' : (P out).Property { down := false }) → motive ⟨{ down := false }, h''⟩) → motive __do_lift
-- Mathlib.Data.Nat.Bitwise
/-- Note that the LHS is the expression used within `Std.BitVec.append`, hence the name.  -/
Nat.append_lt : ∀ {x y n m : ℕ}, x < 2 ^ n → y < 2 ^ m → y <<< n ||| x < 2 ^ (n + m)
-- Mathlib.Logic.Equiv.Set
Equiv.Set.sumDiffSubset_apply_inr : ∀ {α : Type u_3} {s t : Set α} (h : s ⊆ t) [inst : DecidablePred fun x => x ∈ s] (x : ↑(t \ s)),
  (Equiv.Set.sumDiffSubset h) (Sum.inr x) = Set.inclusion ⋯ x
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_empty : ∀ {α : Type u_1} (M : Matroid α), M.contract ∅ = M
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- Polynomial functions in are dense in `C(s, ℝ)` when `s` is compact.

See `polynomialFunctions_closure_eq_top` for the special case `s = Set.Icc a b` which does not use
the full Stone-Weierstrass theorem. Of course, that version could be used to prove this one as
well.  -/
polynomialFunctions.topologicalClosure : ∀ (s : Set ℝ) [inst : CompactSpace ↑s], (polynomialFunctions s).topologicalClosure = ⊤
-- Mathlib.LinearAlgebra.Complex.FiniteDimensional
FiniteDimensional.complexToReal : ∀ (E : Type u_1) [inst : AddCommGroup E] [inst_1 : Module ℂ E] [FiniteDimensional ℂ E], FiniteDimensional ℝ E
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.split.match_1.eq_1 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (pos : s.Pos)
  (h_1 : (pos_1 : s.Pos) → some pos = some pos_1 → motive (some pos_1)) (h_2 : some pos = none → motive none),
  (match hd : some pos with
    | some pos_1 => h_1 pos_1 hd
    | none => h_2 hd) =
    h_1 pos ⋯
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_map : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → γ} (it : Std.IterM m β),
  (Std.IterM.map f it).toListRev = (fun x => List.map f x) <$> it.toListRev
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.toList_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {f : α → β → Bool},
  m.WF → (Std.HashMap.Raw.filter f m).toList.Perm (List.filter (fun p => f p.1 p.2) m.toList)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.lift.eq_1 : ∀ {ι : Type u_1} {G : Type u_3} {H : Type u_4} [inst : Group G] [inst_1 : Group H] (b : FreeGroupBasis ι G),
  b.lift =
    FreeGroup.lift.trans
      { toFun := fun f => f.comp b.repr.toMonoidHom, invFun := fun f => f.comp b.repr.symm.toMonoidHom, left_inv := ⋯,
        right_inv := ⋯ }
-- Mathlib.Algebra.Homology.CochainComplexPlus
CochainComplex.plus_iff : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ), CochainComplex.plus C K ↔ ∃ n, K.IsStrictlyGE n
-- Mathlib.Order.Category.BoolAlg
BoolAlg.str : (self : BoolAlg) → BooleanAlgebra ↑self
-- Mathlib.Order.DirectedInverseSystem
/-- To define a binary function from the direct limit, it suffices to provide one binary function
from each component subject to a compatibility condition.  -/
DirectLimit.lift₂ : {ι : Type u_1} →
  [inst : Preorder ι] →
    {F₁ : ι → Type u_2} →
      {F₂ : ι → Type u_3} →
        {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} →
          (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) →
            [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)] →
              [inst_2 : DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] →
                {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7} →
                  (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) →
                    [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)] →
                      [inst_4 : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] →
                        [inst_5 : IsDirectedOrder ι] →
                          {C : Sort u_9} →
                            (ih : (i : ι) → F₁ i → F₂ i → C) →
                              (∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i),
                                  ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)) →
                                DirectLimit F₁ f₁ → DirectLimit F₂ f₂ → C
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.ofComplex_apply_eq_of_im_nonpos : ∀ {w w' : ℂ}, w.im ≤ 0 → w'.im ≤ 0 → ↑UpperHalfPlane.ofComplex w = ↑UpperHalfPlane.ofComplex w'
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.mulRec.match_1.splitter : (motive : ℕ → Sort u_1) → (s : ℕ) → (Unit → motive 0) → ((s : ℕ) → motive s.succ) → motive s
-- Mathlib.Data.Finset.Sort
Finset.range_orderEmbOfFin : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k), Set.range ⇑(s.orderEmbOfFin h) = ↑s
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.aestronglyMeasurable_traj : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {E : Type u_2} [inst_2 : NormedAddCommGroup E] {a b : ℕ},
  a ≤ b →
    ∀ {f : ((n : ℕ) → X n) → E} {x₀ : (i : ↥(Finset.Iic a)) → X ↑i},
      MeasureTheory.AEStronglyMeasurable f ((ProbabilityTheory.Kernel.traj κ a) x₀) →
        ∀ᵐ (x : (i : ↥(Finset.Iic b)) → X ↑i) ∂(ProbabilityTheory.Kernel.partialTraj κ a b) x₀,
          MeasureTheory.AEStronglyMeasurable f ((ProbabilityTheory.Kernel.traj κ b) x)
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- A functor `F : C ⥤ D` between monoidal categories is oplax monoidal if it is
equipped with morphisms `η : F.obj (𝟙_ C) ⟶ 𝟙 _D` and `δ X Y : F.obj (X ⊗ Y) ⟶ F.obj X ⊗ F.obj Y`,
satisfying the appropriate coherences.  -/
CategoryTheory.Functor.OplaxMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [CategoryTheory.MonoidalCategory D] → CategoryTheory.Functor C D → Type (max u₁ v₂)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.unop_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y P : C} (ι₁ : Opposite.op X ⟶ Opposite.op P)
  (ι₂ : Opposite.op Y ⟶ Opposite.op P),
  (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).unop = CategoryTheory.Limits.BinaryFan.mk ι₁.unop ι₂.unop
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallWithContext.mk : Lean.Syntax →
  ℕ →
    Array Lean.Expr →
      ℕ → Array Lean.Expr → Lean.Elab.WF.GuessLex.SavedLocalContext → Lean.Elab.WF.GuessLex.RecCallWithContext
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.lift_of_comp : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) (j : N →* P), f.lift ⋯ = j
-- Mathlib.Data.Finmap
/-- Given `l : List (Sigma β)`, create a term of type `Finmap β` by removing
entries with duplicate keys.  -/
List.toFinmap : {α : Type u} → {β : α → Type v} → [DecidableEq α] → List (Sigma β) → Finmap β
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
AlgebraicGeometry.IsSchemeTheoreticallyDominant.of_isPullback : ∀ {X Y Z S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {pX : Z ⟶ X} {pY : Z ⟶ Y},
  CategoryTheory.IsPullback pX pY f g →
    ∀ [AlgebraicGeometry.IsSchemeTheoreticallyDominant f] [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.Flat g],
      AlgebraicGeometry.IsSchemeTheoreticallyDominant pY
-- Mathlib.Algebra.Group.Equiv.Opposite
AddHom.op_symm_apply_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N] (f : Mᵃᵒᵖ →ₙ+ Nᵃᵒᵖ) (a : M),
  (AddHom.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a
-- Mathlib.CategoryTheory.GradedObject.Single
/-- The functor which sends `X : C` to the graded object which is `X` in degree `0`
and the initial object in nonzero degrees.  -/
CategoryTheory.GradedObject.single₀ : (J : Type u_1) →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [CategoryTheory.Limits.HasInitial C] →
        [DecidableEq J] → [Zero J] → CategoryTheory.Functor C (CategoryTheory.GradedObject J C)
-- Mathlib.Data.Complex.Basic
Complex.equivRealProdAddHom_apply : ∀ (z : ℂ), Complex.equivRealProdAddHom z = (z.re, z.im)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.forall_eq_iff_forall_eq : ∀ {R : Type u} [inst : Semiring R], (∀ (f g : Polynomial R), f = g) ↔ ∀ (a b : R), a = b
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.neg : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : Preorder E] [AddLeftMono E],
  MeasureTheory.Submartingale f ℱ μ → MeasureTheory.Supermartingale (-f) ℱ μ
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNormEssSup_indicator_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] (s : Set α) (f : α → ε),
  MeasureTheory.eLpNormEssSup (s.indicator f) μ ≤ MeasureTheory.eLpNormEssSup f μ
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.mk.sizeOf_spec : ∀ {ι : Type u_3} {M : Type u_4} [inst : AddCommMonoid M] {I : WithTop (BoxIntegral.Box ι)} [inst_1 : SizeOf ι]
  [inst_2 : SizeOf M] (toFun : BoxIntegral.Box ι → M)
  (sum_partition_boxes' :
    ∀ (J : BoxIntegral.Box ι),
      ↑J ≤ I → ∀ (π : BoxIntegral.Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, toFun Ji = toFun J),
  sizeOf { toFun := toFun, sum_partition_boxes' := sum_partition_boxes' } = 1
-- Mathlib.Data.List.Basic
List.filter_subset_self : ∀ {α : Type u} {p : α → Bool} (l : List α), List.filter p l ⊆ l
-- Lean.Meta.Tactic.Grind.Extension
/-- Similar to `guard`, but checks whether `e` is implied by asserting `¬e`.
 -/
Lean.Meta.Grind.EMatchTheoremConstraint.check : Lean.Expr → Lean.Meta.Grind.EMatchTheoremConstraint
-- Mathlib.Analysis.Meromorphic.Basic
/-- If `f` is meromorphic on a set, then so is its logarithmic derivative.  -/
MeromorphicOn.logDeriv : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} [CompleteSpace 𝕜'] {f : 𝕜 → 𝕜'} {hf : MeromorphicOn f U},
  MeromorphicOn (logDeriv f) U
-- Init.Data.List.Lemmas
List.map_congr_left : ∀ {α : Type u_1} {l : List α} {α_1 : Type u_2} {f g : α → α_1}, (∀ a ∈ l, f a = g a) → List.map f l = List.map g l
-- Init.Data.List.Basic
/-- Replaces the element at the given index, if it exists, with the result of applying `f` to it. If the
index is invalid, the list is returned unmodified.

Examples:
 * `[1, 2, 3].modify 0 (· * 10) = [10, 2, 3]`
 * `[1, 2, 3].modify 2 (· * 10) = [1, 2, 30]`
 * `[1, 2, 3].modify 3 (· * 10) = [1, 2, 3]`
 -/
List.modify : {α : Type u} → List α → ℕ → (α → α) → List α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp], ∅.maxKey? = none
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.monotone_defaultRatCDF : Monotone ProbabilityTheory.defaultRatCDF
-- Mathlib.Data.PNat.Interval
PNat.card_Ioc : ∀ (a b : ℕ+), (Finset.Ioc a b).card = ↑b - ↑a
-- Mathlib.Tactic.CategoryTheory.CheckCompositions
/-- Check the typing of categorical compositions in an expression.  -/
Mathlib.Tactic.CheckCompositions.checkCompositions : Lean.Expr → Lean.MetaM Unit
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.mk.inj : ∀ {M : Type u_10} {N : Type u_11} {inst : Add M} {inst_1 : Add N} {toFun : M → N}
  {map_add' : ∀ (x y : M), toFun (x + y) = toFun x + toFun y} {toFun_1 : M → N}
  {map_add'_1 : ∀ (x y : M), toFun_1 (x + y) = toFun_1 x + toFun_1 y},
  { toFun := toFun, map_add' := map_add' } = { toFun := toFun_1, map_add' := map_add'_1 } → toFun = toFun_1
-- Mathlib.Topology.Sheaves.Limits
TopCat.instHasLimitsOfShapeSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{v_1, w} J]
  [CategoryTheory.Limits.HasLimitsOfShape J C] (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape J (TopCat.Sheaf C X)
-- Mathlib.Analysis.Seminorm
/-- `SeminormClass F 𝕜 E` states that `F` is a type of seminorms on the `𝕜`-module `E`.

You should extend this class when you extend `Seminorm`.  -/
SeminormClass : (F : Type u_12) →
  (𝕜 : outParam (Type u_13)) →
    (E : outParam (Type u_14)) → [SeminormedRing 𝕜] → [AddGroup E] → [SMul 𝕜 E] → [FunLike F E ℝ] → Prop
-- Lean.Meta.CollectMVars
/-- Return metavariables occurring in the given expression. See `collectMVars`  -/
Lean.Meta.getMVars : Lean.Expr → Lean.MetaM (Array Lean.MVarId)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a b : α},
  (a == b) = true → Std.ExtDHashMap.Const.get? m a = Std.ExtDHashMap.Const.get? m b
-- Mathlib.Order.RelIso.Basic
RelHom.ext : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r →r s⦄, (∀ (x : α), f x = g x) → f = g
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.CategoryWithFibrations.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → HomotopicalAlgebra.CategoryWithFibrations C
-- Aesop.ElabM
Aesop.ElabM.Context.mk.injEq : ∀ (parsePriorities : Bool) (goal : Lean.MVarId) (parsePriorities_1 : Bool) (goal_1 : Lean.MVarId),
  ({ parsePriorities := parsePriorities, goal := goal } = { parsePriorities := parsePriorities_1, goal := goal_1 }) =
    (parsePriorities = parsePriorities_1 ∧ goal = goal_1)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.map_id : ∀ {X : Type u_1}, OnePoint.map id = id
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.degreeLT.eq_1 : ∀ (R : Type u) [inst : Semiring R] (n : ℕ), Polynomial.degreeLT R n = ⨅ k, ⨅ (_ : k ≥ n), (Polynomial.lcoeff R k).ker
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- If the action is pretransitive, then the trivial blocks condition implies preprimitivity
(based condition)  -/
MulAction.IsPreprimitive.of_isTrivialBlock_base : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [MulAction.IsPretransitive G X] (a : X),
  (∀ {B : Set X}, a ∈ B → MulAction.IsBlock G B → MulAction.IsTrivialBlock B) → MulAction.IsPreprimitive G X
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_obj_obj_obj : ∀ (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Functor J₁ C) (X_1 : CategoryTheory.Functor J₂ C)
  (X_2 : J₁) (X_3 : J₂),
  ((((CategoryTheory.MonoidalCategory.externalProductBifunctorCurried J₁ J₂ C).obj X).obj X_1).obj X_2).obj X_3 =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (X.obj X_2) (X_1.obj X_3)
-- Mathlib.Data.List.Infix
List.sublist_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α), l.Sublist (List.insert a l)
-- Batteries.Data.List.Lemmas
List.next?_nil : ∀ {α : Type u_1}, [].next? = none
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_of_Y_ne' : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 = Q 0 * P 2 →
            P 1 * Q 2 ≠ W.negY Q * P 2 →
              W.add P Q =
                W.dblZ P •
                  ![W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2)
                      (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                    W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2)
                      (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                    1]
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.prehaar.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] (K₀ U : Set G) (K : TopologicalSpace.Compacts G),
  MeasureTheory.Measure.haar.prehaar K₀ U K =
    ↑(MeasureTheory.Measure.haar.index (↑K) U) / ↑(MeasureTheory.Measure.haar.index K₀ U)
-- Init.Data.UInt.Bitwise
UInt64.xor_right_inj : ∀ {a b : UInt64} (c : UInt64), c ^^^ a = c ^^^ b ↔ a = b
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
NumberField.instIsTopologicalRingInfiniteAdeleRing : ∀ (K : Type u_1) [inst : Field K], IsTopologicalRing (NumberField.InfiniteAdeleRing K)
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.instCoeSortType : (R : Type u) → [inst : Semiring R] → CoeSort (SemimoduleCat R) (Type v)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_one : ∀ {α : Type u} [inst : One α], ↑1 = 1
-- Mathlib.Algebra.Torsor.Basic
/-- Dividing the point `p` by other points is an injective function.  -/
sdiv_right_injective : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (p : P), Function.Injective fun x => p /ₛ x
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
/-- If `f : X ⟶ Y` and `g : Y ⟶ Z` are composable morphisms,
then the cokernel of `φ f g : X ⊞ Y ⟶ Y ⊞ Z` identifies
to `cokernel (f ≫ g)`.  -/
CategoryTheory.kernelCokernelCompSequence.isColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y Z : C} →
        (f : X ⟶ Y) →
          (g : Y ⟶ Z) →
            CategoryTheory.Limits.IsColimit
              (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.kernelCokernelCompSequence.π f g) ⋯)
-- Mathlib.Data.Option.Basic
Option.pbind_eq_none : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {f : (a : α) → a ∈ x → Option β},
  (∀ (a : α) (H : a ∈ x), f a H = none → x = none) → (x.pbind f = none ↔ x = none)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instMonad : Monad FreeAddGroup
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.transEquiv_source : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (f' : β ≃ γ), (e.transEquiv f').source = e.source
-- Mathlib.FieldTheory.Relrank
/-- The `Nat` version of `IntermediateField.relrank`.
If `B / A ⊓ B` is an infinite extension, then it is zero.  -/
IntermediateField.relfinrank : {F : Type u} →
  {E : Type v} →
    [inst : Field F] → [inst_1 : Field E] → [inst_2 : Algebra F E] → IntermediateField F E → IntermediateField F E → ℕ
-- Mathlib.Topology.Order.OrderClosed
isOpen_Ioo : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {a b : α},
  IsOpen (Set.Ioo a b)
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.refl : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation.below ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.eq_2 : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) (val : Bool),
  Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig (Std.Tactic.BVDecide.BoolExpr.const val) cache =
    { result := ⟨{ aig := aig, ref := aig.mkConstCached val }, ⋯⟩, cache := cache }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_eq_getKeyD_default : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α}, m.getKey! a = m.getKeyD a default
-- Mathlib.Data.List.Basic
List.singleton_eq : ∀ {α : Type u} (x : α), {x} = [x]
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.ResultingUniverseResult.mk : Lean.Level → Option (Lean.LMVarId × Lean.Level) → Lean.Elab.Command.ResultingUniverseResult✝
-- Mathlib.Algebra.Group.Submonoid.Operations
MulEquiv.ofLeftInverse'.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) {g : N → M}
  (h : Function.LeftInverse g ⇑f),
  MulEquiv.ofLeftInverse' f h =
    { toFun := ⇑f.mrangeRestrict, invFun := g ∘ ⇑(MonoidHom.mrange f).subtype, left_inv := h, right_inv := ⋯,
      map_mul' := ⋯ }
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.PInfty_f_0 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C},
  AlgebraicTopology.DoldKan.PInfty.f 0 =
    CategoryTheory.CategoryStruct.id ((AlgebraicTopology.AlternatingFaceMapComplex.obj X).X 0)
-- Mathlib.Logic.Equiv.Prod
/-- `PEmpty` type is a left absorbing element for type product up to an equivalence.  -/
Equiv.pemptyProd : (α : Type u_9) → PEmpty.{u_10 + 1} × α ≃ PEmpty.{u_11}
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_cast : ∀ {w v k : ℕ} {x : BitVec w} {h : w = v}, BitVec.setWidth k (BitVec.cast h x) = BitVec.setWidth k x
-- Mathlib.Order.Cover
/-- An `iff` version of `CovBy.eq_or_eq` and `covBy_of_eq_or_eq`.  -/
covBy_iff_lt_and_eq_or_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⋖ b ↔ a < b ∧ ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.forget₂Group_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommGrpCat GrpCat)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The functor which sends `S : SnakeInput C` to its third line `S.L₃`.  -/
CategoryTheory.ShortComplex.SnakeInput.functorL₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) (CategoryTheory.ShortComplex C)
-- Mathlib.RepresentationTheory.Rep.Iso
Rep.counitIsoAddEquiv.eq_1 : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {M : ModuleCat (MonoidAlgebra k G)},
  Rep.counitIsoAddEquiv =
    id ((Representation.ofModule ↑M).asModuleEquiv.toAddEquiv.trans (RestrictScalars.addEquiv k (MonoidAlgebra k G) ↑M))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.Equiv t₂ → t₁.getD k fallback = t₂.getD k fallback
-- Mathlib.RingTheory.Coalgebra.Basic
DFinsupp.instIsCocomm : ∀ (R : Type u) (ι : Type v) (A : ι → Type w) [inst : DecidableEq ι] [inst_1 : CommSemiring R]
  [inst_2 : (i : ι) → AddCommMonoid (A i)] [inst_3 : (i : ι) → Module R (A i)] [inst_4 : (i : ι) → Coalgebra R (A i)]
  [∀ (i : ι), Coalgebra.IsCocomm R (A i)], Coalgebra.IsCocomm R (Π₀ (i : ι), A i)
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_left : ∀ {R : Type u} [inst : CommRing R] {M N P : Type u} [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P] [inst_7 : Coalgebra R M]
  [inst_8 : Coalgebra R N] [inst_9 : Coalgebra R P], CoalgebraStruct.counit = CoalgebraStruct.counit
-- Mathlib.Topology.Algebra.Monoid
MonoidHom.isClosed_range_coe : ∀ (M₁ : Type u_6) (M₂ : Type u_7) [inst : TopologicalSpace M₂] [T2Space M₂] [inst_2 : MulOneClass M₁]
  [inst_3 : MulOneClass M₂] [ContinuousMul M₂], IsClosed (Set.range DFunLike.coe)