mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_erase : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k a : α}, a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- A net of lower hemicontinuous set-valued functions converging uniformly (along a
filter `l`) in the Hausdorff uniformity has a lower hemicontinuous limit  -/
TendstoUniformly.lowerHemicontinuous : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {ι : Type u_3} {F : ι → α → Set β}
  {l : Filter ι} [l.NeBot] [inst_2 : UniformSpace β],
  TendstoUniformly F f l → (∀ (n : ι), LowerHemicontinuous (F n)) → LowerHemicontinuous f
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
/-- Turn an element of a type `F` satisfying
`[FunLike F A B] [GradedFunLike F 𝒜 ℬ] [AlgHomClass F R A B]` into an actual `GradedAlgHom`.

In future mathlib this will be deprioritised in favour of using structural projections.  -/
GradedAlgHom.ofClass : {R : Type u_1} →
  {A : Type u_6} →
    {B : Type u_7} →
      {ι : Type u_10} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : DecidableEq ι] →
                    [inst_6 : AddMonoid ι] →
                      {𝒜 : ι → Submodule R A} →
                        {ℬ : ι → Submodule R B} →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] →
                              {F : Type u_11} →
                                [inst_9 : FunLike F A B] →
                                  [GradedFunLike F 𝒜 ℬ] → [AlgHomClass F R A B] → F → 𝒜 →ₐᵍ[R] ℬ
-- Mathlib.Order.Partition.Finpartition
Finpartition.parts_nonempty : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (P : Finpartition a), a ≠ ⊥ → P.parts.Nonempty
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- For `1 ≤ r`, the logarithmic counting function for the poles of a sum `∑ a ∈ s, f a` is less than or
equal to the sum of the logarithmic counting functions for the poles of the `f ·`.
 -/
ValueDistribution.logCounting_sum_top_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {α : Type u_3} (s : Finset α) (f : α → 𝕜 → E) {r : ℝ},
  (∀ a ∈ s, Meromorphic (f a)) →
    1 ≤ r → ValueDistribution.logCounting (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, ValueDistribution.logCounting (f a) ⊤) r
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.forM_eq_forM_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → m PUnit.{w + 1}}, (forM t fun a => f a.1) = t.keys.forM f
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.prod_div_distrib_of_ne_zero : ∀ {ι : Type u_1} {f g : ι → ENNReal} {s : Finset ι},
  (∀ i ∈ s, g i ≠ 0) → ∏ i ∈ s, f i / g i = (∏ i ∈ s, f i) / ∏ i ∈ s, g i
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.of_comp_antilipschitzWith : ∀ {p : ENNReal} {α : Type u_6} {E : Type u_7} {F : Type u_8} {K' : NNReal} [inst : MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] {f : α → E} {g : E → F},
  MeasureTheory.MemLp (g ∘ f) p μ → UniformContinuous g → AntilipschitzWith K' g → g 0 = 0 → MeasureTheory.MemLp f p μ
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
/-- The Eulerian cycle of `cycleGraph (n + 3)`  -/
SimpleGraph.cycleGraph.cycle : (n : ℕ) → (SimpleGraph.cycleGraph (n + 3)).Walk 0 0
-- Mathlib.Analysis.Calculus.Deriv.Abs
HasFDerivAt.abs : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasFDerivAt f f' x → f x ≠ 0 → HasFDerivAt (fun x => |f x|) (↑(SignType.sign (f x)) • f') x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.inter_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → (t₁ ∩ t₃).Equiv (t₂ ∩ t₃)
-- Mathlib.GroupTheory.OrderOfElement
/-- **Alias** of the forward direction of `isOfFinAddOrder_neg_iff`.

---

Inverses of elements of finite additive order
have finite additive order.  -/
IsOfFinAddOrder.of_neg : ∀ {G : Type u_1} [inst : AddGroup G] {x : G}, IsOfFinAddOrder (-x) → IsOfFinAddOrder x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  (t.insertMany l).contains k = (t.contains k || (List.map Sigma.fst l).contains k)
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.one_lt_toENat : ∀ {c : Cardinal.{u}}, 1 < Cardinal.toENat c ↔ 1 < c
-- Mathlib.Data.Quot
Quot.induction_on₂ : ∀ {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} {s : β → β → Prop} {δ : Quot r → Quot s → Prop} (q₁ : Quot r)
  (q₂ : Quot s), (∀ (a : α) (b : β), δ (Quot.mk r a) (Quot.mk s b)) → δ q₁ q₂
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- There is a canonical equivalence between the structured arrow category with domain `c` on
the functor `Comma.fst F G : Comma F G ⥤ F` and the comma category over
`Under.forget c ⋙ F : Under c ⥤ T` and `G`.  -/
CategoryTheory.StructuredArrow.ofCommaSndEquivalence : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor C T) →
              (G : CategoryTheory.Functor D T) →
                (c : C) →
                  CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G) ≌
                    CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.CommaMorphism.zero_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Preadditive A] {B : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} B] [inst_3 : CategoryTheory.Preadditive B] {T : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} T] [inst_5 : CategoryTheory.Preadditive T] (L : CategoryTheory.Functor A T)
  [inst_6 : L.Additive] (R : CategoryTheory.Functor B T) [inst_7 : R.Additive] {u v : CategoryTheory.Comma L R},
  CategoryTheory.CommaMorphism.left 0 = 0
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- If `f : M → N` is a subadditive function, `f (x + y) ≤ f x + f y` and `g i`, `i ∈ s`, is a
nonempty finite family of elements of `M`, then `f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)`.  -/
Finset.le_sum_nonempty_of_subadditive : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [inst_2 : Preorder N]
  [IsOrderedAddMonoid N] (f : M → N),
  (∀ (x y : M), f (x + y) ≤ f x + f y) →
    ∀ {s : Finset ι}, s.Nonempty → ∀ (g : ι → M), f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.mul_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {l : Type u_7} [inst : Fintype m] [inst_1 : Mul A]
  [inst_2 : AddCommMonoid A] {M : CStarMatrix l m A} {N : CStarMatrix m n A} {i : l} {k : n},
  (M * N) i k = ∑ j, M i j * N j k
-- Mathlib.SetTheory.Ordinal.Basic
RelIso.ordinal_lift_type_eq : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s]
  (f : r ≃r s), Ordinal.lift.{v, u} (Ordinal.type r) = Ordinal.lift.{u, v} (Ordinal.type s)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pushforwardIsoBind_hom_s₀_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X)
  (a : (CategoryTheory.PreZeroHypercover.pushforward f E).I₀),
  ((CategoryTheory.PreZeroHypercover.pushforwardIsoBind f E).hom.s₀ a).fst = PUnit.unit
-- Mathlib.GroupTheory.Schreier
/-- A theorem of Schur: A group with finitely many commutators has finite commutator subgroup.  -/
Subgroup.instFiniteSubtypeMemCommutatorOfElemCommutatorSet : ∀ (G : Type u_1) [inst : Group G] [Finite ↑(commutatorSet G)], Finite ↥(commutator G)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.End.addOppositeEquiv.eq_1 : ∀ {M : Type u_2} [inst : AddMonoid M],
  AddActionHom.End.addOppositeEquiv =
    { toFun := fun f => f 0, invFun := fun m => { toFun := fun x => m + x, map_vadd' := ⋯ }, left_inv := ⋯,
      right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.Data.Finset.Card
Multiset.toFinset_card_of_nodup : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α}, m.Nodup → m.toFinset.card = m.card
-- Lean.Parser.Extra
Lean.Parser.ppRealFill.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_prod : ∀ {R : Type u} [inst : Monoid R] {A : Type v} {B : Type w} {C : Type w₁} [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : NonUnitalNonAssocSemiring C]
  [inst_5 : DistribMulAction R B] [inst_6 : DistribMulAction R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C),
  ⇑(f.prod g) = Function.prod ⇑f ⇑g
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
/-- An auxiliary lemma saying that if `b ≠ 0`,
then `(a / b ^ n + n * b) / (n + 1) + 1` is a strict upper estimate on `√[n + 1] a`.
 -/
Nat.nthRoot.lt_pow_go_succ_aux : ∀ {n a b : ℕ}, b ≠ 0 → a < ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.instReprMCasesPat : Repr Lean.Parser.Tactic.MCasesPat
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
/-- **Alias** of `BddAbove.add`. -/
Set.BddAbove.add : ∀ {M : Type u_3} [inst : Add M] [inst_1 : Preorder M] [AddLeftMono M] [AddRightMono M] {s t : Set M},
  BddAbove s → BddAbove t → BddAbove (s + t)
-- Mathlib.Data.Nat.MaxPowDiv
_private.Mathlib.Data.Nat.MaxPowDiv.0.Nat.maxPowDvdDiv.match_1.splitter : (motive : ℕ × ℕ → Sort u_1) → (x : ℕ × ℕ) → ((e q : ℕ) → motive (e, q)) → motive x
-- Mathlib.Computability.Reduce
manyOneEquiv_refl : ∀ {α : Type u_1} [inst : Primcodable α] (p : α → Prop), ManyOneEquiv p p
-- Batteries.Data.Array.Scan
Array.toList_scanl : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : Array α},
  (Array.scanl f init as).toList = List.scanl f init as.toList
-- Batteries.Data.String.Lemmas
String.Pos.Raw.get?.eq_1 : ∀ (x : String) (x_1 : String.Pos.Raw), String.Pos.Raw.get? x x_1 = String.Pos.Raw.utf8GetAux? x.toList 0 x_1
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.decompId_p_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Idempotents.Karoubi C),
  P.decompId_p.f = P.p
-- Lean.Class
/-- Add a new type class with the given name to the environment.
`declName` must not be the name of an existing type class,
and it must be the name of constant in `env`.
`declName` must be a inductive datatype or axiom.
Recall that all structures are inductive datatypes.
 -/
Lean.addClass : Lean.Environment → Lean.Name → Except Lean.MessageData Lean.Environment
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.unitOfDetInvertible_eq_nonsingInvUnit : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  [inst_3 : Invertible A.det], A.unitOfDetInvertible = A.nonsingInvUnit ⋯
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_mul : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (φ ψ : PowerSeries R),
  (PowerSeries.coeff n) (φ * ψ) =
    ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, (PowerSeries.coeff p.1) φ * (PowerSeries.coeff p.2) ψ
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_eq_preBeth : ∀ (o : Ordinal.{u_1}), Cardinal.beth o = Cardinal.preBeth (Ordinal.omega0 + o)
-- Mathlib.Algebra.Order.Interval.Basic
Interval.length_add_le : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α] (s t : Interval α),
  (s + t).length ≤ s.length + t.length
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated derivative commutes with shifting the function by a constant on the right.  -/
iteratedFDeriv_comp_add_right : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  (n : ℕ) (a x : E), iteratedFDeriv 𝕜 n (fun z => f (z + a)) x = iteratedFDeriv 𝕜 n f (x + a)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.coe_mk_comp : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] {ψ : K →+* ℂ} {f : k →+* K}
  (h : Function.Injective ⇑f), ↑(NumberField.InfinitePlace.mk (ψ.comp f)) = (↑(NumberField.InfinitePlace.mk ψ)).comp h
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The cokernel cofork `cc` is a colimit.  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isColimitCc : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    (r r' : ℤ) →
                      (hrr' : r + 1 = r') →
                        (hr : r₀ ≤ r) →
                          (pq pq' : κ) →
                            (c r).prev pq' = pq →
                              (i₀ i₁ i₂ i₃ i₃' : ι) →
                                (hi₀ : i₀ = data.i₀ r pq' ⋯) →
                                  (hi₁ : i₁ = data.i₁ pq') →
                                    (hi₂ : i₂ = data.i₂ pq') →
                                      (hi₃ : i₃ = data.i₃ r pq' ⋯) →
                                        (hi₃' : i₃' = data.i₃ r' pq' ⋯) →
                                          (n₀ n₁ n₂ : ℤ) →
                                            (hn₁' : n₁ = data.deg pq') →
                                              [X.HasSpectralSequence data] →
                                                (hn₁ :
                                                    autoParam (n₀ + 1 = n₁)
                                                      CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isColimitCc._auto_1) →
                                                  (hn₂ :
                                                      autoParam (n₁ + 1 = n₂)
                                                        CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isColimitCc._auto_3) →
                                                    CategoryTheory.Limits.IsColimit
                                                      (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.cc
                                                        X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃'
                                                        n₀ n₁ n₂ hn₁' ⋯ ⋯)
-- Mathlib.Topology.Algebra.ProperConstSMul
/-- A mixin typeclass saying that `(c • ·)` is a proper map for all `c`.

Note that this is **not** the same as a proper multiplicative action (not yet in `Mathlib`).  -/
ProperConstSMul : (M : Type u_1) → (X : Type u_2) → [SMul M X] → [TopologicalSpace X] → Prop
-- Mathlib.GroupTheory.Coxeter.Basic
/-- If two homomorphisms with domain `W` agree on all simple reflections, then they are equal.  -/
CoxeterSystem.ext_simple : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {G : Type u_5}
  [inst_1 : MulOneClass G] {φ₁ φ₂ : W →* G}, (∀ (i : B), φ₁ (cs.simple i) = φ₂ (cs.simple i)) → φ₁ = φ₂
-- Mathlib.Data.Seq.Defs
/-- The `ENat`-valued length of a sequence. For non-terminating sequences, it is `⊤`.  -/
Stream'.Seq.length' : {α : Type u} → Stream'.Seq α → ℕ∞
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.Slice.intercalate.match_1.eq_1 : ∀ (motive : List String.Slice → Sort u_1) (h_1 : Unit → motive [])
  (h_2 : (a : String.Slice) → (as : List String.Slice) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBlastCpopLayerTargetBlastCpopLayer : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.map_eq_natCast_iff : ∀ {α : Type u} {β : Type v} [inst : AddMonoidWithOne α] {f : β → α} {n : ℕ} {a : WithBot β},
  WithBot.map f a = ↑n ↔ ∃ x, a = ↑x ∧ f x = ↑n
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a limit for `F : Jᵒᵖ ⥤ Cᵒᵖ` into a colimit for `F.unop : J ⥤ C`.  -/
CategoryTheory.Limits.isColimitOfConeOfCoconeUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cocone F.unop} →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeUnop c) → CategoryTheory.Limits.IsColimit c
-- Mathlib.Data.Analysis.Topology
LocallyFinite.Realizer.to_locallyFinite : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {F : Ctop.Realizer α} {f : β → Set α}
  (R : LocallyFinite.Realizer F f), LocallyFinite f
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_toBitVec : ∀ (a : UInt64), { toBitVec := a.toBitVec } = a
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.zpow : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {s : 𝕜 → 𝕜'} {U : Set 𝕜}, MeromorphicOn s U → ∀ (n : ℤ), MeromorphicOn (s ^ n) U
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.differentiableAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {x : E} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → x ∈ s → DifferentiableAt ℝ f x
-- Aesop.Forward.RuleInfo
Aesop.ForwardRuleInfo.mk.inj : ∀ {numPremises numLevelParams : ℕ} {slotClusters : Array (Array Aesop.Slot)} {conclusionDeps : Array Aesop.PremiseIndex}
  {rulePatternInfo? : Option (Aesop.RulePattern × Aesop.PremiseIndex)} {numPremises_1 numLevelParams_1 : ℕ}
  {slotClusters_1 : Array (Array Aesop.Slot)} {conclusionDeps_1 : Array Aesop.PremiseIndex}
  {rulePatternInfo?_1 : Option (Aesop.RulePattern × Aesop.PremiseIndex)},
  { numPremises := numPremises, numLevelParams := numLevelParams, slotClusters := slotClusters,
        conclusionDeps := conclusionDeps, rulePatternInfo? := rulePatternInfo? } =
      { numPremises := numPremises_1, numLevelParams := numLevelParams_1, slotClusters := slotClusters_1,
        conclusionDeps := conclusionDeps_1, rulePatternInfo? := rulePatternInfo?_1 } →
    numPremises = numPremises_1 ∧
      numLevelParams = numLevelParams_1 ∧
        slotClusters = slotClusters_1 ∧ conclusionDeps = conclusionDeps_1 ∧ rulePatternInfo? = rulePatternInfo?_1
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.exists_smodEq_pow_add_one_smul : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N},
  Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f) →
    ∀ {y : N} {n : ℕ}, y ∈ I ^ n • ⊤ → ∃ x ∈ I ^ n • ⊤, f x ≡ y [SMOD I ^ (n + 1) • ⊤]
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateMulAct.instCommMonoid : {α : Type u_1} → {f : α → α} → CommMonoid (IterateMulAct f)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan f g)
    (AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.comp
      AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace)
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.ProbabilityMeasure.map.congr_simp : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
  (ν ν_1 : MeasureTheory.ProbabilityMeasure Ω) (e_ν : ν = ν_1) {f f_1 : Ω → Ω'} (e_f : f = f_1)
  (f_aemble : AEMeasurable f ↑ν), ν.map f_aemble = ν_1.map ⋯
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- A linearly-ordered abelian group is cyclic iff it is isomorphic to `Multiplicative ℤ` as an
ordered monoid.  -/
LinearOrderedCommGroup.isCyclic_iff_nonempty_equiv_int : ∀ {G : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [Nontrivial G],
  IsCyclic G ↔ Nonempty (G ≃*o Multiplicative ℤ)
-- Mathlib.Combinatorics.Matroid.IndepAxioms
Matroid.ofBase_E : ∀ {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) (exists_isBase : ∃ B, IsBase B)
  (isBase_exchange : Matroid.ExchangeProperty IsBase)
  (maximality : ∀ X ⊆ E, Matroid.ExistsMaximalSubsetProperty (fun x => ∃ B, IsBase B ∧ x ⊆ B) X)
  (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E),
  (Matroid.ofBase E IsBase exists_isBase isBase_exchange maximality subset_ground).E = E
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k a : α}, (t.erase k).getKey! a = if cmp k a = Ordering.eq then default else t.getKey! a
-- Mathlib.Probability.Process.Stopping
MeasureTheory.StronglyAdapted.stronglyMeasurable_stoppedProcess : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : Nonempty ι] [inst_3 : LinearOrder ι]
  [inst_4 : TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [inst_7 : MeasurableSpace ι]
  [BorelSpace ι] {f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [TopologicalSpace.MetrizableSpace ι],
  MeasureTheory.StronglyAdapted f u →
    (∀ (ω : Ω), Continuous fun i => u i ω) →
      MeasureTheory.IsStoppingTime f τ →
        ∀ (n : ι), MeasureTheory.StronglyMeasurable (MeasureTheory.stoppedProcess u τ n)
-- Mathlib.Analysis.Convex.Segment
Convex.min_le_combo : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : Module 𝕜 E] [PosSMulMono 𝕜 E] {a b : 𝕜} (x y : E),
  0 ≤ a → 0 ≤ b → a + b = 1 → min x y ≤ a • x + b • y
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
MeasureTheory.iteratedFDeriv_charFun : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [BorelSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] {n : ℕ}
  {t : E},
  MeasureTheory.MemLp id (↑n) μ →
    ∀ (x : Fin n → E),
      (iteratedFDeriv ℝ n (MeasureTheory.charFun μ) t) x =
        Complex.I ^ n * ∫ (y : E), ↑(∏ i, inner ℝ y (x i)) * Complex.exp (↑(inner ℝ y t) * Complex.I) ∂μ
-- Init.Data.Vector.Algebra
Vector.getElem_mul : ∀ {α : Type u_1} {n : ℕ} [inst : Mul α] (xs ys : Vector α n) (i : ℕ) (h : i < n), (xs * ys)[i] = xs[i] * ys[i]
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.rowLen.eq_1 : ∀ (μ : YoungDiagram) (i : ℕ), μ.rowLen i = Nat.find ⋯