mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.aux4 : ∀ {n a b c : ℕ}, a < b * c → c ≤ n → a < b * n
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.closure_le_centralizer_centralizer : ∀ {M : Type u_1} [inst : Monoid M] (s : Set M), Submonoid.closure s ≤ Submonoid.centralizer ↑(Submonoid.centralizer s)
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
IsLocalRing.map_ringEquiv_maximalIdeal : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsLocalRing R]
  [inst_3 : IsLocalRing S] (e : R ≃+* S), Ideal.map e (IsLocalRing.maximalIdeal R) = IsLocalRing.maximalIdeal S
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.liftHomology.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} [inst_2 : S.HasHomology] (k k_1 : A ⟶ S.opcycles) (e_k : k = k_1)
  (hk : CategoryTheory.CategoryStruct.comp k S.fromOpcycles = 0), S.liftHomology k hk = S.liftHomology k_1 ⋯
-- Mathlib.RingTheory.Jacobson.Radical
Ring.map_jacobson_le : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Ring R] [inst_1 : Ring R₂] (f : R →+* R₂) [inst_2 : RingHomSurjective f],
  Submodule.map f.toSemilinearMap (Ring.jacobson R) ≤ Ring.jacobson R₂
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegal.spineToSimplex_edge : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path n) (j l : ℕ) (hjl : j + l ≤ n),
  (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.intervalEdge j l hjl).op)) (sx.spineToSimplex f) =
    sx.spineToDiagonal (f.interval j l hjl)
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A]
  {X W : CategoryTheory.Sheaf J A} (f : W ⟶ X),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.obj f.hom
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.Plus.instAdditiveSingleFunctor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (n : ℤ), (HomotopyCategory.Plus.singleFunctor C n).Additive
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Power.denote.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | k => h_3 k) =
    h_2 ()
-- Mathlib.Algebra.Homology.QuasiIso
quasiIsoAt_iff_comp_left : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L)
  (φ' : L ⟶ M) (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : M.HasHomology i]
  [hφ : QuasiIsoAt φ i], QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i ↔ QuasiIsoAt φ' i
-- Mathlib.Algebra.Group.End
/-- Isomorphic groups have isomorphic automorphism groups.  -/
MulAut.congr : {G : Type u_3} → [inst : Group G] → {H : Type u_7} → [inst_1 : Group H] → G ≃* H → MulAut G ≃* MulAut H
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.nondegenerate_toLinearMap₂'_of_det_ne_zero' : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] [IsDomain R]
  {M : Matrix n n R}, M.det ≠ 0 → ((Matrix.toLinearMap₂' R) M).Nondegenerate
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_of_isEmpty : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a fallback : α}, m.isEmpty = true → m.getD a fallback = fallback
-- Mathlib.Algebra.Group.Hom.Defs
/-- The proposition that the function preserves 0  -/
ZeroHom.map_zero' : ∀ {M : Type u_10} {N : Type u_11} [inst : Zero M] [inst_1 : Zero N] (self : ZeroHom M N), self.toFun 0 = 0
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenLowerSections.union : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f g : α → Set β},
  HasOpenLowerSections f → HasOpenLowerSections g → HasOpenLowerSections fun x => f x ∪ g x
-- Mathlib.Topology.Order.NhdsSet
Icc_mem_nhdsSet_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c d : α},
  a < b → c ≤ d → Set.Icc a d ∈ nhdsSet (Set.Ico b c)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.restrictFunctor_map_left : ∀ (X : AlgebraicGeometry.Scheme) {U V : X.Opens} (i : U ⟶ V), (X.restrictFunctor.map i).left = X.homOfLE ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.instIsDomain : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [IsDomain R], IsDomain W'.CoordinateRing
-- Mathlib.Analysis.Convex.Segment
Prod.image_mk_segment_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] (x₁ x₂ : E) (y : F),
  (fun x => (x, y)) '' segment 𝕜 x₁ x₂ = segment 𝕜 (x₁, y) (x₂, y)
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.oneCochainOfTwoSplitting.congr_simp : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] (E : LieAlgebra.Extension R M L) {s₁ s₁_1 : L →ₗ[R] E.L}
  (e_s₁ : s₁ = s₁_1) {s₂ s₂_1 : L →ₗ[R] E.L} (e_s₂ : s₂ = s₂_1) (hs₁ : Function.LeftInverse ⇑E.proj ⇑s₁)
  (hs₂ : Function.LeftInverse ⇑E.proj ⇑s₂), E.oneCochainOfTwoSplitting hs₁ hs₂ = E.oneCochainOfTwoSplitting ⋯ ⋯
-- Aesop.Tree.Data
Aesop.Rapp.subgoals : {m : Type → Type} → [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → Aesop.Rapp → m (Array Aesop.GoalRef)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- Embed a non-zero element of a `GroupWithZero` into the unit group.
By combining this function with the operations on units,
or the `/ₚ` operation, it is possible to write a division
as a partial function with three arguments.  -/
Units.mk0 : {G₀ : Type u_3} → [inst : GroupWithZero G₀] → (a : G₀) → a ≠ 0 → G₀ˣ
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalListExpr : {α : Type} → (Lean.Expr → Lean.MetaM α) → Lean.Expr → optParam Bool false → Lean.MetaM (List α)
-- Std.Sync.Channel
/-- Try to receive a value from the channel, if this can be completed right away without blocking return
`some value`, otherwise return `none`.
 -/
Std.Channel.Sync.tryRecv : {α : Type} → Std.Channel.Sync α → BaseIO (Option α)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.ι_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (c : C)
  {X Y : ↑(F.obj c)} (f : X ⟶ Y),
  (CategoryTheory.Grothendieck.ι F c).map f =
    { base := CategoryTheory.CategoryStruct.id { base := c, fiber := X }.base,
      fiber := CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f }
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k fallback : α},
  (Std.ExtTreeMap.filter f t).getKeyD k fallback = ((t.getKey? k).pfilter fun x h' => f x t[x]).getD fallback
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pos.skipWhile.eq_1 : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  pos.skipWhile pat =
    match pos.skip? pat with
    | some nextCurr => if pos < nextCurr then nextCurr.skipWhile pat else pos
    | none => pos
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.id_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  (A : CategoryTheory.Endofunctor.Algebra F),
  (CategoryTheory.CategoryStruct.id A).f = CategoryTheory.CategoryStruct.id A.a
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure.below.of_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)]
  {motive : (a : C) → P.colimitsClosure J a → Prop} (X : C) (hX : P X),
  CategoryTheory.ObjectProperty.colimitsClosure.below ⋯
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.setNextDeclToEnd : Lean.Meta.Grind.GoalM Unit
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_of_not_sub_sigma_measurable : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) (P : MeasureTheory.Measure Ω)
  [hσ : MeasureTheory.SigmaFinite (P.trim hm)] {X : Ω → ENNReal},
  ¬Measurable X → P⁻[X | mΩ] = ((P.withDensity X).trim hm).rnDeriv (P.trim hm)
-- Init.Data.List.Range
List.head_range : ∀ {n : ℕ} (h : List.range n ≠ []), (List.range n).head h = 0
-- Lean.Elab.App
/-- Create an implicit argument using the given `BinderInfo`.  -/
Lean.Elab.Term.ElabElim.mkImplicitArg : Lean.Expr → Lean.BinderInfo → Lean.Elab.Term.ElabElim.M Lean.Expr
-- Batteries.Recycling.RBTree.Basic
/-- The core of the `insert` function. This adds an element `x` to a balanced red-black tree.
Importantly, the result of calling `ins` is not a proper red-black tree,
because it has a broken balance invariant.
(See `Balanced.ins` for the balance invariant of `ins`.)
The `insert` function does the final fixup needed to restore the invariant.
 -/
RBTree.RBNode.ins : {α : Type u_1} → (α → α → Ordering) → α → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `add_tsub_cancel_right` for the equality if `AddLeftReflectLE α`.  -/
add_tsub_le_right : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [OrderedSub α] {a b : α}, a + b - b ≤ a
-- Mathlib.Logic.Equiv.Fintype
/-- Given two injective functions `f` and `g` from a finite type `α` to any type `β`,
there exists a permutation of `β` that maps `f` to `g`.  -/
Equiv.Perm.exists_extending_pair : ∀ {α : Type u_1} {β : Type u_2} [Finite α] (f g : α → β),
  Function.Injective f → Function.Injective g → ∃ σ, ∀ (a : α), σ (f a) = g a
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.dual_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : BoundedOrder α] [inst_2 : Lattice β]
  [inst_3 : BoundedOrder β] (f : BoundedLatticeHom α β) (a : α), (BoundedLatticeHom.dual f) a = f a
-- Mathlib.LinearAlgebra.Lagrange
Polynomial.exists_eval_eq_iff : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_3} [Finite ι] (x y : ι → F),
  (∃ q, ∀ (i : ι), Polynomial.eval (x i) q = y i) ↔ ∀ (i j : ι), x i = x j → y i = y j
-- Mathlib.GroupTheory.Rank
AddSubgroup.rank_closure_finset_le_card : ∀ {G : Type u_1} [inst : AddGroup G] (s : Finset G), AddGroup.rank ↥(AddSubgroup.closure ↑s) ≤ s.card
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} {fallback : β k}, k ∈ m₂ → (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Topology.Maps.Proper.Basic
/-- A binary product of proper maps is proper.  -/
IsProperMap.prodMap : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {W : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : X → Y} {g : Z → W},
  IsProperMap f → IsProperMap g → IsProperMap (Prod.map f g)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.ext_iff : ∀ {n d : ℕ} {x y : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := d })},
  x = y ↔ ∀ (i : Fin (d + 1)), x i = y i
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.insertMin.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Sort u_3)
  (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (h_1 : (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hr)
  (h_2 :
    (sz : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) →
              motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr),
  (match Std.DTreeMap.Internal.Impl.leaf, hr with
    | Std.DTreeMap.Internal.Impl.leaf, hr => h_1 hr
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hr => h_2 sz k' v' l' r' hr) =
    h_1 hr
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_sub_Iio : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => a - x) ⁻¹' Set.Iio b = Set.Ioi (a - b)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.instToSnapshotTreeTacticParsedSnapshot : Lean.Language.ToSnapshotTree Lean.Elab.Tactic.TacticParsedSnapshot
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.denoteTerm.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ) (m : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.denoteTerm ctx k m =
    bif k == 1 then Lean.Grind.CommRing.Mon.denote' ctx m else k • Lean.Grind.CommRing.Mon.denote' ctx m
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
/-- The underlying continuous function of `Proj ℬ ⟶ Proj 𝒜` on the level of points.  -/
AlgebraicGeometry.ProjectiveSpectrum.comap : {A : Type u_1} →
  {B : Type u_2} →
    {σ : Type u_4} →
      {τ : Type u_5} →
        [inst : CommRing A] →
          [inst_1 : SetLike σ A] →
            [inst_2 : AddSubgroupClass σ A] →
              [inst_3 : CommRing B] →
                [inst_4 : SetLike τ B] →
                  [inst_5 : AddSubgroupClass τ B] →
                    {𝒜 : ℕ → σ} →
                      {ℬ : ℕ → τ} →
                        [inst_6 : GradedRing 𝒜] →
                          [inst_7 : GradedRing ℬ] →
                            (f : 𝒜 →+*ᵍ ℬ) →
                              HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜) →
                                C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)
-- Mathlib.FieldTheory.IsPerfectClosure
/-- The absolute perfect closure `PerfectClosure` is a `p`-radical extension over the base ring.
In particular, it is a perfect closure of the base ring, that is,
`IsPerfectClosure (PerfectClosure.of K p) p`.  -/
PerfectClosure.isPRadical : ∀ (K : Type u_1) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p],
  IsPRadical (PerfectClosure.of K p) p
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.BimonObj.mul_comul_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (M : C) [self : CategoryTheory.BimonObj M] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M M ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.ComonObj.comul)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul) h))
-- Mathlib.Order.Filter.Defs
/-- The filter is nontrivial: `f ≠ ⊥` or equivalently, `∅ ∉ f`.  -/
Filter.NeBot.ne' : ∀ {α : Type u_1} {f : Filter α} [self : f.NeBot], f ≠ ⊥
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsMulIndecomposable.baseOf_subset_one_lt : ∀ {ι : Type u_1} {M : Type u_2} {S : Type u_4} [inst : Monoid M] [inst_1 : LinearOrder S] [inst_2 : Monoid S]
  (v : ι → M) (f : M →* S), IsMulIndecomposable.baseOf v f ⊆ {i | 1 < f (v i)}
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- An equivalence `F` induces an equivalence `StructuredArrow X F ≌ Under X`.  -/
CategoryTheory.StructuredArrow.isEquivalence_toUnder : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor D T) [F.IsEquivalence], (CategoryTheory.StructuredArrow.toUnder X F).IsEquivalence
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_whiskerLeft : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [inst_6 : CategoryTheory.Category.{v₇, u₇} A₂]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} B₂] [inst_8 : CategoryTheory.Category.{v₉, u₉} C₂]
  {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₇)
  [inst_9 : CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  {φ φ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂} (α : φ ⟶ φ'),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ α) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ φ).hom
      (CategoryTheory.CategoryStruct.comp
        (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).whiskerLeft
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map α))
        (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ φ').inv)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.smul_apply : ∀ {R : Type u_1} {A : Type u_2} {ι : Type u_3} {E : ι → Type u_4} [inst : (i : ι) → SMul R (E i)] (c : R)
  (x : WithCStarModule A ((i : ι) → E i)) (i : ι), (c • x) i = c • x i
-- Mathlib.Algebra.WithConv
WithConv.symm_equiv_apply : ∀ {A : Type u_2} (x : A), (WithConv.equiv A).symm x = WithConv.toConv x
-- Mathlib.Algebra.Notation.Lemmas
ite_lt_one : ∀ {α : Type u_1} [inst : One α] {p : Prop} [inst_1 : Decidable p] {a b : α} [inst_2 : LT α],
  a < 1 → b < 1 → (if p then a else b) < 1
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Pretrivialization.continuousLinearMapCoordChange_apply : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] (e₁ e₁' : Bundle.Trivialization F₁ Bundle.TotalSpace.proj)
  (e₂ e₂' : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) [inst_13 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_14 : FiberBundle F₁ E₁] [inst_15 : (x : B) → TopologicalSpace (E₂ x)] [inst_16 : FiberBundle F₂ E₂]
  [inst_17 : Bundle.Trivialization.IsLinear 𝕜₁ e₁] [inst_18 : Bundle.Trivialization.IsLinear 𝕜₁ e₁']
  [inst_19 : Bundle.Trivialization.IsLinear 𝕜₂ e₂] [inst_20 : Bundle.Trivialization.IsLinear 𝕜₂ e₂'],
  ∀ b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet),
    ∀ (L : F₁ →SL[σ] F₂),
      (Bundle.Pretrivialization.continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂' b) L =
        (↑(Bundle.Pretrivialization.continuousLinearMap σ e₁' e₂')
            ⟨b, (Bundle.Pretrivialization.continuousLinearMap σ e₁ e₂).symm b L⟩).2
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.toList_roo : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.toList_roo._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap.Raw α β cmp},
  t.WF →
    ∀ {lowerBound upperBound : α},
      Std.Slice.toList (Std.Roo.Sliceable.mkSlice t lowerBound<...upperBound) =
        List.filter (fun e => decide ((cmp e.1 lowerBound).isGT = true ∧ (cmp e.1 upperBound).isLT = true)) t.toList
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.restrict_iInf_restrict : ∀ {α : Type u_1} {ι : Sort u_2} (s : Set α) (m : ι → MeasureTheory.OuterMeasure α),
  (MeasureTheory.OuterMeasure.restrict s) (⨅ i, (MeasureTheory.OuterMeasure.restrict s) (m i)) =
    (MeasureTheory.OuterMeasure.restrict s) (⨅ i, m i)
-- Init.Data.Array.Lemmas
Array.swapIfInBounds_def : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ},
  xs.swapIfInBounds i j = if h₁ : i < xs.size then if h₂ : j < xs.size then xs.swap i j h₁ h₂ else xs else xs
-- Mathlib.CategoryTheory.Sites.Spaces
/-- The Grothendieck topology associated to a topological space.  -/
Opens.grothendieckTopology : (T : Type u) → [inst : TopologicalSpace T] → CategoryTheory.GrothendieckTopology (TopologicalSpace.Opens T)
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.aestronglyMeasurable : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν → MeasureTheory.AEStronglyMeasurable X (ν.bind ⇑κ)
-- Mathlib.Analysis.Normed.Unbundled.InvariantExtension
/-- The algebra norm `invariantExtension` extends the norm on `K`.  -/
IsUltrametricDist.invariantExtension_extends : ∀ (K : Type u_1) [inst : NormedField K] (L : Type u_2) [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (x : K),
  (IsUltrametricDist.invariantExtension K L) ((algebraMap K L) x) = ‖x‖
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.instPreservesEffectiveEpisOfIsRegularEpiCategoryOfPreservesEpimorphismsOfHasPullbacks : ∀ {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.IsRegularEpiCategory D]
  (F : CategoryTheory.Functor C D) [F.PreservesEpimorphisms] [CategoryTheory.Limits.HasPullbacks D],
  F.PreservesEffectiveEpis
-- Mathlib.Tactic.Linarith.Datatypes
/-- `l.get n` returns the value in `l` associated with key `n`, if it exists, and `none` otherwise.
This function assumes that `l` is sorted in decreasing order of the first argument,
that is, it will return `none` as soon as it finds a key smaller than `n`.
 -/
Mathlib.Tactic.Linarith.Linexp.get : ℕ → Mathlib.Tactic.Linarith.Linexp → Option ℤ
-- Mathlib.Data.Matrix.Basic
Matrix.proj_comp_diagLinearMap : ∀ {m : Type u_2} {R : Type u_7} {α : Type u_11} [inst : Semiring R] [inst_1 : AddCommMonoid α] [inst_2 : Module R α]
  (i : m), LinearMap.proj i ∘ₗ Matrix.diagLinearMap m R α = Matrix.entryLinearMap R α i i
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α (β × γ)} [h : ProbabilityTheory.IsFiniteKernel κ.snd],
  ProbabilityTheory.IsFiniteKernel κ