mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
instCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (A : Type u)
  [inst_9 : TopologicalSpace A] [inst_10 : ChartedSpace H A] [inst_11 : CommGroup A] [inst_12 : LieGroup I (↑⊤) A]
  (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ),
  instCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf IM I M A U =
    { toGroup := instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf IM I M A U, mul_comm := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_maxKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {he : t.isEmpty = false} {fallback : α}, t.getKeyD (t.maxKey he) fallback = t.maxKey he
-- Mathlib.Algebra.Lie.CartanSubalgebra
LieSubalgebra.ne_bot_of_isCartanSubalgebra : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [Nontrivial L]
  (H : LieSubalgebra R L) [H.IsCartanSubalgebra], H ≠ ⊥
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.toBitVec_maxValueSealed_eq_intMaxSealed : Int16.maxValueSealed✝.toBitVec = BitVec.Signed.intMaxSealed✝ 16
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_mk_subset : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {s : Finset ι} {x : (i : ↑↑s) → β ↑i},
  (DFinsupp.mk s x).support ⊆ s
-- Aesop.Tree.Data
Aesop.Goal.isRoot : Aesop.Goal → BaseIO Bool
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- The direct sum of tensor powers of a direct sum of `R`-algebras,
before taking the quotient by the free product relation  -/
LinearAlgebra.FreeProduct.PowerAlgebra : {I : Type u} →
  (R : Type v) →
    [inst : CommSemiring R] →
      (A : I → Type w) → [inst_1 : (i : I) → Semiring (A i)] → [(i : I) → Algebra R (A i)] → Type (max (max w u) v)
-- Mathlib.RingTheory.KrullDimension.Basic
/-- A ring has finite Krull dimension if its `PrimeSpectrum` is
finite-dimensional (and non-empty).  -/
FiniteRingKrullDim : (R : Type u_3) → [CommSemiring R] → Prop
-- Mathlib.Geometry.Manifold.StructureGroupoid
StructureGroupoid.restr_mem_of_eqOn : ∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G]
  {e e' : OpenPartialHomeomorph H H},
  e ∈ G → ∀ {s : Set H}, IsOpen s → Set.EqOn (↑e) (↑e') s → e'.source ∩ s ⊆ e.source → e'.restr s ∈ G
-- Lean.Elab.Match
/-- Easy case: elaborate discriminant when the match-type has been explicitly provided by the user.   -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchTypeAndDiscrs.elabDiscrsWithMatchType : Array Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM (Array Lean.Elab.Term.Discr × Bool)
-- Mathlib.RingTheory.Ideal.Over
Ideal.LiesOver.over : ∀ {A : Type u_2} {inst : CommSemiring A} {B : Type u_3} {inst_1 : Semiring B} {inst_2 : Algebra A B} {P : Ideal B}
  {p : Ideal A} [self : P.LiesOver p], p = Ideal.under A P
-- Mathlib.CategoryTheory.Sites.LocalSite
CategoryTheory.GrothendieckTopology.IsLocalSite.instFaithfulSheafCoconstantSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_2 : J.IsLocalSite] (A : Type u')
  [inst_3 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  [inst_5 : CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A],
  (CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A).Faithful
-- Mathlib.GroupTheory.ResiduallyFinite
AddGroup.residuallyFinite_def : ∀ {G : Type u_1} [inst : AddGroup G], AddGroup.ResiduallyFinite G ↔ ⨅ H, H.toAddSubgroup = ⊥
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.instMonoCommRingCatToTotalQuotientPresheafPresheaf : ∀ {X : TopCat} (F : TopCat.Sheaf CommRingCat X), CategoryTheory.Mono F.presheaf.toTotalQuotientPresheaf
-- Init.Data.Nat.Basic
Nat.mul_one : ∀ (n : ℕ), n * 1 = n
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IndepSetFree.eq_1 : ∀ {α : Type u_1} (G : SimpleGraph α) (n : ℕ), G.IndepSetFree n = ∀ (t : Finset α), ¬G.IsNIndepSet n t
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.vlt_of_vle_of_vlt`. -/
ValuativeRel.vle.trans_vlt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, x ≤ᵥ y → y <ᵥ z → x <ᵥ z
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_eq_sum : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [L.LeAtTop] {s : Finset β}, (∀ b ∉ s, f b = 0) → ∑'[L] (b : β), f b = ∑ b ∈ s, f b
-- Mathlib.Algebra.Module.Defs
/-- A semiring is `Nontrivial` provided that there exists a nontrivial module over this semiring.  -/
Module.nontrivial : ∀ (R : Type u_5) (M : Type u_6) [inst : MonoidWithZero R] [Nontrivial M] [inst_2 : Zero M] [MulActionWithZero R M],
  Nontrivial R
-- Mathlib.Analysis.Fourier.FourierTransform
Real.vector_fourierIntegral_eq_integral_exp_smul : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_4} [inst_2 : AddCommGroup V]
  [inst_3 : Module ℝ V] [inst_4 : MeasurableSpace V] {W : Type u_5} [inst_5 : AddCommGroup W] [inst_6 : Module ℝ W]
  (L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ) (μ : MeasureTheory.Measure V) (f : V → E) (w : W),
  VectorFourier.fourierIntegral Real.fourierChar μ L f w =
    ∫ (v : V), Complex.exp (↑(-2 * Real.pi * (L v) w) * Complex.I) • f v ∂μ
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.incMatrix_mul_transpose_diag : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : NonAssocSemiring R] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] {a : α} [inst_3 : Fintype (Sym2 α)] [inst_4 : Fintype ↑(G.neighborSet a)],
  (SimpleGraph.incMatrix R G * (SimpleGraph.incMatrix R G).transpose) a a = ↑(G.degree a)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.one_def : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁], 1 = ContinuousLinearMap.id R₁ M₁
-- Mathlib.RingTheory.Perfection
Perfection.pthRootMonoidHom_eq_powMulEquiv_symm : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ}, Perfection.pthRootMonoidHom M p = ↑(powMulEquiv (Perfection M p) p).symm
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_le_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} (hc : Std.Internal.List.containsKey k l = true), (compare (Std.Internal.List.minKey l ⋯) k).isLE = true
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    ⟨k, v⟩ ∈ l → (Std.DHashMap.Raw.ofList l).getD k' fallback = cast ⋯ v
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- Special case of `zeta_eq_tsum_one_div_nat_cpow` when the argument is in `ℕ`, so the power
function can be expressed using naïve `pow` rather than `cpow`.  -/
zeta_nat_eq_tsum_of_gt_one : ∀ {k : ℕ}, 1 < k → riemannZeta ↑k = ∑' (n : ℕ), 1 / ↑n ^ k
-- Mathlib.RingTheory.SurjectiveOnStalks
/-- If `R → T` is surjective on stalks, and `J` is some prime of `T`,
then every element `x` in `S ⊗[R] T` satisfies `(1 ⊗ r • t) * x = a ⊗ t` for some
`r : R`, `a : S`, and `t : T` such that `r • t ∉ J`.
 -/
RingHom.SurjectiveOnStalks.exists_mul_eq_tmul : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {T : Type u_3} [inst_2 : CommRing T]
  [inst_3 : Algebra R T] [inst_4 : Algebra R S],
  (algebraMap R T).SurjectiveOnStalks →
    ∀ (x : TensorProduct R S T) (J : Ideal T), J.IsPrime → ∃ t r a, r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_pow : ∀ {α : Type u_1} [inst : Lean.Grind.CommSemiring α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly)
  (k : ℕ), p.NonnegCoeffs → Lean.Grind.CommRing.Poly.denoteS ctx (p.pow k) = Lean.Grind.CommRing.Poly.denoteS ctx p ^ k
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.symm_apply_mem_iff : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
  e.IsImage s t → ∀ ⦃y : β⦄, y ∈ e.target → (↑e.symm y ∈ s ↔ y ∈ t)
-- Mathlib.Order.Atoms
IsCoatom.not_codisjoint_iff_le : ∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α}, IsCoatom a → (¬Codisjoint a b ↔ b ≤ a)
-- Init.Data.Iterators.Consumers.Access
/-- Returns the `n`-th value emitted by `it`, or `none` if `it` terminates earlier.

For monadic iterators, the monadic effects of this operation may differ from manually iterating
to the `n`-th value because `atIdx?` can take shortcuts. By the signature, the return value
is guaranteed to plausible in the sense of `IterM.IsPlausibleNthOutputStep`.

This function is only available for iterators that explicitly support it by implementing
the `IteratorAccess` typeclass.
 -/
Std.Iter.atIdx? : {α β : Type u_1} → [inst : Std.Iterator α Id β] → [Std.IteratorAccess α Id] → ℕ → Std.Iter β → Option β
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_eq_getD_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} [inst_1 : Inhabited (β a)], t.get! a = t.getD a default
-- Mathlib.Data.Finmap
Finmap.insert.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) (s : Finmap β),
  Finmap.insert a b s = s.liftOn (fun t => (AList.insert a b t).toFinmap) ⋯
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → ∀ {h : k' ∈ m.insertMany l}, (m.insertMany l)[k'] = v
-- Lean.Widget.InteractiveCode
Lean.Widget.CodeWithInfos.mergePosMap : {m : Type → Type u_1} →
  {α : Type u_2} →
    [Monad m] →
      (Lean.Widget.SubexprInfo → α → m Lean.Widget.SubexprInfo) →
        Lean.SubExpr.PosMap α → Lean.Widget.CodeWithInfos → m Lean.Widget.CodeWithInfos
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- The constant coefficient of a formal power series.  -/
MvPowerSeries.constantCoeff : {σ : Type u_1} → {R : Type u_2} → [inst : Semiring R] → MvPowerSeries σ R →+* R
-- Mathlib.Algebra.Notation.Support
Function.disjoint_mulSupport_iff : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] {f : ι → M} {s : Set ι},
  Disjoint s (Function.mulSupport f) ↔ Set.EqOn f 1 s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.keys_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter! f t).keys =
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (t.get x ⋯))
        t.keys.attach).unattach
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.ext_iff : ∀ {X : Type u_3} {x y : FundamentalGroupoid X}, x = y ↔ x.as = y.as
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsEmbedding : (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] =>
    Topology.IsEmbedding).RespectsIso
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
LinearMap.mkContinuousOfExistsBound_coe : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Ring 𝕜] [inst_1 : Ring 𝕜₂]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜₂ F]
  {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (h : ∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖x‖), ↑(f.mkContinuousOfExistsBound h) = f
-- Mathlib.RingTheory.Polynomial.Content
/-- An irreducible nonconstant polynomial over a domain is primitive.  -/
Irreducible.isPrimitive : ∀ {R : Type u_1} [inst : CommSemiring R] [NoZeroDivisors R] {p : Polynomial R},
  Irreducible p → p.natDegree ≠ 0 → p.IsPrimitive
-- Lean.Server.ServerTask
Lean.Server.ServerTask.mk.injEq : ∀ {α : Type u} (task task_1 : Task α), ({ task := task } = { task := task_1 }) = (task = task_1)
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_ne_zero : ∀ (x : ℂ), Complex.exp x ≠ 0
-- Mathlib.Data.Fin.Rev
Fin.revPerm_symm : ∀ {n : ℕ}, Equiv.symm Fin.revPerm = Fin.revPerm
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.setTermStructId : Lean.Expr → Lean.Meta.Grind.Arith.Linear.LinearM Unit
-- Mathlib.CategoryTheory.FintypeCat
/-- If `u` and `v` are two arbitrary universes, we may construct a functor
`uSwitch.{u, v} : FintypeCat.{u} ⥤ FintypeCat.{v}` by sending
`X : FintypeCat.{u}` to `ULift.{v} (Fin (Fintype.card X))`.  -/
FintypeCat.uSwitch : CategoryTheory.Functor FintypeCat FintypeCat
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.sublist : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.Red.Step L₁ L₂ → L₂.Sublist L₁
-- Mathlib.Order.UpperLower.Basic
isUpperSet_iff_forall_lt : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α}, IsUpperSet s ↔ ∀ ⦃a b : α⦄, a < b → a ∈ s → b ∈ s
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
AnalyticAt.differentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E}, AnalyticAt 𝕜 f x → DifferentiableAt 𝕜 f x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.preconnected_top : ∀ {V : Type u}, ⊤.Preconnected
-- Mathlib.Logic.Equiv.Fintype
Equiv.Perm.viaFintypeEmbedding_apply_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (e : Equiv.Perm α) (f : α ↪ β) (a : α),
  (e.viaFintypeEmbedding f) (f a) = f (e a)
-- Std.Data.String.ToInt
_private.Std.Data.String.ToInt.0.String.Slice.isInt.match_1.splitter : (motive : Option String.Slice → Sort u_1) →
  (x : Option String.Slice) → ((rest : String.Slice) → motive (some rest)) → (Unit → motive none) → motive x
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_eq_some_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] (he : t ≠ ∅),
  t.max? = some (t.max he)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.edist_dist : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f g : ↥(MeasureTheory.Lp E p μ)), edist f g = ENNReal.ofReal (dist f g)
-- Mathlib.Algebra.Module.LinearMap.End
/-- The tautological action by `Module.End R M` (aka `M →ₗ[R] M`) on `M`.

This generalizes `Function.End.applyMulAction`.  -/
Module.End.applyModule : {R : Type u_1} →
  {M : Type u_4} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Module (Module.End R M) M
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.self_cocomplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) [inst_3 : CategoryTheory.Injective Z],
  (CategoryTheory.InjectiveResolution.self Z).cocomplex = (CochainComplex.single₀ C).obj Z
-- Std.Async.System
/-- A group identifier, represented by a numeric ID in UNIX systems (e.g. 1000).
 -/
Std.Async.System.GroupId : Type
-- Mathlib.LinearAlgebra.TensorProduct.Basis
/-- Given a basis `ℬ` of `M`, `x ∈ M ⊗ N` can be written as `∑ᵢ ℬ i ⊗ nᵢ`. The coefficient `nᵢ`
equals the `i`-th coordinate functional applied to the left tensor factor.  -/
TensorProduct.equivFinsuppOfBasisLeft_apply : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq ι]
  (ℬ : Module.Basis ι R M) (x : TensorProduct R M N) (i : ι),
  ((TensorProduct.equivFinsuppOfBasisLeft ℬ) x) i = (TensorProduct.lid R N) ((LinearMap.rTensor N (ℬ.coord i)) x)
-- Mathlib.Combinatorics.Enumerative.Composition
/-- List of positive integers summing to `n`  -/
Composition.blocks : {n : ℕ} → Composition n → List ℕ
-- Mathlib.RingTheory.Localization.FractionRing
FractionRing.isScalarTower_liftAlgebra : ∀ (R : Type u_1) [inst : CommRing R] (K : Type u_5) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : FaithfulSMul R K], IsScalarTower R (FractionRing R) K
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mk_eq_one_iff : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Invertible R M], CommRing.Pic.mk R M = 1 ↔ Nonempty (M ≃ₗ[R] R)
-- Mathlib.Algebra.Module.PUnit
PUnit.instSMulZeroClass : {R : Type u_1} → [inst : Zero R] → SMulZeroClass PUnit.{u_3 + 1} R
-- Mathlib.CategoryTheory.Join.Sum
/-- Characterization of `fromSum` with respect to the right inclusion.  -/
CategoryTheory.Join.inrCompFromSum : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (CategoryTheory.Sum.inr_ C D).comp (CategoryTheory.Join.fromSum C D) ≅ CategoryTheory.Join.inclRight C D
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.neg_mk : ∀ {α : Type u} {L : List (α × Bool)}, -FreeAddGroup.mk L = FreeAddGroup.mk (FreeAddGroup.negRev L)
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.hom_ext : ∀ {R : Type u} [inst : CommRing R] {M N : CoalgCat R} (f g : M ⟶ N),
  CoalgCat.Hom.toCoalgHom f = CoalgCat.Hom.toCoalgHom g → f = g
-- Mathlib.Order.SetDissipate
Set.exists_dissipate_eq_empty_iff_of_directed : ∀ {α : Type u_1} {s : ℕ → Set α}, Directed (fun x1 x2 => x1 ⊇ x2) s → ((∃ n, Set.dissipate s n = ∅) ↔ ∃ n, s n = ∅)
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of the forward direction of `Order.succ_le_succ_iff`. -/
Order.le_of_succ_le_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  Order.succ a ≤ Order.succ b → a ≤ b
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Functor.instEssSurjQuotientHomRelLift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) [L.EssSurj],
  (CategoryTheory.Quotient.lift L.homRel L ⋯).EssSurj
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.preEquivalence.functor_obj_left : ∀ {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 : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e)
  (g : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f),
  ((CategoryTheory.CostructuredArrow.preEquivalence.functor F f).obj g).left = g.left.left
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.brecOn.eq : ∀ {motive_1 : Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u}
  {motive_2 : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u}
  {motive_3 : List (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u}
  {motive_4 : String × Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u} (t : Lean.Elab.ConfigEval.HandlerTrie✝)
  (F_1 : (t : Lean.Elab.ConfigEval.HandlerTrie✝) → Lean.Elab.ConfigEval.HandlerTrie.below✝ t → motive_1 t)
  (F_2 :
    (t : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝)) → Lean.Elab.ConfigEval.HandlerTrie.below_1✝ t → motive_2 t)
  (F_3 :
    (t : List (String × Lean.Elab.ConfigEval.HandlerTrie✝)) → Lean.Elab.ConfigEval.HandlerTrie.below_2✝ t → motive_3 t)
  (F_4 : (t : String × Lean.Elab.ConfigEval.HandlerTrie✝) → Lean.Elab.ConfigEval.HandlerTrie.below_3✝ t → motive_4 t),
  Lean.Elab.ConfigEval.HandlerTrie.brecOn✝ t F_1 F_2 F_3 F_4 =
    F_1 t (Lean.Elab.ConfigEval.HandlerTrie.brecOn.go✝ t F_1 F_2 F_3 F_4).2
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.toTree.processBinOp : Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Elab.TermElabM FBinopElab.Tree✝
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.unop_inv_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : Cᵒᵖ),
  (β_ X Y).inv.unop = (β_ (Opposite.unop Y) (Opposite.unop X)).inv
-- Lean.Parser.Term.Basic
Lean.Parser.Term.optType : Lean.Parser.Parser
-- Init.Data.List.Count
List.count_le_count_cons : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {l : List α}, List.count a l ≤ List.count a (b :: l)
-- Init.Data.Nat.Lemmas
Nat.decidableExistsFin : {n : ℕ} → (P : Fin n → Prop) → [DecidablePred P] → Decidable (∃ i, P i)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedState.mk.sizeOf_spec : ∀ («meta» : Lean.Meta.SavedState) («elab» : Lean.Elab.Term.State),
  sizeOf { «meta» := «meta», «elab» := «elab» } = 1 + sizeOf «meta» + sizeOf «elab»
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_strictMonoOn : StrictMonoOn (⇑Cardinal.toENat) (Set.Iic Cardinal.aleph0)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodePi.match_1.eq_1 : ∀ (n : ℕ) (motive : Fin n → Sort u_1) (i : ℕ) (hi : i < n) (h_1 : (i : ℕ) → (hi : i < n) → motive ⟨i, hi⟩),
  (match ⟨i, hi⟩ with
    | ⟨i, hi⟩ => h_1 i hi) =
    h_1 i hi
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.shortComplexTruncLEX₃ToTruncGE.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℤ) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁),
  K.shortComplexTruncLEX₃ToTruncGE n₀ n₁ h = K.shortComplexTruncLEX₃ToTruncGE n₀ n₁ h
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsAdjointPair.comp : ∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M₂] [inst_7 : AddCommMonoid M₃] [inst_8 : Module R M₃] {I : R →+* R}
  {B : M →ₗ[R] M →ₛₗ[I] M₃} {B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃} {B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] M₃} {f : M → M₁} {g : M₁ → M}
  {f' : M₁ → M₂} {g' : M₂ → M₁},
  B.IsAdjointPair B' f g → B'.IsAdjointPair B'' f' g' → B.IsAdjointPair B'' (f' ∘ f) (g ∘ g')
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.le_expect : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : Module ℚ≥0 α] {s : Finset ι} {f : ι → α} [PosSMulMono ℚ≥0 α] {a : α},
  s.Nonempty → (∀ x ∈ s, a ≤ f x) → a ≤ s.expect fun i => f i
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.norm_of : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), (FreeAddGroup.of a).norm = 1
-- Mathlib.Order.Lex
toColex_inj : ∀ {α : Type u_1} {a b : α}, toColex a = toColex b ↔ a = b
-- Mathlib.Data.Finsupp.ToDFinsupp
sigmaFinsuppLequivDFinsupp_apply : ∀ {ι : Type u_1} (R : Type u_2) {η : ι → Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid N]
  [inst_2 : Module R N] (a : (i : ι) × η i →₀ N),
  (sigmaFinsuppLequivDFinsupp R) a = sigmaFinsuppAddEquivDFinsupp.toFun a
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.expPartialHomeomorph_apply : ∀ (x : ℝ), ↑Real.expPartialHomeomorph x = Real.exp x