mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.SymmDiff
Finset.symmDiff_nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, (symmDiff s t).Nonempty ↔ s ≠ t
-- Mathlib.Order.Bounds.Image
MonotoneOn.image_lowerBounds_subset_lowerBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α},
  MonotoneOn f t → s ⊆ t → f '' (lowerBounds s ∩ t) ⊆ lowerBounds (f '' s)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The distance to a set is controlled by the Hausdorff distance.  -/
Metric.infDist_le_hausdorffDist_of_mem : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {x : α},
  x ∈ s → Metric.hausdorffEDist s t ≠ ⊤ → Metric.infDist x t ≤ Metric.hausdorffDist s t
-- Mathlib.Util.Tactic
/-- `modifyLocalContext mvarId f` updates the local context of the metavariable
`mvarId` with `f`. The new local context must contain the same fvars as the old
local context and the types (and values, if any) of the fvars in the new local
context must be defeq to their equivalents in the old local context.

If `mvarId` does not refer to a declared metavariable, nothing happens.
 -/
Mathlib.Tactic.modifyLocalContext : {m : Type → Type} → [Lean.MonadMCtx m] → Lean.MVarId → (Lean.LocalContext → Lean.LocalContext) → m Unit
-- Mathlib.Algebra.Group.Basic
inv_mul' : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α), (a * b)⁻¹ = a⁻¹ / b
-- Init.Data.Array.MapIdx
Array.mapFinIdx_eq_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β} {g : ℕ → α → β},
  (∀ (i : ℕ) (h : i < xs.size), f i xs[i] h = g i xs[i]) → xs.mapFinIdx f = Array.mapIdx g xs
-- Std.Http.Internal.Char
_private.Std.Http.Internal.Char.0.Std.Http.Internal.Char.qdtext.match_1.eq_3 : ∀ (motive : Char → Sort u_1) (h_1 : Unit → motive '\t') (h_2 : Unit → motive ' ') (h_3 : Unit → motive '!')
  (h_4 : (x : Char) → motive x),
  (match '!' with
    | '\t' => h_1 ()
    | ' ' => h_2 ()
    | '!' => h_3 ()
    | x => h_4 x) =
    h_3 ()
-- Mathlib.Probability.Moments.CovarianceBilinDual
StrongDual.toLpₗ.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {𝕜 : Type u_2}
  [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : NormedSpace 𝕜 E] (μ : MeasureTheory.Measure E) (p : ENNReal),
  StrongDual.toLpₗ μ p =
    if h_Lp : MeasureTheory.MemLp id p μ then
      { toFun := fun L => MeasureTheory.MemLp.toLp ⇑L ⋯, map_add' := ⋯, map_smul' := ⋯ }
    else 0
-- Mathlib.Data.Multiset.MapFold
Multiset.foldl_add : ∀ {α : Type u_1} {β : Type v} (f : β → α → β) [inst : RightCommutative f] (b : β) (s t : Multiset α),
  Multiset.foldl f b (s + t) = Multiset.foldl f (Multiset.foldl f b s) t
-- Lean.Parser.Command
Lean.Parser.Command.importPath.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).get k h' = t₂.get k ⋯
-- Init.Data.Fin.Lemmas
Fin.val_ofNat : ∀ (n : ℕ) [inst : NeZero n] (a : ℕ), ↑(Fin.ofNat n a) = a % n
-- Lean.Language.Basic
Lean.Language.SnapshotTree.mk.sizeOf_spec : ∀ (element : Lean.Language.Snapshot) (children : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)),
  sizeOf { element := element, children := children } = 1 + sizeOf element + sizeOf children
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Continuous.clog : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℂ},
  Continuous f → (∀ (x : α), f x ∈ Complex.slitPlane) → Continuous fun t => Complex.log (f t)
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Constructs a morphism to `star` from `of X`.  -/
CategoryTheory.WithTerminal.homFrom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) → CategoryTheory.WithTerminal.incl.obj X ⟶ CategoryTheory.WithTerminal.star
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.d₃_eq_zero : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄),
  ¬c₃.Rel i₃ (c₃.next i₃) → HomologicalComplex.mapBifunctor₁₂.d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0
-- Mathlib.Order.PropInstances
/-- Propositions form a distributive lattice.  -/
Prop.instDistribLattice : DistribLattice Prop
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.addCommMonoid : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] → [inst_4 : Module R M₂] → AddCommMonoid (MultilinearMap R M₁ M₂)
-- Mathlib.RingTheory.PrincipalIdealDomain
IsBezout.span_pair_isPrincipal : ∀ {R : Type u} [inst : Ring R] [IsBezout R] (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
-- Mathlib.Algebra.Prime.Lemmas
comap_prime : ∀ {M : Type u_1} {N : Type u_2} [inst : CommMonoidWithZero M] [inst_1 : CommMonoidWithZero N] {F : Type u_3}
  {G : Type u_4} [inst_2 : FunLike F M N] [MonoidWithZeroHomClass F M N] [inst_4 : FunLike G N M] [MulHomClass G N M]
  (f : F) (g : G) {p : M}, (∀ (a : M), g (f a) = a) → Prime (f p) → Prime p
-- Mathlib.Order.SuccPred.InitialSeg
PrincipalSeg.isSuccPrelimit_apply_iff : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α <i β),
  Order.IsSuccPrelimit (f.toRelEmbedding a) ↔ Order.IsSuccPrelimit a
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.ofHom_apply : ∀ {X Y : Type u} [inst : AddGroup X] [inst_1 : TopologicalSpace X] [inst_2 : IsTopologicalAddGroup X]
  [inst_3 : CompactSpace X] [inst_4 : TotallyDisconnectedSpace X] [inst_5 : AddGroup Y] [inst_6 : TopologicalSpace Y]
  [inst_7 : IsTopologicalAddGroup Y] [inst_8 : CompactSpace Y] [inst_9 : TotallyDisconnectedSpace Y] (f : X →ₜ+ Y)
  (x : X), (ProfiniteAddGrp.Hom.hom (ProfiniteAddGrp.ofHom f)) x = f x
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
/-- `minimalPrimes R` is the set of minimal primes of `R`.
This is defined as `Ideal.minimalPrimes ⊥`.  -/
minimalPrimes : (R : Type u_1) → [inst : CommSemiring R] → Set (Ideal R)
-- Mathlib.Algebra.Group.Units.Opposite
isUnit_unop : ∀ {M : Type u_2} [inst : Monoid M] {m : Mᵐᵒᵖ}, IsUnit (MulOpposite.unop m) ↔ IsUnit m
-- Batteries.Control.Nondet.Basic
/-- Lift a list of monadic values to a nondeterministic value.
We ensure that each monadic value is evaluated with the same backtrackable state.
 -/
Nondet.ofListM : {σ : Type} → {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α : Type} → List (m α) → Nondet m α
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.trans_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P P' : HomotopicalAlgebra.PrepathObject A)
  [inst_1 : CategoryTheory.Limits.HasPullback P.p₁ P'.p₀],
  (P.trans P').ι = CategoryTheory.Limits.pullback.lift P.ι P'.ι ⋯
-- Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
HasFDerivWithinAt.of_restrictScalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {f : E → F} {f' : E →L[𝕜'] F}
  {s : Set E} {x : E} {g' : E →L[𝕜] F},
  HasFDerivWithinAt f g' s x → ContinuousLinearMap.restrictScalars 𝕜 f' = g' → HasFDerivWithinAt f f' s x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
_private.Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected.0.SimpleGraph.Reachable.mem_subgraphVerts.aux : ∀ {V : Type u} {G : SimpleGraph V} {v : V} {H : G.Subgraph},
  (∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w) → ∀ {v' : V}, v' ∈ H.verts → ∀ (p : G.Walk v' v), v ∈ H.verts
-- Mathlib.Order.CompleteLattice.Defs
/-- In a linearly ordered type, we assume the order relations are all decidable.  -/
CompleteLinearOrder.toDecidableLE : {α : Type u_8} → [self : CompleteLinearOrder α] → DecidableLE α
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The full set is a block.  -/
MulAction.IsBlock.univ : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X], MulAction.IsBlock G Set.univ
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS₂_two : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), complEDS₂ b c d 2 = d
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α},
  k ∉ m₁ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- To construct a morphism from the explicit finite coproduct, it suffices to
specify a morphism from each of its factors.
This is essentially the universal property of the coproduct.
 -/
CompHausLike.finiteCoproduct.desc : {P : TopCat → Prop} →
  {α : Type w} →
    [inst : Finite α] →
      (X : α → CompHausLike P) →
        [inst_1 : CompHausLike.HasExplicitFiniteCoproduct X] →
          {B : CompHausLike P} → ((a : α) → X a ⟶ B) → (CompHausLike.finiteCoproduct X ⟶ B)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α} {h' : k ∈ Std.ExtDHashMap.filter f m},
  (Std.ExtDHashMap.filter f m).get k h' = m.get k ⋯
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- An induction principle for `C(s, 𝕜)`.  -/
ContinuousMap.induction_on : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {s : Set 𝕜} {p : C(↑s, 𝕜) → Prop},
  (∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)) →
    p (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) →
      p (star (ContinuousMap.restrict s (ContinuousMap.id 𝕜))) →
        (∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)) →
          (∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)) →
            ((∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f) → ∀ (f : C(↑s, 𝕜)), p f
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_sub_natCast : ∀ {x : NNReal}, x ≠ 0 → ∀ (y : ℝ) (n : ℕ), x ^ (y - ↑n) = x ^ y / x ^ n
-- Mathlib.Analysis.Quaternion
Quaternion.coe_ofComplex : ⇑Quaternion.ofComplex = Quaternion.coeComplex
-- Mathlib.Topology.List
List.Vector.continuous_eraseIdx : ∀ {α : Type u_1} [inst : TopologicalSpace α] {n : ℕ} {i : Fin (n + 1)}, Continuous (List.Vector.eraseIdx i)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {X : C} (h : F.cocones.CorepresentableBy X) (s : CategoryTheory.Limits.Cocone F),
  CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone h s = h.homEquiv.symm s.ι
-- Mathlib.SetTheory.Ordinal.Enum
/-- An order isomorphism between an unbounded set of ordinals and the ordinals.  -/
Ordinal.enumOrdOrderIso : (s : Set Ordinal.{u_1}) → ¬BddAbove s → Ordinal.{u_1} ≃o ↑s
-- Lean.Parser.Command
Lean.Parser.Command.checkAssertions.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.Internal.List.Associative
Std.Internal.List.minEntry?_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l l' : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → l.Perm l' → Std.Internal.List.minEntry? l = Std.Internal.List.minEntry? l'
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k a : α} {h' : a ∈ t.erase k}, (t.erase k).get a h' = t.get a ⋯
-- Mathlib.GroupTheory.Perm.Fin
Equiv.Perm.sign_eq_prod_prod_Ioi : ∀ {n : ℕ} (σ : Equiv.Perm (Fin n)), Equiv.Perm.sign σ = ∏ i, ∏ j > i, if σ i < σ j then 1 else -1
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instReprHost : Repr Std.Http.Header.Host
-- Mathlib.Analysis.Analytic.OfScalars
/-- The sum of the formal power series. Takes the value `0` outside the radius of convergence.  -/
FormalMultilinearSeries.ofScalarsSum : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : Field 𝕜] →
      [inst_1 : Ring E] → [Algebra 𝕜 E] → [inst : TopologicalSpace E] → [IsTopologicalRing E] → (ℕ → 𝕜) → E → E
-- Mathlib.Data.FP.Basic
FP.Float.inf.inj : ∀ {C : FP.FloatCfg} {a a_1 : Bool}, FP.Float.inf a = FP.Float.inf a_1 → a = a_1
-- Mathlib.Order.Birkhoff
OrderEmbedding.birkhoffSet_sup : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : Fintype α] [inst_2 : DecidablePred SupIrred] (a b : α),
  OrderEmbedding.birkhoffSet (a ⊔ b) = OrderEmbedding.birkhoffSet a ∪ OrderEmbedding.birkhoffSet b
-- Mathlib.CategoryTheory.Yoneda
/-- The data which expresses that a functor `F : C ⥤ Type v` is corepresentable by `X : C`.  -/
CategoryTheory.Functor.CorepresentableBy : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor C (Type v) → C → Type (max (max u₁ v) v₁)
-- Mathlib.Analysis.Calculus.FDeriv.Congr
fderivWithin_congr_set_nhdsNE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s t : Set E},
  s =ᶠ[nhdsWithin x {x}ᶜ] t → fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
-- Mathlib.CategoryTheory.Presentable.Adjunction
CategoryTheory.Equivalence.isAccessibleCategory : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (e : C ≌ D) [CategoryTheory.IsAccessibleCategory.{w, v, u} C], CategoryTheory.IsAccessibleCategory.{w, v', u'} D
-- Mathlib.Order.Interval.Set.SuccOrder
Set.Iic.coe_succ_of_not_isMax : ∀ {J : Type u_1} [inst : PartialOrder J] [inst_1 : SuccOrder J] {j : J} {i : ↑(Set.Iic j)},
  ¬IsMax i → ↑(Order.succ i) = Order.succ ↑i
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instTransVltVle : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : ValuativeRel R] → Trans ValuativeRel.vlt ValuativeRel.vle ValuativeRel.vlt
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_iSup : ∀ {X Y : TopCat} (f : X ⟶ Y) {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑Y),
  (TopologicalSpace.Opens.map f).obj (iSup U) = iSup ((TopologicalSpace.Opens.map f).obj ∘ U)
-- Init.Data.Option.Lemmas
Option.isSome.eq_2 : ∀ {α : Type u_1}, none.isSome = false
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi.eq_1 : ∀ (x : ℝ), Chebyshev.psi x = ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, ArithmeticFunction.vonMangoldt n
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.instEvalExprCutsatConfig : Lean.Elab.ConfigEval.EvalExpr Lean.Grind.CutsatConfig
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_continuous_ofLp : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β],
  Continuous WithLp.ofLp
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.zeroEquiv_ιMulti : ∀ {R : Type u} [inst : CommRing R] {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Fin 0 → M),
  (exteriorPower.zeroEquiv R M) ((exteriorPower.ιMulti R 0) f) = 1
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- A kernel pair gives rise to an equivalence relation.  -/
CategoryTheory.IsKernelPair.equivalenceRelation : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        {R : C} →
          (p₁ p₂ : R ⟶ X) →
            {t : CategoryTheory.Limits.PullbackCone p₂ p₁} →
              CategoryTheory.Limits.IsLimit t →
                CategoryTheory.IsKernelPair f p₁ p₂ → CategoryTheory.EquivalenceRelation p₁ p₂
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.polar_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E),
  ∀ y ∈ B.polar s, ∀ x ∈ s, ‖(B x) y‖ ≤ 1
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.OfLocalizationSpanTarget.ofLocalizationSpan : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.OfLocalizationSpanTarget P →
    RingHom.StableUnderCompositionWithLocalizationAwaySource P → RingHom.OfLocalizationSpan P
-- ProofWidgets.Presentation.Expr
/-- An `Expr` presenter is similar to a delaborator but outputs HTML trees instead of syntax, and
the output HTML can contain elements which interact with the original `Expr` in some way. We call
interactive outputs with a reference to the original input *presentations*.  -/
ProofWidgets.ExprPresenter : Type
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.widePullbackι.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  [inst_2 : CategoryTheory.WellPowered.{w, v₁, u₁} C] [inst_3 : CategoryTheory.Limits.HasWidePullbacks C] {A : C}
  (s : Set (CategoryTheory.Subobject A)),
  CategoryTheory.Subobject.widePullbackι s = CategoryTheory.Limits.limit.π (CategoryTheory.Subobject.wideCospan s) none
-- Mathlib.Combinatorics.Quiver.Symmetric
Prefunctor.map_reverse : ∀ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] [inst_2 : Quiver.HasReverse U]
  [inst_3 : Quiver.HasReverse V] (φ : U ⥤q V) [φ.MapReverse] {u v : U} (e : u ⟶ v),
  φ.map (Quiver.reverse e) = Quiver.reverse (φ.map e)
-- Mathlib.Topology.Instances.Irrational
Irrational.eventually_forall_le_dist_cast_rat_of_den_le : ∀ {x : ℝ}, Irrational x → ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in nhds 0, ∀ (r : ℚ), r.den ≤ n → ε ≤ dist x ↑r
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaAddGrpObj_obj_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (G : C)
  [inst_2 : CategoryTheory.AddGrpObj G] (X : Cᵒᵖ), ↑((CategoryTheory.yonedaAddGrpObj G).obj X) = (Opposite.unop X ⟶ G)
-- Mathlib.CategoryTheory.Limits.Presentation
/-- `X` is the colimit of the `Dᵢ` via `sᵢ`.  -/
CategoryTheory.Limits.ColimitPresentation.isColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} →
          (self : CategoryTheory.Limits.ColimitPresentation J X) →
            CategoryTheory.Limits.IsColimit { pt := X, ι := self.ι }
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- A typeclass for when a `MulAction X G` descends to the quotient `G ⧸ H`.  -/
MulAction.QuotientAction : {G : Type u} → (X : Type v) → [inst : Group G] → [inst_1 : Monoid X] → [MulAction X G] → Subgroup G → Prop
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- **Alias** of `tprod_setElem_eq_tprod_setElem_sdiff`.

---

If `f b = 1` for all `b ∈ t`, then the product of `f a` with `a ∈ s` is the same as the
product of `f a` with `a ∈ s ∖ t`.  -/
tprod_setElem_eq_tprod_setElem_diff : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} (s t : Set β),
  (∀ b ∈ t, f b = 1) → ∏' (a : ↑s), f ↑a = ∏' (a : ↑(s \ t)), f ↑a
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- Construct an affine equivalence from a linear equivalence and two base points.

Given a linear equivalence `A : V ≃ₗ[k] V` and base points `p₀ p₁ : P`, this constructs
the affine equivalence `T x = A (x -ᵥ p₀) +ᵥ p₁`. This is the standard way to convert
a linear automorphism into an affine automorphism with specified base point mapping.  -/
AffineEquiv.ofLinearEquiv : {k : Type u_10} →
  {V : Type u_11} →
    {P : Type u_12} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → (V ≃ₗ[k] V) → P → P → P ≃ᵃ[k] P
-- Lean.Util.Diff
/-- A histogram entry consists of the number of times the element occurs in the left and right input
arrays along with an index at which the element can be found, if applicable.
 -/
Lean.Diff.Histogram.Entry : Type u → ℕ → ℕ → Type
-- Mathlib.Order.RelIso.Basic
RelEmbedding.symm : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [Std.Symm s], Std.Symm r
-- Mathlib.Algebra.Quandle
/-- The universal enveloping group for the rack R.
 -/
Rack.EnvelGroup : (R : Type u_1) → [Rack R] → Type u_1
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The (degenerate) `m`-simplex in the standard simplex concentrated in vertex `k`.  -/
SSet.stdSimplex.const : (n : ℕ) → Fin (n + 1) → (m : SimplexCategoryᵒᵖ) → (SSet.stdSimplex.obj { len := n }).obj m
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.mono : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α},
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ {ν : MeasureTheory.Measure α}, ν.AbsolutelyContinuous μ → MeasureTheory.IsAddFundamentalDomain G s ν
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.delete.eq_1 : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  c.delete l = { clause := List.erase c.clause l, nodupkey := ⋯, nodup := ⋯ }
-- Mathlib.Algebra.Group.Pi.Basic
Pi.negZeroClass.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → NegZeroClass (f i)],
  Pi.negZeroClass = { toZero := Pi.instZero, toNeg := Pi.instNeg, neg_zero := ⋯ }
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.map_single : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S) (r : R) (m : M),
  MonoidAlgebra.map f (MonoidAlgebra.single m r) = MonoidAlgebra.single m (f r)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.braiding_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C] (M N : CategoryTheory.Mon C), (β_ M N).hom.hom = (β_ M.X N.X).hom
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.instInfSet.eq_1 : ∀ {M : Type u_1} [inst : Add M],
  AddCon.instInfSet = { sInf := fun S => { r := fun x y => ∀ c ∈ S, c x y, iseqv := ⋯, add' := ⋯ } }