mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Intertwining
/-- Any representation is equivalent to itself.  -/
Representation.Equiv.refl : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module A V] → (ρ : Representation A G V) → ρ.Equiv ρ
-- Init.Data.Nat.Lemmas
Nat.one_sub : ∀ (n : ℕ), 1 - n = if n = 0 then 1 else 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- Variant of `IsPullback.of_bot`, where `v₁₁` is induced from a morphism `v₃₁ : X₁₁ ⟶ X₃₁`, and
the universal property of the bottom square.

The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂
|            |
v₁₁          v₁₂
↓            ↓
X₂₁ - h₂₁ -> X₂₂
|            |
v₂₁          v₂₂
↓            ↓
X₃₁ - h₃₁ -> X₃₂
```
 -/
CategoryTheory.IsPullback.of_bot' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₃₁ : X₁₁ ⟶ X₃₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂}
  (s : CategoryTheory.IsPullback h₁₁ v₃₁ (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁)
  (t : CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁),
  CategoryTheory.IsPullback h₁₁ (t.lift (CategoryTheory.CategoryStruct.comp h₁₁ v₁₂) v₃₁ ⋯) v₁₂ h₂₁
-- Aesop.Script.SScript
Aesop.Script.SScript.onGoal.injEq : ∀ (goalPos : ℕ) (step : Aesop.Script.Step) (tail : Aesop.Script.SScript) (goalPos_1 : ℕ) (step_1 : Aesop.Script.Step)
  (tail_1 : Aesop.Script.SScript),
  (Aesop.Script.SScript.onGoal goalPos step tail = Aesop.Script.SScript.onGoal goalPos_1 step_1 tail_1) =
    (goalPos = goalPos_1 ∧ step = step_1 ∧ tail = tail_1)
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.ins.match_3.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α)
  (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 : (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a y b))
  (h_3 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b)),
  (match RBTree.RBNode.node RBTree.RBColor.black a y b with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node RBTree.RBColor.red a y b => h_2 a y b
    | RBTree.RBNode.node RBTree.RBColor.black a y b => h_3 a y b) =
    h_3 a y b
-- Mathlib.LinearAlgebra.Dimension.DivisionRing
/-- If a vector space has a finite dimension, the index set of `Basis.ofVectorSpace` is finite.  -/
Module.Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0 : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Module.rank K V < Cardinal.aleph0 → (Module.Basis.ofVectorSpaceIndex K V).Finite
-- Mathlib.CategoryTheory.Limits.Filtered
CategoryTheory.Limits.hasFilteredColimitsOfSize_shrink : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasFilteredColimitsOfSize.{max w' w₂', max w w₂, v, u} C],
  CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, v, u} C
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
/-- If the derivatives within a set of `g` at `f x` are bounded by `C`, and the `i`-th derivative
within a set of `f` at `x` is bounded by `D^i` for all `1 ≤ i ≤ n`, then the `n`-th derivative
of `g ∘ f` is bounded by `n! * C * D^n`.
This lemma proves this estimate assuming additionally that two of the spaces live in the same
universe, to make an induction possible. Use instead `norm_iteratedFDerivWithin_comp_le` that
removes this assumption.  -/
norm_iteratedFDerivWithin_comp_le_aux : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {Fu Gu : Type u} [inst_3 : NormedAddCommGroup Fu] [inst_4 : NormedSpace 𝕜 Fu]
  [inst_5 : NormedAddCommGroup Gu] [inst_6 : NormedSpace 𝕜 Gu] {g : Fu → Gu} {f : E → Fu} {n : ℕ} {s : Set E}
  {t : Set Fu} {x : E},
  ContDiffOn 𝕜 (↑n) g t →
    ContDiffOn 𝕜 (↑n) f s →
      UniqueDiffOn 𝕜 t →
        UniqueDiffOn 𝕜 s →
          Set.MapsTo f s t →
            x ∈ s →
              ∀ {C D : ℝ},
                (∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
                  (∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
                    ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n.factorial * C * D ^ n
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.PostponeBehavior.ofBool : Bool → Lean.Elab.Term.PostponeBehavior
-- Mathlib.GroupTheory.Subgroup.Center
/-- The center of an additive group is isomorphic to the center of its opposite.  -/
AddSubgroup.centerToAddOpposite : (G : Type u_1) → [inst : AddGroup G] → ↥(AddSubgroup.center G) ≃+ ↥(AddSubgroup.center Gᵃᵒᵖ)
-- Init.Data.Order.Ord
Std.LawfulBEqCmp.lawfulEqCmp : ∀ {α : Type u} [inst : BEq α] {cmp : α → α → Ordering} [inst_1 : Std.LawfulBEqCmp cmp] [LawfulBEq α],
  Std.LawfulEqCmp cmp
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H1π_eq_zero_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x : ↥(groupHomology.cycles₁ A)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H1π A)) x = 0 ↔ ↑x ∈ groupHomology.boundaries₁ A
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_inv_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.OplaxRightLinear C] (d : D) {Z : D'}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d)
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).inv h =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.sep_empty : ∀ (p : ZFSet.{u_1} → Prop), ZFSet.sep p ∅ = ∅
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.denote.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (e : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.denote ctx e =
    Lean.Grind.CommRing.Expr.rec (fun k => Lean.Grind.CommRing.denoteInt k) (fun k => ↑k) (fun k => IntCast.intCast k)
      (fun x => Lean.Grind.CommRing.Var.denote ctx x) (fun x ih => -ih) (fun x x_1 ih₁ ih₂ => ih₁ + ih₂)
      (fun x x_1 ih₁ ih₂ => ih₁ - ih₂) (fun x x_1 ih₁ ih₂ => ih₁ * ih₂) (fun x k ih => ih ^ k) e
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.leftUnitorImpl_hom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  X.leftUnitorImpl.hom.f = CategoryTheory.Limits.prod.snd
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_fun_neg : ∀ {𝕜 : 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] {f : E → F}
  {x : E}, fderiv 𝕜 (fun y => -f y) x = -fderiv 𝕜 f x
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- If a function is continuous on an open set `s`, then it is strongly measurable at the filter
`𝓝 x` for all `x ∈ s` if either the source space or the target space is second-countable.  -/
ContinuousOn.stronglyMeasurableAtFilter : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace α] [OpensMeasurableSpace α]
  [inst_2 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [SecondCountableTopologyEither α β]
  {f : α → β} {s : Set α} {μ : MeasureTheory.Measure α},
  IsOpen s → ContinuousOn f s → ∀ x ∈ s, StronglyMeasurableAtFilter f (nhds x) μ
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_add : ∀ {𝕜 : 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] {f g : E → F}
  {x : E}, DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → fderiv 𝕜 (f + g) x = fderiv 𝕜 f x + fderiv 𝕜 g x
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  (X_1 : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)),
  ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso F U).hom.app X_1).hom =
    CategoryTheory.CategoryStruct.id X_1.pt
-- Mathlib.Algebra.Group.Finsupp
Finsupp.induction_linear : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] {motive : (ι →₀ M) → Prop} (f : ι →₀ M),
  motive 0 →
    (∀ (f g : ι →₀ M), motive f → motive g → motive (f + g)) → (∀ (a : ι) (b : M), motive fun₀ | a => b) → motive f
-- Mathlib.Data.List.DropRight
List.rdropWhile_prefix : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.rdropWhile p l <+: l
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.dist_cons_cons_eq_one : ∀ {α : Type u_1} {x y : α} {s t : Stream'.Seq α}, x ≠ y → dist (Stream'.Seq.cons x s) (Stream'.Seq.cons y t) = 1
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.f_pOpcycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] {Z : C} (h : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.f (CategoryTheory.CategoryStruct.comp S.pOpcycles h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instToJsonFileSystemWatcher : Lean.ToJson Lean.Lsp.FileSystemWatcher
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.norm_inner_symm : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F), ‖inner 𝕜 x y‖ = ‖inner 𝕜 y x‖
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.isHermitian : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] {M : Matrix n n R},
  M.PosSemidef → M.IsHermitian
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.toSubsemiring_mono : ∀ {R : Type u_1} [inst : CommRing R], Monotone RingPreordering.toSubsemiring
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.closure_realFundSystem_sup_torsion : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K],
  Subgroup.closure (Set.range (NumberField.IsCMField.realFundSystem K)) ⊔ NumberField.Units.torsion K =
    NumberField.IsCMField.realUnits K ⊔ NumberField.Units.torsion K
-- Mathlib.GroupTheory.Exponent
Monoid.ExponentExists.eq_1 : ∀ (G : Type u) [inst : Monoid G], Monoid.ExponentExists G = ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1
-- Mathlib.LinearAlgebra.Alternating.Curry
AlternatingMap.curryLeft_apply_toMultilinearMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : M),
  ↑(f.curryLeft m) = (↑f).curryLeft m
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.ofArray_eq_ofList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (a : Array α),
  Std.HashSet.Raw.ofArray a = Std.HashSet.Raw.ofList a.toList
-- Mathlib.Topology.Closure
Set.Finite.closure_sUnion : ∀ {X : Type u} [inst : TopologicalSpace X] {S : Set (Set X)}, S.Finite → closure (⋃₀ S) = ⋃ s ∈ S, closure s
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.meas_iInter : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : ι → Type u_8} {mβ : (i : ι) → MeasurableSpace (β i)}
  {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α}
  {s : ι → Set Ω} {f : (x : ι) → Ω → β x} [inst : Fintype ι],
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), MeasurableSet (s i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i, s i) = ∏ i, (κ a) (s i)
-- Lean.Linter.UnusedVariables
/-- Adds a new builtin `IgnoreFunction`.
This function should only be used from within the `Lean` package.  -/
Lean.Linter.addBuiltinUnusedVariablesIgnoreFn : Lean.Linter.IgnoreFunction → IO Unit
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stmts₁.eq_7 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4},
  Turing.TM2.stmts₁ Turing.TM2.Stmt.halt = {Turing.TM2.Stmt.halt}
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.add_h₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄), (h.add h').h₂ = h.h₂ + h'.h₂
-- Mathlib.GroupTheory.CoprodI
/-- Given `i : ι`, any reduced word can be decomposed into a pair `p` such that `w = rcons p`.  -/
_private.Mathlib.GroupTheory.CoprodI.0.Monoid.CoprodI.Word.equivPairAux : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      [DecidableEq ι] →
        [inst_2 : (i : ι) → DecidableEq (M i)] →
          (i : ι) → (w : Monoid.CoprodI.Word M) → { p // Monoid.CoprodI.Word.rcons p = w }
-- Aesop.Util.EqualUpToIds
/-- A map from metavariables which are unassigned in the right goal
to their corresponding expression in the left goal. Only used when
`allowAssignmentDiff = true`.  -/
Aesop.EqualUpToIdsM.State.rightUnassignedMVarValues : Aesop.EqualUpToIdsM.State → Std.HashMap Lean.MVarId Lean.Expr
-- Std.Net.Addr
Std.Net.instDecidableEqIPAddr.decEq : (x x_1 : Std.Net.IPAddr) → Decidable (x = x_1)
-- Lean.Elab.Tactic.Omega.MinNatAbs
Lean.Elab.Tactic.Omega.List.nonzeroMinimum_eq_zero_iff : ∀ {xs : List ℕ}, Lean.Elab.Tactic.Omega.List.nonzeroMinimum xs = 0 ↔ ∀ x ∈ xs, x = 0
-- Mathlib.Data.Set.Card
/-- Given a subset `s` of a set `t`, of sizes at most and at least `n` respectively, there exists a
set `u` of size `n` which is both a superset of `s` and a subset of `t`.  -/
Set.exists_subsuperset_card_eq : ∀ {α : Type u_1} {s t : Set α} {n : ℕ}, s ⊆ t → s.ncard ≤ n → n ≤ t.ncard → ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false →
    (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)).getKey? k = t.getKey? k
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.IsVonNBounded.restrict_scalars : ∀ (𝕜 : Type u_1) {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] [inst_3 : Zero E] [inst_4 : TopologicalSpace E] [inst_5 : SMul 𝕜 E]
  [inst_6 : MulActionWithZero 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {s : Set E},
  Bornology.IsVonNBounded 𝕜' s → Bornology.IsVonNBounded 𝕜 s
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- Reinterpret an equivalence relation as a symmetric relation.  -/
CategoryTheory.EquivalenceRelation.toSymmetricRelation : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} → {p₁ p₂ : R ⟶ X} → CategoryTheory.EquivalenceRelation p₁ p₂ → CategoryTheory.SymmetricRelation p₁ p₂
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsNonempty.eq_1 : ∀ {α : Type u_1} (H : Hypergraph α), H.IsNonempty = (H.vertexSet.Nonempty ∨ H.edgeSet.Nonempty)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCoseparator_pi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w}
  (f : β → C) [inst_2 : CategoryTheory.Limits.HasProduct f],
  CategoryTheory.IsCoseparator (∏ᶜ f) ↔ (CategoryTheory.ObjectProperty.ofObj f).IsCoseparating
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.lie_e_pow_toEnd_e : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {e : L}
  {m : M} (n : ℕ), ⁅e, ((LieModule.toEnd R L M) e ^ n) m⁆ = ((LieModule.toEnd R L M) e ^ (n + 1)) m
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.to_continuousMap_injective : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] {f g : P →ᴬ[R] Q}, ↑f = ↑g → f = g
-- Lean.Server.Requests
Lean.Server.RequestError.mk.sizeOf_spec : ∀ (code : Lean.JsonRpc.ErrorCode) (message : String),
  sizeOf { code := code, message := message } = 1 + sizeOf code + sizeOf message
-- Std.Time.Zoned.Database.TzIf
/-- Optionally, the data for version 2 of the TZif file.
 -/
Std.Time.TimeZone.TZif.TZif.v2 : Std.Time.TimeZone.TZif.TZif → Option Std.Time.TimeZone.TZif.TZifV2
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.instSemigroupWithZero : {α : Type u_1} → [DecidableEq α] → [inst : SemigroupWithZero α] → [NoZeroDivisors α] → SemigroupWithZero (WithTop α)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_sPolynomial_lt_sup_degree : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {f g : MvPolynomial σ R},
  m.sPolynomial f g ≠ 0 → m.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.isFractional_div_of_ne_zero : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K] [IsFractionRing R₁ K]
  [IsDomain R₁] {I J : FractionalIdeal (nonZeroDivisors R₁) K}, J ≠ 0 → IsFractional (nonZeroDivisors R₁) (↑I / ↑J)
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_isoBot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C],
  (Φ.transfiniteCompositionOfShapeιIteration J).isoBot = Φ.iterationFunctorObjBotIso J
-- Mathlib.CategoryTheory.Discrete.SumsProducts
_private.Mathlib.CategoryTheory.Discrete.SumsProducts.0.CategoryTheory.sum.match_3.eq_1 : ∀ (C : Type u_1) (D : Type u_2) (motive : C ⊕ D → Sort u_3) (X : C) (h_1 : (X : C) → motive (Sum.inl X))
  (h_2 : (X : D) → motive (Sum.inr X)),
  (match Sum.inl X with
    | Sum.inl X => h_1 X
    | Sum.inr X => h_2 X) =
    h_1 X
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.sub_apply : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommGroup (β i)] (g₁ g₂ : DirectSum ι fun i => β i) (i : ι),
  (g₁ - g₂) i = g₁ i - g₂ i
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.instInhabitedState : Inhabited Lean.Meta.Grind.Arith.Linear.State
-- Mathlib.Analysis.Convex.Segment
openSegment_eq_image₂ : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (x y : E),
  openSegment 𝕜 x y = (fun p => p.1 • x + p.2 • y) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
-- Mathlib.Topology.Maps.Proper.Basic
IsProperMap.mk : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → (∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) → IsProperMap f
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.smul_ofFunction : ∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {c : ENNReal},
  c ≠ ⊤ → c • MeasureTheory.OuterMeasure.ofFunction m m_empty = MeasureTheory.OuterMeasure.ofFunction (c • m) ⋯
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.QInfty_idem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C},
  CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty AlgebraicTopology.DoldKan.QInfty =
    AlgebraicTopology.DoldKan.QInfty
-- Mathlib.Geometry.Manifold.Notation
Manifold.Elab.instCoeExprFindModelResult : Coe Lean.Expr Manifold.Elab.FindModelResult
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.PushoutCocone.pasteHoriz.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ : C} {f₁ : X₁ ⟶ X₂} {f₂ : X₂ ⟶ X₃} {i₁ : X₁ ⟶ Y₁}
  (t₁ : CategoryTheory.Limits.PushoutCocone i₁ f₁) {i₂ : X₂ ⟶ t₁.pt}
  (t₂ t₂_1 : CategoryTheory.Limits.PushoutCocone i₂ f₂),
  t₂ = t₂_1 → ∀ (hi₂ : i₂ = t₁.inr), t₁.pasteHoriz t₂ hi₂ = t₁.pasteHoriz t₂_1 hi₂
-- Lean.Level
/-- Cached hash code, cached results, and other data for `Level`.
hash      : 32-bits
hasMVar   : 1-bit
hasParam  : 1-bit
depth     : 24-bits  -/
Lean.Level.Data : Type
-- Mathlib.Algebra.Ring.Subring.Defs
/-- Copy of a subring with a new `carrier` equal to the old one. Useful to fix definitional
equalities.  -/
Subring.copy : {R : Type u} → [inst : NonAssocRing R] → (S : Subring R) → (s : Set R) → s = ↑S → Subring R
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₈_of_isCharTwoJEqZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF], W.b₈ = -W.a₄ ^ 2
-- Lean.Server.CodeActions.Basic
/-- Handles a `textDocument/codeAction` request.

This is implemented by calling all of the registered `CodeActionProvider` functions.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_codeAction).  -/
Lean.Server.handleCodeAction : Lean.Lsp.CodeActionParams → Lean.Server.RequestM (Lean.Server.RequestTask (Array Lean.Lsp.CodeAction))
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedCommMonoid.mk : {E : Type u_8} →
  [inst : TopologicalSpace E] →
    [toESeminormedMonoid : ESeminormedMonoid E] → (∀ (a b : E), a * b = b * a) → ESeminormedCommMonoid E
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrX_XIsoBiprod_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i) {Z : C} (h : F.X i ⊞ G.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.XIsoBiprod φ j i hij).hom h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h
-- Mathlib.Topology.UniformSpace.Equicontinuity
uniformEquicontinuous_finite : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] [Finite ι] {F : ι → β → α},
  UniformEquicontinuous F ↔ ∀ (i : ι), UniformContinuous (F i)
-- Mathlib.Analysis.Complex.RealDeriv
HasDerivWithinAt.complexToReal_fderiv : ∀ {f : ℂ → ℂ} {s : Set ℂ} {f' x : ℂ}, HasDerivWithinAt f f' s x → HasFDerivWithinAt f (f' • 1) s x