mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
/-- Invariant vector fields are invariant under pullbacks.  -/
mpullback_addInvariantVectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] [LieAddGroup I (minSmoothness 𝕜 3) G]
  (g : G) (v : AddGroupLieAlgebra I G),
  VectorField.mpullback I I (fun x => g + x) (addInvariantVectorField v) = addInvariantVectorField v
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z)
  [inst_1 : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion g]
  (e :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)),
  (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq f g e).inv =
    AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift f g ⋯
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Find and remove the the minimum element from the binomial heap.  -/
Batteries.BinomialHeap.Imp.Heap.deleteMin : {α : Type u_1} → (α → α → Bool) → Batteries.BinomialHeap.Imp.Heap α → Option (α × Batteries.BinomialHeap.Imp.Heap α)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Reinterpret a `LinearIsometry` as a `LinearIsometryEquiv` to the range.  -/
LinearIsometry.equivRange : {E : Type u_5} →
  {F : Type u_9} →
    [inst : SeminormedAddCommGroup E] →
      [inst_1 : NormedAddCommGroup F] →
        {R : Type u_11} →
          {S : Type u_12} →
            [inst_2 : Semiring R] →
              [inst_3 : Ring S] →
                [inst_4 : Module S E] →
                  [inst_5 : Module R F] →
                    {σ₁₂ : R →+* S} →
                      {σ₂₁ : S →+* R} →
                        [inst_6 : RingHomInvPair σ₁₂ σ₂₁] →
                          [inst_7 : RingHomInvPair σ₂₁ σ₁₂] → (f : F →ₛₗᵢ[σ₁₂] E) → F ≃ₛₗᵢ[σ₁₂] ↥f.range
-- Mathlib.Data.Fin.Fin2
/-- This is a simple type class inference prover for proof obligations
of the form `m < n` where `m n : ℕ`.  -/
Fin2.IsLT : ℕ → ℕ → Prop
-- Mathlib.Analysis.Calculus.Deriv.Basic
deriv_intCast : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : IntCast F] (z : ℤ), deriv ↑z = 0
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.flatten_congr : ∀ {α : Type u} {c1 c2 : Computation (Stream'.WSeq α)},
  Computation.LiftRel Stream'.WSeq.Equiv c1 c2 → Stream'.WSeq.flatten c1 ~ʷ Stream'.WSeq.flatten c2
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.sum_zero_index : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] (f : ℕ → R → S), Polynomial.sum 0 f = 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Complex.continuousAt_ofReal_cpow_const : ∀ (x : ℝ) (y : ℂ), 0 < y.re ∨ x ≠ 0 → ContinuousAt (fun a => ↑a ^ y) x
-- Mathlib.Data.Set.Opposite
Set.op_mem_op : ∀ {α : Type u_1} {s : Set α} {a : α}, Opposite.op a ∈ s.op ↔ a ∈ s
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The underlying morphism  -/
CategoryTheory.Mod.Hom.hom : {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.MonoidalLeftAction C D] →
            {A : C} → [inst_4 : CategoryTheory.MonObj A] → {M N : CategoryTheory.Mod D A} → M.Hom N → (M.X ⟶ N.X)
-- Aesop.Tree.Data
Aesop.GoalState.unprovable.sizeOf_spec : sizeOf Aesop.GoalState.unprovable = 1
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.add_isLittleO : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, f₁ =O[l] g → f₂ =o[l] g → (fun x => f₁ x + f₂ x) =O[l] g
-- Mathlib.Topology.ContinuousMap.Polynomial
/-- The algebra map from `R[X]` to continuous functions `C(R, R)`.
 -/
Polynomial.toContinuousMapAlgHom : {R : Type u_1} →
  [inst : CommSemiring R] →
    [inst_1 : TopologicalSpace R] → [inst_2 : IsTopologicalSemiring R] → Polynomial R →ₐ[R] C(R, R)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- The invertible kronecker matrix of invertible matrices.  -/
Matrix.GeneralLinearGroup.kronecker : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type u_3} →
        {m : Type u_4} →
          [inst_2 : CommSemiring R] → [inst_3 : Fintype m] → [inst_4 : DecidableEq m] → GL n R → GL m R → GL (n × m) R
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₀ : ∀ (l : ℕ) (r : ℤ) (pq : ℤ × Fin l) (hr : 2 ≤ r),
  (CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin l).i₀ r pq hr = ⟨(↑↑pq.2 - (r - 2)).toNat, ⋯⟩
-- Mathlib.Tactic.Simps.Basic
/-- If a structure has a field that corresponds to a coercion to functions or sets, or corresponds
  to notation, find the custom projection that uses this coercion or notation.
  Returns the custom projection and the name of the projection used.

We catch most errors this function causes, so that we don't fail if an unrelated projection has
an applicable name. (e.g. `Iso.inv`)

Implementation note: getting rid of TermElabM is tricky, since `Expr.mkAppOptM` doesn't allow to
keep metavariables around, which are necessary for `OutParam`.  -/
Simps.findAutomaticProjectionsAux : Lean.Name → Simps.ParsedProjectionData → Array Lean.Expr → Lean.Elab.TermElabM (Option (Lean.Expr × Lean.Name))
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.notCore.sizeOf_spec : ∀ (e : Lean.Expr) (lhs rhs : Lean.Grind.CommRing.Expr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.notCore e lhs rhs) = 1 + sizeOf e + sizeOf lhs + sizeOf rhs
-- Lean.Meta.Tactic.Revert
/-- Reverts all free variables in the goal `mvarId`.
**Remark**: Auxiliary local declarations are cleared.
 -/
Lean.MVarId.revertAll : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_list_eq_foldl : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Internal.Raw₀ α fun x => Unit} {l : List α},
  ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l) = List.foldl (fun a b => a.insertIfNew b ()) m l
-- Std.Do.WP.SimpLemmas
Std.Do.WP.throw_ReaderT : ∀ {m : Type u → Type v} {sh : Std.Do.PostShape} {ε : Type u_1} {ρ α : Type u} {e : ε}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ sh)} [inst : Std.Do.WP m sh] [Monad m] [inst_2 : MonadExceptOf ε m],
  (Std.Do.wp (MonadExceptOf.throw e)).apply Q = (Std.Do.wp (MonadLift.monadLift (MonadExceptOf.throw e))).apply Q
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `M`-equivariant functions `X → Y` with respect to the action of `M`.
This is the same as `X →ₑ[@id M] Y`.  -/
«MulActionHomIdLocal≺» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Group.Arithmetic
Finset.aemeasurable_fun_prod : ∀ {M : Type u_2} {ι : Type u_3} {α : Type u_4} [inst : CommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, AEMeasurable (f i) μ) → AEMeasurable (fun a => ∏ i ∈ s, f i a) μ
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.comp_toLinearMap : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] (ρ : Representation A G V) (σ : Representation A G W)
  (τ : Representation A G U) (f : σ.IntertwiningMap τ) (g : ρ.IntertwiningMap σ),
  (f.comp g).toLinearMap = f.toLinearMap ∘ₗ g.toLinearMap
-- Mathlib.SetTheory.Ordinal.Arithmetic
Cardinal.instNonemptyToTypeOrdAleph0 : Nonempty Cardinal.aleph0.ord.ToType
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsLeftUniformGroup.toIsTopologicalGroup : ∀ {G : Type u_7} {inst : UniformSpace G} {inst_1 : Group G} [self : IsLeftUniformGroup G], IsTopologicalGroup G
-- Init.Data.BitVec.Bitblast
BitVec.ult_eq_not_carry : ∀ {w : ℕ} (x y : BitVec w), x.ult y = !BitVec.carry w x (~~~y) true
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.jacobson_bot : ∀ {R : Type u} [inst : Ring R], ⊥.jacobson = Ring.jacobson R
-- Lean.Meta.LazyDiscrTree
/-- Lazy entries at this trie that are not processed.  -/
Lean.Meta.LazyDiscrTree.Trie.pending : {α : Type} → Lean.Meta.LazyDiscrTree.Trie α → Array (Lean.Meta.LazyDiscrTree.LazyEntry α)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
/-- The binary fan provided by `fst'` and `snd'` is a binary product in `Over X`.  -/
CategoryTheory.ChosenPullbacksAlong.binaryFanIsBinaryProduct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      (Y Z : CategoryTheory.Over X) →
        [inst_1 : CategoryTheory.ChosenPullbacksAlong Z.hom] →
          CategoryTheory.Limits.IsLimit (CategoryTheory.ChosenPullbacksAlong.binaryFan Y Z)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_ε : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).functor =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_sub : ∀ (x y : ℂ), Complex.exp (x - y) = Complex.exp x / Complex.exp y
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f],
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.cokernel.π f) = 0
-- Std.Internal.Do.ExceptPost
Std.Internal.Do.EPost.Cons.mk.injEq : ∀ {eh : Type u} {et : Type v} (head : eh) (tail : et) (head_1 : eh) (tail_1 : et),
  (EPost.Cons.mk✝ head tail = EPost.Cons.mk✝ head_1 tail_1) = (head = head_1 ∧ tail = tail_1)
-- Mathlib.Order.Filter.Lift
Filter.lift'_inf : ∀ {α : Type u_1} {β : Type u_2} (f g : Filter α) {s : Set α → Set β},
  (∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂) → (f ⊓ g).lift' s = f.lift' s ⊓ g.lift' s
-- Mathlib.Data.DFinsupp.Multiset
Multiset.toDFinsupp_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α),
  Multiset.toDFinsupp (s ∩ t) = Multiset.toDFinsupp s ⊓ Multiset.toDFinsupp t
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfOrdArgs.le : {α : Type u} →
  (self : Std.Packages.LinearPreorderOfOrdArgs α) →
    let this := self.ord;
    LE α
-- Mathlib.Topology.Algebra.ProperConstSMul
instProperConstSMulProd : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : SMul M X] [inst_1 : TopologicalSpace X] [ProperConstSMul M X]
  [inst_3 : SMul M Y] [inst_4 : TopologicalSpace Y] [ProperConstSMul M Y], ProperConstSMul M (X × Y)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- Given a family of elements `x` for the sieve `S` generated by a presieve `R`, if `x` is restricted
to `R` and then extended back up to `S`, the resulting extension equals `x`.
 -/
CategoryTheory.Presieve.extend_restrict : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X}
  {x : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows},
  x.Compatible → (CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x).sieveExtend = x
-- Mathlib.LinearAlgebra.Pi
/-- `Equiv.sumArrowEquivProdArrow` as a linear equivalence.
 -/
LinearEquiv.sumArrowLequivProdArrow : (α : Type u_5) →
  (β : Type u_6) →
    (R : Type u_7) →
      (M : Type u_8) →
        [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (α ⊕ β → M) ≃ₗ[R] (α → M) × (β → M)
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
CommGrpCat.forget_isCorepresentable : (CategoryTheory.forget CommGrpCat).IsCorepresentable
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousOn_ciInf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {ι : Sort u_4} {δ' : Type u_6}
  [inst_1 : ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'},
  (∀ x ∈ s, BddBelow (Set.range fun i => f i x)) →
    (∀ (i : ι), UpperSemicontinuousOn (f i) s) → UpperSemicontinuousOn (fun x' => ⨅ i, f i x') s
-- Mathlib.Topology.SmallInductiveDimension
HasSmallInductiveDimensionLT.mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m n : ℕ},
  m ≤ n → HasSmallInductiveDimensionLT X m → HasSmallInductiveDimensionLT X n
-- Mathlib.Algebra.Group.Equiv.Opposite
MulHom.fromOpposite_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)),
  ⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- If `t.coef > 0` then `t.toFun` is eventually positive.  -/
Tactic.ComputeAsymptotics.Monomial.toFun_pos : ∀ {t : Tactic.ComputeAsymptotics.Monomial} {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis → 0 < t.coef → ∀ᶠ (x : ℝ) in Filter.atTop, 0 < t.toFun basis x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
/-- A sheaf of modules is locally free if it is locally isomorphic to free sheaves:
There exist local generators satisfying `IsLocallyFreeData`.  -/
SheafOfModules.IsLocallyFree : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] → SheafOfModules R → Prop
-- Mathlib.RepresentationTheory.Equiv
Representation.freeLiftLEquiv_apply : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {k : Type u} [inst_2 : CommSemiring k]
  [inst_3 : Module k V] (σ : Representation k G V) (α : Type w') (f : (Representation.free k G α).IntertwiningMap σ)
  (i : α), (σ.freeLiftLEquiv α) f i = f fun₀ | i => MonoidAlgebra.single 1 1
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.inl_v_descShortComplex_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (i j : ℤ) (h : i + -1 = j) {Z : C} (h_1 : S.X₃.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl S.f).v i j h)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.descShortComplex S).f j) h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
Std.Iter.takeWhile_eq : ∀ {α β : Type u_1} [Std.Iterator α Id β] {P : β → Bool} {it : Std.Iter β},
  Std.Iter.takeWhile P it = (Std.IterM.takeWhile P it.toIterM).toIter
-- Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
/-- Let `K` be the field of fraction of an integrally closed domain `R` and let `L` be an extension
of `K`, generated by an integral power basis `B` such that the minimal polynomial of `B.gen` is
Eisenstein at `p`. Given `z : L` integral over `R`, if `p ^ n • z ∈ R[B.gen]`, then
`z ∈ R[B.gen]`. Together with `Algebra.discr_mul_isIntegral_mem_adjoin` this result often
allows to compute the ring of integers of `L`.  -/
mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt : ∀ {R : Type u} {K : Type v} {L : Type z} {p : R} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : Algebra R L] [inst_5 : Algebra R K] [IsScalarTower R K L] [IsDomain R]
  [IsFractionRing R K] [IsIntegrallyClosed R] {B : PowerBasis K L},
  Prime p →
    IsIntegral R B.gen →
      ∀ {n : ℕ} {z : L}, IsIntegral R z → p ^ n • z ∈ R[B.gen] → (minpoly R B.gen).IsEisensteinAt (R ∙ p) → z ∈ R[B.gen]
-- Mathlib.Algebra.Group.UniqueProds.Basic
uniqueMul_of_twoUniqueMul : ∀ {G : Type u_1} [inst : Mul G] {A B : Finset G},
  (1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2) →
    A.Nonempty → B.Nonempty → ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
-- Mathlib.Tactic.Ring.Basic
/-- Converts a proof by `norm_num` that `e` is a numeral, into a normalization as a monomial:

* `e = 0` if `norm_num` returns `IsNat e 0`
* `e = Nat.rawCast n + 0` if `norm_num` returns `IsNat e n`
* `e = Int.rawCast n + 0` if `norm_num` returns `IsInt e n`
* `e = NNRat.rawCast n d + 0` if `norm_num` returns `IsNNRat e n d`
* `e = Rat.rawCast n d + 0` if `norm_num` returns `IsRat e n d`
 -/
Mathlib.Tactic.Ring.evalCast : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {e : Q(«$α»)} →
        Mathlib.Meta.NormNum.Result e → Option (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.ExSum sα) e)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.prodAux_eq : ∀ {M : Type u_4} [inst : Monoid M] (l : List M), FreeMonoid.prodAux l = l.prod
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearIsometryEquiv.conjStarAlgEquiv_trans : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] {K : Type u_6} [inst_4 : NormedAddCommGroup K] [inst_5 : InnerProductSpace 𝕜 K]
  [inst_6 : CompleteSpace K] {G : Type u_7} [inst_7 : NormedAddCommGroup G] [inst_8 : InnerProductSpace 𝕜 G]
  [inst_9 : CompleteSpace G] (e : H ≃ₗᵢ[𝕜] K) (f : K ≃ₗᵢ[𝕜] G),
  (e.trans f).conjStarAlgEquiv = e.conjStarAlgEquiv.trans f.conjStarAlgEquiv
-- Std.Data.TreeSet.Slice
Std.TreeSet.toList_roi : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.toList_roi._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet α cmp} {bound : α},
  Std.Slice.toList (Std.Roi.Sliceable.mkSlice t bound<...*) = List.filter (fun e => (cmp e bound).isGT) t.toList
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len w outWidth : ℕ} (aig : Std.Sat.AIG α) (iterNum : ℕ)
  (oldLayer : aig.RefVec (len * w)) (newLayer : aig.RefVec (iterNum * w)) (hold : 2 * (iterNum - 1) < len)
  (hout : outWidth = (len + 1) / 2 * w),
  aig.decls.size ≤
    (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go iterNum oldLayer newLayer hold hout).aig.decls.size
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.toContinuousMultilinearMap_smul : ∀ {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [inst_4 : Monoid R']
  [inst_5 : Semiring A] [inst_6 : Module A M] [inst_7 : Module A N] [inst_8 : DistribMulAction R' N]
  [inst_9 : ContinuousConstSMul R' N] [inst_10 : SMulCommClass A R' N] (c : R') (f : M [⋀^ι]→L[A] N),
  (c • f).toContinuousMultilinearMap = c • f.toContinuousMultilinearMap
-- Mathlib.Algebra.Category.Ring.Basic
RingEquiv.toCommSemiRingCatIso_hom : ∀ {R S : Type u} [inst : CommSemiring R] [inst_1 : CommSemiring S] (e : R ≃+* S),
  e.toCommSemiRingCatIso.hom = CommSemiRingCat.ofHom ↑e
-- Mathlib.Data.Set.Subsingleton
Set.Subsingleton.strictMonoOn : ∀ {α : Type u} {β : Type v} {s : Set α} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  s.Subsingleton → StrictMonoOn f s
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_natCast : ∀ (n : ℕ), Cardinal.preAleph ↑n = ↑n
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterMap.match_1.eq_1 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (h_1 : none = none → motive none)
  (h_2 : (out' : γ) → none = some out' → motive (some out')),
  (match h' : none with
    | none => h_1 h'
    | some out' => h_2 out' h') =
    h_1 ⋯
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.FixPoint.State.usedFVarsMap : Lean.Elab.Term.MutualClosure.FixPoint.State → Lean.Elab.Term.MutualClosure.UsedFVarsMap
-- Mathlib.Topology.Sober
IsGenericPoint.specializes_iff_mem : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x y : α} {S : Set α}, IsGenericPoint x S → (x ⤳ y ↔ y ∈ S)
-- Mathlib.Topology.Order.IntermediateValue
/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `b`, and the set `s ∩ (a, b]` has no minimal point, then `a ∈ s`.  -/
IsClosed.mem_of_ge_of_forall_exists_lt : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {a b : α}
  {s : Set α}, IsClosed (s ∩ Set.Icc a b) → b ∈ s → a ≤ b → (∀ x ∈ s ∩ Set.Ioc a b, (s ∩ Set.Ico a x).Nonempty) → a ∈ s
-- Mathlib.Control.Basic
fish_pipe : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {α β : Type u} (f : α → m β), pure >=> f = f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryGE?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, t₁.Equiv t₂ → Std.DTreeMap.Const.getEntryGE? t₁ k = Std.DTreeMap.Const.getEntryGE? t₂ k
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toArray_eq_match_step : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.toArray =
    match ↑it.step with
    | Std.IterStep.yield it' out => #[out] ++ it'.toArray
    | Std.IterStep.skip it' => it'.toArray
    | Std.IterStep.done => #[]
-- Mathlib.Order.MinMax
min_max_distrib_left : ∀ {α : Type u} [inst : LinearOrder α] (a b c : α), min a (max b c) = max (min a b) (min a c)
-- Batteries.Data.BinomialHeap.Basic
/-- `O(1)`. Make a new empty binomial heap.  -/
Batteries.mkBinomialHeap : (α : Type u) → (le : α → α → Bool) → Batteries.BinomialHeap α le
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulDysonETransform.smul_finset_snd_subset_fst : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommGroup α] {e : α} {x : Finset α × Finset α},
  e • (Finset.mulDysonETransform e x).2 ⊆ (Finset.mulDysonETransform e x).1
-- Mathlib.CategoryTheory.ExtremalEpi
/-- An extremal epimorphism `f : X ⟶ Y` is an epimorphism which does not
factor through any proper subobject of `Y`.  -/
CategoryTheory.ExtremalEpi : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → Prop
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.compare_def : compare =
  compareLex (compareOn fun x => x.hour)
    (compareLex (compareOn fun x => x.minute)
      (compareLex (compareOn fun x => x.second) (compareOn fun x => x.nanosecond)))
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `lowerHemicontinuousOn_iff_frequently`. -/
LowerHemicontinuousOn.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α},
  LowerHemicontinuousOn f s → ∀ x ∈ s, ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ t) → f x ⊆ t