mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.Quotient.addSubgroup_quotient_eq_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : AddSubgroup G}
  {x : AddAction.orbitRel.Quotient G α} {a b : ↑x.orbit}, ⟦a⟧ = ⟦b⟧ ↔ ⟦↑a⟧ = ⟦↑b⟧
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.dist_single_same : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (i : ι) (a b : 𝕜),
  dist (EuclideanSpace.single i a) (EuclideanSpace.single i b) = dist a b
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
IsZGroup.of_squarefree : ∀ {G : Type u_1} [inst : Group G], Squarefree (Nat.card G) → IsZGroup G
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂.run'.eq_3 : ∀ {α : Type u_1} (le : α → α → Bool) (n_1 : ℕ) (xs : { l // l.length = n_1 + 2 }),
  List.MergeSort.Internal.mergeSortTR₂.run'✝ le xs =
    match List.MergeSort.Internal.splitRevInTwo' xs with
    | (l, r) =>
      List.MergeSort.Internal.mergeTR (List.MergeSort.Internal.mergeSortTR₂.run'✝ le r)
        (List.MergeSort.Internal.mergeSortTR₂.run✝ le l) le
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The full subgroupoid on a set `D : Set C`  -/
CategoryTheory.Subgroupoid.full : {C : Type u} → [inst : CategoryTheory.Groupoid C] → Set C → CategoryTheory.Subgroupoid C
-- Mathlib.RingTheory.Kaehler.Polynomial
instFreeMvPolynomialKaehlerDifferential : ∀ (R : Type u) [inst : CommRing R] (σ : Type u_1), Module.Free (MvPolynomial σ R) Ω[MvPolynomial σ R⁄R]
-- Mathlib.Order.Defs.LinearOrder
min_ind : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} {motive : α → Prop},
  (a ≤ b → motive a) → (b ≤ a → motive b) → motive (min a b)
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Real.hasDerivAt_fourier : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E},
  MeasureTheory.Integrable f MeasureTheory.volume →
    MeasureTheory.Integrable (fun x => x • f x) MeasureTheory.volume →
      ∀ (w : ℝ),
        HasDerivAt (FourierTransform.fourier f)
          (FourierTransform.fourier (fun x => (-2 * ↑Real.pi * Complex.I * ↑x) • f x) w) w
-- Mathlib.Algebra.WithConv
WithConv.instAddAction : {R : Type u_1} → {A : Type u_2} → [inst : AddMonoid R] → [AddAction R A] → AddAction R (WithConv A)
-- Mathlib.Topology.MetricSpace.HolderNorm
MemHolder.add : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : NormedAddCommGroup Y] {r : NNReal} {f g : X → Y},
  MemHolder r f → MemHolder r g → MemHolder r (f + g)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.equiv_iff_toArray_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ Std.DTreeMap.Raw.Const.toArray t₁ = Std.DTreeMap.Raw.Const.toArray t₂)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX_d' : ∀ {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 i j),
  ¬c.Rel j (c.next j) →
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ j i hij)
        (HomologicalComplex.homotopyCofiber.d φ i j) =
      CategoryTheory.CategoryStruct.comp (φ.f j) (HomologicalComplex.homotopyCofiber.inrX φ j)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, k ∈ m₂ → (m₁ ∩ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.Data.Finset.Sups
Finset.empty_sups : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {t : Finset α}, ∅ ⊻ t = ∅
-- Mathlib.Order.BoundedOrder.Lattice
min_ne_bot : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderBot α] {a b : α}, a ≠ ⊥ → b ≠ ⊥ → min a b ≠ ⊥
-- Mathlib.RingTheory.Noetherian.Basic
Submodule.finite_ne_bot_of_iSupIndep : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsNoetherian R M]
  {ι : Type u_5} {N : ι → Submodule R M}, iSupIndep N → {i | N i ≠ ⊥}.Finite
-- Mathlib.Algebra.NoZeroSMulDivisors.Defs
/-- Pullback a `NoZeroSMulDivisors` instance along an injective function.  -/
Function.Injective.noZeroSMulDivisors : ∀ {R : Type u_4} {M : Type u_5} {N : Type u_6} [inst : Zero R] [inst_1 : Zero M] [inst_2 : Zero N] [inst_3 : SMul R M]
  [inst_4 : SMul R N] [NoZeroSMulDivisors R N] (f : M → N),
  Function.Injective f → f 0 = 0 → (∀ (c : R) (x : M), f (c • x) = c • f x) → NoZeroSMulDivisors R M
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.symm : ∀ {α : Type u_1} {V : Type u_2} [inst : Zero α] [inst_1 : One α] {A : Matrix V V α}, A.IsAdjMatrix → A.IsSymm
-- Mathlib.Data.Multiset.Lattice
Multiset.sup_cons : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (a : α) (s : Multiset α), (a ::ₘ s).sup = a ⊔ s.sup
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
min_mul_mul_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Mul α] [MulLeftMono α] (a b c : α), min (a * b) (a * c) = a * min b c
-- Std.Do.SPred.SVal
Std.Do.SVal.getThe_here : ∀ {σs : List (Type u)} (σ : Type u) (s : σ), Std.Do.SVal.getThe σ s = Std.Do.SVal.curry fun x => s
-- Mathlib.Logic.Equiv.Defs
Equiv.refl_symm : ∀ {α : Sort u}, (Equiv.refl α).symm = Equiv.refl α
-- Mathlib.Logic.Equiv.Basic
/-- A subtype of a dependent triple which pins down both bases is equivalent to the
respective fiber.  -/
Equiv.sigmaSigmaSubtype : {α : Type u_9} →
  {β : α → Type u_10} →
    {γ : (a : α) → β a → Type u_11} →
      (p : (a : α) × β a → Prop) →
        [uniq : Unique { ab // p ab }] → {a : α} → {b : β a} → p ⟨a, b⟩ → { s // p ⟨s.fst, s.snd.fst⟩ } ≃ γ a b
-- Mathlib.Order.UpperLower.Basic
/-- **Alias** of `isUpperSet_setOfPred`. -/
isUpperSet_setOf : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop}, IsUpperSet {a | p a} ↔ Monotone p
-- Mathlib.SetTheory.Ordinal.Univ
RelEmbedding.ofMonotone.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : Std.Trichotomous r] [inst_1 : Std.Asymm s]
  (f f_1 : α → β) (e_f : f = f_1) (H : ∀ (a b : α), r a b → s (f a) (f b)),
  RelEmbedding.ofMonotone f H = RelEmbedding.ofMonotone f_1 ⋯
-- Init.Data.String.Lemmas.Iterate
/-- A list of all positions strictly before `p`, ordered from largest to smallest.

This function is not meant to be used in actual programs. Actual programs should use
`Slice.revPositionsFrom` and `Slice.revPositions`.
 -/
String.Model.revPositionsFrom : {s : String} → s.Pos → List { p // p ≠ s.endPos }
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.Score.isAwful : Lean.FuzzyMatching.Score✝ → Bool
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.rotCompInvRot.hom.app X).hom₁ =
    (CategoryTheory.shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app X.obj₁
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.lift_ofList : ∀ {α : Type u_1} {M : Type u_4} [inst : AddMonoid M] (f : α → M) (l : List α),
  (FreeAddMonoid.lift f) (FreeAddMonoid.ofList l) = (List.map f l).sum
-- Init.Data.Array.Basic
/-- Finds the index of the first element of an array for which the monadic predicate `p` returns `true`.
Elements are examined in order from left to right, and the search is terminated when an element that
satisfies `p` is found. If no such element exists in the array, then `none` is returned.
 -/
Array.findIdxM? : {α : Type u} → {m : Type → Type u_1} → [Monad m] → (α → m Bool) → Array α → m (Option ℕ)
-- Mathlib.Order.Filter.Ker
Filter.ker_sInf : ∀ {α : Type u_2} (S : Set (Filter α)), (sInf S).ker = ⋂ f ∈ S, f.ker
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
RCLike.uniqueNonUnitalContinuousFunctionalCalculus : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace A] [T2Space A] [inst_3 : NonUnitalRing A]
  [inst_4 : StarRing A] [inst_5 : Module 𝕜 A] [inst_6 : IsScalarTower 𝕜 A A] [inst_7 : SMulCommClass 𝕜 A A],
  ContinuousMapZero.UniqueHom 𝕜 A
-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
/-- If the operation `Φ` on sections of vector bundles `V` and `V'` is tensorial at `x` in each
argument, then it depends only on the value of the sections at `x`.  -/
TensorialAt.pointwise₂ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {F' : Type u_7}
  [inst_13 : NormedAddCommGroup F'] [inst_14 : NormedSpace 𝕜 F'] {V' : M → Type u_8}
  [inst_15 : TopologicalSpace (Bundle.TotalSpace F' V')] [inst_16 : (x : M) → AddCommGroup (V' x)]
  [inst_17 : (x : M) → Module 𝕜 (V' x)] [inst_18 : (x : M) → TopologicalSpace (V' x)] [inst_19 : FiberBundle F' V']
  {A : Type u_9} [inst_20 : AddCommGroup A] [inst_21 : Module 𝕜 A] [inst_22 : VectorBundle 𝕜 F V]
  [inst_23 : VectorBundle 𝕜 F' V'] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 F']
  [ContMDiffVectorBundle 1 F V I] [ContMDiffVectorBundle 1 F' V' I] {Φ : ((x : M) → V x) → ((x : M) → V' x) → A}
  {x : M},
  (∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun x => Φ x τ) x) →
    (∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (fun x => Φ σ x) x) →
      ∀ {σ σ' : (x : M) → V x} {τ τ' : (x : M) → V' x},
        MDiffAt (T% σ) x →
          MDiffAt (T% σ') x → MDiffAt (T% τ) x → MDiffAt (T% τ') x → σ x = σ' x → τ x = τ' x → Φ σ τ = Φ σ' τ'
-- Mathlib.Order.Monotone.Defs
AntitoneOn.comp_MonotoneOn : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α} {t : Set β}, AntitoneOn g t → MonotoneOn f s → Set.MapsTo f s t → AntitoneOn (g ∘ f) s
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.of_isCoveringMap_restrictPreimage : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} (s : Set X),
  IsOpen s → IsOpen (f ⁻¹' s) → IsCoveringMap (s.restrictPreimage f) → IsCoveringMapOn f s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiffAt.cos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {n : WithTop ℕ∞},
  ContDiffAt ℝ n f x → ContDiffAt ℝ n (fun x => Real.cos (f x)) x
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- Proof that `f(p) = H(0 ⟶ 0, p)`, with the appropriate casts  -/
ContinuousMap.Homotopy.apply_zero_path : ∀ {X Y : TopCat} {f g : C(↑X, ↑Y)} (H : f.Homotopy g) {x₀ x₁ : ↑X}
  (p : FundamentalGroupoid.fromTop x₀ ⟶ FundamentalGroupoid.fromTop x₁),
  (FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom f)).map p =
    CategoryTheory.CategoryStruct.comp (ContinuousMap.Homotopy.hcast ⋯)
      (CategoryTheory.CategoryStruct.comp
        ((FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom H.uliftMap)).map
          (ContinuousMap.Homotopy.prodToProdTopI
            (CategoryTheory.CategoryStruct.id (FundamentalGroupoid.fromTop { down := 0 })) p))
        (ContinuousMap.Homotopy.hcast ⋯))
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
/-- `Submodule.mkQ` as a `ContinuousLinearMap`.  -/
Submodule.mkQL : {R : Type u_1} →
  [inst : Ring R] →
    {M : Type u_3} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → (S : Submodule R M) → M →L[R] M ⧸ S
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.SolverExtension.mk.sizeOf_spec : ∀ {σ : Type} [inst : SizeOf σ] (id : ℕ) (mkInitial : IO σ)
  (internalize : Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM Unit)
  (newEq newDiseq : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit) (mbtc : Lean.Meta.Grind.GoalM Bool)
  (action : Lean.Meta.Grind.Action) (check : Lean.Meta.Grind.GoalM Bool) (checkInv : Lean.Meta.Grind.GoalM Unit),
  sizeOf
      { id := id, mkInitial := mkInitial, internalize := internalize, newEq := newEq, newDiseq := newDiseq,
        mbtc := mbtc, action := action, check := check, checkInv := checkInv } =
    1 + sizeOf id
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.min?_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : Min α]
  [inst_1 : LE α] [Std.LawfulOrderOrd α] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α] [Std.LawfulEqOrd α],
  t.WF → t.keys.min? = t.minKey?
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sInf_caratheodory : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {m : Set (MeasureTheory.Measure α)} (s : Set α),
  MeasurableSet s → MeasurableSet s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → t.contains k = t.contains k'
-- Mathlib.Order.Filter.Pointwise
Filter.add_neBot_iff : ∀ {α : Type u_2} [inst : Add α] {f g : Filter α}, (f + g).NeBot ↔ f.NeBot ∧ g.NeBot
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- The image of `I` in the localization at `I.primeCompl` is a maximal ideal, and in particular
it is the unique maximal ideal given by the local ring structure `AtPrime.isLocalRing`  -/
Localization.AtPrime.map_eq_maximalIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} [hI : I.IsPrime],
  Ideal.map (algebraMap R (Localization.AtPrime I)) I = IsLocalRing.maximalIdeal (Localization I.primeCompl)
-- Mathlib.Algebra.Module.Defs
Module.ext : ∀ {R : Type u} {M : Type v} {inst : Semiring R} {inst_1 : AddCommMonoid M} {x y : Module R M},
  SMul.smul = SMul.smul → x = y
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.map_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Continuous f) (x : α), TopologicalSpace.Compacts.map f hf {x} = {f x}
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filterMap!.eq_def : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] (f : (a : α) → β a → Option (γ a))
  (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.filterMap! f t =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => Std.DTreeMap.Internal.Impl.leaf
    | Std.DTreeMap.Internal.Impl.inner size k v l r =>
      match f k v with
      | none => (Std.DTreeMap.Internal.Impl.filterMap! f l).link2! (Std.DTreeMap.Internal.Impl.filterMap! f r)
      | some v' =>
        Std.DTreeMap.Internal.Impl.link! k v' (Std.DTreeMap.Internal.Impl.filterMap! f l)
          (Std.DTreeMap.Internal.Impl.filterMap! f r)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- Every acyclic subgraph can be extended to a spanning forest.  -/
SimpleGraph.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic : ∀ {V : Type u_1} {G H : SimpleGraph V},
  H ≤ G → H.IsAcyclic → ∃ F, H ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.sc'Map_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S₁ S₂ : CategoryTheory.ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex)
  (i j k : ℕ) (hij : autoParam (i + 1 = j) CategoryTheory.ComposableArrows.sc'Map._auto_1)
  (hjk : autoParam (j + 1 = k) CategoryTheory.ComposableArrows.sc'Map._auto_3)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.sc'Map._auto_5),
  (CategoryTheory.ComposableArrows.sc'Map φ h₁ h₂ i j k hij hjk hk).τ₃ = φ.app ⟨k, ⋯⟩
-- Mathlib.Data.PNat.Basic
PNat.pos_of_div_pos : ∀ {n : ℕ+} {a : ℕ}, a ∣ ↑n → 0 < a
-- Mathlib.Topology.OmegaCompletePartialOrder
Scott.isOpen_univ : ∀ (α : Type u) [inst : OmegaCompletePartialOrder α], Scott.IsOpen α Set.univ
-- Mathlib.CategoryTheory.ConcreteCategory.Representable
/-- The natural bijection `(X ⟶ Y) ≃ F.obj (op X)`.  -/
CategoryTheory.Functor.RepresentableBy.homEquiv' : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F : CategoryTheory.Functor Cᵒᵖ D} →
          {CD : D → Type u_3} →
            {FD : D → D → Type u_4} →
              [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                [inst_3 : CategoryTheory.ConcreteCategory D FD] →
                  {Y : C} →
                    (F.comp (CategoryTheory.forget D)).RepresentableBy Y →
                      {X : C} → (X ⟶ Y) ≃ CategoryTheory.ToType (F.obj (Opposite.op X))
-- Mathlib.Analysis.Normed.Ring.Units
NormedRing.inverse_one_sub_norm : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R], (fun t => Ring.inverse (1 - t)) =O[nhds 0] fun _t => 1
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.toEnd_apply : ∀ {G : Type u_1} [inst : Add G] {a : G}, ⇑AddConstMap.toEnd = DFunLike.coe
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic.0.MeasureTheory.simpleFuncAux.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : MeasurableSingletonClass α] (f f_1 : α → β),
  f = f_1 →
    ∀ (g g_1 : ℕ → α),
      g = g_1 → ∀ (a a_1 : ℕ), a = a_1 → MeasureTheory.simpleFuncAux✝ f g a = MeasureTheory.simpleFuncAux✝ f_1 g_1 a_1
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.symm_homotopyInvHomId : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : HomotopyEquiv C D),
  f.symm.homotopyInvHomId = f.homotopyHomInvId
-- Mathlib.CategoryTheory.WithTerminal.Cone
/-- The category of functors `J ⥤ Over X` can be seen as part of a comma category,
namely the comma category constructed from the identity of the category of functors
`J ⥤ C` and the functor that maps `X : C` to the constant functor `J ⥤ C`.

Given a functor `K : J ⥤ Over X`, it is mapped to a natural transformation from the
obvious functor `J ⥤ C` to the constant functor `X`.  -/
CategoryTheory.WithTerminal.commaFromOver : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {X : C} →
          CategoryTheory.Functor (CategoryTheory.Functor J (CategoryTheory.Over X))
            (CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor J C))
              (CategoryTheory.Functor.const J))
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.instRpcEncodable : {α : Type} → [Lean.Server.RpcEncodable α] → Lean.Server.RpcEncodable (Lean.Widget.TaggedText α)
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.interedges_eq_biUnion : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β}
  [inst_1 : DecidableEq α] [inst_2 : DecidableEq β],
  Rel.interedges r s t = s.biUnion fun x => Finset.map { toFun := fun x_1 => (x, x_1), inj' := ⋯ } ({y ∈ t | r x y})
-- Mathlib.Algebra.Group.Basic
sub_add_eq_sub_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a - (b + c) = a - b - c
-- Mathlib.GroupTheory.Rank
AddGroup.rank_le_of_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] [inst_2 : AddGroup.FG G]
  [inst_3 : AddGroup.FG H] (f : G →+ H), Function.Surjective ⇑f → AddGroup.rank H ≤ AddGroup.rank G
-- Mathlib.RingTheory.Congruence.Basic
RingCon.smulCommClass : ∀ {α : Type u_1} {R : Type u_3} [inst : Add R] [inst_1 : MulOneClass R] [inst_2 : SMul α R]
  [inst_3 : IsScalarTower α R R] [SMulCommClass α R R] (c : RingCon R), SMulCommClass α c.Quotient c.Quotient
-- Mathlib.GroupTheory.Perm.List
List.form_perm_zpow_apply_mem_imp_mem : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), ∀ x ∈ l, ∀ (n : ℤ), (l.formPerm ^ n) x ∈ l
-- Mathlib.Data.ENat.Basic
ENat.add_le_add_iff_left : ∀ {m n k : ℕ∞}, k ≠ ⊤ → (k + n ≤ k + m ↔ n ≤ m)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toListRev.go.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} [inst : Monad m] {β : Type w} [inst_1 : Std.Iterator α m β] (it : Std.IterM m β)
  (acc : List β),
  Std.IterM.toListRev.go it acc =
    WellFounded.extrinsicFix₂ (InvImage Std.IterM.TerminationMeasures.Finite.Rel fun x => x.fst.finitelyManySteps!)
      (fun it acc recur => do
        let __do_lift ← it.step
        match __do_lift.inflate with
          | ⟨Std.IterStep.yield it' out, h⟩ => recur it' (out :: acc) ⋯
          | ⟨Std.IterStep.skip it', h⟩ => recur it' acc ⋯
          | ⟨Std.IterStep.done, property⟩ => pure acc)
      it acc
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.CoextendScalars.instCoeFunCarrierObjCoextendScalarsForall : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) → (M : ModuleCat R) → CoeFun ↑((ModuleCat.coextendScalars f).obj M) fun x => S → ↑M
-- Mathlib.Topology.Order.LowerUpperTopology
/-- The closure of a singleton `{a}` in the lower topology is the left-closed right-infinite interval
$[a, ∞)$.
 -/
Topology.IsLower.closure_singleton : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α] (a : α), closure {a} = Set.Ici a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_apply : ∀ {F : Type u} [inst : Field F] (W : WeierstrassCurve.Jacobian F) [inst_1 : DecidableEq F] (P : W.Point),
  (WeierstrassCurve.Jacobian.Point.toAffineAddEquiv W) P = P.toAffineLift
-- Mathlib.Topology.Constructions
/-- Let `s, t ⊆ X` be two subsets of a topological space `X`.  If `t ⊆ s` and the topology induced
by `X` on `s` is discrete, then also the topology induces on `t` is discrete.

(Compare `IsDiscrete.mono` which is the same thing stated without using subtypes.)  -/
DiscreteTopology.of_subset : ∀ {X : Type u_5} [inst : TopologicalSpace X] {s t : Set X}, DiscreteTopology ↑s → t ⊆ s → DiscreteTopology ↑t
-- Mathlib.Analysis.Calculus.FDeriv.WithLp
differentiableAt_piLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup H] [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedSpace 𝕜 H] [Finite ι] (p : ENNReal) [Fact (1 ≤ p)] {f : H → PiLp p E} {y : H},
  DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun x => (f x).ofLp i) y
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def
ProbabilityTheory.HasGaussianLaw.isGaussian_map : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E]
  [inst_2 : Module ℝ E] [mE : MeasurableSpace E] {X : Ω → E} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.HasGaussianLaw X P → ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map X P)
-- Mathlib.RingTheory.RegularLocalRing.Defs
IsRegularLocalRing.instOfIsLocalRingOfIsDomainOfIsPrincipalIdealRing : ∀ (R : Type u_1) [inst : CommRing R] [IsLocalRing R] [IsDomain R] [IsPrincipalIdealRing R], IsRegularLocalRing R
-- Mathlib.Order.Category.LinOrd
LinOrd.Iso.mk_inv : ∀ {α β : LinOrd} (e : ↑α ≃o ↑β), (LinOrd.Iso.mk e).inv = LinOrd.ofHom ↑e.symm
-- Mathlib.Order.Sublattice
Sublattice.pi_univ_bot : ∀ {κ : Type u_5} {π : κ → Type u_6} [inst : (i : κ) → Lattice (π i)] [Nonempty κ],
  (Sublattice.pi Set.univ fun x => ⊥) = ⊥