mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.BifunctorHomotopy
HomologicalComplex.mapBifunctorMapHomotopy.comm₁ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6}
  [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} D] [inst_3 : CategoryTheory.Preadditive C₁]
  [inst_4 : CategoryTheory.Preadditive C₂] [inst_5 : CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁}
  {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁')
  {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [inst_8 : DecidableEq J]
  [inst_9 : TotalComplexShape c₁ c₂ c] [inst_10 : K₁.HasMapBifunctor K₂ F c] [inst_11 : L₁.HasMapBifunctor L₂ F c]
  (j : J),
  (HomologicalComplex.mapBifunctorMap f₁ f₂ F c).f j =
    CategoryTheory.CategoryStruct.comp ((K₁.mapBifunctor K₂ F c).d j (c.next j))
          (HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c (c.next j) j) +
        CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j (c.prev j))
          ((L₁.mapBifunctor L₂ F c).d (c.prev j) j) +
      (HomologicalComplex.mapBifunctorMap f₁' f₂ F c).f j
-- Mathlib.Algebra.Ring.Subsemiring.Defs
RingHom.eqLocusS_same : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S), f.eqLocusS f = ⊤
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ioo₀ : ∀ {G₀ : Type u_2} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {c : G₀} (a b : G₀),
  0 < c → (fun x => c * x) ⁻¹' Set.Ioo a b = Set.Ioo (a / c) (b / c)
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.μ_algSpec_left : ∀ {R : CommRingCat} (X Y : (CommAlgCat ↑R)ᵒᵖ),
  CategoryTheory.Over.Hom.left (CategoryTheory.Functor.LaxMonoidal.μ (AlgebraicGeometry.algSpec R) X Y) =
    (AlgebraicGeometry.pullbackSpecIso ↑R ↑(Opposite.unop X) ↑(Opposite.unop Y)).hom
-- Mathlib.Tactic.ProxyType
Mathlib.ProxyType.ProxyEquivConfig.mk.injEq : ∀ (proxyName proxyEquivName : Lean.Name)
  (mkCtorProxyType : List (Lean.Expr × Lean.Name) → Lean.Elab.TermElabM (Lean.Expr × Lean.Term))
  (mkProxyType :
    Array (Lean.Name × Lean.Expr × Lean.Term) →
      Lean.Elab.TermElabM (Lean.Expr × Array Lean.Term × Lean.TSyntax `tactic))
  (proxyName_1 proxyEquivName_1 : Lean.Name)
  (mkCtorProxyType_1 : List (Lean.Expr × Lean.Name) → Lean.Elab.TermElabM (Lean.Expr × Lean.Term))
  (mkProxyType_1 :
    Array (Lean.Name × Lean.Expr × Lean.Term) →
      Lean.Elab.TermElabM (Lean.Expr × Array Lean.Term × Lean.TSyntax `tactic)),
  ({ proxyName := proxyName, proxyEquivName := proxyEquivName, mkCtorProxyType := mkCtorProxyType,
        mkProxyType := mkProxyType } =
      { proxyName := proxyName_1, proxyEquivName := proxyEquivName_1, mkCtorProxyType := mkCtorProxyType_1,
        mkProxyType := mkProxyType_1 }) =
    (proxyName = proxyName_1 ∧
      proxyEquivName = proxyEquivName_1 ∧ mkCtorProxyType = mkCtorProxyType_1 ∧ mkProxyType = mkProxyType_1)
-- Mathlib.CategoryTheory.Presentable.Adjunction
CategoryTheory.Equivalence.hasCardinalFilteredGenerator : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (e : C ≌ D) (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular] [CategoryTheory.HasCardinalFilteredGenerator C κ],
  CategoryTheory.HasCardinalFilteredGenerator D κ
-- Lean.Meta.WHNF
/-- Eagerly unfold `dite` constants in `e`. This is an auxiliary function used to reduce match expressions.
See comment above.
 -/
_private.Lean.Meta.WHNF.0.Lean.Meta.unfoldNestedDIte : Lean.Expr → Lean.CoreM Lean.Expr
-- Lean.Meta.Tactic.Grind.Arith.CommRing.PP
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.PP.0.Lean.Meta.Grind.Arith.CommRing.ppRing? : Lean.Meta.Grind.Arith.CommRing.M✝ (Option Lean.MessageData)
-- Mathlib.FieldTheory.KummerExtension
AdjoinRootXPowSubCEquivToRootsOfUnity.eq_1 : ∀ {K : Type u} [inst : Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K}
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) [inst_1 : NeZero n]
  (σ : AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)),
  AdjoinRootXPowSubCEquivToRootsOfUnity hζ H σ =
    (rootsOfUnityEquivOfPrimitiveRoots ⋯ hζ).symm
      (rootsOfUnity.mkOfPowEq
        (if a = 0 then 1
        else
          σ (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)) / AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a))
        ⋯)
-- Init.Data.Int.DivMod.Lemmas
Int.le_mul_iff_le_right : ∀ {x y z : ℤ}, 0 < y → (x ≤ y * z ↔ (x + y - 1) / y ≤ z)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_span_singleton : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x y : M},
  x ∈ R ∙ y ↔ ∃ a, a • y = x
-- Mathlib.Algebra.Category.Ring.Under.Limits
CommRingCat.Under.equalizerFork_ι : ∀ {R : CommRingCat} {A B : CategoryTheory.Under R} (f g : A ⟶ B),
  (CommRingCat.Under.equalizerFork f g).ι = ((CommRingCat.toAlgHom f).equalizer (CommRingCat.toAlgHom g)).val.toUnder
-- Mathlib.Algebra.Order.Module.Defs
smul_le_smul_iff_of_pos_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [PosSMulMono α β] [PosSMulReflectLE α β], 0 < a → (a • b₁ ≤ a • b₂ ↔ b₁ ≤ b₂)
-- Init.Data.Array.Attach
Array.reverse_attachWith : ∀ {α : Type u_1} {P : α → Prop} {xs : Array α} {H : ∀ a ∈ xs, P a},
  (xs.attachWith P H).reverse = xs.reverse.attachWith P ⋯
-- Mathlib.Algebra.GroupWithZero.Invertible
Invertible.toNeZero : ∀ {α : Type u} [inst : MulZeroOneClass α] [Nontrivial α] (a : α) [Invertible a], NeZero a
-- Mathlib.Order.SuccPred.Basic
Order.Icc_succ_left : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Set.Icc (Order.succ a) b = Set.Ioc a b
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.eq_iff_le_carrier_eq : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {L₁ L₂ : IntermediateField.Lifts F E K},
  L₁ = L₂ ↔ L₁ ≤ L₂ ∧ L₁.carrier = L₂.carrier
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.inv_hom_apply : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} (e : M ≅ N) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Lean.Meta.DiscrTree.Main
/-- The discrimination tree ignores implicit arguments and proofs.
We use the following auxiliary id as a "mark".  -/
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.tmpMVarId : Lean.MVarId
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.orderedListIndicator : Lean.Doc.Parser.OrderedListType → Lean.Parser.ParserFn
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.codLift_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (f : M →ₛₗ[σ₁₂] M₂) {M₂' : Type u_10} [inst_6 : AddCommMonoid M₂'] [inst_7 : Module R₂ M₂'] (p : M₂' →ₗ[R₂] M₂)
  (hp : Function.Injective ⇑p) (h : ∀ (c : M), f c ∈ Set.range ⇑p) (x : M), (f.codLift p hp h) x = Exists.choose ⋯
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_iSup_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F},
  Function.Injective ⇑f → ∀ (S : ι → AddSubmonoid M), AddSubmonoid.comap f (⨆ i, AddSubmonoid.map f (S i)) = iSup S
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.δ_comp_σ_self : ∀ {n : ℕ} {i : Fin (n + 1)},
  CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i.castSucc) (SimplexCategoryGenRel.σ i) =
    CategoryTheory.CategoryStruct.id (SimplexCategoryGenRel.mk n)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.zpow_eq_one : ∀ {G : Type u_3} [inst : DivisionCommMonoid G] {k : ℕ} {ζ : G}, IsPrimitiveRoot ζ k → ζ ^ ↑k = 1
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_le_measure_union_right : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α}, μ t ≤ μ (s ∪ t)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.leadingCoeff_Φ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [Nontrivial R] (n : ℤ), (W.Φ n).leadingCoeff = 1
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.RwLemma.mk.inj : ∀ {name : Mathlib.Tactic.ClickSuggestions.Premise} {symm : Bool} {name_1 : Mathlib.Tactic.ClickSuggestions.Premise}
  {symm_1 : Bool}, { name := name, symm := symm } = { name := name_1, symm := symm_1 } → name = name_1 ∧ symm = symm_1
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue!_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited β] {f : α → β → Bool}
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      Std.Internal.List.getKey? k l = some k' →
        Std.Internal.List.getValue! k (List.filter (fun p => f p.fst p.snd) l) =
          (Option.filter (fun x => f k' x) (Std.Internal.List.getValue? k l)).get!
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInlayHintLabel : Lean.ToJson Lean.Lsp.InlayHintLabel
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- Builds a continuous linear equivalence from a continuous linear map on a finite-dimensional
vector space whose determinant is nonzero.  -/
ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero : {𝕜 : Type u} →
  [hnorm : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst : AddCommGroup E] →
        [inst_1 : Module 𝕜 E] →
          [inst_2 : TopologicalSpace E] →
            [IsTopologicalAddGroup E] →
              [ContinuousSMul 𝕜 E] →
                [CompleteSpace 𝕜] → [T2Space E] → [FiniteDimensional 𝕜 E] → (f : E →L[𝕜] E) → f.det ≠ 0 → E ≃L[𝕜] E
-- Mathlib.RingTheory.Filtration
/-- **Krull's intersection theorem** for Noetherian domains.  -/
Ideal.iInf_pow_eq_bot_of_isDomain : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [IsNoetherianRing R] [IsDomain R], I ≠ ⊤ → ⨅ i, I ^ i = ⊥
-- Mathlib.Order.UpperLower.Basic
isLowerSet_iff_forall_lt : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α}, IsLowerSet s ↔ ∀ ⦃a b : α⦄, b < a → a ∈ s → b ∈ s
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsAtomic.liftAt : ∀ {L : FirstOrder.Language} {α : Type u'} {l : ℕ} {φ : L.BoundedFormula α l} {k m : ℕ},
  φ.IsAtomic → (FirstOrder.Language.BoundedFormula.liftAt k m φ).IsAtomic
-- Mathlib.Data.Rat.Defs
Rat.mk'_mul_mk' : ∀ (n₁ n₂ : ℤ) (d₁ d₂ : ℕ) (hd₁ : d₁ ≠ 0) (hd₂ : d₂ ≠ 0) (hnd₁ : n₁.natAbs.Coprime d₁) (hnd₂ : n₂.natAbs.Coprime d₂)
  (h₁₂ : n₁.natAbs.Coprime d₂) (h₂₁ : n₂.natAbs.Coprime d₁),
  { num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ } * { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ } =
    { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }
-- Mathlib.Data.Finset.Sups
Finset.biUnion_image_inf_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] (s t : Finset α),
  (s.biUnion fun a => Finset.image (fun x => a ⊓ x) t) = s ⊼ t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.baseChange_dblY : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Projective R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).dblY (⇑f ∘ P) = f ((W'.baseChange A).dblY P)
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat
CategoryTheory.Pseudofunctor.mapComp'_hom_naturality : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (hfg : CategoryTheory.CategoryStruct.comp f g = fg) (a : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((F.map fg).toFunctor.map a) ((F.mapComp' f g fg hfg).hom.toNatTrans.app Y) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.toNatTrans.app X)
      ((F.map g).toFunctor.map ((F.map f).toFunctor.map a))
-- Mathlib.Analysis.Calculus.Deriv.Basic
differentiableWithinAt_of_derivWithin_ne_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, derivWithin f s x ≠ 0 → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- The resolvent is a unit when the argument is in the resolvent set.  -/
spectrum.isUnit_resolvent : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : A},
  r ∈ resolventSet R a ↔ IsUnit (resolvent a r)
-- Mathlib.Algebra.Category.Grp.Basic
/-- Build a `MulEquiv` from an isomorphism in the category `CommGrpCat`.  -/
CategoryTheory.Iso.commGroupIsoToMulEquiv : {X Y : CommGrpCat} → (X ≅ Y) → ↑X ≃* ↑Y
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.SplitKind.both.sizeOf_spec : sizeOf Lean.Meta.SplitKind.both = 1
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_inj : ∀ {M : Type u_2} [inst : Add M] {S T : AddSubsemigroup M}, S.op = T.op ↔ S = T
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X' X : CategoryTheory.SimplicialObject C} (f : X ⟶ X') {n : ℕ}
  (i : Fin (n + 2)),
  CategoryTheory.CategoryStruct.comp (X.δ i) (f.app (Opposite.op { len := n })) =
    CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n + 1 })) (X'.δ i)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RiiSliceData.range : {α : Type u} → {β : Type v} → Std.DTreeMap.Internal.Const.RiiSliceData α β → Std.Rii α
-- Mathlib.Topology.MetricSpace.Similarity
/-- A similarity pairwise scales non-negative distance. Forward direction of
`similar_iff_exists_pairwise_nndist_eq`.  -/
Similar.exists_pairwise_nndist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  Similar v₁ v₂ → ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ => nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)
-- Mathlib.Combinatorics.SetFamily.Compression.UV
UV.compress_self : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  (u a : α), UV.compress u u a = a
-- Mathlib.Order.Partition.Basic
Partition.coe_removeBot : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α] (P : Set α) (indep : sSupIndep P) (hsSup : sSup P = s),
  ↑(Partition.removeBot P indep hsSup) = P \ {⊥}
-- Init.Data.List.Lemmas
List.map_set : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {i : ℕ} {a : α},
  List.map f (l.set i a) = (List.map f l).set i (f a)
-- Mathlib.Order.Filter.Basic
Filter.inf_principal : ∀ {α : Type u} {s t : Set α}, Filter.principal s ⊓ Filter.principal t = Filter.principal (s ∩ t)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.mk.inj : ∀ {X : SSet} {A : X.Subcomplex} {I II : Set A.N} {inter : I ∩ II = ∅} {union : I ∪ II = Set.univ} {p : ↑II ≃ ↑I}
  {I_1 II_1 : Set A.N} {inter_1 : I_1 ∩ II_1 = ∅} {union_1 : I_1 ∪ II_1 = Set.univ} {p_1 : ↑II_1 ≃ ↑I_1},
  { I := I, II := II, inter := inter, union := union, p := p } =
      { I := I_1, II := II_1, inter := inter_1, union := union_1, p := p_1 } →
    I = I_1 ∧ II = II_1 ∧ p ≍ p_1
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.univ : ∀ {α : Type v} [inst : LinearOrder α], IsClub Set.univ
-- Init.Data.BitVec.Lemmas
BitVec.toInt_setWidth' : ∀ {m n : ℕ} (p : m ≤ n) {x : BitVec m}, (BitVec.setWidth' p x).toInt = if m = n then x.toInt else ↑x.toNat
-- Mathlib.Data.List.Sigma
List.Perm.kerase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)},
  l₁.NodupKeys → l₁.Perm l₂ → (List.kerase a l₁).Perm (List.kerase a l₂)
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_finVal : ∀ (n : Fin UInt8.size), UInt8.ofNatLT ↑n ⋯ = UInt8.ofFin n
-- Mathlib.RingTheory.TensorProduct.Free
Algebra.TensorProduct.basis.eq_1 : ∀ {R : Type u_1} (A : Type u_2) {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (b : Module.Basis ι R M),
  Algebra.TensorProduct.basis A b =
    {
      repr :=
        let __src := Algebra.TensorProduct.basisAux A b;
        { toAddHom := (↑__src).toAddHom, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ } }
-- Mathlib.Topology.MetricSpace.PiNat
/-- The map from the subset of `∀ i, Y i` to `X`.  -/
Metric.PiNatEmbed.ofPiNat : {ι : Type u_2} → {X : Type u_5} → {Y : ι → Type u_6} → {f : (i : ι) → X → Y i} → Metric.PiNatEmbed X Y f → X
-- Mathlib.Topology.UniformSpace.Defs
uniformity_lift_le_swap : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {g : SetRel α α → Filter β} {f : Filter β},
  Monotone g → ((uniformity α).lift fun s => g (Prod.swap ⁻¹' s)) ≤ f → (uniformity α).lift g ≤ f
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.odd_zsmul_antiperiodic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → ∀ (n : ℤ), Function.Antiperiodic f ((2 * n + 1) • c)
-- Mathlib.Order.Category.Preord
Preord.Iso.mk_inv : ∀ {α β : Preord} (e : ↑α ≃o ↑β), (Preord.Iso.mk e).inv = Preord.ofHom ↑e.symm
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.δ_μ : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.Monoidal] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
      (CategoryTheory.Functor.LaxMonoidal.μ F X Y) =
    CategoryTheory.CategoryStruct.id (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
-- Std.Time.Time.Unit.Second
Std.Time.Second.instReprOrdinal : {leap : Bool} → Repr (Std.Time.Second.Ordinal leap)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_norm_ofLp : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (f : WithLp ⊤ (α × β)), ‖f.ofLp‖ = ‖f‖
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.conjAut_pow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X) (n : ℕ),
  α.conjAut (f ^ n) = α.conjAut f ^ n
-- Mathlib.Order.LatticeIntervals
Set.Ioi.semilatticeSup : {α : Type u_1} → [inst : SemilatticeSup α] → {a : α} → SemilatticeSup ↑(Set.Ioi a)
-- Init.Data.Order.Lemmas
Std.le_of_eq : ∀ {α : Type u_1} [inst : LE α] [Std.Refl fun x1 x2 => x1 ≤ x2] {a b : α}, a = b → a ≤ b
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.zero_comp : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂),
  NormedAddGroupHom.comp 0 f = 0
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The monad for manipulating 2-morphisms in a monoidal category or bicategory.  -/
Mathlib.Tactic.BicategoryLike.CoherenceM : Type → Type → Type
-- Init.Data.SInt.Lemmas
Int32.toInt_bmod : ∀ (x : Int32), x.toInt.bmod 4294967296 = x.toInt
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `glue` which can be used in the absence of balance information but still
assumes the preconditions of `glue`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.glue! : {α : Type u} →
  {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Init.Grind.Ring.Envelope
_private.Init.Grind.Ring.Envelope.0.Lean.Grind.Ring.OfSemiring.r.match_1.eq_1 : ∀ (α : Type u_1) (motive : α × α → α × α → Sort u_2) (a b c d : α) (h_1 : (a b c d : α) → motive (a, b) (c, d)),
  (match (a, b), (c, d) with
    | (a, b), (c, d) => h_1 a b c d) =
    h_1 a b c d
-- Mathlib.Algebra.Group.Units.Defs
mul_divp_cancel : ∀ {α : Type u} [inst : Monoid α] (a : α) (u : αˣ), a * ↑u /ₚ u = a
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
/-- Basic data: `h i : Xₙ ⟶ Yₙ₊₁` for `i : Fin (n + 1)`.  -/
CategoryTheory.SimplicialObject.Homotopy.h : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : CategoryTheory.SimplicialObject C} →
      {f g : X ⟶ Y} →
        CategoryTheory.SimplicialObject.Homotopy f g →
          {n : ℕ} → Fin (n + 1) → (X.obj (Opposite.op { len := n }) ⟶ Y.obj (Opposite.op { len := n + 1 }))
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.mono'' : ∀ {α : Type u_1} {m₁ m₂ : MeasureTheory.OuterMeasure α} {s₁ s₂ : Set α}, m₁ ≤ m₂ → s₁ ⊆ s₂ → m₁ s₁ ≤ m₂ s₂
-- Lean.Parser.Term.Basic
Lean.Parser.Term.optType.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.cond_cond_eq_cond_inter' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s t : Set Ω},
  MeasurableSet s → MeasurableSet t → μ s ≠ ⊤ → μ[|s][|t] = μ[|s ∩ t]
-- Std.Http.Data.URI.Encoding
/-- Encodes a raw string into an encoded query parameter.
 -/
Std.Http.URI.EncodedQueryParam.encode : String → Std.Http.URI.EncodedQueryParam
-- Mathlib.Order.ModularLattice
IsUpperModularLattice.mk : ∀ {α : Type u_2} [inst : Lattice α], (∀ {a b : α}, a ⊓ b ⋖ a → b ⋖ a ⊔ b) → IsUpperModularLattice α
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.has_colimits_of_finite_and_filtered : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C]
  [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C],
  CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.dist_eq : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [IsometryClass F α β] (f : F) (x y : α), dist (f x) (f y) = dist x y
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.forget.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.AddGrp.forget C = (CategoryTheory.AddGrp.forget₂Mon C).comp (CategoryTheory.AddMon.forget C)
-- Mathlib.Data.List.Rotate
List.getElem?_rotate : ∀ {α : Type u} {l : List α} {n m : ℕ}, m < l.length → (l.rotate n)[m]? = l[(m + n) % l.length]?
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsMonHom.mul_hom_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M N : C}
  {inst_2 : CategoryTheory.MonObj M} {inst_3 : CategoryTheory.MonObj N} (f : M ⟶ N) [self : CategoryTheory.IsMonHom f]
  {Z : C} (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)
-- Init.Data.Option.Monadic
_private.Init.Data.Option.Monadic.0.Option.instDecidableEq.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (val : α) (h_1 : Unit → motive none)
  (h_2 : (val : α) → motive (some val)),
  (match some val with
    | none => h_1 ()
    | some val => h_2 val) =
    h_2 val
-- Mathlib.Topology.Algebra.Group.Basic
continuousOn_inv : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [ContinuousInv G] {s : Set G}, ContinuousOn Inv.inv s