mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A partial diffeomorphism is also a local homeomorphism.  -/
PartialDiffeomorph.toOpenPartialHomeomorph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        {I : ModelWithCorners 𝕜 E H₁} →
                          {J : ModelWithCorners 𝕜 F H₂} →
                            {M : Type u_8} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H₁ M] →
                                  {N : Type u_9} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H₂ N] →
                                        {n : WithTop ℕ∞} → PartialDiffeomorph I J M N n → OpenPartialHomeomorph M N
-- Std.Sat.AIG.Basic
Std.Sat.AIG.CacheHit.mk : {α : Type} →
  {decls : Array (Std.Sat.AIG.Decl α)} →
    {decl : Std.Sat.AIG.Decl α} →
      (idx : ℕ) → (hbound : idx < decls.size) → decls[idx] = decl → Std.Sat.AIG.CacheHit decls decl
-- Mathlib.RingTheory.Ideal.Maps
AlgHom.coe_ideal_map : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (I : Ideal A), Ideal.map f I = Ideal.map (↑f) I
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallCache.mk''.injEq : ∀ (callerName : Lean.Name) (decrTactic? : Option Lean.Elab.DecreasingBy)
  (callerMeasures calleeMeasures : Array Lean.Elab.WF.GuessLex.BasicMeasure)
  (rcc : Lean.Elab.WF.GuessLex.RecCallWithContext)
  (cache : IO.Ref (Array (Array (Option Lean.Elab.WF.GuessLex.GuessLexRel)))) (callerName_1 : Lean.Name)
  (decrTactic?_1 : Option Lean.Elab.DecreasingBy)
  (callerMeasures_1 calleeMeasures_1 : Array Lean.Elab.WF.GuessLex.BasicMeasure)
  (rcc_1 : Lean.Elab.WF.GuessLex.RecCallWithContext)
  (cache_1 : IO.Ref (Array (Array (Option Lean.Elab.WF.GuessLex.GuessLexRel)))),
  ({ callerName := callerName, decrTactic? := decrTactic?, callerMeasures := callerMeasures,
        calleeMeasures := calleeMeasures, rcc := rcc, cache := cache } =
      { callerName := callerName_1, decrTactic? := decrTactic?_1, callerMeasures := callerMeasures_1,
        calleeMeasures := calleeMeasures_1, rcc := rcc_1, cache := cache_1 }) =
    (callerName = callerName_1 ∧
      decrTactic? = decrTactic?_1 ∧
        callerMeasures = callerMeasures_1 ∧ calleeMeasures = calleeMeasures_1 ∧ rcc = rcc_1 ∧ cache = cache_1)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [inst_3 : CategoryTheory.IsIso h],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).inv
      (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h
-- Mathlib.Topology.MetricSpace.Infsep
Set.Finite.einfsep_pos : ∀ {α : Type u_1} [inst : EMetricSpace α] {s : Set α}, s.Finite → 0 < s.einfsep
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_neg : ∀ (x : GaussianInt), GaussianInt.toComplex (-x) = -GaussianInt.toComplex x
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f)
  (X : ↑(F.obj b₀)),
  (F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp
        ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X))
        ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X))
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_ι_assoc : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : ↥X) (hxU : x ∈ U) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) (CategoryTheory.CategoryStruct.comp U.ι h) =
    CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) h
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
Matrix.discr.congr_simp : ∀ {R : Type u_1} {n : Type u_2} [inst : CommRing R] [inst_1 : Fintype n] {inst_2 : DecidableEq n}
  [inst_3 : DecidableEq n] (A A_1 : Matrix n n R), A = A_1 → A.discr = A_1.discr
-- Mathlib.Topology.Algebra.ProperConstSMul
ProperConstSMul.mk : ∀ {M : Type u_1} {X : Type u_2} [inst : SMul M X] [inst_1 : TopologicalSpace X],
  (∀ (c : M), IsProperMap fun x => c • x) → ProperConstSMul M X
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeSubtype.match_1.eq_1 : ∀ (n : ℕ) (P : Fin (n + 1) → Prop) (motive : { i // P i.succ } → Sort u_1) (i : ℕ) (hi : i < n) (hp : P ⟨i, hi⟩.succ)
  (h_1 : (i : ℕ) → (hi : i < n) → (hp : P ⟨i, hi⟩.succ) → motive ⟨⟨i, hi⟩, hp⟩),
  (match ⟨⟨i, hi⟩, hp⟩ with
    | ⟨⟨i, hi⟩, hp⟩ => h_1 i hi hp) =
    h_1 i hi hp
-- Mathlib.Order.Closure
/-- Closures are idempotent  -/
ClosureOperator.idempotent' : ∀ {α : Type u_1} [inst : Preorder α] (self : ClosureOperator α) (x : α), self.toFun (self.toFun x) = self.toFun x
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.ssubset_univ_iff : ∀ {α : Type u_1} [inst : Fintype α] {s : Finset α}, s ⊂ Finset.univ ↔ s ≠ Finset.univ
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.homQuotientZPowOfHom_comp : ∀ {A B : Type u} [inst : CommGroup A] [inst_1 : CommGroup B] (f : A →* B) (g : B →* A) (n : ℤ),
  QuotientGroup.homQuotientZPowOfHom (f.comp g) n =
    (QuotientGroup.homQuotientZPowOfHom f n).comp (QuotientGroup.homQuotientZPowOfHom g n)
-- Mathlib.Algebra.Module.Presentation.Differentials
/-- Same as `comm₂₃` below, but here we have not yet constructed `differentialsSolution`.  -/
Algebra.Presentation.differentials.comm₂₃' : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (pres : Algebra.Presentation R S ι σ),
  pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm =
    Finsupp.linearCombination S fun g => (KaehlerDifferential.D R S) (pres.val g)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.AtPrime.instIsLiesOverAlgebra : ∀ {A : Type u_4} {B : Type u_5} [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Algebra A B] (p : Ideal A)
  [inst_3 : p.IsPrime] (P : Ideal B) [inst_4 : P.IsPrime] [inst_5 : P.LiesOver p],
  Localization.AtPrime.IsLiesOverAlgebra p P
-- Mathlib.RingTheory.Ideal.Basis
/-- If `I : Ideal S` has a basis over `R`,
`x ∈ I` iff it is a linear combination of basis vectors.  -/
Basis.mem_ideal_iff : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  {I : Ideal S} (b : Module.Basis ι R ↥I) {x : S}, x ∈ I ↔ ∃ c, x = c.sum fun i x => x • ↑(b i)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- The yoneda embedding for `Mon C` is fully faithful.  -/
CategoryTheory.yonedaMonFullyFaithful : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.yonedaMon.FullyFaithful
-- Mathlib.Data.Sum.Basic
Sum.LiftRel.exists_of_isLeft_right : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ},
  Sum.LiftRel r s x y → y.isLeft = true → ∃ a c, r a c ∧ x = Sum.inl a ∧ y = Sum.inl c
-- Lean.Parser.Term
Lean.Parser.Term.throwNamedErrorMacro.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Coalgebra.Basic
Finsupp.instCoalgebraStruct : (R : Type u) →
  (ι : Type v) →
    (A : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [CoalgebraStruct R A] → CoalgebraStruct R (ι →₀ A)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.isoMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra}
  (h h_1 : A.A ≅ B.A) (e_h : h = h_1)
  (w : CategoryTheory.CategoryStruct.comp (T.map h.hom) B.a = CategoryTheory.CategoryStruct.comp A.a h.hom),
  CategoryTheory.Monad.Algebra.isoMk h w = CategoryTheory.Monad.Algebra.isoMk h_1 ⋯
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instIsStableUnderShiftTop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A], ⊤.IsStableUnderShift A
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The weak operator topology is the coarsest topology such that `fun A => y (A x)` is
continuous for all `x, y`.  -/
ContinuousLinearMapWOT.instTopologicalSpace : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_3} →
            {F : Type u_4} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : Module 𝕜₂ F] →
                          [IsTopologicalAddGroup F] → [ContinuousConstSMul 𝕜₂ F] → TopologicalSpace (E →SWOT[σ] F)
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.ofHom_hom : ∀ {X Y : GrpCat} (f : X ⟶ Y), GrpCat.ofHom (GrpCat.Hom.hom f) = f
-- Mathlib.Data.List.Cycle
List.next_getLast_cons : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α),
  ∀ x ∈ l, ∀ (y : α) (h : x ∈ y :: l), x ≠ y → x = (y :: l).getLast ⋯ → l.Nodup → (y :: l).next x h = y
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasProd_one_iff_of_one_le : ∀ {ι : Type u_4} {α : Type u_5} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : PartialOrder α]
  [IsOrderedMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} [L.LeAtTop] [L.NeBot],
  (∀ (i : ι), 1 ≤ f i) → (HasProd f 1 L ↔ f = 1)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProdNat.mul.sizeOf_spec : ∀ {x e b : Q(ℕ)} (a : Mathlib.Tactic.Ring.Common.ExBaseNat x) (a_1 : Mathlib.Tactic.Ring.Common.ExProdNat e)
  (a_2 : Mathlib.Tactic.Ring.Common.ExProdNat b),
  sizeOf (Mathlib.Tactic.Ring.Common.ExProdNat.mul a a_1 a_2) =
    1 + sizeOf x + sizeOf e + sizeOf b + sizeOf a + sizeOf a_1 + sizeOf a_2
-- Lean.Elab.PreDefinition.FixedParams
/-- Intersperses the fixed and varying parameters to be in the original parameter order.
Can handle over- or under-application (extra or missing varying args), as long
as there are all varying parameters that go before fixed parameters.
(We expect to always find all fixed parameters, else they wouldn't be fixed parameters.)
 -/
Lean.Elab.FixedParamPerm.buildArgs : {α : Type u_1} → Lean.Elab.FixedParamPerm → Array α → Array α → Array α
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv_apply : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] (e : R ≃+* S)
  (v : IsDedekindDomain.HeightOneSpectrum R),
  (IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv e) v = IsDedekindDomain.HeightOneSpectrum.comap ↑e.symm ⋯ v
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_union_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.contains k m₂ = false →
    Std.DTreeMap.Internal.Impl.Const.get! (m₁.union m₂ ⋯ ⋯) k = Std.DTreeMap.Internal.Impl.Const.get! m₁ k
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.mem_closure_self : ∀ {α : Type u_2} (M : Matroid α) (e : α), autoParam (e ∈ M.E) Matroid.mem_closure_self._auto_1 → e ∈ M.closure {e}
-- Mathlib.Order.Bounds.Image
BddAbove.range_comp_left : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {g : β → γ},
  BddAbove (Set.range f) → Monotone g → BddAbove (Set.range fun x => g (f x))
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
/-- The cohomological degree of objects in the pages  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg : {ι : Type u_2} →
  {κ : Type u_3} →
    [inst : Preorder ι] →
      {c : ℤ → ComplexShape κ} →
        {r₀ : ℤ} → CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀ → κ → ℤ
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.prod_empty : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)], Monoid.CoprodI.Word.empty.prod = 1
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.finiteCoproduct.ι_desc : ∀ {P : TopCat → Prop} {α : Type w} [inst : Finite α] (X : α → CompHausLike P)
  [inst_1 : CompHausLike.HasExplicitFiniteCoproduct X] {B : CompHausLike P} (e : (a : α) → X a ⟶ B) (a : α),
  CategoryTheory.CategoryStruct.comp (CompHausLike.finiteCoproduct.ι X a) (CompHausLike.finiteCoproduct.desc X e) = e a
-- Init.Meta.Defs
Lean.Syntax.isLit? : Lean.SyntaxNodeKind → Lean.Syntax → Option String
-- Mathlib.Topology.Category.LightProfinite.Extend
LightProfinite.Extend.functor_map : ∀ {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite))
  {X Y : ℕᵒᵖ} (f : X ⟶ Y), (LightProfinite.Extend.functor c).map f = CategoryTheory.StructuredArrow.homMk (F.map f) ⋯
-- Std.Http.Data.Method
Std.Http.Method.merge.sizeOf_spec : sizeOf Std.Http.Method.merge = 1
-- Mathlib.Analysis.Convex.Cone.Dual
/-- Geometric interpretation of **Farkas' lemma**. Also stronger version of the
**Hahn-Banach separation theorem** for proper cones.  -/
ProperCone.hyperplane_separation : ∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [IsTopologicalAddGroup E] [inst_3 : Module ℝ E]
  [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {K : Set E} (C : ProperCone ℝ E),
  Convex ℝ K → IsCompact K → Disjoint K ↑C → ∃ f, (∀ x ∈ C, 0 ≤ f x) ∧ ∀ x ∈ K, f x < 0
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.apply_ne : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α}, f.IsCycleOn s → s.Nontrivial → a ∈ s → f a ≠ a
-- Std.Time.DateTime.PlainDateTime
Std.Time.instTransOrdPlainDateTime : Std.TransOrd Std.Time.PlainDateTime
-- Mathlib.InformationTheory.Hamming
Hamming.instSub : {ι : Type u_2} → {β : ι → Type u_3} → [(i : ι) → Sub (β i)] → Sub (Hamming β)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_eq_some_getKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  (h' : a ∈ t), t.getKey? a = some (t.getKey a h')
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.toSeq?.go : List Lean.Grind.AC.Var → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.toWord_inj : ∀ {α : Type u_1} [inst : DecidableEq α] {x y : FreeGroup α}, x.toWord = y.toWord ↔ x = y
-- Mathlib.RingTheory.FormalGroup.Basic
/-- An abbreviation of $F(X,0)$ for a formal group $F$.  -/
FormalGroup.Xzero : {R : Type u_1} → [inst : CommRing R] → FormalGroup R → PowerSeries R
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- For any element `a : A` and any set `B` in the submodule basis on `A`,
there is another basis element `B'` such that `a • B'` is in `B`.  -/
SubmodulesRingBasis.leftMul : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {B : ι → Submodule R A}, SubmodulesRingBasis B → ∀ (a : A) (i : ι), ∃ j, a • B j ≤ B i
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.add : ℤ → Int.Internal.Linear.Var → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.instLinearId : ∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C],
  CategoryTheory.Functor.Linear R (CategoryTheory.Functor.id C)
-- Mathlib.Data.Fintype.Perm
permsOfList.eq_def : ∀ {α : Type u_1} [inst : DecidableEq α] (x : List α),
  permsOfList x =
    match x with
    | [] => [1]
    | a :: l => permsOfList l ++ List.flatMap (fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l
-- Batteries.Lean.Meta.SavedState
/-- Returns the mvars that are not declared in `preState`, but declared and
unassigned in `postState`. Delayed-assigned mvars are considered assigned.
 -/
Lean.Meta.getIntroducedExprMVars : Lean.Meta.SavedState → Lean.Meta.SavedState → Lean.MetaM (Array Lean.MVarId)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- Notation for `Measure` with respect to a non-standard σ-algebra in the domain.  -/
MeasureTheory.«termMeasure[_]_» : Lean.ParserDescr
-- Mathlib.Order.Monotone.Basic
StrictAnti.wellFoundedGT : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} [WellFoundedLT β],
  StrictAnti f → WellFoundedGT α
-- Lean.Parser.Term
Lean.Parser.Term.whereDecls.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.State.exprToStructId : Lean.Meta.Grind.Arith.Linear.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Suggest merging `tac; grind` into just `grind` if that also solves the goal.  -/
linter.tacticAnalysis.mergeWithGrind : Lean.Option Bool
-- Mathlib.FieldTheory.Differential.Basic
Differential.instAdjoinRootOfIrreduciblePolynomialOfFactMonic : {F : Type u_2} →
  [inst : Field F] →
    [Differential F] →
      [CharZero F] → (p : Polynomial F) → [Fact (Irreducible p)] → [Fact p.Monic] → Differential (AdjoinRoot p)
-- Lean.Meta.Tactic.Grind.PP
Lean.Meta.Grind.ppEqc : List Lean.Expr → optParam (Array Lean.MessageData) #[] → Lean.MessageData
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise multiplication of
`f` and `g`, which monovary together on `s`, is strictly decreased by a permutation if and only if
`f ∘ σ` and `g` do not monovary together on `s`. Stated by permuting the entries of `f`.  -/
MonovaryOn.sum_comp_perm_mul_lt_sum_mul_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
  MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f (σ i) * g i < ∑ i ∈ s, f i * g i ↔ ¬MonovaryOn (f ∘ ⇑σ) g ↑s)
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.comp_toCoalgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C] (φ₁ : B →ₐc[R] C)
  (φ₂ : A →ₐc[R] B), ↑(φ₁.comp φ₂) = (↑φ₁).comp ↑φ₂
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∈ t₂ → (t₁ \ t₂).getD k fallback = fallback
-- Mathlib.Logic.Relation
Relation.EqvGen.below.refl : ∀ {α : Type u_1} {r : α → α → Prop} {motive : (a a_1 : α) → Relation.EqvGen r a a_1 → Prop} (x : α),
  Relation.EqvGen.below ⋯
-- Init.Core
/-- Delays evaluation. The delayed code is evaluated at most once.

A thunk is code that constructs a value when it is requested via `Thunk.get`, `Thunk.map`, or
`Thunk.bind`. The resulting value is cached, so the code is executed at most once. This is also
known as lazy or call-by-need evaluation.

The Lean runtime has special support for the `Thunk` type in order to implement the caching
behavior.
 -/
Thunk : Type u → Type u
-- Mathlib.Topology.Algebra.UniformRing
/-- A ring isomorphism `α ≃+* β` between uniform rings, uniformly continuous in both directions,
lifts to a ring isomorphism between corresponding uniform space completions.  -/
UniformSpace.Completion.mapRingEquiv : {α : Type u_1} →
  [inst : Ring α] →
    [inst_1 : UniformSpace α] →
      [IsTopologicalRing α] →
        [IsUniformAddGroup α] →
          {β : Type u} →
            [inst_4 : UniformSpace β] →
              [inst_5 : Ring β] →
                [IsUniformAddGroup β] →
                  [IsTopologicalRing β] →
                    (f : α ≃+* β) →
                      Continuous ⇑f → Continuous ⇑f.symm → UniformSpace.Completion α ≃+* UniformSpace.Completion β
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.isZero_trivial : ∀ (D : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D], CategoryTheory.Limits.IsZero (CategoryTheory.Mon.trivial D)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b c : E} {ω : E → E →L[𝕜] F}
  {γab : Path a b},
  CurveIntegrable ω γab →
    ∀ (γbc : Path b c), IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) MeasureTheory.volume 0 (1 / 2)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.size_toArray : ∀ {α : Type u} {r : Std.Rio α} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxo.HasSize α] [inst_5 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.Rxo.IsAlwaysFinite α] [Std.Rxo.LawfulHasSize α],
  r.toArray.size = r.size
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.IsWeaklyEisensteinAt.mem : ∀ {R : Type u} [inst : CommSemiring R] {f : Polynomial R} {𝓟 : Ideal R},
  f.IsWeaklyEisensteinAt 𝓟 → ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.copy_eq : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂)
  (h : f' = ⇑f), f.copy f' h = f
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.toPoly'.go.eq_2 : ∀ (coeff : ℤ) (v : Int.Internal.Linear.Var),
  Int.Internal.Linear.Expr.toPoly'.go coeff (Int.Internal.Linear.Expr.var v) = fun x =>
    Int.Internal.Linear.Poly.add coeff v x
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.ne_zero : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : Zero α] [IsBotZeroClass α], Order.IsSuccLimit a → a ≠ 0
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertEntryIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)),
  Std.Internal.List.insertEntryIfNew k v l = bif Std.Internal.List.containsKey k l then l else ⟨k, v⟩ :: l
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.orthonormal : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E), Orthonormal 𝕜 ⇑b