mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_const_mul_self : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] (c : R) (f : α → R) (l : Filter α),
  Asymptotics.IsBigOWith ‖c‖ l (fun x => c * f x) f
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.negPart.eq_1 : ∀ {α : Type u_1} {E : Type u_2} [inst : LinearOrder E] [inst_1 : Zero E] [inst_2 : MeasurableSpace α] [inst_3 : Neg E]
  (f : MeasureTheory.SimpleFunc α E), f.negPart = (-f).posPart
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- Identity map as a `ContinuousAffineEquiv`.  -/
ContinuousAffineEquiv.refl : (k : Type u_1) →
  (P₁ : Type u_2) →
    {V₁ : Type u_6} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] →
          [inst_2 : Module k V₁] → [inst_3 : AddTorsor V₁ P₁] → [inst_4 : TopologicalSpace P₁] → P₁ ≃ᴬ[k] P₁
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.unitOfList_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α},
  (Std.TreeMap.unitOfList l cmp).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) ∅ l)
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.trace_natCast : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (n : ℕ), QuadraticAlgebra.trace ↑n = 2 * ↑n
-- Mathlib.FieldTheory.IntermediateField.Algebraic
_private.Mathlib.FieldTheory.IntermediateField.Algebraic.0.IntermediateField.eq_of_le_of_finrank_le'' : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  [FiniteDimensional K L], F ≤ E → Module.finrank (↥F) L ≤ Module.finrank (↥E) L → F = E
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.mem_support_iff_exists_mem_edges_of_not_nil : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v}, ¬p.Nil → (w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e)
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.sInf_univ : sInf Set.univ = 0
-- Mathlib.Order.RelSeries
RelSeries.head_smash : ∀ {α : Type u_1} {r : SetRel α α} {p q : RelSeries r} (h : p.last = q.head), (p.smash q h).head = p.head
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.addCommGroup_isAddCommutative : ∀ {G : Type u_3} [inst : AddCommGroup G] (H : AddSubgroup G), IsAddCommutative ↥H
-- Mathlib.Tactic.NormNum.Result
Rat.rawCast.eq_1 : ∀ {α : Type u} [inst : DivisionRing α] (n : ℤ) (d : ℕ), Rat.rawCast n d = ↑n / ↑d
-- Lean.Parser.Types
Lean.Parser.Parser : Type
-- Lean.Structure
/-- The projection function associated to the field.  -/
Lean.StructureFieldInfo.projFn : Lean.StructureFieldInfo → Lean.Name
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.toList_ric : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.toList_ric._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet.Raw α cmp},
  t.WF →
    ∀ {bound : α},
      Std.Slice.toList (Std.Ric.Sliceable.mkSlice t *...=bound) = List.filter (fun e => (cmp e bound).isLE) t.toList
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment.eq_1 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos.addPosAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.evenEquivEvenNeg_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (a : ↥(CliffordAlgebra.even Q)),
  (CliffordAlgebra.evenEquivEvenNeg Q) a = (CliffordAlgebra.evenToNeg Q (-Q) ⋯) a
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.TriangleMorphism.comp_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ T₃ : CategoryTheory.Pretriangulated.Triangle C} (f : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂)
  (g : CategoryTheory.Pretriangulated.TriangleMorphism T₂ T₃),
  (f.comp g).hom₁ = CategoryTheory.CategoryStruct.comp f.hom₁ g.hom₁
-- Mathlib.RingTheory.Ideal.Prime
Ideal.mem_primeCompl_iff : ∀ {α : Type u} [inst : Semiring α] {P : Ideal α} [inst_1 : P.IsPrime] {x : α}, x ∈ P.primeCompl ↔ x ∉ P
-- Mathlib.Order.Lattice
sup_eq_iff_inf_eq : ∀ {α : Type u} [inst : Lattice α] {a b : α}, a ⊔ b = b ↔ a ⊓ b = a
-- Init.Dynamic
_private.Init.Dynamic.0.DynamicPointed : NonemptyType
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.coe_mul : ∀ {G : Type u_1} [inst : Add G] {a : G} (f g : AddConstMap G G a a), ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddCancelMonoid : {α : Type u_1} → [AddCancelMonoid α] → AddCancelMonoid αᵒᵈ
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `vectorSpan` of a finite set is finite-dimensional.  -/
finiteDimensional_vectorSpan_of_finite : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P}, s.Finite → FiniteDimensional k ↥(vectorSpan k s)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.sigmaFinsetFunEquiv_apply_snd_coe : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (a : Π₀ (i : ι), β i)
  (i : ↥((Equiv.sigmaFiberEquiv DFinsupp.support).symm a).fst), ↑((DFinsupp.sigmaFinsetFunEquiv a).snd i) = a ↑i
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.support_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c), Function.support ↑f = Metric.ball c f.rOut
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- A space with `MeasurableSpace` and `TopologicalSpace` structures such that
the `σ`-algebra of measurable sets is exactly the `σ`-algebra generated by open sets.  -/
BorelSpace : (α : Type u_6) → [TopologicalSpace α] → [MeasurableSpace α] → Prop
-- Aesop.Frontend.Saturate
Aesop.Frontend.elabGlobalRuleSets : Array Lean.Ident → Lean.CoreM (Array (Aesop.GlobalRuleSet × Lean.Name × Lean.Name))
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.inlCompSum'_inv_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A C)
  (G : CategoryTheory.Functor B C) (X : A),
  (F.inlCompSum' G).inv.app X = CategoryTheory.CategoryStruct.id ((F.sum' G).obj (Sum.inl X))
-- Mathlib.Order.Iterate
Function.monotone_iterate_of_id_le : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α}, id ≤ f → Monotone fun m => f^[m]
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.ShiftSequence.shiftIso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] (n a a' : ℤ) (ha' : n + a = a') (K : CochainComplex C ℤ),
  (CochainComplex.ShiftSequence.shiftIso C n a a' ha').hom.app K =
    CategoryTheory.ShortComplex.homologyMap ((CochainComplex.shiftShortComplexFunctorIso C n a a' ha').hom.app K)
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.lineCount_eq_lineCount : ∀ {P : Type u_1} (L : Type u_2) [inst : Membership P L] [Configuration.ProjectivePlane P L] [Finite P] [Finite L]
  (p q : P), Configuration.lineCount L p = Configuration.lineCount L q
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_const_smul_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_15} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : NormedDivisionRing 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [inst_3 : Module 𝕜 E'] [NormSMulClass 𝕜 E']
  {c : 𝕜}, c ≠ 0 → ((fun x => c • f' x) =o[l] g ↔ f' =o[l] g)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.union.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m₁ m₁_1 : Std.ExtDHashMap α β),
  m₁ = m₁_1 → ∀ (m₂ m₂_1 : Std.ExtDHashMap α β), m₂ = m₂_1 → m₁.union m₂ = m₁_1.union m₂_1
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.inertiaEquiv.eq_1 : ∀ {M : Type u_1} [inst : Group M] {N : Type u_4} [inst_1 : Group N] {R : Type u_5} [inst_2 : Ring R]
  [inst_3 : MulSemiringAction M R] [inst_4 : MulSemiringAction N R] (I : Ideal R) (e : M ≃* N)
  (he : ∀ (m : M) (x : R), e m • x = m • x), I.inertiaEquiv e he = { toEquiv := (↑e).subtypeEquiv ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Group.Center
Set.decidableMemAddCenter.eq_1 : ∀ {M : Type u_1} [inst : AddSemigroup M] [inst_1 : (a : M) → Decidable (∀ (b : M), b + a = a + b)] (x : M),
  Set.decidableMemAddCenter x = decidable_of_iff' (∀ (g : M), g + x = x + g) ⋯
-- Mathlib.Algebra.Star.Subalgebra
/-- Copy of a star subalgebra with a new `carrier` equal to the old one. Useful to fix definitional
equalities.  -/
StarSubalgebra.copy : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Algebra R A] →
              [inst_5 : StarModule R A] → (S : StarSubalgebra R A) → (s : Set A) → s = ↑S → StarSubalgebra R A
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- For a set `W`, `T` is a neighborhood of `1` which is open, stable under inverse and satisfies
`T * W ⊆ W`.  -/
IsTopologicalGroup.mulInvClosureNhd : {G : Type u_1} → [TopologicalSpace G] → Set G → Set G → [Group G] → Prop
-- Aesop.Tree.Data
Aesop.GoalData.depth : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → ℕ
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.ofObj_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {ι : Type u'} (X : ι → C) (Y : C),
  CategoryTheory.ObjectProperty.ofObj X Y ↔ ∃ i, X i = Y
-- Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
SSet.horn.face.congr_simp : ∀ {n : ℕ} (i j j_1 : Fin (n + 2)) (e_j : j = j_1) (h : j ≠ i), SSet.horn.face i j h = SSet.horn.face i j_1 ⋯
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coe_div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Group G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : LieGroup I' n G] (f g : ContMDiffMap I I' N G n), ⇑(f / g) = ⇑f / ⇑g
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.factor_δ_spec : ∀ {m n : ℕ} (f : { len := m } ⟶ { len := n + 1 }) (j : Fin (n + 2)),
  (∀ (k : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f) k ≠ j) →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.factor_δ f j) (SimplexCategory.δ j) = f
-- Mathlib.RingTheory.Trace.Basic
trace_eq_trace_adjoin : ∀ (K : Type u_4) {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L]
  (x : L),
  (Algebra.trace K L) x = Module.finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (IntermediateField.AdjoinSimple.gen K x)
-- Mathlib.Data.PFun
/-- Evaluate a partial function  -/
PFun.fn : {α : Type u_1} → {β : Type u_2} → (f : α →. β) → (a : α) → a ∈ f.Dom → β
-- Mathlib.Order.Hom.Lattice
LatticeHom.coe_comp_sup_hom' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  (f : LatticeHom β γ) (g : LatticeHom α β),
  { toFun := ⇑f ∘ ⇑g, map_sup' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }
-- Mathlib.MeasureTheory.Function.SimpleFunc
_private.Mathlib.MeasureTheory.Function.SimpleFunc.0.MeasureTheory.SimpleFunc.eapproxDiff.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPFieldNotationGeneralized : Lean.Options → Bool
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc).H = c.pt
-- Mathlib.Data.Num.ZNum
ZNum.bit1_of_bit1 : ∀ (n : ZNum), n + n + 1 = n.bit1
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
continuousAt_extChartAt' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x x' : M},
  x' ∈ (extChartAt I x).source → ContinuousAt (↑(extChartAt I x)) x'
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.mk.congr_simp : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {β : Type u_5} [inst_1 : TopologicalSpace β]
  (f f_1 : α → β) (e_f : f = f_1) (hf : MeasureTheory.AEStronglyMeasurable f μ),
  MeasureTheory.AEEqFun.mk f hf = MeasureTheory.AEEqFun.mk f_1 ⋯
-- Mathlib.Algebra.Order.Group.Abs
mabs_eq : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b : G},
  1 ≤ b → (|a|ₘ = b ↔ a = b ∨ a = b⁻¹)
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.totalAux.ιMapObj_D₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' : I₁₂) (i : I₁ × I₂) (h : c₁.π c₂ c₁₂ i = i₁₂),
  CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h) (K.D₁ c₁₂ i₁₂ i₁₂') =
    K.d₁ c₁₂ i.1 i.2 i₁₂'
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.map_pullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z W : C} {f : X ⟶ Y} {g : X ⟶ Z} {h : Y ⟶ W} {k : Z ⟶ W} [inst_2 : CategoryTheory.Mono h]
  [inst_3 : CategoryTheory.Mono g]
  (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
  (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk f g comm)) (p : CategoryTheory.Subobject Y),
  (CategoryTheory.Subobject.map g).obj ((CategoryTheory.Subobject.pullback f).obj p) =
    (CategoryTheory.Subobject.pullback k).obj ((CategoryTheory.Subobject.map h).obj p)
-- Mathlib.Order.Filter.Prod
/-- A useful lemma when dealing with uniformities.  -/
Filter.map_swap4_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : Filter α} {g : Filter β} {h : Filter γ}
  {k : Filter δ}, Filter.map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k
-- Mathlib.Order.Sublattice
/-- A sublattice of a lattice inherits an infimum.  -/
Sublattice.instInfCoe : {α : Type u_2} → [inst : Lattice α] → {L : Sublattice α} → Min ↥L
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instIsProbabilityMeasureForallVolume : ∀ {ι : Type u_1} [inst : Fintype ι] {α : ι → Type u_4} [inst_1 : (i : ι) → MeasureTheory.MeasureSpace (α i)]
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume],
  MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.instBEqAbsoluteLspSemanticToken.beq : Lean.Server.FileWorker.AbsoluteLspSemanticToken → Lean.Server.FileWorker.AbsoluteLspSemanticToken → Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
WeierstrassCurve.isHomogeneous_addSubMapCoeff : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) (ij : Fin 3 × Fin 3),
  (W.addSubMapCoeff ij).IsHomogeneous 2
-- Mathlib.Algebra.Ring.Action.Basic
RingHom.smul_def : ∀ (R : Type v) [inst : Semiring R] (f : R →+* R) (a : R), f • a = f a
-- Mathlib.Logic.Relation
/-- **Alias** of `Relation.SymmGen.of_ge`. -/
LE.le.symmGen_symm : ∀ {α : Type u_7} [inst : LE α] {a b : α}, b ≤ a → Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.Discrete.Arrows.id : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (c : C),
  CategoryTheory.Subgroupoid.Discrete.Arrows c c (CategoryTheory.CategoryStruct.id c)
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- Meta version of `CategoryTheory.FreeBicategory.normalizeIso`.  -/
Mathlib.Tactic.BicategoryLike.normalize : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
      Mathlib.Tactic.BicategoryLike.NormalizedHom →
        Mathlib.Tactic.BicategoryLike.Mor₁ →
          Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Normalize.Result
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The inverse of a bijective equivariant map is equivariant.  -/
MulActionHom.inverse' : {M : Type u_2} →
  {N : Type u_3} →
    {φ : M → N} →
      {X : Type u_5} →
        [inst : SMul M X] →
          {Y : Type u_6} →
            [inst_1 : SMul N Y] →
              {φ' : N → M} →
                (f : X →ₑ[φ] Y) →
                  (g : Y → X) →
                    Function.RightInverse φ' φ → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → Y →ₑ[φ'] X
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.commandMake_elab_grind_config__ : Lean.ParserDescr
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsBrownianReal.mk : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsBrownianReal._auto_1},
  ProbabilityTheory.IsPreBrownianReal X P →
    (∀ᵐ (ω : Ω) ∂P, Continuous fun x => X x ω) → ProbabilityTheory.IsBrownianReal X P
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_of_mem_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α}, a ∈ m.erase k → a ∈ m
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_univ_two' : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : ι → M) (a b : ι), ∑ i, f (![a, b] i) = f a + f b
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `MonoidAlgebra.coeff_smul_apply`. -/
MonoidAlgebra.smul_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {A : Type u_8} [inst_1 : SMulZeroClass A R] (a : A)
  (x : MonoidAlgebra R M) (m : M), (a • x).coeff m = a • x.coeff m
-- Init.Data.Array.Lemmas
Array.toList_range : ∀ {n : ℕ}, (Array.range n).toList = List.range n
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.coe_top : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LE α], ↑⊤ = Set.univ
-- Mathlib.RingTheory.PrincipalIdealDomain
/-- A choice of gcd of two elements in a Bézout domain.

Note that the choice is usually not unique.  -/
IsBezout.gcd : {R : Type u} → [inst : Ring R] → (x y : R) → [Submodule.IsPrincipal (Ideal.span {x, y})] → R
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- Composition of `StrictlyUnitaryLaxFunctor`.  -/
CategoryTheory.StrictlyUnitaryLaxFunctor.comp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {D : Type u₃} →
          [inst_2 : CategoryTheory.Bicategory D] →
            CategoryTheory.StrictlyUnitaryLaxFunctor B C →
              CategoryTheory.StrictlyUnitaryLaxFunctor C D → CategoryTheory.StrictlyUnitaryLaxFunctor B D
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryLE.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    [inst : Ord α] →
      (k : α) →
        (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Ordered → (∃ a ∈ x, (compare a k).isLE = true) → Sort u_3) →
          (x : Std.DTreeMap.Internal.Impl α β) →
            (x_1 : x.Ordered) →
              (x_2 : ∃ a ∈ x, (compare a k).isLE = true) →
                ((x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
                    (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isLE = true) →
                      motive Std.DTreeMap.Internal.Impl.leaf x he) →
                  ((size : ℕ) →
                      (ky : α) →
                        (y : β ky) →
                          (l r : Std.DTreeMap.Internal.Impl α β) →
                            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
                              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isLE = true) →
                                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he) →
                    motive x x_1 x_2
-- Init.Data.Range.Polymorphic.SInt
Int32.instRxoHasSize : Std.Rxo.HasSize Int32
-- Mathlib.Logic.Equiv.Basic
/-- Transport dependent functions through
an equivalence of the base spaces and a family
of equivalences of the matching fibers.
 -/
Equiv.piCongr : {α : Sort u_1} →
  {β : Sort u_4} →
    {W : α → Sort w} → {Z : β → Sort z} → (h₁ : α ≃ β) → ((a : α) → W a ≃ Z (h₁ a)) → ((a : α) → W a) ≃ ((b : β) → Z b)
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The functions satisfying `isLocallyFraction` form a submodule.  -/
AlgebraicGeometry.StructureSheaf.sectionsSubmodule : {R : Type u} →
  (M : Type u) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
            Submodule R ((x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations M ↑x)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapRingEquiv_trans : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Semiring T] [inst_3 : Monoid M] (e₁ : R ≃+* S) (e₂ : S ≃+* T),
  MonoidAlgebra.mapRingEquiv M (e₁.trans e₂) = (MonoidAlgebra.mapRingEquiv M e₁).trans (MonoidAlgebra.mapRingEquiv M e₂)
-- Mathlib.GroupTheory.OrderOfElement
AddRightCancelMonoid.finite_multiples : ∀ {G : Type u_1} [inst : AddRightCancelMonoid G] {a : G}, (↑(AddSubmonoid.multiples a)).Finite ↔ IsOfFinAddOrder a
-- Init.Data.UInt.Lemmas
UInt32.pow_zero : ∀ (x : UInt32), x ^ 0 = 1
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.push : Turing.PartrecToTM2.K' →
  (Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') → Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Λ'
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.hasNoLoop_down' : ∀ {α : Type u_2} [inst : AddZeroClass α] [inst_1 : IsRightCancelAdd α] [IsLeftCancelAdd α] (a : α),
  a ≠ 0 → (ComplexShape.down' a).HasNoLoop
-- Mathlib.SetTheory.Cardinal.Free
nonempty_commSemiring_iff : ∀ (α : Type u), Nonempty (CommSemiring α) ↔ Nonempty α
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (V : X.Opens) (h : U ≤ V),
  AlgebraicGeometry.Scheme.Hom.app hU.fromSpec V =
    CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.homOfLE h).op)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv
        ((AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).presheaf.map (CategoryTheory.homOfLE ⋯).op))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k a : α} {h' : Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.erase! k t) = true},
  (Std.DTreeMap.Internal.Impl.erase! k t).getKey a h' = t.getKey a ⋯