mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypePreimage_apply : ∀ {α : Sort u_1} {β : Sort u_4} (p : α → Prop) [inst : DecidablePred p] (x₀ : { a // p a } → β)
  (x : { x // x ∘ Subtype.val = x₀ }) (a : { a // ¬p a }), (Equiv.subtypePreimage p x₀) x a = ↑x ↑a
-- Std.Data.Iterators.Lemmas.Combinators.Drop
Std.Iter.drop_eq : ∀ {α β : Type u_1} [Std.Iterator α Id β] {n : ℕ} {it : Std.Iter β},
  Std.Iter.drop n it = (Std.IterM.drop n it.toIterM).toIter
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ResidueField.algHom_ext : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {I : Ideal A} [inst_5 : I.IsPrime] {f g : I.ResidueField →ₐ[R] B},
  f.comp (IsScalarTower.toAlgHom R A I.ResidueField) = g.comp (IsScalarTower.toAlgHom R A I.ResidueField) → f = g
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_le_mul_iff_left₀ : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [MulPosMono α] [MulPosReflectLE α],
  0 < a → (b * a ≤ c * a ↔ b ≤ c)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.toUnder_obj_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor D T)
  (X_1 : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))),
  ((CategoryTheory.StructuredArrow.toUnder X F).obj X_1).right = F.obj X_1.right
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.forIn_eq_forIn_toList : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'],
  m.WF → ∀ {f : α × β → δ → m' (ForInStep δ)} {init : δ}, forIn m init f = forIn m.toList init f
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isNone_getElem?_toArray_rco_eq : ∀ {m n i : ℕ}, ((m...n).toArray[i]?.isNone = true) = (n ≤ i + m)
-- Mathlib.Analysis.Convex.Gauge
mem_closure_of_gauge_le_one : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} [inst_2 : TopologicalSpace E]
  [ContinuousSMul ℝ E], Convex ℝ s → 0 ∈ s → Absorbent ℝ s → gauge s x ≤ 1 → x ∈ closure s
-- Init.Core
DoResultSBC.pureReturn.sizeOf_spec : ∀ {α σ : Type u} [inst : SizeOf α] [inst_1 : SizeOf σ] (a : α) (a_1 : σ),
  sizeOf (DoResultSBC.pureReturn a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coreflection_apply_coroot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι),
  (P.coreflection i) (P.coroot j) = P.coroot j - P.pairing i j • P.coroot i
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- `H` and `h` are kept as separate hypothesis since H is used in constructing the quotient map.  -/
Ideal.quotientMap_injective' : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] {J : Ideal R} {I : Ideal S} [inst_2 : I.IsTwoSided]
  [inst_3 : J.IsTwoSided] {f : R →+* S} {H : J ≤ Ideal.comap f I},
  Ideal.comap f I ≤ J → Function.Injective ⇑(Ideal.quotientMap I f H)
-- Std.Http.Server.Connection
/-- Computes the active `PollSources` for the current connection state.
Determines which IO sources need attention and whether to include the socket.
 -/
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.buildPollSources : {α β : Type} →
  [Std.Http.Transport α] →
    α →
      Std.CancellationContext →
        Std.Http.Server.Connection.ConnectionState✝ β → Std.Async.Async (Std.Http.Server.Connection.PollSources✝ α β)
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.coe_id : ∀ {X : GrpCat}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
/-- A finite product of nonnegative monotone functions is monotone. See also
`Monotone.finsetProd'` for the case of an ordered commutative multiplicative monoid.  -/
Monotone.finsetProd : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : Preorder R] [ZeroLEOneClass R] [PosMulMono R]
  {s : Finset ι} {γ : Type u_4} [inst_4 : Preorder γ] {f : ι → γ → R},
  (∀ i ∈ s, Monotone (f i)) → (∀ i ∈ s, ∀ (x : γ), 0 ≤ f i x) → Monotone fun x => ∏ i ∈ s, f i x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.connected_iff : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph}, H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.instHasDetPlusMinusOneHSMulConjActGeneralLinearGroup : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R]
  (Γ : Subgroup (GL n R)) [Γ.HasDetPlusMinusOne] (g : ConjAct (GL n R)), (g • Γ).HasDetPlusMinusOne
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- While the tensor product will automatically inherit a ℤ-module structure from
`AddCommGroup.toIntModule`, that structure won't be compatible with lemmas like `tmul_smul` unless
we use a `ℤ-Module` instance provided by `TensorProduct.left_module`.

When `R` is a `Ring` we get the required `TensorProduct.compatible_smul` instance through
`IsScalarTower`, but when it is only a `Semiring` we need to build it from scratch.
The instance diamond in `compatible_smul` doesn't matter because it's in `Prop`.
 -/
TensorProduct.CompatibleSMul.int : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {P : Type u_4} [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup P] [inst_3 : Module R M] [inst_4 : Module R P], TensorProduct.CompatibleSMul R ℤ M P
-- Lean.Widget.UserWidget
Lean.Widget.addPanelWidgetScoped : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadResolveName m] → UInt64 → Lean.Name → m Unit
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H2π_comp_map_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {Z : ModuleCat k} (h : groupHomology B 2 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.H2π A)
      (CategoryTheory.CategoryStruct.comp (groupHomology.map f φ 2) h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₂ f φ)
      (CategoryTheory.CategoryStruct.comp (groupHomology.H2π B) h)
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_union_of_symm : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α} [Std.Symm r],
  (s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.IsInvertedBy.rightOp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {W : CategoryTheory.MorphismProperty C} {L : CategoryTheory.Functor Cᵒᵖ D},
  W.op.IsInvertedBy L → W.IsInvertedBy L.rightOp
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] (f : BoundedLatticeHom β γ)
  (g : BoundedLatticeHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_4} [inst_3 : NormedRing R] [inst_4 : Module R E] [IsBoundedSMul R E]
  [SMulCommClass 𝕜 R E] {x : 𝕜} {f : 𝕜 → E}, MeromorphicAt f x → ∀ (c : R), MeromorphicAt (c • f) x
-- Mathlib.Data.Matrix.DMatrix
DMatrix.map_map : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} {M : DMatrix m n α} {β : m → n → Type w} {γ : m → n → Type z}
  {f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j} {g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j},
  (M.map f).map g = M.map fun x x_1 x_2 => g (f x_2)
-- Init.Data.Option.Lemmas
Option.exists : ∀ {α : Type u_1} {p : Option α → Prop}, (∃ x, p x) ↔ p none ∨ ∃ x, p (some x)
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.IsLeftQuasiInverse.congr : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃},
  u.IsLeftQuasiInverse v → u' ≈ u → v' ≈ v → u'.IsLeftQuasiInverse v'
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.sumCongr_inl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_9} [inst_6 : TopologicalSpace M]
  [inst_7 : ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_13} [inst_8 : TopologicalSpace M']
  [inst_9 : ChartedSpace H M'] {N : Type u_15} [inst_10 : TopologicalSpace N] [inst_11 : ChartedSpace H N]
  {J : ModelWithCorners 𝕜 E' H} {N' : Type u_17} [inst_12 : TopologicalSpace N'] [inst_13 : ChartedSpace H N']
  (φ : Diffeomorph I J M N n) (ψ : Diffeomorph I J M' N' n), ⇑(φ.sumCongr ψ) ∘ Sum.inl = Sum.inl ∘ ⇑φ
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.GeometricallyConnected.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.geometrically (fun x => ConnectedSpace ↥x) f → AlgebraicGeometry.GeometricallyConnected f
-- Init.Data.List.MinMaxIdx
List.minIdxOn?_eq_some_zero_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β}, List.minIdxOn? f xs = some 0 ↔ ∃ (h : xs ≠ []), ∀ x ∈ xs, f (xs.head h) ≤ f x
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateWithAnchor.e : Lean.Meta.Grind.SplitCandidateWithAnchor → Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.Bimon C)
-- Mathlib.Data.Set.Card
Set.encard_sdiff_singleton_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → (s \ {a}).encard = s.encard - 1
-- Mathlib.Data.Set.Function
Set.invOn_id : ∀ {α : Type u_1} (s : Set α), Set.InvOn id id s s
-- Mathlib.Algebra.Lie.Basic
LieEquiv.trans_apply : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieRing L₂] [inst_3 : LieRing L₃] [inst_4 : LieAlgebra R L₁] [inst_5 : LieAlgebra R L₂]
  [inst_6 : LieAlgebra R L₃] (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) (x : L₁), (e₁.trans e₂) x = e₂ (e₁ x)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- A smooth partition of unity `f i` is subordinate to a family of sets `U i` indexed by the same
type if for each `i` the closure of the support of `f i` is a subset of `U i`.  -/
SmoothPartitionOfUnity.IsSubordinate : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] → {s : Set M} → SmoothPartitionOfUnity ι I M s → (ι → Set M) → Prop
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instRatCast : {R : Type u_1} → [inst : Field R] → [inst_1 : StarRing R] → RatCast ↥(selfAdjoint R)
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_apply_eq_top' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α},
  MeasurableSet s → (MeasureTheory.Measure.count s = ⊤ ↔ s.Infinite)
-- Lean.Parser.Term
Lean.Parser.Term.letNegOpt.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivAt_comp_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} (a : E), HasFDerivAt (fun x => f (x - a)) f' x ↔ HasFDerivAt f f' (x - a)
-- Std.Http.Data.Extensions
_private.Std.Http.Data.Extensions.0.Std.Http.Extensions.mk.injEq : ∀ (data data_1 : Std.TreeMap Lean.Name Dynamic Std.Http.Extensions.compareName),
  ({ data := data } = { data := data_1 }) = (data = data_1)
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.InfoCacheKey.mk.sizeOf_spec : ∀ (configKey : UInt64) (expr : Lean.Expr) (nargs? : Option ℕ),
  sizeOf { configKey := configKey, expr := expr, nargs? := nargs? } = 1 + sizeOf configKey + sizeOf expr + sizeOf nargs?
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- Pullback of a summation filter along an embedding.  -/
SummationFilter.comap : {β : Type u_2} → {γ : Type u_3} → SummationFilter β → (γ ↪ β) → SummationFilter γ
-- Mathlib.Data.Finset.Empty
Finset.instOrderBot : {α : Type u_1} → OrderBot (Finset α)
-- Mathlib.Algebra.Notation.Support
Function.support_const : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {c : M}, c ≠ 0 → (Function.support fun x => c) = Set.univ
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.commIsometry_comp_rTensor_comp_commIsometry_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E →L[𝕜] F),
  ↑↑(TensorProduct.commIsometry 𝕜 G F) ∘SL ContinuousLinearMap.lTensor G f ∘SL ↑↑(TensorProduct.commIsometry 𝕜 E G) =
    ContinuousLinearMap.rTensor G f
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.Homotopy.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} [inst_1 : SizeOf C] (H : (i : E.I₀) → F.I₁ (f.s₀ i) (g.s₀ i))
  (a : (i : E.I₀) → E.X i ⟶ F.Y (H i))
  (wl : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (a i) (F.p₁ (H i)) = f.h₀ i)
  (wr : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (a i) (F.p₂ (H i)) = g.h₀ i),
  sizeOf { H := H, a := a, wl := wl, wr := wr } = 1
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.fold_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad n Pred EPred] [inst_8 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_10 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Std.Iterators.PostconditionT n (Option γ)} {g : δ → γ → δ}
  {init : δ} {it : Std.IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.IterM.foldM
        (fun d b => do
          let __x ← (f b).run
          match __x with
            | some c => pure (g d c)
            | x => pure d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.IterM.filterMapWithPostcondition f it) ⦃ Q; eQ ⦄
-- Mathlib.RingTheory.FreeCommRing
/-- **Alias** of `freeRingPEmptyEquivInt`.

---

The free ring on the empty type is isomorphic to `ℤ`.  -/
freeRingPemptyEquivInt : FreeRing PEmpty.{u + 1} ≃+* ℤ
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.mem_iUnion : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) {x : ι → ℝ},
  x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J
-- Mathlib.MeasureTheory.Measure.Sub
MeasureTheory.Measure.sub_eq_zero_of_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ ≤ ν → μ - ν = 0
-- Mathlib.Algebra.Polynomial.Bivariate
/-- If the evaluation (`evalEval`) of a bivariate polynomial `p : R[X][Y]` at a point (x,y)
is zero, then `Polynomial.evalEval x y` factors through `AdjoinRoot.evalEval`, a ring homomorphism
from `AdjoinRoot p` to `R`.  -/
AdjoinRoot.evalEval : {R : Type u_1} →
  [inst : CommRing R] → {x y : R} → {p : Polynomial (Polynomial R)} → Polynomial.evalEval x y p = 0 → AdjoinRoot p →+* R
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.instSliceableRioSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.instSliceableRioSlice._auto_1) →
      Std.Rio.Sliceable (Std.DTreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.RioSlice α β)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The natural bijection between `α → β × γ` and `(α → β) × (α → γ)`, upgraded to a uniform
isomorphism between `α →ᵤ[𝔖] β × γ` and `(α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)`.  -/
UniformOnFun.uniformEquivProdArrow : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : UniformSpace β] →
        {𝔖 : Set (Set α)} →
          [inst_1 : UniformSpace γ] → UniformOnFun α (β × γ) 𝔖 ≃ᵤ UniformOnFun α β 𝔖 × UniformOnFun α γ 𝔖
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.rightpad.eq_1 : ∀ {α : Type u} (n : ℕ) (a : α) (xs : Array α), Array.rightpad n a xs = xs ++ Array.replicate (n - xs.size) a
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.sub : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {l : Filter α} {f g : α → E},
  MeasureTheory.IntegrableAtFilter f l μ →
    MeasureTheory.IntegrableAtFilter g l μ → MeasureTheory.IntegrableAtFilter (f - g) l μ
-- Mathlib.RepresentationTheory.FDRep
FDRep.of_ρ : ∀ {R : Type u} {G : Type v} [inst : CommRing R] [inst_1 : Monoid G] {V : Type u} [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : Module.Finite R V] (ρ : Representation R G V),
  (FDRep.of ρ).ρ =
    CategoryTheory.InducedCategory.endEquiv.symm.toMonoidHom.comp
      ((ModuleCat.of R V).endRingEquiv.symm.toMonoidHom.comp ρ)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.nthRoots_two_eq_zero_iff : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {r : R}, Polynomial.nthRoots 2 r = 0 ↔ ¬IsSquare r
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.ofEq_coe : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y), (MulActionHom.ofEq h f).toFun = f.toFun
-- Lean.Meta.Sym.Canon
/-- Similar to `canonInsideType`, but skips the `isProp` check.
Use only when `e` is known not to be a proposition.
 -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonInsideType' : Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_ne_zero : ∀ {x y : ℝ}, 0 ≤ x → y ≠ 0 → (x ^ y ≠ 0 ↔ x ≠ 0)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_eq_getValue? : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [instBEq : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.Ordered → Std.DTreeMap.Internal.Impl.Const.get? t k = Std.Internal.List.getValue? k t.toListModel
-- Mathlib.RingTheory.Valuation.Basic
Valuation.exists_div_eq_of_unit : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ), ∃ r s, 0 < v r ∧ 0 < v s ∧ v.restrict r / v.restrict s = ↑γ
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- If `v'` is a left quasi-inverse of `v` and `w` is a right quasi-inverse of `v ∘ₗ u`,
then `w ∘ₗ v` is a right quasi-inverse of `u`.  -/
LinearMap.IsRightQuasiInverse.of_comp_right : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V]
  [inst_2 : Module K V] [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : AddCommGroup V₃]
  [inst_6 : Module K V₃] {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} {v' : V₃ →ₗ[K] V₂} {w : V₃ →ₗ[K] V},
  v'.IsLeftQuasiInverse v → w.IsRightQuasiInverse (v ∘ₗ u) → (w ∘ₗ v).IsRightQuasiInverse u
-- Mathlib.Data.List.ProdSigma
List.product_cons : ∀ {α : Type u_1} {β : Type u_2} (a : α) (l₁ : List α) (l₂ : List β),
  (a :: l₁) ×ˢ l₂ = List.map (fun b => (a, b)) l₂ ++ l₁ ×ˢ l₂
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.id_r : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a : CategoryTheory.Bicategory.Adj B),
  (CategoryTheory.CategoryStruct.id a).r = CategoryTheory.CategoryStruct.id a.obj
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.sdiv_union : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s t₁ t₂ : Set β}, s /ₛ (t₁ ∪ t₂) = s /ₛ t₁ ∪ (s /ₛ t₂)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.subset_zero_iff_eq : ∀ {α : Type u_2} [inst : Zero α] {s : Finset α}, s ⊆ 0 ↔ s = ∅ ∨ s = 0
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataT_snd_assoc : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens) {Z : AlgebraicGeometry.Scheme}
  (h : ↑(↑V ⊓ ↑U) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.glueDataT U V)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (I.glueDataObjι V) (X.homOfLE ⋯)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯))
      (CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯) h)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k k' : α} {v : β},
      List.find? (fun a => a.1 == k) (Std.DHashMap.Raw.Const.toList ↑m) = some (k', v) ↔
        m.getKey? k = some k' ∧ Std.DHashMap.Internal.Raw₀.Const.get? m k = some v
-- Std.Sync.Broadcast
/-- Whether the channel has been closed, preventing new messages.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.State.closed : {α : Type} → Std.Bounded.State✝ α → Bool
-- Mathlib.Topology.MetricSpace.IsometricSMul
dist_div_right : ∀ {M : Type u} [inst : DivInvMonoid M] [inst_1 : PseudoMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M),
  dist (a / c) (b / c) = dist a b
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The tautological 1-pre-hypercover induced by `S : J.Cover X`. Its index type `I₀`
is given by `S.Arrow` (i.e. all the morphisms in the sieve `S`), while `I₁` is given
by all possible pullback cones.  -/
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} → {X : C} → J.Cover X → CategoryTheory.PreOneHypercover X
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
ContDiffOn.deriv_of_isOpen : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m n : WithTop ℕ∞} {f : 𝕜 → F} {s : Set 𝕜},
  ContDiffOn 𝕜 n f s → IsOpen s → m + 1 ≤ n → ContDiffOn 𝕜 m (deriv f) s
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.smulCommClass : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] {S₂ : Type u_9} {T₂ : Type u_10}
  [inst_8 : DistribSMul S₂ M₂] [inst_9 : SMulCommClass R₂ S₂ M₂] [inst_10 : ContinuousConstSMul S₂ M₂]
  [inst_11 : DistribSMul T₂ M₂] [inst_12 : SMulCommClass R₂ T₂ M₂] [inst_13 : ContinuousConstSMul T₂ M₂]
  [SMulCommClass S₂ T₂ M₂], SMulCommClass S₂ T₂ (M₁ →SL[σ₁₂] M₂)