mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.Adj.counit_naturality : ∀ {C₁ C₂ : CategoryTheory.Bicategory.Adj CategoryTheory.Cat} (α : C₁ ⟶ C₂) {X Y : ↑C₂.obj} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (α.l.toFunctor.map (α.r.toFunctor.map f)) (α.adj.counit.toNatTrans.app Y) =
    CategoryTheory.CategoryStruct.comp (α.adj.counit.toNatTrans.app X) f
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.ground_apply : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₚₗ[R] N) (m : M),
  f.ground m = (TensorProduct.lid R N) (f.toFun' R (1 ⊗ₜ[R] m))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.left.sizeOf_spec : sizeOf CategoryTheory.Limits.WalkingPair.left = 1
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.instBEqPoly.beq.match_1.eq_3 : ∀ (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Sort u_1) (x x_1 : Lean.Grind.CommRing.Poly)
  (h_1 : (a b : ℤ) → motive (Lean.Grind.CommRing.Poly.num a) (Lean.Grind.CommRing.Poly.num b))
  (h_2 :
    (a : ℤ) →
      (a_1 : Lean.Grind.CommRing.Mon) →
        (a_2 : Lean.Grind.CommRing.Poly) →
          (b : ℤ) →
            (b_1 : Lean.Grind.CommRing.Mon) →
              (b_2 : Lean.Grind.CommRing.Poly) →
                motive (Lean.Grind.CommRing.Poly.add a a_1 a_2) (Lean.Grind.CommRing.Poly.add b b_1 b_2))
  (h_3 : (x x_2 : Lean.Grind.CommRing.Poly) → motive x x_2),
  (∀ (a b : ℤ), x = Lean.Grind.CommRing.Poly.num a → x_1 = Lean.Grind.CommRing.Poly.num b → False) →
    (∀ (a : ℤ) (a_1 : Lean.Grind.CommRing.Mon) (a_2 : Lean.Grind.CommRing.Poly) (b : ℤ) (b_1 : Lean.Grind.CommRing.Mon)
        (b_2 : Lean.Grind.CommRing.Poly),
        x = Lean.Grind.CommRing.Poly.add a a_1 a_2 → x_1 = Lean.Grind.CommRing.Poly.add b b_1 b_2 → False) →
      (match x, x_1 with
        | Lean.Grind.CommRing.Poly.num a, Lean.Grind.CommRing.Poly.num b => h_1 a b
        | Lean.Grind.CommRing.Poly.add a a_1 a_2, Lean.Grind.CommRing.Poly.add b b_1 b_2 => h_2 a a_1 a_2 b b_1 b_2
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.preComp_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasImage g]
  [inst_2 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)] {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.preComp f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) h
-- Init.Data.List.Erase
List.Nodup.eraseIdx : ∀ {α : Type u_1} {l : List α} (k : ℕ), l.Nodup → (l.eraseIdx k).Nodup
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.univ : ∀ {α : Type u_1} {m : MeasurableSpace α}, MeasurableSet Set.univ
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mem_stabilizer_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a : α} {g : G},
  g ∈ AddAction.stabilizer G a ↔ g +ᵥ a = a
-- Mathlib.Order.UpperLower.Basic
OrderEmbedding.image_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β),
  IsUpperSet (Set.range ⇑e) → ∀ (a : α), ⇑e '' Set.Ici a = Set.Ici (e a)
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.instCategory.eq_1 : AddCommMonCat.instCategory =
  { Hom := fun X Y => X.Hom Y, id := fun X => { hom' := AddMonoidHom.id ↑X },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @AddCommMonCat.instCategory._proof_1,
    comp_id := @AddCommMonCat.instCategory._proof_2, assoc := @AddCommMonCat.instCategory._proof_3 }
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.range_eq_bot_iff : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] {f : G →+ G'}, f.range = ⊥ ↔ f = 0
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.toEssImage_map_hom : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y), (F.toEssImage.map f).hom = F.map f
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.instCategory.eq_1 : FiniteGrp.instCategory =
  { Hom := FiniteGrp.instCategory._aux_1, id := FiniteGrp.instCategory._aux_3, comp := @FiniteGrp.instCategory._aux_5,
    id_comp := @FiniteGrp.instCategory._proof_7, comp_id := @FiniteGrp.instCategory._proof_8,
    assoc := @FiniteGrp.instCategory._proof_9 }
-- Init.PropLemmas
exists_or_eq_imp' : ∀ {α : Sort u_1} {p q : α → Prop} {a' : α}, (∃ a, (q a ∨ a' = a) ∧ p a) ↔ (∃ a, q a ∧ p a) ∨ p a'
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.toCoalgebraStruct : {R : Type u} →
  {A : Type v} →
    {inst : CommSemiring R} →
      {inst_1 : AddCommMonoid A} → {inst_2 : Module R A} → [self : Coalgebra R A] → CoalgebraStruct R A
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.isPlausibleIndirectOutput_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {it : Std.Iter α} {out : α},
  it.IsPlausibleIndirectOutput out ↔ ∃ n, (it.internalState.next.bind fun x => Std.PRange.succMany? n x) = some out
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.instOne.eq_1 : ∀ (M : Type u_4) [inst : MulOne M], Monoid.End.instOne M = { one := MonoidHom.id M }
-- Init.Data.Bool
Bool.cond_false_right : ∀ (c t : Bool), (bif c then t else false) = (c && t)
-- Mathlib.Analysis.Calculus.ContDiff.Basic
ftaylorSeries_fun_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F],
  (ftaylorSeries 𝕜 fun x => 0) = 0
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.instEpiHomologyπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology], CategoryTheory.Epi S.homologyπ
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.nilpotencyClass_le_of_ker_le_center`. -/
nilpotencyClass_le_of_ker_le_center : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (f : G →* H),
  f.ker ≤ Subgroup.center G → ∀ [Group.IsNilpotent H], Group.nilpotencyClass G ≤ Group.nilpotencyClass H + 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_diff! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_contains : Std.DTreeMap.Internal.Impl.contains k (m₁.diff! m₂) = true},
  Std.DTreeMap.Internal.Impl.Const.get (m₁.diff! m₂) k h_contains = Std.DTreeMap.Internal.Impl.Const.get m₁ k ⋯
-- Mathlib.GroupTheory.IndexNSmul
/-- The index of the image of the multiplication-by-`n` map on an additive group `M` that is free
and finitely generated as a `ℤ`-module is `n ^ finrank ℤ M`.  -/
AddSubgroup.index_range_nsmul : ∀ (M : Type u_1) [inst : AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (n : ℕ),
  (nsmulAddMonoidHom n).range.index = n ^ Module.finrank ℤ M
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.Equivalence.prun_liftInner_step : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} {n : Type u_1 → Type u_3} {γ : Type u_1}
  [inst : Std.Iterator α m β] [inst_1 : Monad m] [inst_2 : Monad n] [inst_3 : MonadLiftT m n] [LawfulMonad m]
  [LawfulMonad n] [LawfulMonadLiftT m n] {it : Std.IterM m β}
  {f : (step : Std.IterStep (Std.IterM m β) β) → (Std.Iterators.HetT.liftInner n it.stepAsHetT).Property step → n γ},
  (Std.Iterators.HetT.liftInner n it.stepAsHetT).prun f = do
    let step ← liftM it.step
    f ↑step.inflate ⋯
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.mul_scaleRoots' : ∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) (r : R),
  p.leadingCoeff * q.leadingCoeff ≠ 0 → (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.sumPiEquivProdPi_symm_apply : ∀ (R : Type u_9) [inst : Semiring R] (S : Type u_10) (T : Type u_11) (A : S ⊕ T → Type u_12)
  [inst_1 : (st : S ⊕ T) → AddCommMonoid (A st)] [inst_2 : (st : S ⊕ T) → Module R (A st)],
  ⇑(LinearEquiv.sumPiEquivProdPi R S T A).symm = ⇑(Equiv.sumPiEquivProdPi A).symm
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_embDomain : ∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {v : α →₀ M}
  {f : α ↪ β} {g : β → M → N}, (Finsupp.embDomain f v).prod g = v.prod fun a b => g (f a) b
-- Mathlib.Data.Nat.Factors
Nat.dvd_of_primeFactorsList_subperm : ∀ {a b : ℕ}, a ≠ 0 → a.primeFactorsList.Subperm b.primeFactorsList → a ∣ b
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.instEpiGCokernelSequenceE : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  CategoryTheory.Epi (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k k' fallback : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
          k ∈ List.map Sigma.fst l → (↑(m.insertMany l)).getKeyD k' fallback = k
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.applySMulCommClass' : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : ContinuousAdd M₁], SMulCommClass (M₁ →L[R₁] M₁) R₁ M₁
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.map_target : ∀ {X : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] {f : Equidecomp X G} {x : X},
  x ∈ f.target → ↑f.symm.toPartialEquiv x ∈ f.source
-- Mathlib.Logic.Relation
Relation.EqvGen.reflGen_le_eqvGen : ∀ {α : Type u_1} (r : α → α → Prop), Relation.ReflGen r ≤ Relation.EqvGen r
-- Mathlib.Tactic.Sat.FromLRAT
/-- `v.satisfies c` asserts that clause `c` satisfied by the valuation.
It is written in a negative way: A clause like `a ∨ ¬b ∨ c` is rewritten as
`¬a → b → ¬c → False`, so we are asserting that it is not the case that
all literals in the clause are falsified.  -/
Sat.Valuation.satisfies : Sat.Valuation → Sat.Clause → Prop
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isNonloop_iff : ∀ {α : Type u_1} (M : Matroid α) (e : α), M.IsNonloop e ↔ ¬M.IsLoop e ∧ e ∈ M.E
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g)
  (p : ↥(AlgebraicGeometry.Spec T.tensor)),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap T.SpecTensorTo p))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.ofPointTensor (T.SpecTensorTo p)))
        (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯).hom)) =
    (AlgebraicGeometry.Spec T.tensor).fromSpecResidueField p
-- Mathlib.RingTheory.PrincipalIdealDomain
Submodule.IsPrincipal.generator_bot : ∀ {R : Type u} {M : Type v} [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M],
  Submodule.IsPrincipal.generator ⊥ = 0
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Context.mk.sizeOf_spec : ∀ (instName : Lean.Name) (typeInfos : Array Lean.InductiveVal) (auxFunNames : Array Lean.Name) (usePartial : Bool),
  sizeOf { instName := instName, typeInfos := typeInfos, auxFunNames := auxFunNames, usePartial := usePartial } =
    1 + sizeOf instName + sizeOf typeInfos + sizeOf auxFunNames + sizeOf usePartial
-- Lean.ImportingFlag
_private.Lean.ImportingFlag.0.Lean.runInitializersRef : IO.Ref Bool
-- Lean.PrettyPrinter
_private.Lean.PrettyPrinter.0.Lean.PrettyPrinter.noContext : Lean.MessageData → Lean.MessageData
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_sub_right : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ)
  (f g₁ g₂ : (i : ι) → E i), ⟪f, g₁ - g₂⟫_[𝕜, w] = ⟪f, g₁⟫_[𝕜, w] - ⟪f, g₂⟫_[𝕜, w]
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.canonicalEmbedding.mem_span_latticeBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {x : (K →+* ℂ) → ℂ},
  x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.canonicalEmbedding.latticeBasis K)) ↔
    x ∈ ((NumberField.canonicalEmbedding K).comp (algebraMap (NumberField.RingOfIntegers K) K)).range
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_mul_monomial : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R] (n m : ℕ) (r s : R),
  (SkewPolynomial.monomial n) r * (SkewPolynomial.monomial m) s =
    (SkewPolynomial.monomial (n + m)) (r * (⇑SkewPolynomial.φ)^[n] s)
-- Std.Internal.UV.System
Std.Internal.UV.System.instReprGroupInfo.repr : Std.Internal.UV.System.GroupInfo → ℕ → Std.Format
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_prefix.sizeOf_spec : ∀ (lhs : Bool) (s : Lean.Grind.AC.Seq) (c₁ : Lean.Meta.Grind.AC.EqCnstr) (c₂ : Lean.Meta.Grind.AC.DiseqCnstr),
  sizeOf (Lean.Meta.Grind.AC.DiseqCnstrProof.simp_prefix lhs s c₁ c₂) =
    1 + sizeOf lhs + sizeOf s + sizeOf c₁ + sizeOf c₂
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.NatTrans.hcomp_eq_whiskerLeft_comp_whiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D}
  {H K : CategoryTheory.Functor D E} (α : F ⟶ G) (β : H ⟶ K),
  α ◫ β = CategoryTheory.CategoryStruct.comp (F.whiskerLeft β) (CategoryTheory.Functor.whiskerRight α K)
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcOptions.mk : Option Lean.Lsp.HighlightMatchesOptions → Option Lean.Lsp.RpcWireFormat → Lean.Lsp.RpcOptions
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.instReflBoundedFormula : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ}, Std.Refl T.Iff
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.pos_eq_of_eq_right : ∀ {s : String.Slice} {p q : s.Pos} {s_1 s' t : String}, p.Splits s_1 t → q.Splits s' t → p = q
-- Init.Data.Vector.OfFn
_private.Init.Data.Vector.OfFn.0.Vector.ofFnM_go_succ : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {i : ℕ} {xs : Array α} {n : ℕ} [inst : Monad m] [LawfulMonad m]
  {f : Fin (n + 1) → m α} (hi : autoParam (i ≤ n) Vector.ofFnM_go_succ._auto_5✝) {h : xs.size = i},
  Vector.ofFnM.go✝ f i ⋯ xs h = do
    let as ← Vector.ofFnM.go✝ (fun i => f i.castSucc) i hi xs h
    let a ← f (Fin.last n)
    pure (as.push a)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_le_size_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List ((a : α) × β a)}, t.size ≤ (t.insertMany l).size
-- Mathlib.Order.Interval.Set.Monotone
StrictMonoOn.Ici_le_id : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] [OrderTop α] {n : α} {φ : α → α},
  StrictMonoOn φ (Set.Ici n) → ∀ (m : α), n ≤ m → φ m ≤ m
-- Mathlib.Algebra.Opposites
MulOpposite.instInvolutiveInv : {α : Type u_1} → [InvolutiveInv α] → InvolutiveInv αᵐᵒᵖ
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_int32ToBitVec : ∀ (x : Int32), Int8.ofBitVec (BitVec.signExtend 8 x.toBitVec) = x.toInt8
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.boundedBy_eq_ofFunction : ∀ {α : Type u_1} {m : Set α → ENNReal} (m_empty : m ∅ = 0) (s : Set α),
  (MeasureTheory.OuterMeasure.boundedBy m) s = (MeasureTheory.OuterMeasure.ofFunction m m_empty) s
-- Mathlib.Order.SuccPred.Limit
Order.not_isPredLimit_of_noMin : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : PredOrder α] [IsPredArchimedean α] [NoMinOrder α],
  ¬Order.IsPredLimit a
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.reduce_of_pos : ∀ {m : ℤ} {A : FixedDetMatrix (Fin 2) ℤ m},
  ↑A 1 0 = 0 → 0 < ↑A 0 0 → FixedDetMatrices.reduce A = ModularGroup.T ^ (-(↑A 0 1 / ↑A 1 1)) • A
-- Mathlib.Order.Concept
Concept.mk : {α : Type u_2} →
  {β : Type u_3} →
    {r : α → β → Prop} →
      (extent : Set α) → (intent : Set β) → upperPolar r extent = intent → lowerPolar r intent = extent → Concept α β r
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (t.insertMany l).getKey? k' = some k
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.levyProkhorovEDist.eq_1 : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] (μ ν : MeasureTheory.Measure Ω),
  MeasureTheory.levyProkhorovEDist μ ν =
    sInf
      {ε |
        ∀ (B : Set Ω),
          MeasurableSet B → μ B ≤ ν (Metric.thickening ε.toReal B) + ε ∧ ν B ≤ μ (Metric.thickening ε.toReal B) + ε}
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.mul_congr : ∀ {R : Type u_1} [inst : CommSemiring R] {a a' b b' c : R}, a = a' → b = b' → a' * b' = c → a * b = c
-- Aesop.Util.UnionFind
_private.Aesop.Util.UnionFind.0.Aesop.UnionFind.findRep : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → USize → Aesop.UnionFind α → USize × Aesop.UnionFind α
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.congr_arg : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) {x y : ι → M}, x = y → f x = f y
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyEntourage_empty : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X}, Dynamics.coverEntropyEntourage T ∅ U = ⊥
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsGreatest.nnnorm_cfc_nnreal : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A] [inst_3 : PartialOrder A]
  [inst_4 : StarOrderedRing A] [inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_6 : NonnegSpectrumClass ℝ A] [Nontrivial A] (f : NNReal → NNReal) (a : A),
  autoParam (ContinuousOn f (spectrum NNReal a)) IsGreatest.nnnorm_cfc_nnreal._auto_1 →
    autoParam (0 ≤ a) IsGreatest.nnnorm_cfc_nnreal._auto_3 → IsGreatest (f '' spectrum NNReal a) ‖cfc f a‖₊
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.dest_corec : ∀ {P : PFunctor.{uA, uB}} {α : Type u_2} (g : α → ↑P α) (x : α),
  (PFunctor.M.corec g x).dest = P.map (PFunctor.M.corec g) (g x)
-- Init.Prelude
Monad.toApplicative : {m : Type u → Type v} → [self : Monad m] → Applicative m
-- Mathlib.GroupTheory.Congruence.BigOperators
/-- **Alias** of `Con.finsetProd`.

---

Multiplicative congruence relations preserve finite product.  -/
Con.finset_prod : ∀ {ι : Type u_1} {M : Type u_2} [inst : CommMonoid M] (c : Con M) (s : Finset ι) {f g : ι → M},
  (∀ i ∈ s, c (f i) (g i)) → c (s.prod f) (s.prod g)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_empty : ∀ {α : Type u} {β : α → Type v} [BEq α] [Hashable α], ∅.isEmpty = true
-- Init.Data.Nat.Div.Lemmas
Nat.ext_div_mod_iff : ∀ (n a b : ℕ), a = b ↔ a / n = b / n ∧ a % n = b % n
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
Float.Model.UnpackedFloat.unpackExponent_packComponents : ∀ {spec : Float.Model.Format} {sign : Float.Model.UnpackedFloat.Sign} {exponent : BitVec spec.exponentBits}
  {mantissa : BitVec spec.mantissaBitsWithoutImplicit},
  Float.Model.UnpackedFloat.unpackExponent (Float.Model.UnpackedFloat.packComponents spec sign exponent mantissa) =
    exponent
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addPrehaar_mem_addHaarProduct : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G},
  (interior U).Nonempty → MeasureTheory.Measure.haar.addPrehaar (↑K₀) U ∈ MeasureTheory.Measure.haar.addHaarProduct ↑K₀
-- Mathlib.GroupTheory.OrderOfElement
/-- An injective homomorphism of monoids preserves orders of elements.  -/
orderOf_injective : ∀ {G : Type u_1} [inst : Monoid G] {H : Type u_6} [inst_1 : Monoid H] (f : G →* H),
  Function.Injective ⇑f → ∀ (x : G), orderOf (f x) = orderOf x
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropWhile_dropWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String}, (s.dropWhile pat).dropWhile pat = s.dropWhile pat
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] (J : Type w)
  [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J], CategoryTheory.Limits.HasLimitsOfShape J C
-- Lean.Util.CollectFVars
Lean.CollectFVars.State.fvarSet : Lean.CollectFVars.State → Lean.FVarIdSet
-- Mathlib.Algebra.Group.Submonoid.Defs
pow_mem : ∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : SetLike A M] [SubmonoidClass A M] {S : A} {x : M},
  x ∈ S → ∀ (n : ℕ), x ^ n ∈ S
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.comap_abs_atTop : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G],
  Filter.comap abs Filter.atTop = Filter.atBot ⊔ Filter.atTop
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `ExponentExists.isMulTorsion`.

---

If a group exponent exists, the group is torsion.  -/
ExponentExists.isTorsion : ∀ {G : Type u_1} [inst : Group G], Monoid.ExponentExists G → IsMulTorsion G
-- Mathlib.Data.DFinsupp.BigOperators
AddMonoidHom.map_dfinsuppSumAddHom : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {R : Type u_1} {S : Type u_2} [inst_1 : AddCommMonoid R]
  [inst_2 : AddCommMonoid S] [inst_3 : (i : ι) → AddZeroClass (β i)] (h : R →+ S) (f : Π₀ (i : ι), β i)
  (g : (i : ι) → β i →+ R), h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun i => h.comp (g i)) f
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLT!_eq_get!_getKeyLT? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α} [inst_1 : Inhabited α],
  Std.DTreeMap.Internal.Impl.getKeyLT! k t = (Std.DTreeMap.Internal.Impl.getKeyLT? k t).get!
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
/-- A characterization of `Order.enum s _`: it is the unique strictly monotone function
with range `s`.  -/
Order.enum_eq_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [inst_2 : IsRegularCardinalOrder α] {s : Set α}
  {hs : IsCofinal s} {f : α → α}, Subtype.val ∘ ⇑(Order.enum s hs) = f ↔ StrictMono f ∧ Set.range f = s