mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.isClopen_preimage : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X) (A : Set (Quotient S.toSetoid)),
  IsClopen (S.proj ⁻¹' A)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexWF.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (m₁ m₂ : Lean.Grind.CommRing.Mon)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit)
  (h_2 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m))
  (h_3 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit)
  (h_4 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)),
  m₁ = Lean.Grind.CommRing.Mon.unit →
    m₂ = Lean.Grind.CommRing.Mon.unit →
      (match m₁, m₂ with
        | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => h_1 ()
        | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.mult p m => h_2 p m
        | Lean.Grind.CommRing.Mon.mult p m, Lean.Grind.CommRing.Mon.unit => h_3 p m
        | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_4 pw₁ m₁ pw₂ m₂) ≍
        h_1 ()
-- Mathlib.Algebra.Homology.Embedding.Restriction
HomologicalComplex.restriction_X : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i : ι), (K.restriction e).X i = K.X (e.f i)
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.uliftYonedaEquiv_presheafHom_uliftYoneda_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}
  {G :
    CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂)))
      (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))}
  (φ : F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂} ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp G)
  (X : C),
  CategoryTheory.uliftYonedaEquiv
      (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.presheafHom φ
        (CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.obj X)) =
    (CategoryTheory.ConcreteCategory.hom ((φ.app X).app (F.op.obj (Opposite.op X))))
      { down := CategoryTheory.CategoryStruct.id (Opposite.unop (F.op.obj (Opposite.op X))) }
-- Std.Async.Process
Std.IO.Process.instInhabitedResourceUsageStats : Inhabited Std.IO.Process.ResourceUsageStats
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_of_contains_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β k}, (t.insert k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ D` creates finite products, then `F.rightOp : C ⥤ Dᵒᵖ` creates finite
coproducts.  -/
CategoryTheory.Limits.createsFiniteCoproductsRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ D) →
          [CategoryTheory.Limits.CreatesFiniteProducts F] → CategoryTheory.Limits.CreatesFiniteCoproducts F.rightOp
-- Mathlib.GroupTheory.Sylow
Group.card_dvd_prod_orderOf : ∀ (G : Type u) [inst : Group G] [inst_1 : Fintype G], Nat.card G ∣ ∏ g, orderOf g
-- Lean.Util.NumObjs
_private.Lean.Util.NumObjs.0.Lean.Expr.numObjs.unsafe_1 : Lean.Expr → ℕ
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- **Alias** of the reverse direction of `isAddCommutative_iff_of_setLike`. -/
IsAddCommutative.of_setLike_add_comm : ∀ {S : Type u_3} {M : Type u_4} [inst : SetLike S M] [inst_1 : Add M] [inst_2 : AddMemClass S M] {s : S},
  (∀ a ∈ s, ∀ b ∈ s, a + b = b + a) → IsAddCommutative ↥s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go_get : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (hidx : idx < curr),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go input distance curr hcurr s).get idx ⋯ =
    s.get idx hidx
-- Lean.Data.Json.FromToJson.Basic
Lean.Json.instFromJsonStructured : Lean.FromJson Lean.Json.Structured
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is meromorphic on `U` and `x ∈ U`, then conversion to normal form at `x`
and conversion to normal form on `U` agree in a neighborhood of `x`.
 -/
toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜},
  MeromorphicOn f U → x ∈ U → toMeromorphicNFOn f U =ᶠ[nhds x] toMeromorphicNFAt f x
-- Mathlib.CategoryTheory.Limits.Presentation
/-- The diagram `{Dᵢ}`.  -/
CategoryTheory.Limits.LimitPresentation.diag : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} → CategoryTheory.Limits.LimitPresentation J X → CategoryTheory.Functor J C
-- Mathlib.Data.Multiset.Powerset
Multiset.powerset_strictMono : ∀ {α : Type u_1}, StrictMono Multiset.powerset
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousOn_inv_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} [inst_1 : PartialOrder β]
  [inst_2 : CommGroup β] [IsOrderedMonoid β], LowerSemicontinuousOn f⁻¹ s ↔ UpperSemicontinuousOn f s
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.not_isSimplyLaced_F₄ : ¬CartanMatrix.F₄.IsSimplyLaced
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.isAffineHom_π_app : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] (i : I), AlgebraicGeometry.IsAffineHom (c.π.app i)
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_inter : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s t : Set α}
  {x : α}, t ∈ nhds x → (ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x)
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.throwInvalidPattern : {α : Type} → Lean.Elab.Term.CollectPatternVars.M α
-- Mathlib.Order.BourbakiWitt
/-- **Alias** of `ChainCompletePartialOrder.IsExtremePt.setOfPred_isExtremePt_eq_bot`. -/
ChainCompletePartialOrder.IsExtremePt.setOf_isExtremePt_eq_bot : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α},
  (∀ (x : α), x ≤ f x) → {y | ChainCompletePartialOrder.IsExtremePt x f y} = ChainCompletePartialOrder.bot x f
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndependent.option_iff : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] {a : A},
  (AlgebraicIndependent R fun o => o.elim a x) ↔
    AlgebraicIndependent R x ∧ Transcendental (↥(Algebra.adjoin R (Set.range x))) a
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.splitRevAt.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → List α → Sort u_2) (xs : List α) (x : ℕ) (acc : List α)
  (h_1 : (x : α) → (xs : List α) → (n : ℕ) → (acc : List α) → motive (x :: xs) n.succ acc)
  (h_2 : (xs : List α) → (x : ℕ) → (acc : List α) → motive xs x acc),
  (∀ (x_1 : α) (xs_1 : List α) (n : ℕ), xs = x_1 :: xs_1 → x = n.succ → False) →
    (match xs, x, acc with
      | x :: xs, n.succ, acc => h_1 x xs n acc
      | xs, x, acc => h_2 xs x acc) =
      h_2 xs x acc
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.balanceₘ.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.size > Std.DTreeMap.Internal.delta * l.size → Sort u_3) (size : ℕ)
  (rk : α) (rv : β rk) (rl rr : Std.DTreeMap.Internal.Impl α β)
  (h : (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size > Std.DTreeMap.Internal.delta * l.size)
  (h_1 :
    (h : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * l.size) →
      motive Std.DTreeMap.Internal.Impl.leaf h)
  (h_2 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rl rr : Std.DTreeMap.Internal.Impl α β) →
            (h : (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size > Std.DTreeMap.Internal.delta * l.size) →
              motive (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr) h),
  (match Std.DTreeMap.Internal.Impl.inner size rk rv rl rr, h with
    | Std.DTreeMap.Internal.Impl.leaf, h => h_1 h
    | Std.DTreeMap.Internal.Impl.inner size rk rv rl rr, h => h_2 size rk rv rl rr h) =
    h_2 size rk rv rl rr h
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instFaithfulIndFunctorOppositeTypeInclusion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.Ind.inclusion C).Faithful
-- Init.Data.Option.Lemmas
Option.isSome_choice_iff_nonempty : ∀ {α : Type u_1}, (Option.choice α).isSome = true ↔ Nonempty α
-- Init.Prelude
instHDiv : {α : Type u_1} → [Div α] → HDiv α α α
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.range_mk : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α}, Set.range QuotientGroup.mk = Set.univ
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.coe_mul : ∀ {α : Type u₁} {β : Type u₂} [inst : MulZeroClass β] (g₁ g₂ : α →₀ β), ⇑(g₁ * g₂) = ⇑g₁ * ⇑g₂
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.sum_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
  {J : Type u_1} (s : Finset J) (f : J → (P ⟶ Q)) (g : Q ⟶ R),
  CategoryTheory.CategoryStruct.comp (∑ j ∈ s, f j) g = ∑ j ∈ s, CategoryTheory.CategoryStruct.comp (f j) g
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.isNNRat_zpow_pos : ∀ {α : Type u_1} [inst : DivisionSemiring α] {a : α} {b : ℤ} {nb num den : ℕ},
  Mathlib.Meta.NormNum.IsNat b nb →
    Mathlib.Meta.NormNum.IsNNRat (a ^ nb) num den → Mathlib.Meta.NormNum.IsNNRat (a ^ b) num den
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_div_Icc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => a / x) ⁻¹' Set.Icc b c = Set.Icc (a / c) (a / b)
-- Mathlib.Data.Nat.Choose.Sum
/-- A special case of the **binomial theorem**  -/
sub_pow : ∀ {R : Type u_1} [inst : CommRing R] (x y : R) (n : ℕ),
  (x - y) ^ n = ∑ m ∈ Finset.range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)
-- Mathlib.Data.Sym.Basic
Sym.card_coe : ∀ {α : Type u_1} {n : ℕ} {s : Sym α n}, (↑s).card = n
-- Batteries.Util.ProofWanted
DerivedWanted.ofVal.inj : ∀ {α : Sort u} {val val_1 : α}, { val := val } = { val := val_1 } → val = val_1
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
/-- To show that `f : X ⟶ Y` is formally unramified,
it suffices to check for that every following commuting diagram
```
Spec R --→ X
  |        |
  ↓        ↓
Spec S --→ Y
```
with `S = R/I` for some `I² = 0`, there exists at most one arrow `Spec S ⟶ X` making
the diagram commute.
 -/
AlgebraicGeometry.FormallyUnramified.of_hom_ext : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  (∀ (R S : CommRingCat) (φ : R ⟶ S),
      Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom φ) →
        RingHom.ker (CommRingCat.Hom.hom φ) ^ 2 = ⊥ →
          ∀ (g₁ g₂ : AlgebraicGeometry.Spec R ⟶ X),
            CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map φ) g₁ =
                CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map φ) g₂ →
              CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → g₁ = g₂) →
    AlgebraicGeometry.FormallyUnramified f
-- Lean.Parser.Command
Lean.Parser.Command.check : Lean.Parser.Parser
-- Mathlib.Topology.ContinuousOn
continuous_prod_of_discrete_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [DiscreteTopology β] {f : α × β → γ},
  Continuous f ↔ ∀ (b : β), Continuous fun x => f (x, b)
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_subset_coe : ∀ {α : Type u_1} [inst : LE α] {s t : LowerSet α}, ↑s ⊆ ↑t ↔ s ≤ t
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpOptions.triggerCharacters? : Lean.Lsp.SignatureHelpOptions → Option (Array String)
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.range_le_ker_iff : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {M : Type u_7} [inst_2 : MulOneClass M]
  (f : G →* G') (g : G' →* M), f.range ≤ g.ker ↔ g.comp f = 1
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- `G.PreservesLeftKanExtension F L` asserts that `G` preserves all pointwise left Kan extensions
of `F` along `L`.  -/
CategoryTheory.Functor.PreservesPointwiseLeftKanExtension : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                CategoryTheory.Functor B D → CategoryTheory.Functor A B → CategoryTheory.Functor A C → Prop
-- Mathlib.MeasureTheory.Measure.EverywherePos
MeasureTheory.Measure.everywherePosSubset.eq_1 : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α),
  μ.everywherePosSubset s = {x | x ∈ s ∧ ∀ n ∈ nhdsWithin x s, 0 < μ n}
-- Lean.Meta.Instances
Lean.Meta.InstanceKey : Type
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_maxKey?_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.maxKey? (Std.Internal.List.insertEntryIfNew k v l)).isSome = true
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- The `mixedEmbedding.norm` of `a : integerSet K` as a natural number, see also
`intNorm_coe`.  -/
NumberField.mixedEmbedding.fundamentalCone.intNorm : {K : Type u_1} →
  [inst : Field K] → [inst_1 : NumberField K] → ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K) → ℕ
-- Mathlib.GroupTheory.RegularWreathProduct
instFiniteIteratedWreathProduct : ∀ (G : Type u) (n : ℕ) [Finite G], Finite (IteratedWreathProduct G n)
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- One implication of the portmanteau theorem: if for all closed sets `F` we have the limsup
condition `limsup μsₙ(F) ≤ μ(F)`, then the measures `μsₙ` converge weakly to the measure `μ`.
Formulated here for countably generated filters.  -/
MeasureTheory.tendsto_of_forall_isClosed_limsup_le : ∀ {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [inst : TopologicalSpace Ω] [inst_1 : OpensMeasurableSpace Ω]
  {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} {L : Filter ι}
  [L.IsCountablyGenerated],
  (∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => (μs i) F) L ≤ μ F) → Filter.Tendsto μs L (nhds μ)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.sub_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f g : T₁ ⟶ T₂), (f - g).hom₃ = f.hom₃ - g.hom₃
-- Mathlib.Analysis.Fourier.AddCircle
/-- We define `fourierBasis` to be a `ℤ`-indexed Hilbert basis for `Lp ℂ 2 haarAddCircle`,
which by definition is an isometric isomorphism from `Lp ℂ 2 haarAddCircle` to `ℓ²(ℤ, ℂ)`.  -/
fourierBasis : {T : ℝ} → [hT : Fact (0 < T)] → HilbertBasis ℤ ℂ ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)
-- Mathlib.Topology.Gluing
TopCat.GlueData.ι_eq_iff_rel : ∀ (D : TopCat.GlueData) (i j : D.J) (x : ↑(D.U i)) (y : ↑(D.U j)),
  (CategoryTheory.ConcreteCategory.hom (D.ι i)) x = (CategoryTheory.ConcreteCategory.hom (D.ι j)) y ↔
    D.Rel ⟨i, x⟩ ⟨j, y⟩
-- Mathlib.Algebra.Group.Graph
MonoidHom.mem_graph : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {f : G →* H} {x : G × H}, x ∈ f.graph ↔ f x.1 = x.2
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewRawFact.prop : Lean.Meta.Grind.NewRawFact → Lean.Expr
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
/-- Functional equation for the exponential zeta function.  -/
HurwitzZeta.expZeta_one_sub : ∀ (a : UnitAddCircle) {s : ℂ},
  (∀ (n : ℕ), s ≠ 1 - ↑n) →
    HurwitzZeta.expZeta a (1 - s) =
      (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s *
        (Complex.exp (↑Real.pi * Complex.I * s / 2) * HurwitzZeta.hurwitzZeta a s +
          Complex.exp (-↑Real.pi * Complex.I * s / 2) * HurwitzZeta.hurwitzZeta (-a) s)
-- Mathlib.Data.QPF.Univariate.Basic
QPF.id_map : ∀ {F : Type u → Type v} [q : QPF F] {α : Type u} (x : F α), id <$> x = x
-- Mathlib.Analysis.Convex.Function
StrictConvexOn.comp_strictConcaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α},
  StrictConvexOn 𝕜 (f '' s) g →
    StrictConcaveOn 𝕜 s f → StrictAntiOn g (f '' s) → Set.InjOn f s → StrictConvexOn 𝕜 s (g ∘ f)
-- Mathlib.Probability.Independence.Kernel.Indep
/-- **Alias** of the forward direction of `ProbabilityTheory.Kernel.iIndepSets_congr`. -/
ProbabilityTheory.Kernel.iIndepSets.congr : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ι → Set (Set Ω)},
  ⇑κ =ᵐ[μ] ⇑η → ProbabilityTheory.Kernel.iIndepSets π κ μ → ProbabilityTheory.Kernel.iIndepSets π η μ
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.LeftExactFunctor.whiskeringRight_map_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : D ⥤ₗ E} (η : F ⟶ G) (H : C ⥤ₗ D),
  ((CategoryTheory.LeftExactFunctor.whiskeringRight C D E).map η).app H =
    CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringRight C D E).map η.hom).app H.obj)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
DifferentiableOn.sin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E},
  DifferentiableOn ℝ f s → DifferentiableOn ℝ (fun x => Real.sin (f x)) s
-- Mathlib.Analysis.Convex.Strict
StrictConvex.eq : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommMonoid E] [inst_4 : SMul 𝕜 E] {s : Set E} {x y : E} {a b : 𝕜},
  StrictConvex 𝕜 s → x ∈ s → y ∈ s → 0 < a → 0 < b → a + b = 1 → a • x + b • y ∉ interior s → x = y
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedGE_map_ofDual`. -/
List.SortedLE.of_map_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, l.SortedLE → (List.map (⇑OrderDual.ofDual) l).SortedGE
-- Mathlib.RepresentationTheory.Rep.Iso
Rep.free_projective : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {α : Type (max w u)},
  CategoryTheory.Projective (Rep.free k G α)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.toAlgHom_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_2} {S' : Type u_1} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f : P.Hom P') (x : P.Ring), f.toAlgHom x = f.toRingHom x
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.aleph0_mul_ofENat : ∀ {m : ℕ∞}, m ≠ 0 → Cardinal.aleph0 * ↑m = Cardinal.aleph0
-- Mathlib.Algebra.Star.Subalgebra
Subalgebra.copy.congr_simp : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S S_1 : Subalgebra R A) (e_S : S = S_1) (s s_1 : Set A) (e_s : s = s_1) (hs : s = ↑S), S.copy s hs = S_1.copy s_1 ⋯
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_union : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E]
  [inst_3 : TopologicalSpace E] {s t : Set E},
  Bornology.IsVonNBounded 𝕜 (s ∪ t) ↔ Bornology.IsVonNBounded 𝕜 s ∧ Bornology.IsVonNBounded 𝕜 t
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.smulAntidiagonal_min_smul_min : ∀ {G : Type u_1} {P : Type u_2} [inst : LinearOrder G] [inst_1 : LinearOrder P] [inst_2 : SMul G P]
  [inst_3 : IsOrderedCancelSMul G P] {s : Set G} {t : Set P} (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty)
  (hnt : t.Nonempty), Finset.SMulAntidiagonal (hs.min hns • ht.min hnt) ⋯ = {(hs.min hns, ht.min hnt)}
-- Init.Ext
funext_iff : ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}, f = g ↔ ∀ (x : α), f x = g x
-- Lean.Util.ReplaceLevel
Lean.Expr.ReplaceLevelImpl.State : Type
-- Mathlib.Computability.ContextFreeGrammar
/-- **Alias** of the reverse direction of `ContextFreeGrammar.generates_reverse`. -/
ContextFreeGrammar.Generates.reverse : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)}, g.Generates u → g.reverse.Generates u.reverse
-- Std.Tactic.Do.Syntax
/-- Duplicate a stateful `Std.Do.SPred` hypothesis.  -/
Lean.Parser.Tactic.mdup : Lean.ParserDescr
-- Mathlib.Data.Nat.ChineseRemainder
Nat.chineseRemainderOfList.congr_simp : ∀ {ι : Type u_1} (a s : ι → ℕ) (l : List ι) (a_1 : List.Pairwise (Function.onFun Nat.Coprime s) l),
  Nat.chineseRemainderOfList a s l a_1 = Nat.chineseRemainderOfList a s l a_1
-- Mathlib.Algebra.Star.Module
starLinearEquiv_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A] (a : A), (starLinearEquiv R) a = star a
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.initial_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y},
  CategoryTheory.Factorisation.initial.π = f
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_self_eq : ∀ (𝕜 : Type u_1) {E : Type u_2} {H : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {x : H}, ↑(extChartAt I x) = ↑I
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.IsModHom.map_smul_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X] {Y : C}
  [inst_4 : CategoryTheory.ModObj M Y] (f : X ⟶ Y) [CategoryTheory.IsModHom M f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X)
  {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (m • x) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (m • CategoryTheory.CategoryStruct.comp x f) h