mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.pointed_toConvexCone : ∀ {R : Type u_2} {E : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] (C : ProperCone R E), (↑↑C).Pointed
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- A family of gluing data consists of
1. An index type `J`
2. A sheafed space `U i` for each `i : J`.
3. A sheafed space `V i j` for each `i j : J`.
   (Note that this is `J × J → SheafedSpace C` rather than `J → J → SheafedSpace C` to
   connect to the limits library more easily.)
4. An open immersion `f i j : V i j ⟶ U i` for each `i j : J`.
5. A transition map `t i j : V i j ⟶ V j i` for each `i j : J`.

such that
6. `f i i` is an isomorphism.
7. `t i i` is the identity.
8. `V i j ×[U i] V i k ⟶ V i j ⟶ V j i` factors through `V j k ×[U j] V j i ⟶ V j i` via some
   `t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i`.
9. `t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _`.

We can then glue the spaces `U i` together by identifying `V i j` with `V j i`, such
that the `U i`'s are open subspaces of the glued space.
 -/
AlgebraicGeometry.SheafedSpace.GlueData : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u (v + 1))
-- Mathlib.Topology.Category.Sequential
Sequential.instInhabited : Inhabited Sequential
-- Mathlib.Data.Set.Lattice
Set.nonempty_iInter : ∀ {α : Type u_1} {ι : Sort u_5} {f : ι → Set α}, (⋂ i, f i).Nonempty ↔ ∃ x, ∀ (i : ι), x ∈ f i
-- Init.Prelude
/-- Creates a `UInt64` from a `BitVec 64`. This function is overridden with a native implementation.
 -/
UInt64.ofBitVec : BitVec 64 → UInt64
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instGroup.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → Group (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)],
  DirectLimit.instGroup =
    { toMonoid := DirectLimit.instMonoid, inv := DirectLimit.map f f (fun x x_1 => x_1⁻¹) ⋯,
      div := DirectLimit.map₂ f f f (fun x x1 x2 => x1 / x2) ⋯,
      zpow := fun n => DirectLimit.map f f (fun x x_1 => x_1 ^ n) ⋯, div_eq_mul_inv := ⋯, zpow_zero' := ⋯,
      zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Mathlib.Topology.UrysohnsBounded
/-- **Urysohn's lemma**: if `s` and `t` are two disjoint closed sets in a normal topological
space `X`, then there exists a continuous function `f : X → ℝ` such that

* `f` equals zero on `s`;
* `f` equals one on `t`;
* `0 ≤ f x ≤ 1` for all `x`.
 -/
exists_bounded_zero_one_of_closed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NormalSpace X] {s t : Set X},
  IsClosed s → IsClosed t → Disjoint s t → ∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
-- Init.Data.List.Basic
List.Mem.below : {α : Type u} → {a : α} → {motive : (a_1 : List α) → List.Mem a a_1 → Prop} → {a_1 : List α} → List.Mem a a_1 → Prop
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_eq_get! : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m).WF →
    ∀ {a : α} {h : m.contains a = true},
      Std.DHashMap.Internal.Raw₀.Const.get m a h = Std.DHashMap.Internal.Raw₀.Const.get! m a
-- Mathlib.Control.EquivFunctor
EquivFunctor.mapEquiv.eq_1 : ∀ (f : Type u₀ → Type u₁) [inst : EquivFunctor f] {α β : Type u₀} (e : α ≃ β),
  EquivFunctor.mapEquiv f e =
    { toFun := EquivFunctor.map e, invFun := EquivFunctor.map e.symm, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.instIsMonHomComonHomEquivMonComonCounitIsoAppX : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  CategoryTheory.IsMonHom (CategoryTheory.Bimon.equivMonComonCounitIsoAppX M).hom
-- Mathlib.CategoryTheory.Limits.Shapes.Equivalence
CategoryTheory.Equivalence.hasInitial_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), CategoryTheory.Limits.HasInitial C ↔ CategoryTheory.Limits.HasInitial D
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T) {Z : C} (h : T.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd R.hom T.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd R.hom S.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f) h)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.tensor : {C : Type u} →
  CategoryTheory.FreeMonoidalCategory C → CategoryTheory.FreeMonoidalCategory C → CategoryTheory.FreeMonoidalCategory C
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.closure_insert_zero : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G), AddSubgroup.closure (insert 0 s) = AddSubgroup.closure s
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeffOn.const_mul : ∀ {a b : ℝ} (f : ℝ → ℂ) (c : ℂ) (n : ℤ) (hab : a < b),
  fourierCoeffOn hab (fun x => c * f x) n = c * fourierCoeffOn hab f n
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Differentiable.comp_mdifferentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {F' : Type u_11} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F'] {g : F → F'}
  {f : M → F}, Differentiable 𝕜 g → MDiff f → MDiff (g ∘ f)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.dist_le_half_iff : ∀ {α : Type u_1} {s t : Stream'.Seq α},
  dist s t ≤ 2⁻¹ ↔
    s = Stream'.Seq.nil ∧ t = Stream'.Seq.nil ∨ ∃ hd s' t', s = Stream'.Seq.cons hd s' ∧ t = Stream'.Seq.cons hd t'
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat), CategoryTheory.Limits.PreservesFiniteLimits (SheafOfModules.toSheaf R)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.mfderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  MDiffAt[s] f x →
    mfderiv[s] f x =
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.centralizer_toNonUnitalSubalgebra : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] [inst_5 : SMulCommClass R A A] (s : Set A),
  (NonUnitalStarSubalgebra.centralizer R s).toNonUnitalSubalgebra = NonUnitalSubalgebra.centralizer R (s ∪ star s)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.self_trans_symm : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), e.trans e.symm = LinearIsometryEquiv.refl R E
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.iteratedDeriv_odd_cos : ∀ (n : ℕ), iteratedDeriv (2 * n + 1) Real.cos = (-1) ^ (n + 1) * Real.sin
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.instIsScalarTower : ∀ {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N] {R' : Type u_7} {R'' : Type u_8} {A : Type u_9}
  [inst_4 : Monoid R'] [inst_5 : Monoid R''] [inst_6 : Semiring A] [inst_7 : Module A M] [inst_8 : Module A N]
  [inst_9 : DistribMulAction R' N] [inst_10 : ContinuousConstSMul R' N] [inst_11 : SMulCommClass A R' N]
  [inst_12 : DistribMulAction R'' N] [inst_13 : ContinuousConstSMul R'' N] [inst_14 : SMulCommClass A R'' N]
  [inst_15 : SMul R' R''] [IsScalarTower R' R'' N], IsScalarTower R' R'' (M [⋀^ι]→L[A] N)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.isCircuit_def : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C ↔ Minimal M.Dep C
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.isoMk_hom_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (l : f.left ≅ g.left)
  (r : f.right ≅ g.right)
  (h :
    autoParam (CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom)
      CategoryTheory.Arrow.isoMk._auto_1),
  (CategoryTheory.Arrow.isoMk l r h).hom.right = r.hom
-- Mathlib.Topology.Bornology.Constructions
boundedSpace_subtype_iff : ∀ {α : Type u_1} [inst : Bornology α] {p : α → Prop}, BoundedSpace (Subtype p) ↔ Bornology.IsBounded {x | p x}
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₁.ι_comp_t_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  (d : CategoryTheory.OrthogonalReflection.D₁ W Z) {Z_1 : C} (h : ∐ CategoryTheory.OrthogonalReflection.D₁.obj₂ ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι CategoryTheory.OrthogonalReflection.D₁.obj₁ d)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.D₁.t W Z) h) =
    CategoryTheory.CategoryStruct.comp (↑d.fst).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι CategoryTheory.OrthogonalReflection.D₁.obj₂ d)
        h)
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.univ : ∀ {α : Type u_2} [inst : LE α], CountableInfClosed Set.univ
-- Init.Data.String.Lemmas.Slice
String.Slice.Pos.get?_endPos : ∀ {s : String.Slice}, s.endPos.get? = none
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.ae_mem_finset_iff_map_eq_sum_dirac : ∀ {α : Type u_4} {β : Type u_5} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α]
  {f : β → α} {s : Finset α} {μ : MeasureTheory.Measure β},
  AEMeasurable f μ →
    ((∀ᵐ (b : β) ∂μ, f b ∈ s) ↔ MeasureTheory.Measure.map f μ = ∑ a ∈ s, μ (f ⁻¹' {a}) • MeasureTheory.Measure.dirac a)
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.chebyshev_U_eq_dickson_two_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  Polynomial.Chebyshev.U R ↑n = (Polynomial.dickson 2 1 n).comp (2 * Polynomial.X)
-- Mathlib.Algebra.Homology.ShortComplex.Ab
/-- Given a short complex `S` of abelian groups, this is the isomorphism between
the abstract `S.cycles` of the homology API and the more concrete description as
`AddMonoidHom.ker S.g`.  -/
CategoryTheory.ShortComplex.abCyclesIso : (S : CategoryTheory.ShortComplex Ab) → S.cycles ≅ AddCommGrpCat.of ↥(AddCommGrpCat.Hom.hom S.g).ker
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.inhabitedLiftsToColimit : {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] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor C D) →
                [CategoryTheory.CreatesColimit K F] →
                  (c : CategoryTheory.Limits.Cocone (K.comp F)) →
                    (t : CategoryTheory.Limits.IsColimit c) → Inhabited (CategoryTheory.LiftsToColimit K F c t)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.apply_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : α → β) (h : ∀ (x : β), MeasurableSet (f ⁻¹' {x}))
  (h' : (Set.range f).Finite) (x : α), { toFun := f, measurableSet_fiber' := h, finite_range' := h' } x = f x
-- Init.Data.Nat.Basic
Nat.mul_le_mul_left : ∀ {n m : ℕ} (k : ℕ), n ≤ m → k * n ≤ k * m
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.Hom.id_eq_id : ∀ {J : CategoryTheory.Limits.MulticospanShape} (X : CategoryTheory.Limits.WalkingMulticospan J),
  CategoryTheory.Limits.WalkingMulticospan.Hom.id X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.cells_ssubset_iff : ∀ {μ ν : YoungDiagram}, μ.cells ⊂ ν.cells ↔ μ < ν
-- Mathlib.Tactic.DeriveCountable
_private.Mathlib.Tactic.DeriveCountable.0.Mathlib.Deriving.Countable.mkInjThmMatch.mkAlts : Lean.Elab.Deriving.Context → Lean.InductiveVal → Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.matchAlt))
-- Init.Data.UInt.Lemmas
UInt8.le_iff_toNat_le : ∀ {a b : UInt8}, a ≤ b ↔ a.toNat ≤ b.toNat
-- Mathlib.Algebra.Quandle
/-- The identity homomorphism  -/
ShelfHom.id : (S : Type u_4) → [inst : Shelf S] → ShelfHom S S
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCore.sizeOf_spec : ∀ (e : Lean.Expr) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCore e lhs rhs) = 1 + sizeOf e + sizeOf lhs + sizeOf rhs
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
/-- A bounded convergence theorem for a finite measure:
If bounded continuous non-negative functions are uniformly bounded by a constant and tend to a
limit, then their integrals against the finite measure tend to the integral of the limit.
This formulation assumes:
* the functions tend to a limit along a countably generated filter;
* the limit is in the almost everywhere sense;
* boundedness holds almost everywhere;
* integration is `MeasureTheory.lintegral`, i.e., the functions and their integrals are
  `ℝ≥0∞`-valued.
 -/
MeasureTheory.tendsto_lintegral_nn_filter_of_le_const : ∀ {Ω : Type u_1} [inst : TopologicalSpace Ω] [inst_1 : MeasurableSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2}
  {L : Filter ι} [L.IsCountablyGenerated] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ]
  {fs : ι → BoundedContinuousFunction Ω NNReal} {c : NNReal},
  (∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c) →
    ∀ {f : Ω → NNReal},
      (∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun i => (fs i) ω) L (nhds (f ω))) →
        Filter.Tendsto (fun i => ∫⁻ (ω : Ω), ↑((fs i) ω) ∂μ) L (nhds (∫⁻ (ω : Ω), ↑(f ω) ∂μ))
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.comp_apply : ∀ {X Y T : Semigrp} (f : X ⟶ Y) (g : Y ⟶ T) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Lean.Linter.Init
Lean.Linter.addEnvLinterOption : Lean.Option Bool → IO Unit
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.factorThru.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J X Y : C} [inst_1 : CategoryTheory.Injective J]
  (g g_1 : X ⟶ J),
  g = g_1 →
    ∀ (f f_1 : X ⟶ Y) (e_f : f = f_1) [inst_2 : CategoryTheory.Mono f],
      CategoryTheory.Injective.factorThru g f = CategoryTheory.Injective.factorThru g_1 f_1
-- Mathlib.Topology.Order
dense_indiscrete : ∀ {α : Type u_1} {t₂ : TopologicalSpace α} [IndiscreteTopology α] {s : Set α}, s.Nonempty → Dense s
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.prod_linear : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1]
  [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] [inst_7 : AddCommGroup V3]
  [inst_8 : Module k V3] [inst_9 : AddTorsor V3 P3] (f : P1 →ᵃ[k] P2) (g : P1 →ᵃ[k] P3),
  (f.prod g).linear = f.linear.prod g.linear
-- Mathlib.Order.SuccPred.Basic
Order.pred_le_iff_le_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : PredOrder α] {a b : α},
  Order.pred a ≤ b ↔ a ≤ Order.succ b
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
LinearMap.BilinMap.tmul.congr_simp : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid N₁]
  [inst_5 : AddCommMonoid N₂] [inst_6 : Algebra R A] [inst_7 : Module R M₁] [inst_8 : Module A M₁]
  [inst_9 : Module R N₁] [inst_10 : Module A N₁] [inst_11 : SMulCommClass R A M₁] [inst_12 : IsScalarTower R A M₁]
  [inst_13 : SMulCommClass R A N₁] [inst_14 : IsScalarTower R A N₁] [inst_15 : Module R M₂] [inst_16 : Module R N₂]
  (B₁ B₁_1 : LinearMap.BilinMap A M₁ N₁),
  B₁ = B₁_1 → ∀ (B₂ B₂_1 : LinearMap.BilinMap R M₂ N₂), B₂ = B₂_1 → B₁.tmul B₂ = B₁_1.tmul B₂_1
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
MeasureTheory.AEStronglyMeasurable.fourierSMulRight : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  [SecondCountableTopologyEither V (W →L[ℝ] ℝ)] [inst_7 : MeasurableSpace V] [BorelSpace V] {L : V →L[ℝ] W →L[ℝ] ℝ}
  {f : V → E} {μ : MeasureTheory.Measure V},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable (fun v => VectorFourier.fourierSMulRight L f v) μ
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.extend_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {δ : Type u_2}
  [inst_2 : TopologicalSpace δ] [inst_3 : DiscreteTopology δ] (f : α ↪ δ) (g : BoundedContinuousFunction α β)
  (h : BoundedContinuousFunction δ β) (x : α), (BoundedContinuousFunction.extend f g h) (f x) = g x
-- Mathlib.Topology.CWComplex.Classical.Finite
Topology.RelCWComplex.Finite.mk : ∀ {X : Type u_1} [inst : TopologicalSpace X] {C D : Set X} [inst_1 : Topology.RelCWComplex C D]
  [toFiniteDimensional : Topology.RelCWComplex.FiniteDimensional C] [toFiniteType : Topology.RelCWComplex.FiniteType C],
  Topology.RelCWComplex.Finite C
-- Mathlib.Algebra.Star.Subalgebra
/-- The inclusion map between `StarSubalgebra`s given by `Subtype.map id` as a `StarAlgHom`.  -/
StarSubalgebra.inclusion : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Algebra R A] → [inst_5 : StarModule R A] → {S₁ S₂ : StarSubalgebra R A} → S₁ ≤ S₂ → ↥S₁ →⋆ₐ[R] ↥S₂
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- A variant of `prod_range_succ` which pulls off the first term in the product rather than the
last.  -/
List.prod_range_succ' : ∀ {M : Type u_4} [inst : Monoid M] (f : ℕ → M) (n : ℕ),
  (List.map f (List.range n.succ)).prod = f 0 * (List.map (fun i => f i.succ) (List.range n)).prod
-- Mathlib.CategoryTheory.Dialectica.Monoidal
/-- Right unit cancellation `X ⊗ 1 ≅ X` in `Dial C`.  -/
CategoryTheory.Dial.rightUnitorImpl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        (X : CategoryTheory.Dial C) → X.tensorObjImpl CategoryTheory.Dial.tensorUnitImpl ≅ X
-- Mathlib.Tactic.Linter.Style
/-- `unwanted_cdot stx` returns an array of syntax atoms within `stx`
corresponding to `cdot`s that are not written with the character `·`.
This is precisely what the `cdot` linter flags.
 -/
_private.Mathlib.Tactic.Linter.Style.0.Mathlib.Linter.unwanted_cdot : Lean.Syntax → Array Lean.Syntax
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Slice.find?_prop_eq_some_iff_splits : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  s.find? p = some pos ↔ ∃ t c u, pos.Splits t (String.singleton c ++ u) ∧ p c ∧ ∀ d ∈ t.toList, ¬p d
-- Init.Data.Vector.Lemmas
Vector.toArray_eraseIdx : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n), (xs.eraseIdx i h).toArray = xs.toArray.eraseIdx i ⋯
-- Mathlib.Algebra.Group.End
Equiv.addLeft_zero : ∀ {α : Type u_4} [inst : AddGroup α], Equiv.addLeft 0 = 1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_le_maxKey_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {he : t ≠ ∅}, (cmp (t.maxKey he) ((t.insert k v).maxKey ⋯)).isLE = true
-- Mathlib.Order.Shrink
instBotShrink.eq_1 : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Bot α], instBotShrink = { bot := (equivShrink α) ⊥ }
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.instIsScalarTowerCotangent : ∀ {R : Type u_3} {S : Type u_1} {S' : Type u_2} [inst : CommRing R] [inst_1 : CommSemiring S] [inst_2 : Algebra S R]
  [inst_3 : CommSemiring S'] [inst_4 : Algebra S' R] [inst_5 : Algebra S S'] [IsScalarTower S S' R] (I : Ideal R),
  IsScalarTower S S' I.Cotangent
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.blocks_pos' : ∀ {n : ℕ} (c : Composition n) (i : ℕ) (h : i < c.length), 0 < c.blocks[i]
-- Mathlib.Algebra.Group.Defs
isCancelAdd_iff : ∀ (G : Type u) [inst : Add G], IsCancelAdd G ↔ IsLeftCancelAdd G ∧ IsRightCancelAdd G
-- Mathlib.RingTheory.PicardGroup
_private.Mathlib.RingTheory.PicardGroup.0.Module.Invertible.bijective_self_of_surjective : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M] (f : R →ₗ[R] M), Function.Surjective ⇑f → Function.Bijective ⇑f
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The profinite completion of `G` as a projective limit.  -/
ProfiniteGrp.ProfiniteCompletion.completion : GrpCat → ProfiniteGrp.{u}
-- Lean.ExtraModUses
/-- Records an additional import dependency for the current module, using `Environment.isExporting` as
the visibility level.

NOTE: Directly recording a module name does not trigger including indirect dependencies recorded via
`recordIndirectModUse`, prefer `recordExtraModUseFromDecl` instead.
 -/
Lean.recordExtraModUse : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadTrace m] →
        [Lean.MonadOptions m] → [Lean.MonadRef m] → [Lean.AddMessageContext m] → Lean.Name → Bool → m Unit
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.I.homeomorph_one : TopCat.I.homeomorph 1 = 1
-- Lean.Elab.Do.Basic
/-- The cached ``PUnit.unit`` expression.  -/
Lean.Elab.Do.mkPUnitUnit : Lean.Elab.Do.DoElabM Lean.Expr