mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableWithinAt.congr_mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f f₁ : E → F} {s t : Set E}
  {x v : E},
  LineDifferentiableWithinAt 𝕜 f s x v → Set.EqOn f₁ f t → f₁ x = f x → t ⊆ s → LineDifferentiableWithinAt 𝕜 f₁ t x v
-- Mathlib.Analysis.Complex.Trigonometric
Real.sinh_sub : ∀ (x y : ℝ), Real.sinh (x - y) = Real.sinh x * Real.cosh y - Real.cosh x * Real.sinh y
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.mk.sizeOf_spec : ∀ (carrier : Type u) [str : AddCommGroup carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.IsoLift.mk.sizeOf_spec : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂Iso) (eq : Lean.Expr), sizeOf { e := e, eq := eq } = 1 + sizeOf e + sizeOf eq
-- Init.Data.SInt.Lemmas
ISize.sub_right_inj : ∀ {a b : ISize} (c : ISize), c - a = c - b ↔ a = b
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.NormNum.Finset.sum_empty : ∀ {β : Type u_1} {α : Type u_2} [inst : CommSemiring β] (f : α → β), Mathlib.Meta.NormNum.IsNat (∅.sum f) 0
-- Mathlib.Topology.Order.Lattice
/-- Let `L` be a topological space and let `L×L` be equipped with the product topology and let
`⊓:L×L → L` be a supremum. Then `L` is said to have *(jointly) continuous supremum* if the map
`⊓:L×L → L` is continuous.
 -/
ContinuousSup : (L : Type u_1) → [TopologicalSpace L] → [Max L] → Prop
-- Init.Data.Order.MinMaxOn
maxOn_id : ∀ {α : Type u_1} [inst : Max α] [inst_1 : LE α] [inst_2 : DecidableLE α] [Std.LawfulOrderLeftLeaningMax α] {x y : α},
  maxOn id x y = x ⊔ y
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.ofNat : ℕ → Std.Time.Weekday
-- Mathlib.Analysis.Convex.Segment
Icc_subset_segment : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : 𝕜},
  Set.Icc x y ⊆ segment 𝕜 x y
-- Mathlib.CategoryTheory.Action.Limits
Action.instAddHom : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → [CategoryTheory.Preadditive V] → {X Y : Action V G} → Add (X ⟶ Y)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.forM_eq_forM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → m PUnit.{w + 1}}, forM t f = t.toList.forM f
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_dvd_index_of_le : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H ≤ K → H.relIndex K ∣ H.index
-- Init.Data.Array.Lemmas
Array.getElem?_eq_some_getElem! : ∀ {α : Type u_1} [inst : Inhabited α] (xs : Array α), ∀ i < xs.size, xs[i]? = some xs[i]!
-- Mathlib.Order.Filter.Pointwise
/-- The filter `f * g` is generated by `{s * t | s ∈ f, t ∈ g}` in scope `Pointwise`.  -/
Filter.instMul : {α : Type u_2} → [Mul α] → Mul (Filter α)
-- Lean.PrettyPrinter.Delaborator.Metavariable
/-- Approximate check that the application `?m a₁ … aₙ` of the delayed assignment metavariable `?m`
can be pretty printed using the pending metavariable.

Heuristic: we assume the ldecl arguments are correct, and for the cdecls we check that they are
distinct fvars
 -/
Lean.PrettyPrinter.Delaborator.checkDelayedMVarAssignment : Lean.Expr → Lean.DelayedMetavarAssignment → Lean.MetaM Bool
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.truncTotal_subst_of_le : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {f : MvPowerSeries σ R} [inst_3 : Finite τ] {x : σ → ℕ} {k : ℕ}
  [inst_4 : Finite σ],
  (∀ (i : σ), MvPowerSeries.constantCoeff (a i) = 0) →
    (∀ (i : σ), k ≤ x i) →
      (MvPowerSeries.truncTotal k) (MvPowerSeries.subst a f) =
        (MvPowerSeries.truncTotal k)
          (MvPowerSeries.subst (fun i => ↑((MvPowerSeries.truncTotal (x i)) (a i))) ↑((MvPowerSeries.truncTotal k) f))
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.tendsto_logb_nhdsGT_zero_of_base_lt_one : ∀ {b : ℝ}, 0 < b → b < 1 → Filter.Tendsto (Real.logb b) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.toLinearMap_apply_apply_mem_range_algebraMap : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [P.IsValuedIn S] [inst_8 : Module S M] [inst_9 : Module S N]
  [IsScalarTower S R M] [IsScalarTower S R N],
  ∀ x ∈ P.rootSpan S, ∀ y ∈ P.corootSpan S, (P.toLinearMap x) y ∈ (algebraMap S R).range
-- Mathlib.MeasureTheory.Group.Prod
/-- A *right*-invariant measure is quasi-preserved by *left*-multiplication.
This should not be confused with `(measurePreserving_mul_left μ g).quasiMeasurePreserving`.  -/
MeasureTheory.quasiMeasurePreserving_mul_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulRightInvariant] (g : G),
  MeasureTheory.Measure.QuasiMeasurePreserving (fun h => g * h) μ μ
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instSemilatticeInfOpenNormalAddSubgroup.eq_1 : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenNormalAddSubgroup.instSemilatticeInfOpenNormalAddSubgroup = Function.Injective.semilatticeInf SetLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mem_strictlyPositive : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup M]
  [inst_3 : PartialOrder M] [inst_4 : IsOrderedAddMonoid M] [inst_5 : Module R M] [inst_6 : PosSMulStrictMono R M]
  {x : M}, x ∈ ConvexCone.strictlyPositive R M ↔ 0 < x
-- Batteries.Data.MLList.Basic
/-- Take the initial segment of the lazy list,
up to and including the first place where `f` gives `true`.  -/
MLList.takeUpToFirstM : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → (α → m (ULift.{u_1, 0} Bool)) → MLList m α
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.d₀₁.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G),
  groupCohomology.d₀₁ A = ModuleCat.ofHom { toFun := fun m g => (A.ρ g) m - m, map_add' := ⋯, map_smul' := ⋯ }
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {km fallback : α}, t.maxKey? = some km → t.getKeyD km fallback = km
-- Mathlib.Order.InitialSeg
PrincipalSeg.eq : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f g : PrincipalSeg r s)
  (a : α), f.toRelEmbedding a = g.toRelEmbedding a
-- Mathlib.Topology.Instances.Matrix
instT2SpaceMatrix : ∀ {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [T2Space R], T2Space (Matrix m n R)
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
/-- A class describing the property of preserving finite effective epimorphic families.
 -/
CategoryTheory.Functor.PreservesFiniteEffectiveEpiFamilies : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} → [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Data.NNRat.Defs
NNRat.canLift : CanLift ℚ ℚ≥0 NNRat.cast fun q => 0 ≤ q
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  k ∉ m → (f (Std.ExtDHashMap.Const.get? m k)).isNone = true → (Std.ExtDHashMap.Const.alter m k f).size = m.size
-- Mathlib.Control.Basic
Sum.instMonad_mathlib : {e : Type v} → Monad (Sum e)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The natural algebra homomorphism `A / I → A / (I ⊔ J)`.  -/
DoubleQuot.quotLeftToQuotSupₐ : (R : Type u) →
  {A : Type u_1} →
    [inst : CommSemiring R] → [inst_1 : CommRing A] → [inst_2 : Algebra R A] → (I J : Ideal A) → A ⧸ I →ₐ[R] A ⧸ I ⊔ J
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.weightedOrder_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ), MvPowerSeries.weightedOrder w 0 = ⊤
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.incenter_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S), ↑(s.restrict S hS).incenter = s.incenter
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.rightInverseUnitor_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.prod.rightInverseUnitor C).map f =
    CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id { as := PUnit.unit })
-- Init.Data.Array.OfFn
Array.ofFnM_add : ∀ {k : ℕ} {α : Type u_1} {n : ℕ} {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m] {f : Fin (n + k) → m α},
  Array.ofFnM f = do
    let as ← Array.ofFnM fun i => f (Fin.castLE ⋯ i)
    let bs ← Array.ofFnM fun i => f (Fin.natAdd n i)
    pure (as ++ bs)
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.invertiblePso.congr_simp : ∀ (p : Type u_2) (q : Type u_3) (R : Type u₂) [inst : DecidableEq p] [inst_1 : DecidableEq q] [inst_2 : CommRing R]
  [inst_3 : Fintype p] [inst_4 : Fintype q] {i : R} (hi : i * i = -1),
  LieAlgebra.Orthogonal.invertiblePso p q R hi = LieAlgebra.Orthogonal.invertiblePso p q R hi
-- Std.Http.Data.Status
/-- 506 Variant Also Negotiates
 -/
Std.Http.Status.variantAlsoNegotiates : Std.Http.Status
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospan_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.cospan f g).obj CategoryTheory.Limits.WalkingCospan.one = Z
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CongrKey.mk.injEq : ∀ {enodes : Lean.Meta.Grind.ENodeMap} (e e_1 : Lean.Expr), ({ e := e } = { e := e_1 }) = (e = e_1)
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertZoneName : Std.Time.ZoneName → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Topology.Constructions
Continuous.sigma_map : ∀ {ι : Type u_5} {κ : Type u_6} {σ : ι → Type u_7} {τ : κ → Type u_8} [inst : (i : ι) → TopologicalSpace (σ i)]
  [inst_1 : (k : κ) → TopologicalSpace (τ k)] {f₁ : ι → κ} {f₂ : (i : ι) → σ i → τ (f₁ i)},
  (∀ (i : ι), Continuous (f₂ i)) → Continuous (Sigma.map f₁ f₂)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.counit_naturality : ∀ {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 D C} (adj : G ⊣ F) {X Y : C} (f : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp (G.map (F.map f)) (adj.counit.app X) =
    CategoryTheory.CategoryStruct.comp (adj.counit.app Y) f
-- Mathlib.Algebra.Order.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.monoidWithZeroHom_strictMono : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : LinearOrderedCommGroupWithZero B] {f : A →*₀ B},
  StrictMono ⇑(MonoidWithZeroHom.ValueGroup₀.orderMonoidWithZeroHom f)
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- Right-exactness of tensor product (`rTensor`)  -/
rTensor_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (Q : Type u_5)
  [inst_3 : AddCommGroup Q] [inst_4 : Module R Q] (N : Submodule R M),
  (LinearMap.rTensor Q N.mkQ).ker = (LinearMap.rTensor Q N.subtype).range
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.instBEqExtTheorem.beq : Lean.Meta.Ext.ExtTheorem → Lean.Meta.Ext.ExtTheorem → Bool
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Associativity of convex combination (monadic join law).

Use `sConvexComb_sConvexComb` instead.  -/
Convexity.ConvexSpace.assoc : ∀ {R : Type u} {M : Type v} {inst₁ : PartialOrder R} {inst₂ : Semiring R} {inst₃ : IsStrictOrderedRing R}
  [self : Convexity.ConvexSpace R M] (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)),
  Convexity.sConvexComb (Convexity.StdSimplex.map Convexity.sConvexComb f) = Convexity.sConvexComb f.join
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.mono : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (self : I.Filtration M) (i : ℕ), self.N (i + 1) ≤ self.N i
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE : ∀ (p : ℤ), (ComplexShape.embeddingUpIntLE p).IsTruncLE
-- Init.Grind.AC
Lean.Grind.AC.Expr.toSeq'_k.eq_1 : ∀ (e : Lean.Grind.AC.Expr),
  e.toSeq'_k =
    Lean.Grind.AC.Expr.rec (motive := fun x => Lean.Grind.AC.Seq → Lean.Grind.AC.Seq) Lean.Grind.AC.Seq.cons
      (fun x x_1 iha ihb s => iha (ihb s)) e
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.iso₂Mk_hom_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b}
  (el : α.l ≅ β.l) (er : β.r ≅ α.r)
  (h :
    autoParam ((CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) el.hom = er.hom)
      CategoryTheory.Bicategory.Adj.iso₂Mk._auto_1),
  (CategoryTheory.Bicategory.Adj.iso₂Mk el er h).hom.τl = el.hom
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.isOpenMap_coe : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {N : Subgroup G},
  IsOpenMap QuotientGroup.mk
-- Mathlib.SetTheory.Cardinal.Defs
/-- Similar to `mk_pi_congr` with indexing types in different universes. This is not a strict
generalization.  -/
Cardinal.mk_pi_congr' : ∀ {ι : Type u} {ι' : Type v} {f : ι → Type (max w u v)} {g : ι' → Type (max w u v)} (e : ι ≃ ι'),
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) → Cardinal.mk ((i : ι) → f i) = Cardinal.mk ((i : ι') → g i)
-- Mathlib.LinearAlgebra.RootSystem.Chain
/-- **Alias** of `RootPairing.setOfPred_root_add_zsmul_mem_eq_Icc`. -/
RootPairing.setOf_root_add_zsmul_mem_eq_Icc : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    {k | P.root j + k • P.root i ∈ Set.range ⇑P.root} =
      Set.Icc (-↑(RootPairing.chainBotCoeff i j)) ↑(RootPairing.chainTopCoeff i j)
-- Mathlib.Order.WithBot
WithBot.strictAnti_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : WithBot α → β},
  StrictAnti f ↔ (StrictAnti fun a => f ↑a) ∧ ∀ (x : α), f ↑x < f ⊥
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instRatCast : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : DivisionRing R] → (v : Valuation R Γ₀) → RatCast (WithVal v)
-- Mathlib.Data.Set.Disjoint
Disjoint.inter_left' : ∀ {α : Type u_1} {s t : Set α} (u : Set α), Disjoint s t → Disjoint (u ∩ s) t
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SharedExprs.falseExpr : Lean.Meta.Sym.SharedExprs → Lean.Expr
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.mk.injEq : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A}
  (deg : ι) (num den : ↥(𝒜 deg)) (den_mem : ↑den ∈ x) (deg_1 : ι) (num_1 den_1 : ↥(𝒜 deg_1)) (den_mem_1 : ↑den_1 ∈ x),
  ({ deg := deg, num := num, den := den, den_mem := den_mem } =
      { deg := deg_1, num := num_1, den := den_1, den_mem := den_mem_1 }) =
    (deg = deg_1 ∧ num ≍ num_1 ∧ den ≍ den_1)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformly.tendstoUniformlyOn_finsetRange : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] {g : β → α} [inst_1 : UniformSpace α] {f : ℕ → β → α},
  HasProdUniformly f g → TendstoUniformly (fun x1 x2 => ∏ i ∈ Finset.range x1, f i x2) g Filter.atTop
-- Mathlib.Data.PFun
PFun.coe_val : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α), ↑f a = Part.some (f a)
-- Mathlib.Order.BoundedOrder.Basic
Prod.instTop : (α : Type u) → (β : Type v) → [Top α] → [Top β] → Top (α × β)
-- Init.Data.Int.Pow
Int.instNeZeroHPowNat : ∀ {n : ℤ} {m : ℕ} [NeZero n], NeZero (n ^ m)
-- Mathlib.Algebra.Group.Equiv.Opposite
MonoidHom.toOpposite.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N)
  (hf : ∀ (x y : M), Commute (f x) (f y)),
  f.toOpposite hf = { toFun := MulOpposite.op ∘ ⇑f, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
Preorder.frestrictLe₂.eq_def : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} [inst_1 : LocallyFiniteOrderBot α] {a b : α} (hab : a ≤ b),
  Preorder.frestrictLe₂ hab = Finset.restrict₂ ⋯
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.summable_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddCommMonoid β]
  [inst_3 : ContinuousAdd β] {γ : Type u_3} {f : γ → C(α, β)} {L : SummationFilter γ},
  Summable f L → ∀ (x : α), Summable (fun i => (f i) x) L
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Bundle.Trivialization.localFrame.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {M : Type u_4} [inst_1 : TopologicalSpace M] {F : Type u_5}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {V : M → Type u_6}
  [inst_4 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_5 : (x : M) → AddCommGroup (V x)]
  [inst_6 : (x : M) → Module 𝕜 (V x)] [inst_7 : (x : M) → TopologicalSpace (V x)] [inst_8 : FiberBundle F V]
  [inst_9 : VectorBundle 𝕜 F V] {ι : Type u_7} (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [inst_10 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F) (i : ι) (x : M),
  e.localFrame b i x = if hx : x ∈ e.baseSet then (e.basisAt b hx) i else 0
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis'.contract_dep_iff : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  M.IsBasis' I X → ∀ {D : Set α}, (M.contract X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.vanishingIdeal_iUnion : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {γ : Sort u_3} (t : γ → Set (ProjectiveSpectrum 𝒜)),
  ProjectiveSpectrum.vanishingIdeal (⋃ i, t i) = ⨅ i, ProjectiveSpectrum.vanishingIdeal (t i)
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {as : AffineSubspace ℝ P} [inst_4 : Nonempty ↥as]
  [inst_5 : as.direction.HasOrthogonalProjection],
  dist s.center ↑((EuclideanGeometry.orthogonalProjection as) s.center) = s.radius ↔ s.IsTangent as
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.ofFactorizationData_p : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  (h :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C)
      (CategoryTheory.Limits.diag A)),
  (HomotopicalAlgebra.PathObject.ofFactorizationData h).p = h.p
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.isCover_coveringRadius : ∀ {X : Type u_3} [inst : MetricSpace X] (self : Delone.DeloneSet X),
  Metric.IsCover self.coveringRadius Set.univ self.carrier
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ X ω ^ p` is
integrable for all nonnegative `p : ℝ`.  -/
ProbabilityTheory.integrable_rpow_of_integrable_exp_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ≠ 0 →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp (-t * X ω)) μ →
        ∀ {p : ℝ}, 0 ≤ p → MeasureTheory.Integrable (fun ω => X ω ^ p) μ
-- Mathlib.CategoryTheory.Galois.Basic
/-- Every monomorphism in `C` induces an isomorphism on a direct summand (G3).  -/
CategoryTheory.PreGaloisCategory.monoInducesIsoOnDirectSummand : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} [self : CategoryTheory.PreGaloisCategory C] {X Y : C}
  (i : X ⟶ Y) [CategoryTheory.Mono i],
  ∃ Z u, Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk i u))
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
/-- **Alias** of the reverse direction of `Matrix.separatingLeft_iff_separatingRight`. -/
Matrix.SeparatingRight.separatingLeft : ∀ {n : Type u_1} {A : Type u_4} [inst : CommRing A] [IsDomain A] {M : Matrix n n A} [inst_2 : Finite n],
  M.SeparatingRight → M.SeparatingLeft
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_Ici : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] {l : ℝ},
  Filter.Tendsto (↑f) Filter.atTop (nhds l) →
    ∀ (x : R), f.measure (Set.Ici x) = ENNReal.ofReal (l - Function.leftLim (↑f) x)
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.mul_iff_right : ∀ {α : Type u_1} {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace α] [inst_2 : CommGroup G]
  [MeasurableMul₂ G] [MeasurableInv G] {f g : α → G}, Measurable f → (Measurable (f * g) ↔ Measurable g)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If `s` and `t` are two fundamental domains of the same action, then their measures
are equal.  -/
MeasureTheory.IsAddFundamentalDomain.measure_eq : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ → MeasureTheory.IsAddFundamentalDomain G t μ → μ s = μ t
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
AlgebraicGeometry.Scheme.Cover.toPresieveOverProp.congr_simp : ∀ {P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] {X : Q.Over ⊤ S}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X.left)
  [inst_1 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) ⦃Y : Q.Over ⊤ S⦄ (a a_1 : Y ⟶ X),
  a = a_1 → 𝒰.toPresieveOverProp h a = 𝒰.toPresieveOverProp h a_1
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_comp : ∀ {R : Type u} [inst : CommSemiring R] (p q : Polynomial R),
  Polynomial.derivative (p.comp q) = Polynomial.derivative q * (Polynomial.derivative p).comp q
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_zero_right_eq_nil : ∀ {m : ℕ}, (m<...0).toArray = #[]
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.map_star_eq_one : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : NonAssocSemiring α] [inst_2 : StarRing α]
  {M : Matrix n n α}, M.map star = 1 ↔ M = 1
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.inr_toFun : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (i : B), (ContinuousMonoidHom.inr A B) i = (1, i)
-- Mathlib.Order.Interval.Finset.Basic
/-- `Finset.cons` version of `Finset.Iio_insert`.  -/
Finset.Iic_eq_cons_Iio : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderBot α] (b : α),
  Finset.Iic b = Finset.cons b (Finset.Iio b) ⋯