mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- If two functions agree in a neighborhood within `s`, then so do their iterated derivatives.  -/
Filter.EventuallyEq.iteratedFDerivWithin : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E},
  f₁ =ᶠ[nhdsWithin x s] f → ∀ (n : ℕ), iteratedFDerivWithin 𝕜 n f₁ s =ᶠ[nhdsWithin x s] iteratedFDerivWithin 𝕜 n f s
-- Mathlib.Combinatorics.Colex
/-- Colex is an extension of the base order.  -/
Finset.Colex.singleton_le_singleton : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, toColex {a} ≤ toColex {b} ↔ a ≤ b
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.functorProdFunctorEquivCounitIso_inv_app_app : ∀ (A : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (C : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (X : CategoryTheory.Functor A (B × C)) (X_1 : A),
  ((CategoryTheory.functorProdFunctorEquivCounitIso A B C).inv.app X).app X_1 =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.obj X_1).1)
      (CategoryTheory.CategoryStruct.id (X.obj X_1).2)
-- Init.Data.Nat.Fold
Nat.any_succ : ∀ {n : ℕ} (f : (i : ℕ) → i < n + 1 → Bool), (n + 1).any f = ((n.any fun i h => f i ⋯) || f n ⋯)
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.toSubmodule_sup : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} [inst : Semiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] {ρ : Representation A G W} (ρ₁ ρ₂ : Subrepresentation ρ),
  (ρ₁ ⊔ ρ₂).toSubmodule = ρ₁.toSubmodule ⊔ ρ₂.toSubmodule
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso_hom_app_app : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor A B × CategoryTheory.Functor A' B) (X_1 : A'),
  (CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso.hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.2.obj X_1)
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- This result shows that there always exists a next term in the sequence.  -/
NumberField.Units.dirichletUnitTheorem.seq_next : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (w₁ : NumberField.InfinitePlace K) {B : ℕ},
  NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B →
    ∀ {x : NumberField.RingOfIntegers K},
      x ≠ 0 → ∃ y, y ≠ 0 ∧ (∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → w ↑y < w ↑x) ∧ |(Algebra.norm ℚ) ↑y| ≤ ↑B
-- Mathlib.SetTheory.Cardinal.Basic
/-- The cardinality of a union is at most the sum of the cardinalities
of the two sets.  -/
Cardinal.mk_union_le : ∀ {α : Type u} (S T : Set α), Cardinal.mk ↑(S ∪ T) ≤ Cardinal.mk ↑S + Cardinal.mk ↑T
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `η ▷ f` into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.evalWhiskerRightAux : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
      [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
        [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
          Mathlib.Tactic.BicategoryLike.HorizontalComp →
            Mathlib.Tactic.BicategoryLike.Atom₁ →
              Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} {fallback : β},
  Std.ExtDTreeMap.Const.getD (t₁ ∩ t₂) k fallback =
    if k ∈ t₂ then Std.ExtDTreeMap.Const.getD t₁ k fallback else fallback
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.id_comp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β),
  ProbabilityTheory.Kernel.id.comp κ = κ
-- Mathlib.MeasureTheory.Integral.Marginal
/-- Integrate `f(x₁,…,xₙ)` over all variables `xᵢ` where `i ∈ s`. Return a function in the
remaining variables (it will be constant in the `xᵢ` for `i ∈ s`).
This is the marginal distribution of all variables not in `s` when the considered measure
is the product measure.  -/
MeasureTheory.lmarginal : {δ : Type u_1} →
  {X : δ → Type u_3} →
    [inst : (i : δ) → MeasurableSpace (X i)] →
      [DecidableEq δ] →
        ((i : δ) → MeasureTheory.Measure (X i)) → Finset δ → (((i : δ) → X i) → ENNReal) → ((i : δ) → X i) → ENNReal
-- Mathlib.CategoryTheory.Opposites
/-- `Functor.op` transforms identity functors to identity functors.  -/
CategoryTheory.Functor.opId : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (CategoryTheory.Functor.id C).op ≅ CategoryTheory.Functor.id Cᵒᵖ
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- Assume that a localizer morphism `Φ : LocalizerMorphism W₁ W₂` induces
a fully faithful functor on the localized categories.
If `L₂ : C₂ ⥤ D₂` is a localization functor for `W₂` and we have a
factorization `iso : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F` as an essentially surjective
functor `L₁ : C₁ ⥤ D₁` followed by a fully faithful functor `F : D₁ ⥤ D₂`,
then `L₁` is a localization functor for `W₁`.  -/
CategoryTheory.LocalizerMorphism.isLocalization_of_isLocalizedFullyFaithful : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁]
  [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.IsLocalizedFullyFaithful]
  {L₂ : CategoryTheory.Functor C₂ D₂} [L₂.IsLocalization W₂] {L₁ : CategoryTheory.Functor C₁ D₁}
  {F : CategoryTheory.Functor D₁ D₂} (iso : Φ.functor.comp L₂ ≅ L₁.comp F) [F.Full] [F.Faithful] [L₁.EssSurj],
  L₁.IsLocalization W₁
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.leftUnitor_hom_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Center C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.f =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.fst).hom
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_one_eq_id_iff : ∀ {F' : Type u_4} {α : Type u_5} [inst : FunLike F' α α] [inst_1 : One F'] [IsOneApplyEqSelf F' α] (f : F'),
  ⇑f = id ↔ f = 1
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.instDecidableEqDyadic.decEq.match_1.eq_4 : ∀ (motive : Dyadic → Dyadic → Sort u_1) (a a_1 : ℤ) (a_2 : a % 2 = 1) (b b_1 : ℤ) (b_2 : b % 2 = 1)
  (h_1 : Unit → motive Dyadic.zero Dyadic.zero)
  (h_2 : (n k : ℤ) → (hn : n % 2 = 1) → motive Dyadic.zero (Dyadic.ofOdd n k hn))
  (h_3 : (n k : ℤ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n k hn) Dyadic.zero)
  (h_4 :
    (a a_3 : ℤ) →
      (a_4 : a % 2 = 1) → (b b_3 : ℤ) → (b_4 : b % 2 = 1) → motive (Dyadic.ofOdd a a_3 a_4) (Dyadic.ofOdd b b_3 b_4)),
  (match Dyadic.ofOdd a a_1 a_2, Dyadic.ofOdd b b_1 b_2 with
    | Dyadic.zero, Dyadic.zero => h_1 ()
    | Dyadic.zero, Dyadic.ofOdd n k hn => h_2 n k hn
    | Dyadic.ofOdd n k hn, Dyadic.zero => h_3 n k hn
    | Dyadic.ofOdd a a_3 a_4, Dyadic.ofOdd b b_3 b_4 => h_4 a a_3 a_4 b b_3 b_4) =
    h_4 a a_1 a_2 b b_1 b_2
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.realSize.eq_2 : ∀ {α : Type u_1} (rank : ℕ) (val : α) (c : Batteries.BinomialHeap.Imp.HeapNode α)
  (s : Batteries.BinomialHeap.Imp.Heap α),
  (Batteries.BinomialHeap.Imp.Heap.cons rank val c s).realSize = c.realSize + 1 + s.realSize
-- Mathlib.Topology.Algebra.Ring.Basic
Pi.instIsTopologicalSemiring : ∀ {ι : Type u_2} {R : ι → Type u_3} [inst : (i : ι) → TopologicalSpace (R i)]
  [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (R i)] [∀ (i : ι), IsTopologicalSemiring (R i)],
  IsTopologicalSemiring ((i : ι) → R i)
-- Lean.Parser.Types
Lean.Parser.ParserModuleContext.mk : Lean.Environment → Lean.Options → Lean.Name → List Lean.OpenDecl → Lean.Parser.ParserModuleContext
-- Mathlib.GroupTheory.Perm.Centralizer
/-- Given `a : Equiv.Perm.Basis g`,
we define a right inverse of `Equiv.Perm.OnCycleFactors.toPermHom`,
on `range_toPermHom' g`  -/
Equiv.Perm.Basis.toCentralizer : {α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] →
      {g : Equiv.Perm α} → g.Basis → ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g) →* ↥(Subgroup.centralizer {g})
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- Bird's equation (1) : `x^(p)_ij = (-1)^p ∑ { f[iα, jα] | α ∈ S_p(βᵢ) }`.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.Eq1 : {R : Type u_1} → [CommRing R] → {n : ℕ} → Matrix (Fin n) (Fin n) R → ℕ → Prop
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar.congr_simp : ∀ (bytes bytes_1 : ByteArray) (e_bytes : bytes = bytes_1) (i i_1 : ℕ) (e_i : i = i_1)
  (h : (bytes.utf8DecodeChar? i).isSome = true), bytes.utf8DecodeChar i h = bytes_1.utf8DecodeChar i_1 ⋯
-- Std.Data.ExtDTreeMap.Basic
/-- If there is no mapping for the given key, inserts the given mapping into the map. Otherwise,
returns the map unaltered.
 -/
Std.ExtDTreeMap.insertIfNew : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → (a : α) → β a → Std.ExtDTreeMap α β cmp
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableAtFilter_top : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε' : Type u_7} [inst : TopologicalSpace ε']
  [inst_1 : ENormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε'] {f : α → ε'},
  MeasureTheory.IntegrableAtFilter f ⊤ μ ↔ MeasureTheory.Integrable f μ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.map_polynomial : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [inst_1 : CommRing S] (f : R →+* S),
  (W.map f).polynomial = Polynomial.map (Polynomial.mapRingHom f) W.polynomial
-- Mathlib.Order.UpperLower.LocallyFinite
Set.Finite.upperClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [LocallyFiniteOrderTop α], s.Finite → (↑(upperClosure s)).Finite
-- Init.Data.List.Control
List.instFunctor : Functor List
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.WF.of_rankGT : ∀ {α : Type u_1} {le : α → α → Bool} {n' : ℕ} {s : Batteries.BinomialHeap.Imp.Heap α} {n : ℕ},
  s.rankGT n → Batteries.BinomialHeap.Imp.Heap.WF le n' s → Batteries.BinomialHeap.Imp.Heap.WF le (n + 1) s
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.precheckUnop : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.mul_lt_one_of_lt_of_le`.  -/
Right.mul_lt_one_of_lt_of_le : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightStrictMono α] {a b : α},
  a < 1 → b ≤ 1 → a * b < 1
-- Mathlib.Data.Multiset.Fintype
Multiset.card_coe : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), Fintype.card m.ToType = m.card
-- Init.Data.UInt.Lemmas
UInt16.le_total : ∀ (a b : UInt16), a ≤ b ∨ b ≤ a
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instIsSemitopologicalRingId : ∀ {𝕜₂ : Type u_6} {F : Type u_10} [inst : NormedField 𝕜₂] [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] [inst_5 : ContinuousConstSMul 𝕜₂ F],
  IsSemitopologicalRing (F →WOT[𝕜₂] F)
-- Mathlib.Analysis.RCLike.Basic
_private.Mathlib.Analysis.RCLike.Basic.0.RCLike.termImR : Lean.ParserDescr
-- Lean.Elab.PreDefinition.Mutual
/-- Cleans the right-hand-sides of the predefinitions, to prepare for inclusion in the EqnInfos:
* Remove RecAppSyntax markers
* Abstracts nested proofs (and for that, add the `_unsafe_rec` definitions)
 -/
Lean.Elab.Mutual.cleanPreDef : Lean.Elab.PreDefinition → optParam Bool true → Lean.MetaM Lean.Elab.PreDefinition
-- Mathlib.Analysis.Complex.Harmonic.Analytic
/-- **Alias** of `InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_univ_re_eq`.

---

If a function `f : ℂ → ℝ` is harmonic, then `f` is the real part of a holomorphic function.
 -/
InnerProductSpace.harmonic_is_realOfHolomorphic_univ : ∀ {f : ℂ → ℝ}, InnerProductSpace.HarmonicOnNhd f Set.univ → ∃ F, AnalyticOnNhd ℂ F Set.univ ∧ (fun z => (F z).re) = f
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- The line derivative in direction `m` of the inverse Fourier transform is given by the inverse
Fourier transform of the multiplication with `(2 * π * Complex.I) • (inner ℝ · m)`.  -/
SchwartzMap.lineDerivOp_fourierInv_eq : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  (f : SchwartzMap V E) (m : V),
  LineDeriv.lineDerivOp m (FourierTransformInv.fourierInv f) =
    FourierTransformInv.fourierInv ((2 * ↑Real.pi * Complex.I) • (SchwartzMap.smulLeftCLM E fun x => inner ℝ x m) f)
-- Mathlib.Analysis.Calculus.Deriv.Prod
hasDerivWithinAt_pi : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_1} {E' : ι → Type u_2}
  [inst_1 : (i : ι) → NormedAddCommGroup (E' i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E' i)] {φ : 𝕜 → (i : ι) → E' i}
  {φ' : (i : ι) → E' i}, HasDerivWithinAt φ φ' s x ↔ ∀ (i : ι), HasDerivWithinAt (fun x => φ x i) (φ' i) s x
-- Init.System.IO
/-- Creates a new task that waits for `t` to complete, runs the `EIO ε` action `f` on its result, and
then continues as the resulting task. This new task has priority `prio`.

Running the resulting `BaseIO` action causes this new task to be started eagerly. Unlike pure tasks
created by `Task.spawn`, tasks created by this function will run even if the last reference to the
task is dropped. The `act` should explicitly check for cancellation via `IO.checkCanceled` if it
should be terminated or otherwise react to the last reference being dropped. Because `EIO ε` actions
may throw an exception of type `ε`, the result of the task is an `Except ε α`.
 -/
EIO.bindTask : {α : Type u_1} →
  {ε β : Type} →
    Task α →
      (α → EIO ε (Task (Except ε β))) →
        optParam Task.Priority Task.Priority.default → optParam Bool false → BaseIO (Task (Except ε β))
-- Lean.Meta.Basic
Lean.Meta.instHashableDefEqCacheKey : Hashable Lean.Meta.DefEqCacheKey
-- Mathlib.Data.Finsupp.Basic
Finsupp.extendDomain_apply : ∀ {α : Type u_1} {M : Type u_12} [inst : Zero M] {P : α → Prop} [inst_1 : DecidablePred P] (f : Subtype P →₀ M) (a : α),
  f.extendDomain a = if h : P a then f ⟨a, h⟩ else 0
-- Init.Data.Array.Lemmas
Array.extract_size : ∀ {α : Type u_1} {xs : Array α}, xs.extract = xs
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.evaluation₃_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  CategoryTheory.Square.evaluation₃.map φ = φ.τ₃
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.instUniqueOfIsEmpty : {ι : Type u_2} →
  [inst : Preorder ι] →
    (G : ι → Type u_3) →
      [inst_1 : (i : ι) → AddCommMonoid (G i)] →
        (f : (i j : ι) → i ≤ j → G i →+ G j) →
          [inst_2 : DecidableEq ι] → [IsEmpty ι] → Unique (AddCommGroup.DirectLimit G f)
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
Algebra.Extension.tensorCotangentSpace_tmul_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S) (T : Type u_3) [inst_3 : CommRing T] [inst_4 : Algebra R T] (t : T) (s : S)
  (x : Ω[P.Ring⁄R]),
  (P.tensorCotangentSpace T) (t ⊗ₜ[R] (s ⊗ₜ[P.Ring] x)) =
    t ⊗ₜ[R] s ⊗ₜ[P.baseChange.Ring] (KaehlerDifferential.map R T P.Ring P.baseChange.Ring) x
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_symm_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  {H : Type u_8} [inst : AddCommGroup E] [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H]
  [inst_4 : NormedField 𝕜] [inst_5 : NormedField 𝕜₂] [inst_6 : NormedField 𝕜₃] [inst_7 : NormedField 𝕜₄]
  [inst_8 : Module 𝕜 E] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₃ G] [inst_11 : Module 𝕜₄ H]
  [inst_12 : TopologicalSpace E] [inst_13 : TopologicalSpace F] [inst_14 : TopologicalSpace G]
  [inst_15 : TopologicalSpace H] [inst_16 : IsTopologicalAddGroup G] [inst_17 : IsTopologicalAddGroup H]
  [inst_18 : ContinuousConstSMul 𝕜₃ G] [inst_19 : ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄}
  [inst_20 : RingHomInvPair σ₁₂ σ₂₁] [inst_21 : RingHomInvPair σ₂₁ σ₁₂] [inst_22 : RingHomInvPair σ₃₄ σ₄₃]
  [inst_23 : RingHomInvPair σ₄₃ σ₃₄] [inst_24 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [inst_25 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃]
  [inst_26 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_27 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [inst_28 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_29 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [inst_30 : RingHomIsometric σ₁₂]
  [inst_31 : RingHomIsometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : ⋯), ⋯
-- Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
CategoryTheory.MonoidalClosed.ihomUncurry_ihomCurry_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y z : C)
  [inst_2 : CategoryTheory.Closed x] [inst_3 : CategoryTheory.Closed y]
  [inst_4 : CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)] {Z : C} (h : y ⟹ x ⟹ z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.ihomUncurry x y z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.ihomCurry x y z) h) =
    h
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach.0.Std.IterM.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- Affine equivalences preserve affine independence of families of points.  -/
AffineEquiv.affineIndependent_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {p : ι → P} (e : P ≃ᵃ[k] P₂),
  AffineIndependent k (⇑e ∘ p) ↔ AffineIndependent k p
-- Mathlib.Algebra.Group.Pointwise.Finset.BigOperators
Finset.sum_neg_index : ∀ {α : Type u_1} {ι : Type u_2} [inst : AddCommMonoid α] [inst_1 : DecidableEq ι] [inst_2 : InvolutiveNeg ι]
  (s : Finset ι) (f : ι → α), ∑ i ∈ -s, f i = ∑ i ∈ s, f (-i)
-- Mathlib.Geometry.Manifold.HasGroupoid
StructureGroupoid.maximalAtlas_mono : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G G' : StructureGroupoid H}, G ≤ G' → StructureGroupoid.maximalAtlas M G ⊆ StructureGroupoid.maximalAtlas M G'
-- Lean.Data.Lsp.CodeActions
/-- Whether the code action supports the `isPreferred` property.  -/
Lean.Lsp.CodeActionClientCapabilities.isPreferredSupport? : Lean.Lsp.CodeActionClientCapabilities → Option Bool
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- When its possible to compare the two, the composition of two `IsStronglyCocartesian.map` will
also be given by a `IsStronglyCocartesian.map`. In other words, given diagrams
```
a --φ--> b        b'         b''
|        |        |          |
v        v        v          v
R --f--> S --g--> S' --g'--> S'
```
and
```
a --φ'--> b'
|         |
v         v
R --f'--> S'

```
and
```
a --φ''--> b''
|          |
v          v
R --f''--> S''
```
such that `φ` and `φ'` are strongly co-Cartesian morphisms, and such that `f' = f ≫ g` and
`f'' = f' ≫ g'`. Then composing the induced map from `b ⟶ b'` with the induced map from
`b' ⟶ b''` gives the induced map from `b ⟶ b''`.  -/
CategoryTheory.Functor.IsStronglyCocartesian.map_comp_map : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCocartesian f φ]
  {S' S'' : 𝒮} {b' b'' : 𝒳} {f' : R ⟶ S'} {f'' : R ⟶ S''} {g : S ⟶ S'} {g' : S' ⟶ S''}
  (H : f' = CategoryTheory.CategoryStruct.comp f g) (H' : f'' = CategoryTheory.CategoryStruct.comp f' g') (φ' : a ⟶ b')
  (φ'' : a ⟶ b'') [inst_3 : p.IsStronglyCocartesian f' φ'] [inst_4 : p.IsHomLift f'' φ''],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCocartesian.map p f φ H φ')
      (CategoryTheory.Functor.IsStronglyCocartesian.map p f' φ' H' φ'') =
    CategoryTheory.Functor.IsStronglyCocartesian.map p f φ ⋯ φ''
-- Mathlib.CategoryTheory.Grothendieck
/-- The Grothendieck construction as a functor from the functor category `E ⥤ Cat` to the
over category `Over E`.  -/
CategoryTheory.Grothendieck.functor : {E : CategoryTheory.Cat} →
  CategoryTheory.Functor (CategoryTheory.Functor (↑E) CategoryTheory.Cat) (CategoryTheory.Over E)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Do not use this. Use `_root_.mul_lt_mul_of_pos_left` instead.  -/
PosMulStrictMono.mul_lt_mul_of_pos_left : ∀ {α : Type u_1} {inst : Mul α} {inst_1 : Zero α} {inst_2 : Preorder α} [self : PosMulStrictMono α] ⦃a : α⦄,
  0 < a → ∀ ⦃b c : α⦄, b < c → a * b < a * c
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map : ∀ {Ω : Type u_7} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {M : Type u_10} [inst : Monoid M]
  [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] [MeasureTheory.IsFiniteMeasure μ] {f g : Ω → M},
  Measurable f →
    Measurable g →
      ProbabilityTheory.IndepFun f g μ →
        MeasureTheory.Measure.map (f * g) μ = (MeasureTheory.Measure.map f μ).mconv (MeasureTheory.Measure.map g μ)
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapIsometry_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f : X ≃ᵢ Y),
  (Delone.DeloneSet.mapIsometry f).symm = Delone.DeloneSet.mapIsometry f.symm
-- Mathlib.RepresentationTheory.Intertwining
/-- The intertwining map underlying an equivalence of representations.  -/
Representation.Equiv.toIntertwiningMap : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    {ρ : Representation A G V} → {σ : Representation A G W} → ρ.Equiv σ → ρ.IntertwiningMap σ
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- The product of two non-unital subalgebras is a non-unital subalgebra.  -/
NonUnitalSubalgebra.prod : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : Module R A] →
            NonUnitalSubalgebra R A →
              [inst_3 : NonUnitalNonAssocSemiring B] →
                [inst_4 : Module R B] → NonUnitalSubalgebra R B → NonUnitalSubalgebra R (A × B)