mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.hasPullbackAlong : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X)
  [CategoryTheory.ChosenPullbacksAlong g], CategoryTheory.Limits.HasPullbacksAlong g
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- Open immersions are stable under base-change.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z),
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.NumberTheory.LSeries.MellinEqDirichlet
/-- Shortcut version for the commonly arising special case when `p i = π * q i` for some other
sequence `q`.  -/
hasSum_mellin_pi_mul : ∀ {ι : Type u_1} [Countable ι] {a : ι → ℂ} {q : ι → ℝ} {F : ℝ → ℂ} {s : ℂ},
  (∀ (i : ι), a i = 0 ∨ 0 < q i) →
    0 < s.re →
      (∀ t ∈ Set.Ioi 0, HasSum (fun i => a i * ↑(Real.exp (-Real.pi * q i * t))) (F t)) →
        (Summable fun i => ‖a i‖ / q i ^ s.re) →
          HasSum (fun i => ↑Real.pi ^ (-s) * Complex.Gamma s * a i / ↑(q i) ^ s) (mellin F s)
-- Mathlib.LinearAlgebra.Complex.Module
Complex.liftAux_neg_I : Complex.liftAux (-Complex.I) ⋯ = ↑Complex.conjAe
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
HomogeneousSubmodule.mk.congr_simp : ∀ {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A]
  [inst_1 : AddCommMonoid M] [inst_2 : Module A M] {𝒜 : ιA → σA} {ℳ : ιM → σM} [inst_3 : DecidableEq ιA]
  [inst_4 : AddMonoid ιA] [inst_5 : SetLike σA A] [inst_6 : AddSubmonoidClass σA A] [inst_7 : GradedRing 𝒜]
  [inst_8 : DecidableEq ιM] [inst_9 : SetLike σM M] [inst_10 : AddSubmonoidClass σM M]
  [inst_11 : DirectSum.Decomposition ℳ] [inst_12 : VAdd ιA ιM] [inst_13 : SetLike.GradedSMul 𝒜 ℳ]
  (toSubmodule toSubmodule_1 : Submodule A M) (e_toSubmodule : toSubmodule = toSubmodule_1)
  (is_homogeneous' : toSubmodule.IsHomogeneous ℳ),
  { toSubmodule := toSubmodule, is_homogeneous' := is_homogeneous' } =
    { toSubmodule := toSubmodule_1, is_homogeneous' := ⋯ }
-- Init.Data.Nat.Mod
Nat.two_pow_mod_two_eq_zero : ∀ {n : ℕ}, 2 ^ n % 2 = 0 ↔ 0 < n
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.prob_compl_eq_one_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsProbabilityMeasure μ], MeasurableSet s → (μ sᶜ = 1 ↔ μ s = 0)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryGED_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : (a : α) × β a}, t₁.Equiv t₂ → t₁.getEntryGED k fallback = t₂.getEntryGED k fallback
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- **Alias** of `add_apply`. -/
UniformConvergenceCLM.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `DifferentiableOn.fun_finsetProd`. -/
DifferentiableOn.fun_finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} {ι : Type u_2} {𝔸' : Type u_3}
  [inst_1 : NormedCommRing 𝔸'] [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableOn 𝕜 (f i) s) → DifferentiableOn 𝕜 (fun x => ∏ i ∈ u, f i x) s
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.avgRisk_zero_left : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (κ : ProbabilityTheory.Kernel 𝓧 𝓨) (π : MeasureTheory.Measure Θ),
  ProbabilityTheory.avgRisk ℓ 0 κ π = 0
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f * g) x = f x * g x` is a commutative semigroup if `β` is a
commutative semigroup.  -/
FunLike.commSemigroup : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] → [inst_1 : Mul F] → [inst_2 : CommSemigroup β] → [IsMulApply F α β] → CommSemigroup F
-- Mathlib.NumberTheory.RatFunc.Ostrowski
_private.Mathlib.NumberTheory.RatFunc.Ostrowski.0.RatFunc.one_le_valuation_factor : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} (hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty) {a b : Polynomial K},
  v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0 → ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne = a * b → ¬IsUnit b → 1 ≤ v ↑a
-- Mathlib.Algebra.BigOperators.Finprod
/-- Sum of `f x` as `x` ranges over the elements of the support of `f`, if it's finite. Zero
otherwise.  -/
finsum : {M : Type u_7} → {α : Sort u_8} → [AddCommMonoid M] → (α → M) → M
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.funLike : {M : Type u_4} → {N : Type u_5} → [inst : Add M] → [inst_1 : Add N] → FunLike (M →ₙ+ N) M N
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- A function is `C^k` on two open sets iff it is `C^k` on their union.  -/
contMDiffOn_union_iff_of_isOpen : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {n : WithTop ℕ∞} {s t : Set M},
  IsOpen s → IsOpen t → (ContMDiffOn I I' n f (s ∪ t) ↔ ContMDiffOn I I' n f s ∧ ContMDiffOn I I' n f t)
-- Mathlib.NumberTheory.Divisors
/-- Pairs of divisors of a natural number as a finset.

`n.divisorsAntidiagonal` is the finset of pairs `(a, b) : ℕ × ℕ` such that `a * b = n`.
By convention, we set `Nat.divisorsAntidiagonal 0 = ∅`.

O(n).  -/
Nat.divisorsAntidiagonal : ℕ → Finset (ℕ × ℕ)
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.iter : {ρ : Type} → (pat : ρ) → (s : String.Slice) → Std.Iter (String.Slice.Pattern.SearchStep s)
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.toMonComonObj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  M.toMonComonObj.X = (CategoryTheory.Bimon.toComon C).obj M
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_comp_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃)
  [CategoryTheory.Presheaf.IsLocallyInjective J f₂] [CategoryTheory.Presheaf.IsLocallySurjective J f₂],
  CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.CategoryStruct.comp f₁ f₂) ↔
    CategoryTheory.Presheaf.IsLocallySurjective J f₁
-- Mathlib.RingTheory.AdjoinRoot
/-- An unwrapped version of `AdjoinRoot.finite_of_monic` for better discoverability.  -/
Polynomial.Monic.finite_quotient : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R}, g.Monic → Module.Finite R (Polynomial R ⧸ Ideal.span {g})
-- Std.Data.HashMap.Lemmas
Std.HashMap.getThenInsertIfNew?_fst : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {k : α} {v : β},
  (m.getThenInsertIfNew? k v).1 = m[k]?
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C} {J : Type w}
  [inst_2 : CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {j₀ : J} (y : X ⟶ Y.obj j₀)
  {j j' : CategoryTheory.Under j₀} (f : j ⟶ j'),
  (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F y).map f =
    CategoryTheory.MonoOver.homMk
      ((CategoryTheory.Limits.kernel (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y)).map f) ⋯
-- Mathlib.Tactic.ITauto
/-- Constructor for `p ∧ q`.  -/
Mathlib.Tactic.ITauto.IProp.and : Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.instIsOrderedMonoid : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedMonoid α], IsOrderedMonoid αᵐᵒᵖ
-- Batteries.Data.Fin.Lemmas
Fin.isSome_find?_iff : ∀ {n : ℕ} {p : Fin n → Bool}, (Fin.find? p).isSome = true ↔ ∃ i, p i = true
-- Mathlib.Order.Interval.Set.Image
AntitoneOn.image_Iic_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  AntitoneOn f (Set.Iic b) → f '' Set.Iic b ⊆ Set.Ici (f b)
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.liftFromUnderComp_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {X : C}
  {K : CategoryTheory.Functor J (CategoryTheory.Under X)} {F : CategoryTheory.Functor C D}
  (x : CategoryTheory.WithInitial J),
  CategoryTheory.WithInitial.liftFromUnderComp.hom.app x =
    match x with
    | CategoryTheory.WithInitial.star =>
      CategoryTheory.CategoryStruct.id
        ((CategoryTheory.WithInitial.liftFromUnder.obj (K.comp (CategoryTheory.Under.post F))).obj
          CategoryTheory.WithInitial.star)
    | CategoryTheory.WithInitial.of a =>
      CategoryTheory.CategoryStruct.id
        ((CategoryTheory.WithInitial.liftFromUnder.obj (K.comp (CategoryTheory.Under.post F))).obj
          (CategoryTheory.WithInitial.of a))
-- Mathlib.Data.List.Lex
List.lex_cons_iff : ∀ {α : Type u} {r : α → α → Prop} [Std.Irrefl r] {a : α} {l₁ l₂ : List α},
  List.Lex r (a :: l₁) (a :: l₂) ↔ List.Lex r l₁ l₂
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singleton_add : ∀ {α : Type u_2} [inst : Add α] {t : Set α} {a : α}, {a} + t = (fun x => a + x) '' t
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Semantic token information for a given `Syntax`.  -/
Lean.Server.FileWorker.LeanSemanticToken : Type
-- Mathlib.Order.WithBot
WithTop.untopA_le_iff : ∀ {α : Type u_1} {a : α} [inst : LE α] {x : WithTop α} [inst_1 : Nonempty α], x ≠ ⊤ → (x.untopA ≤ a ↔ x ≤ ↑a)
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.cast_zero_smul_eq_zero_mul : ∀ {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {R' : Type u_3}
  [inst : HSMul R' A A] {r' : R'} {r : R}, r = 0 → (∀ (a : A), r • a = r' • a) → ∀ (a : A), r' • a = 0 * a
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instTop : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [Top β] → Top (l.Germ β)
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.instInhabitedFirstObjArrowsBotSieve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) →
      {X : C} → Inhabited (CategoryTheory.Equalizer.FirstObj P ⊥.arrows)
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
CategoryTheory.HomOrthogonal.matrixDecomposition.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C]
  (o : CategoryTheory.HomOrthogonal s) {α β : Type} [inst_3 : Finite α] [inst_4 : Finite β] {f : α → ι} {g : β → ι},
  o.matrixDecomposition = o.matrixDecomposition
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivRight_C : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (r : R),
  (MvPolynomial.optionEquivRight R S₁) (MvPolynomial.C r) = MvPolynomial.C (Polynomial.C r)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.containsThenInsert! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] {k : α} {v : β k} {t : Std.DTreeMap.Internal.Impl α β},
  t.WF → (Std.DTreeMap.Internal.Impl.containsThenInsert! k v t).2.WF
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.closure_union : ∀ {M : Type u_1} [inst : MulOneClass M] (s t : Set M),
  Submonoid.closure (s ∪ t) = Submonoid.closure s ⊔ Submonoid.closure t
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.emptyWithCapacity₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {c : ℕ},
  (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity c)).WF
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
range_cfcₙ_nnreal_eq_image_cfcₙ_real : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : Module ℝ A] [inst_3 : IsScalarTower ℝ A A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : TopologicalSpace A] [IsTopologicalRing A] [T2Space A]
  [inst_8 : PartialOrder A] [inst_9 : NonnegSpectrumClass ℝ A] [inst_10 : StarOrderedRing A]
  [inst_11 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A),
  autoParam (0 ≤ a) range_cfcₙ_nnreal_eq_image_cfcₙ_real._auto_1 →
    (Set.range fun x => cfcₙ x a) = (fun x => cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}
-- Mathlib.Analysis.Convex.Deriv
/-- If `f : ℝ → ℝ` is convex on `S` and differentiable at `y ∈ S`, then the slope of any secant
line with right endpoint at `y` is bounded above by the derivative of `f` at `y`.  -/
ConvexOn.slope_le_of_hasDerivAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ}, ConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivAt f f' y → slope f x y ≤ f'
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The cocone over the proposed colimit commutative ring.  -/
CommRingCat.FilteredColimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → (F : CategoryTheory.Functor J CommRingCat) → CategoryTheory.Limits.Cocone F
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote.eq_2 : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ) (m : Lean.Grind.CommRing.Mon)
  (p_2 : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.add k m p_2) =
    k • Lean.Grind.CommRing.Mon.denote ctx m + Lean.Grind.CommRing.Poly.denote ctx p_2
-- Mathlib.Topology.Separation.Regular
/-- A completely normal space is a normal space.  -/
CompletelyNormalSpace.toNormalSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompletelyNormalSpace X], NormalSpace X
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (toLatticeHom : LatticeHom α β) (map_top' : toLatticeHom.toFun ⊤ = ⊤)
  (map_bot' : toLatticeHom.toFun ⊥ = ⊥) (toLatticeHom_1 : LatticeHom α β) (map_top'_1 : toLatticeHom_1.toFun ⊤ = ⊤)
  (map_bot'_1 : toLatticeHom_1.toFun ⊥ = ⊥),
  ({ toLatticeHom := toLatticeHom, map_top' := map_top', map_bot' := map_bot' } =
      { toLatticeHom := toLatticeHom_1, map_top' := map_top'_1, map_bot' := map_bot'_1 }) =
    (toLatticeHom = toLatticeHom_1)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.sr_mul_self : ∀ {n : ℕ} (i : ZMod n), DihedralGroup.sr i * DihedralGroup.sr i = 1
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U) ↔
    AlgebraicGeometry.IsAffineOpen U
-- Mathlib.Topology.Algebra.Group.Torsor
instIsTopologicalAddTorsorProd : ∀ {V : Type u_1} {W : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : AddCommGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] [inst_5 : AddCommGroup W]
  [inst_6 : TopologicalSpace W] [inst_7 : AddTorsor W Q] [inst_8 : TopologicalSpace Q] [IsTopologicalAddTorsor Q],
  IsTopologicalAddTorsor (P × Q)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` preserves finite colimits, then `F : Cᵒᵖ ⥤ D` preserves finite
limits.  -/
CategoryTheory.Limits.preservesFiniteLimits_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesFiniteColimits F.rightOp],
  CategoryTheory.Limits.PreservesFiniteLimits F
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instToFormatSimpTheorem : Std.ToFormat Lean.Meta.SimpTheorem
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_homCategory_comp_fst : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (X Y : B × C)
  {X_1 Y_1 Z : (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)} (f : (X_1.1 ⟶ Y_1.1) × (X_1.2 ⟶ Y_1.2)) (g : (Y_1.1 ⟶ Z.1) × (Y_1.2 ⟶ Z.2)),
  (CategoryTheory.CategoryStruct.comp f g).1 = CategoryTheory.CategoryStruct.comp f.1 g.1
-- Mathlib.GroupTheory.Coset.Defs
/-- **Alias** of `QuotientAddGroup.mk_out_eq_add`. -/
QuotientAddGroup.mk_out_eq_mul : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (g : α), ∃ h, Quotient.out ↑g = g + ↑h
-- Mathlib.Data.PEquiv
PEquiv.ofSet.congr_simp : ∀ {α : Type u} (s s_1 : Set α),
  s = s_1 →
    ∀ {inst : DecidablePred fun x => x ∈ s} [inst_1 : DecidablePred fun x => x ∈ s_1], PEquiv.ofSet s = PEquiv.ofSet s_1
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_mono_enorm_ae : ∀ {α : Type u_1} {ε : Type u_2} {ε' : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : ENorm ε] [inst_1 : ENorm ε'] {f : α → ε} {g : α → ε'},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) → MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.coeff_mapDomain : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (x : MonoidAlgebra R M),
  (MonoidAlgebra.mapDomain f x).coeff = Finsupp.mapDomain f x.coeff
-- Std.Data.ExtTreeSet.Basic
/-- Given a proof that the tree set is not empty, retrieves the largest element.
 -/
Std.ExtTreeSet.max : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtTreeSet α cmp) → t ≠ ∅ → α
-- Lean.Elab.PreDefinition.Structural.FindRecArg
/-- Result of `findRecArgCandidates`: candidate combinations and a diagnostic report.  -/
Lean.Elab.Structural.RecArgCandidates : Type
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothPresheafCommGroup.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (A : Type u)
  [inst_9 : TopologicalSpace A] [inst_10 : ChartedSpace H A] [inst_11 : CommGroup A] [inst_12 : LieGroup I (↑⊤) A],
  smoothPresheafCommGroup IM I M A =
    { obj := fun U => CommGrpCat.of ((smoothSheaf IM I M A).presheaf.obj U),
      map := fun {X Y} h => CommGrpCat.ofHom (ContMDiffMap.restrictMonoidHom IM I A ⋯), map_id := ⋯, map_comp := ⋯ }
-- Lean.Elab.Command
/-- `State.nextMacroScope` after expansion.  -/
Lean.Elab.Command.MacroExpandedSnapshot.newNextMacroScope : Lean.Elab.Command.MacroExpandedSnapshot → ℕ
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_le_comap_iff_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Surjective ⇑f → ∀ {p q : Submodule R₂ M₂}, Submodule.comap f p ≤ Submodule.comap f q ↔ p ≤ q
-- Mathlib.GroupTheory.Coset.Basic
mem_rightAddCoset_rightAddCoset : ∀ {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) {a : α}, AddOpposite.op a +ᵥ ↑s = ↑s → a ∈ s
-- Mathlib.Algebra.Ring.Defs
NonUnitalCommSemiring.toCommSemigroup : {α : Type u} → [self : NonUnitalCommSemiring α] → CommSemigroup α
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- If `K` is a field and there is no `r : K` such that `r ^ 2 = a + b * r`,
then `QuadraticAlgebra K a b` is a field.  -/
QuadraticAlgebra.instField : {K : Type u_1} →
  [inst : Field K] → {a b : K} → [Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)] → Field (QuadraticAlgebra K a b)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.ofList_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {k : α}, Std.TreeSet.Raw.ofList [k] cmp = ∅.insert k
-- Batteries.CodeAction.Attr
Batteries.CodeAction.instInhabitedTacticCodeActions : Inhabited Batteries.CodeAction.TacticCodeActions
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.mk.sizeOf_spec : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (x : ↥X) (y : ↥Y) (s : ↥S) (hx : f x = s) (hy : g y = s),
  sizeOf { x := x, y := y, s := s, hx := hx, hy := hy } = 1 + sizeOf x + sizeOf y + sizeOf s + sizeOf hx + sizeOf hy
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instSetLike : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → SetLike (FractionalIdeal S P) P
-- Init.Data.BitVec.Lemmas
BitVec.zero_sle_iff_msb_eq_false : ∀ {w : ℕ} {x : BitVec w}, (0#w).sle x = true ↔ x.msb = false
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.coeAddHom_apply : ∀ {α : Type u_1} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α), MeasureTheory.Measure.coeAddHom μ = ⇑μ
-- Mathlib.Topology.Separation.Hausdorff
/-- Two different points can be separated by open sets.  -/
t2_separation : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {x y : X},
  x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Weakening the condition on the structure morphisms is fully faithful.  -/
CategoryTheory.MorphismProperty.Comma.fullyFaithfulChangeProp : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                {P P' : CategoryTheory.MorphismProperty T} →
                  {Q : CategoryTheory.MorphismProperty A} →
                    {W : CategoryTheory.MorphismProperty B} →
                      (hP : P ≤ P') →
                        [inst_3 : Q.IsMultiplicative] →
                          [inst_4 : W.IsMultiplicative] →
                            (CategoryTheory.MorphismProperty.Comma.changeProp L R hP ⋯ ⋯).FullyFaithful
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.unop_sum : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (X Y : Cᵒᵖ)
  {ι : Type u_2} (s : Finset ι) (f : ι → (X ⟶ Y)), (s.sum f).unop = ∑ i ∈ s, (f i).unop
-- Mathlib.Algebra.Order.Ring.Synonym
ofDual_intCast : ∀ {R : Type u_1} [inst : IntCast R] (n : ℤ), OrderDual.ofDual ↑n = ↑n
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- An `AffineTargetMorphismProperty` is a class of morphisms from an arbitrary scheme into an
affine scheme.  -/
AlgebraicGeometry.AffineTargetMorphismProperty : Type (u_1 + 1)
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.getTacticSuggestionGroups : LeanSearchClient.SearchServer → String → ℕ → Lean.MetaM (Array (String × Array Lean.Meta.Tactic.TryThis.Suggestion))