mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.JointEigenspace
/-- The joint eigenspaces of a family of symmetric operators form an
`OrthogonalFamily`.  -/
LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces : ∀ {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {T : n → Module.End 𝕜 E},
  (∀ (i : n), LinearMap.IsSymmetric (T i)) →
    OrthogonalFamily 𝕜 (fun γ => ↥(⨅ j, (T j).eigenspace (γ j))) fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ
-- Mathlib.Data.ENNReal.Holder
/-- This is not marked as an instance so that Lean doesn't always find this one
and a more canonical value of `r` can be used.  -/
ENNReal.HolderTriple.of : ∀ (p q : ENNReal), p.HolderTriple q (p⁻¹ + q⁻¹)⁻¹
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.add_neg_cancel : ∀ {α : Type u} [inst : SubtractionMonoid α] {a : α}, IsAddUnit a → a + -a = 0
-- Mathlib.Algebra.Homology.Localization
HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C]
  [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] [c.QFactorsThroughHomotopy C]
  {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g),
  HomologicalComplexUpToQuasiIso.Q.map f = HomologicalComplexUpToQuasiIso.Q.map g
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Two affine subspaces with the same direction and nonempty intersection are equal.  -/
AffineSubspace.ext_of_direction_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : AffineSubspace k P}, s₁.direction = s₂.direction → (↑s₁ ∩ ↑s₂).Nonempty → s₁ = s₂
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_zero : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (p : ι → Prop) [inst_1 : DecidablePred p],
  DFinsupp.filter p 0 = 0
-- Mathlib.Data.Finsupp.Single
Finsupp.single_left_inj : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a a' : α} {b : M},
  b ≠ 0 → (((fun₀ | a => b) = fun₀ | a' => b) ↔ a = a')
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function has a power series within a set on a ball, then so does its derivative. For a
version without completeness, but assuming that the function is analytic on the set `s`, see
`HasFPowerSeriesWithinOnBall.fderivWithin_of_mem_of_analyticOn`.  -/
HasFPowerSeriesWithinOnBall.fderivWithin_of_mem : ∀ {𝕜 : 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]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E} [CompleteSpace F],
  HasFPowerSeriesWithinOnBall f p s x r →
    UniqueDiffOn 𝕜 s → x ∈ s → HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f s) p.derivSeries s x r
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The proposition that a Jacobian point class on a Weierstrass curve `W` is nonsingular.

If `P` is a Jacobian point representative on `W`, then `W.NonsingularLift ⟦P⟧` is definitionally
equivalent to `W.Nonsingular P`.

Note that this definition is only mathematically accurate for fields.  -/
WeierstrassCurve.Jacobian.NonsingularLift : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Jacobian R → WeierstrassCurve.Jacobian.PointClass R → Prop
-- Mathlib.RepresentationTheory.Character
FDRep.average_char_eq_finrank_invariants : ∀ {k : Type u} [inst : Field k] {G : Type v} [inst_1 : Group G] [inst_2 : Fintype G] [Invertible ↑(Nat.card G)]
  (V : FDRep k G), (↑(Nat.card G))⁻¹ * ∑ g, V.character g = ↑(Module.finrank k ↥(Representation.invariants V.ρ))
-- Init.Data.List.Lemmas
List.length_replace : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {l : List α}, (l.replace a b).length = l.length
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.preprocessConst : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.tendsto_nhdsWithin_nhds : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] {s : Set α} [inst_1 : PseudoEMetricSpace β] {f : α → β}
  {a : α} {b : β},
  Filter.Tendsto f (nhdsWithin a s) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.nonUniforms_mono : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [inst_4 : DecidableRel G.Adj]
  {ε ε' : 𝕜}, ε ≤ ε' → P.nonUniforms G ε' ⊆ P.nonUniforms G ε
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- If `G` is a group object, then `Hom(X, G)` has a group structure.  -/
CategoryTheory.Hom.group : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → {G X : C} → [CategoryTheory.GrpObj G] → Group (X ⟶ G)
-- Mathlib.Order.OmegaCompletePartialOrder
Part.ωSup_eq_none : ∀ {α : Type u_2} {c : OmegaCompletePartialOrder.Chain (Part α)}, (¬∃ a, Part.some a ∈ c) → Part.ωSup c = Part.none
-- Mathlib.Data.Finset.Prod
Finset.diag_nonempty : ∀ {α : Type u_1} {s : Finset α}, s.diag.Nonempty ↔ s.Nonempty
-- Mathlib.NumberTheory.SmoothNumbers
/-- The product of two `s`-factored numbers is again `s`-factored.  -/
Nat.mul_mem_factoredNumbers : ∀ {s : Finset ℕ} {m n : ℕ}, m ∈ Nat.factoredNumbers s → n ∈ Nat.factoredNumbers s → m * n ∈ Nat.factoredNumbers s
-- Mathlib.Tactic.Module
_private.Mathlib.Tactic.Module.0.Mathlib.Tactic.Module.qNF.toNF.match_1.eq_1 : ∀ {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (motive : Q(«$R») × Q(«$M») → Sort u_1) (a : Q(«$R»)) (x : Q(«$M»))
  (h_1 : (a : Q(«$R»)) → (x : Q(«$M»)) → motive (a, x)),
  (match (a, x) with
    | (a, x) => h_1 a x) =
    h_1 a x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
/-- The number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2],
from which one can derive all its properties. For explicit bounds on π,
see `Mathlib/Analysis/Real/Pi/Bounds.lean`.

Denoted `π`, once the `Real` namespace is opened.  -/
Real.termπ : Lean.ParserDescr
-- Init.Data.Array.MapIdx
Array.mapIdx_reverse : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : ℕ → α → β},
  Array.mapIdx f xs.reverse = (Array.mapIdx (fun i => f (xs.size - 1 - i)) xs).reverse
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.equivHomShift_comp_shift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
  {L' : CochainComplex C ℤ} (g : L ⟶ L'),
  CochainComplex.HomComplex.Cocycle.equivHomShift
      (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map g)) =
    (CochainComplex.HomComplex.Cocycle.equivHomShift f).postcomp g
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.disjoint_def : ∀ {G : Type u_1} [inst : Group G] {H₁ H₂ : Subgroup G}, Disjoint H₁ H₂ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1
-- Lean.LabelAttribute
/-- When `attrName` is an attribute created using `register_labelled_attr`,
return the names of all declarations labelled using that attribute.  -/
Lean.labelled : Lean.Name → Lean.CoreM (Array Lean.Name)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBase.exchange_base_of_notMem_closure : ∀ {α : Type u_2} {M : Matroid α} {e f : α} {B : Set α},
  M.IsBase B →
    e ∈ B →
      f ∉ M.closure (B \ {e}) →
        autoParam (f ∈ M.E) Matroid.IsBase.exchange_base_of_notMem_closure._auto_1 → M.IsBase (insert f (B \ {e}))
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.withZeroUnitsEquiv_apply : ∀ {G : Type u_4} [inst : GroupWithZero G] [inst_1 : DecidablePred fun a => a = 0] (n : WithZero Gˣ),
  WithZero.withZeroUnitsEquiv n = WithZero.recZeroCoe 0 Units.val n
-- Mathlib.AlgebraicGeometry.Sites.Small
/-- The pretopology on `Over S` induced by `P` where coverings are given by `P`-covers
of `S`-schemes.  -/
AlgebraicGeometry.Scheme.overPretopology : (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) →
  (S : AlgebraicGeometry.Scheme) →
    [P.IsStableUnderBaseChange] →
      [P.IsMultiplicative] → [P.RespectsIso] → CategoryTheory.Pretopology (CategoryTheory.Over S)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_sub_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.C R (n - 1) = Polynomial.X * Polynomial.Chebyshev.C R n - Polynomial.Chebyshev.C R (n + 1)
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
/-- If `φ : a ≅ b` is an isomorphism lifting `𝟙 S` for some `S : 𝒮`, then `φ⁻¹` also
lifts `𝟙 S`.  -/
CategoryTheory.IsHomLift.lift_id_inv : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) (S : 𝒮) {a b : 𝒳} (φ : a ≅ b)
  [p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ.hom], p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ.inv
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The colimit of `F ⋙ forget₂ AddCommGrpCat AddGrpCat` in the category `AddGrpCat`.
In the following, we will show that this has the structure of a _commutative_ additive group.  -/
AddCommGrpCat.FilteredColimits.G : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J AddCommGrpCat → AddGrpCat
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_conjTranspose_iff : ∀ {α : Type u_1} {n : Type u_4} [inst : InvolutiveStar α] {A : Matrix n n α},
  A.conjTranspose.IsHermitian ↔ A.IsHermitian
-- Mathlib.Order.Filter.Bases.Basic
/-- We say that a filter `l` has an antitone basis `s : ι → Set α`, if `t ∈ l` if and only if `t`
includes `s i` for some `i`, and `s` is decreasing.  -/
Filter.HasAntitoneBasis : {α : Type u_1} → {ι'' : Type u_6} → [Preorder ι''] → Filter α → (ι'' → Set α) → Prop
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.mem_Lp_of_nnnorm_ae_le_mul : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {c : NNReal} {f : α →ₘ[μ] E}
  {g : ↥(MeasureTheory.Lp F p μ)}, (∀ᵐ (x : α) ∂μ, ‖↑f x‖₊ ≤ c * ‖↑↑g x‖₊) → f ∈ MeasureTheory.Lp E p μ
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.eval_surjective : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ), Function.Surjective ⇑(AdicCompletion.eval I M n)
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyReflectEpimorphisms.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  (∀ {X Y : C} (f : X ⟶ Y) [∀ (i : I), CategoryTheory.Epi ((F i).map f)], CategoryTheory.Epi f) →
    CategoryTheory.JointlyReflectEpimorphisms F
-- Init.Data.String.Lemmas.Length
String.length_map : ∀ {f : Char → Char} {s : String}, (String.map f s).length = s.length
-- Mathlib.Data.Set.Sigma
biSup_sigma' : ∀ {ι : Type u_1} {α : ι → Type u_3} {β : Type u_4} [inst : CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i))
  (f : (i : ι) → α i → β), ⨆ i ∈ s, ⨆ j ∈ t i, f i j = ⨆ ij ∈ s.sigma t, f ij.fst ij.snd
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- In conditionally complete orders with a bottom element, the nonempty condition can be omitted
from `lt_csSup_iff`.  -/
lt_csSup_iff' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α},
  BddAbove s → (a < sSup s ↔ ∃ b ∈ s, a < b)
-- Mathlib.Data.Setoid.Basic
/-- A function from α to β is injective iff its kernel is the bottom element of the complete lattice
of equivalence relations on α.  -/
Setoid.injective_iff_ker_bot : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.Injective f ↔ Setoid.ker f = ⊥
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfoldRev.eq_def : ∀ (n : ℕ) {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfoldRev._auto_1 → Type u}
  (f : (i : ℕ) → (h : i < n) → α (i + 1) ⋯ → α i ⋯) (init : α n ⋯),
  n.dfoldRev f init =
    match n, α, f, init with
    | 0, α, f, init => init
    | n.succ, α, f, init => n.dfoldRev (fun i h => f i ⋯) (f n ⋯ init)
-- Mathlib.Topology.MetricSpace.Completion
/-- The new distance is an extension of the original distance.  -/
UniformSpace.Completion.dist_eq : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), dist ↑x ↑y = dist x y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_eq_getElem!_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.minKey! = t.keysArray[0]!
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.mem_idealOfSet : ∀ {X : Type u_1} {R : Type u_2} [inst : TopologicalSpace X] [inst_1 : Semiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] {s : Set X} {f : C(X, R)},
  f ∈ ContinuousMap.idealOfSet R s ↔ ∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_pow : ∀ {a b : ℝ} (n : ℕ), ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)
-- Mathlib.Topology.Algebra.Valued.ValuedField
/-- The topology coming from a valuation on a division ring makes it a topological division ring
[BouAC, VI.5.1 middle of Proposition 1]  -/
Valued.isTopologicalDivisionRing : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : Valued K Γ₀], IsTopologicalDivisionRing K
-- Mathlib.Data.Nat.Init
Nat.leRec_succ' : ∀ {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯)
  (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯),
  Nat.leRec refl le_succ_of_le ⋯ = le_succ_of_le ⋯ refl
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.compContinuousLinearMap_apply : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {ι : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M']
  [inst_5 : Module R M'] [inst_6 : TopologicalSpace M'] [inst_7 : AddCommMonoid N] [inst_8 : Module R N]
  [inst_9 : TopologicalSpace N] (g : M [⋀^ι]→L[R] N) (f : M' →L[R] M) (m : ι → M'),
  (g.compContinuousLinearMap f) m = g (⇑f ∘ m)
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.areaForm_map : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℝ F]
  [hF : Fact (Module.finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) (x y : F),
  (((Orientation.map (Fin 2) φ.toLinearEquiv) o).areaForm x) y = (o.areaForm (φ.symm x)) (φ.symm y)
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.cm3a : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.mem_symplComp_iff : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] {x : H} {S : ClosedSubmodule ℝ H},
  x ∈ S.symplComp ↔ ∀ y ∈ S, (inner ℂ y x).im = 0
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.mulRight_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A : C} [inst_2 : CategoryTheory.GrpObj A] (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A),
  (CategoryTheory.GrpObj.mulRight f).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) f))
      CategoryTheory.MonObj.mul
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.IsSubwalk.copy : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' x y x' y' : V} {p : G.Walk x y} {q : G.Walk u v},
  p.IsSubwalk q → ∀ (hx : x = x') (hy : y = y') (hu : u = u') (hv : v = v'), (p.copy hx hy).IsSubwalk (q.copy hu hv)
-- Mathlib.Order.Defs.Unbundled
RelLowerSet.mk : {α : Type u_1} → [inst : LE α] → {P : α → Prop} → (carrier : Set α) → IsRelLowerSet carrier P → RelLowerSet P
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instIsCardinalFilteredSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredPropSet : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ),
  CategoryTheory.IsCardinalFiltered (Subtype J.PropSet) κ
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_prefix.sizeOf_spec : ∀ (lhs : Bool) (s : Lean.Grind.AC.Seq) (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr),
  sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.simp_prefix lhs s c₁ c₂) = 1 + sizeOf lhs + sizeOf s + sizeOf c₁ + sizeOf c₂
-- Mathlib.Topology.Constructions
Topology.IsClosedEmbedding.piMap : ∀ {ι : Type u_5} {A : ι → Type u_6} {B : ι → Type u_7} [T : (i : ι) → TopologicalSpace (A i)]
  [inst : (i : ι) → TopologicalSpace (B i)] {f : (i : ι) → A i → B i},
  (∀ (i : ι), Topology.IsClosedEmbedding (f i)) → Topology.IsClosedEmbedding (Pi.map f)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.topEquiv.eq_1 : ∀ {M : Type u_5} [inst : MulOneClass M],
  Submonoid.topEquiv = { toFun := fun x => ↑x, invFun := fun x => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b}
  (h : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.id (F.obj b)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b).hom) h =
    CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.id b)).inv
      (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv h))
-- Qq.ForLean.ToExpr
instToExprLevel_qq : Lean.ToExpr Lean.Level
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofNat_mul_re : ∀ {K : Type u_1} [inst : RCLike K] (n : ℕ) [inst_1 : n.AtLeastTwo] (z : K),
  RCLike.re (OfNat.ofNat n * z) = OfNat.ofNat n * RCLike.re z
-- Init.Data.SInt.Lemmas
Int16.toNat_toUInt16_of_le : ∀ {x : Int16}, 0 ≤ x → x.toUInt16.toNat = x.toNatClampNeg
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.pairwise_disjoint_smul_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s : Set β},
  Pairwise (Function.onFun Disjoint fun a => a • s) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_right_inj' : ∀ {w : ℕ} (a b c : BitVec w), (c + a == b + c) = (a == b)
-- Mathlib.Algebra.Category.Grp.Adjunctions
/-- The free-forgetful adjunction for abelian groups.
 -/
AddCommGrpCat.adj : AddCommGrpCat.free ⊣ CategoryTheory.forget AddCommGrpCat
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
panicking if no such key exists.
 -/
Std.TreeMap.getKeyGT! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap α β cmp → α → α
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- Consider a real set `s`. If a property is true almost everywhere in `s ∩ (a, b)` for
all `a, b ∈ s`, then it is true almost everywhere in `s`. Formulated with `μ.restrict`.
See also `ae_of_mem_of_ae_of_mem_inter_Ioo`.  -/
ae_restrict_of_ae_restrict_inter_Ioo : ∀ {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] {s : Set ℝ} {p : ℝ → Prop},
  (∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Set.Ioo a b), p x) → ∀ᵐ (x : ℝ) ∂μ.restrict s, p x
-- Aesop.Frontend.Tactic
_private.Aesop.Frontend.Tactic.0.Aesop.Frontend.elabSimpConfig.unsafe_1 : Lean.Syntax → Lean.Elab.TermElabM Lean.Meta.Simp.Config
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.comap_sectL : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel (α × β) γ) (b : β) {f : δ → α}
  (hf : Measurable f), (κ.sectL b).comap f hf = κ.comap (fun d => (f d, b)) ⋯
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instDistrib : {R : Type u_1} → [Distrib R] → Distrib Rᵃᵒᵖ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_eq_nil : ∀ {m n : ℕ}, n < m → (m...=n).toList = []
-- Mathlib.Data.Finset.Functor
Finset.pure : Pure Finset
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
/-- The Iwasawa structure of `alternatingGroup α` acting on `Set.powersetCard α 4`,
provided `α` has at least 5 elements.  -/
alternatingGroup.iwasawaStructure_four : {α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] → 5 ≤ Nat.card α → MulAction.IwasawaStructure ↥(alternatingGroup α) ↑(Set.powersetCard α 4)
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.unop_adjoin : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set Aᵐᵒᵖ),
  (Algebra.adjoin R s).unop = Algebra.adjoin R (MulOpposite.op ⁻¹' s)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A functor `F : C ⥤ D` reflects limits for `K : J ⥤ C` if
whenever the image of a cone over `K` under `F` is a limit cone in `D`,
the cone was already a limit cone in `C`.
Note that we do not assume a priori that `D` actually has any limits.
 -/
CategoryTheory.Limits.ReflectsLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] → CategoryTheory.Functor J C → CategoryTheory.Functor C D → Prop
-- Init.Data.Range.Polymorphic.PRange
/-- A downward-unbounded range of elements of `α` with an open upper bound.

`*...b` or `*...<b` is the range of all values less than `b : α`.
This is notation for `Rio.mk b`.
 -/
Std.Rio : Type u → Type u
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.contains t.minKey! = true
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
AlgebraicGeometry.Proj.instUniversallyClosedToSpecZeroOfFiniteTypeSubtypeMemOfNatNat : ∀ {σ : Type u_1} {A : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A],
  AlgebraicGeometry.UniversallyClosed (AlgebraicGeometry.Proj.toSpecZero 𝒜)
-- Lean.Util.SCC
Lean.SCC.scc : {α : Type} → [BEq α] → [Hashable α] → List α → (α → List α) → List (List α)
-- Mathlib.LinearAlgebra.Orientation
Orientation.reindex_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι') (x : Orientation R M ι),
  (Orientation.reindex R M e) (-x) = -(Orientation.reindex R M e) x
-- Mathlib.Algebra.Torsor.Basic
/-- If the same point subtracted from two points produces equal
results, those points are equal.  -/
vsub_left_cancel : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p₁ p₂ p : P}, p₁ -ᵥ p = p₂ -ᵥ p → p₁ = p₂
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Ioo : ∀ (x y : ℝ), Real.toEReal ⁻¹' Set.Ioo ↑x ↑y = Set.Ioo x y