mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- `ContinuousLinearMap.prod` as a `LinearEquiv`.

See `ContinuousLinearMap.prodL` for the `ContinuousLinearEquiv` version.  -/
ContinuousLinearMap.prodₗ : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommMonoid M] →
          [inst_3 : Module R M] →
            {M₂ : Type u_3} →
              [inst_4 : TopologicalSpace M₂] →
                [inst_5 : AddCommMonoid M₂] →
                  [inst_6 : Module R M₂] →
                    {M₃ : Type u_4} →
                      [inst_7 : TopologicalSpace M₃] →
                        [inst_8 : AddCommMonoid M₃] →
                          [inst_9 : Module R M₃] →
                            (S : Type u_5) →
                              [inst_10 : Semiring S] →
                                [inst_11 : Module S M₂] →
                                  [inst_12 : ContinuousAdd M₂] →
                                    [inst_13 : SMulCommClass R S M₂] →
                                      [inst_14 : ContinuousConstSMul S M₂] →
                                        [inst_15 : Module S M₃] →
                                          [inst_16 : ContinuousAdd M₃] →
                                            [inst_17 : SMulCommClass R S M₃] →
                                              [inst_18 : ContinuousConstSMul S M₃] →
                                                ((M →L[R] M₂) × (M →L[R] M₃)) ≃ₗ[S] M →L[R] M₂ × M₃
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticSequence.smul : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R}, IsEllipticSequence W → ∀ (x : R), IsEllipticSequence (x • W)
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], Cardinal.toNat (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.coe_ofClass : ∀ {S : Type u_1} {R : Type u_2} [inst : NonAssocSemiring R] [inst_1 : SetLike S R] [inst_2 : StarRing R]
  [inst_3 : SubsemiringClass S R] [inst_4 : StarMemClass S R] (s : S), ↑(StarSubsemiring.ofClass s) = ↑s
-- Mathlib.MeasureTheory.Function.L2Space
/-- For continuous functions `f`, `g` on a compact, finite-measure topological space `α`, the L^2
inner product is the integral of their pointwise inner product.  -/
MeasureTheory.ContinuousMap.inner_toLp : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
  [inst_3 : RCLike 𝕜] (μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.IsFiniteMeasure μ] [inst_5 : CompactSpace α]
  (f g : C(α, 𝕜)),
  inner 𝕜 ((ContinuousMap.toLp 2 μ 𝕜) f) ((ContinuousMap.toLp 2 μ 𝕜) g) = ∫ (x : α), g x * (starRingEnd 𝕜) (f x) ∂μ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_inter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k}, (m₁ ∩ m₂).getD k fallback = if k ∈ m₂ then m₁.getD k fallback else fallback
-- Mathlib.LinearAlgebra.Alternating.DomCoprod
/-- Like `MultilinearMap.domCoprod`, but ensures the result is also alternating.

Note that this is usually defined (for instance, as used in Proposition 22.24 in [Gallier2011Notes])
over integer indices `ιa = Fin n` and `ιb = Fin m`, as
$$
(f \wedge g)(u_1, \ldots, u_{m+n}) =
  \sum_{\operatorname{shuffle}(m, n)} \operatorname{sign}(\sigma)
    f(u_{\sigma(1)}, \ldots, u_{\sigma(m)}) g(u_{\sigma(m+1)}, \ldots, u_{\sigma(m+n)}),
$$
where $\operatorname{shuffle}(m, n)$ consists of all permutations of $[1, m+n]$ such that
$\sigma(1) < \cdots < \sigma(m)$ and $\sigma(m+1) < \cdots < \sigma(m+n)$.

Here, we generalize this by replacing:
* the product in the sum with a tensor product
* the filtering of $[1, m+n]$ to shuffles with an isomorphic quotient
* the additions in the subscripts of $\sigma$ with an index of type `Sum`

The specialized version can be obtained by combining this definition with `finSumFinEquiv` and
`LinearMap.mul'`.
 -/
AlternatingMap.domCoprod : {ιa : Type u_1} →
  {ιb : Type u_2} →
    [Fintype ιa] →
      [Fintype ιb] →
        {R' : Type u_3} →
          {Mᵢ : Type u_4} →
            {N₁ : Type u_5} →
              {N₂ : Type u_6} →
                [inst : CommSemiring R'] →
                  [inst_1 : AddCommGroup N₁] →
                    [inst_2 : Module R' N₁] →
                      [inst_3 : AddCommGroup N₂] →
                        [inst_4 : Module R' N₂] →
                          [inst_5 : AddCommMonoid Mᵢ] →
                            [inst_6 : Module R' Mᵢ] →
                              [DecidableEq ιa] →
                                [DecidableEq ιb] →
                                  Mᵢ [⋀^ιa]→ₗ[R'] N₁ → Mᵢ [⋀^ιb]→ₗ[R'] N₂ → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] TensorProduct R' N₁ N₂
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.point_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {X Y :
    CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C)
      (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))}
  (f : X ⟶ Y), CategoryTheory.CosimplicialObject.Augmented.point.map f = f.left
-- Mathlib.Data.List.Induction
List.twoStepInduction_nil : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (x : α) → motive [x])
  (cons_cons : (x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs)),
  List.twoStepInduction nil singleton cons_cons [] = nil
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.sub : ∀ {M₁ : Type u_3} {M₄ : Type u_5} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁]
  [inst_2 : TopologicalSpace M₄] [inst_3 : AddCommGroup M₄] [IsTopologicalAddGroup M₄] {f g : M₁ → M₄},
  IsCompactOperator f → IsCompactOperator g → IsCompactOperator (f - g)
-- Init.Prelude
Nat.brecOn.go : {motive : ℕ → Sort u} → (t : ℕ) → ((t : ℕ) → Nat.below t → motive t) → motive t ×' Nat.below t
-- Mathlib.RepresentationTheory.Intertwining
Representation.TensorProduct.comm_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring 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) (v : V) (w : W),
  (Representation.TensorProduct.comm ρ σ) (v ⊗ₜ[A] w) = w ⊗ₜ[A] v
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.toPushforwardOfIso_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H₁ : X ≅ Y) {ℱ : TopCat.Presheaf C X}
  {𝒢 : TopCat.Presheaf C Y} (H₂ : (TopCat.Presheaf.pushforward C H₁.hom).obj ℱ ⟶ 𝒢) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (TopCat.Presheaf.toPushforwardOfIso H₁ H₂).app U =
    CategoryTheory.CategoryStruct.comp (ℱ.map (CategoryTheory.eqToHom ⋯))
      (H₂.app (Opposite.op ((TopologicalSpace.Opens.map H₁.inv).obj (Opposite.unop U))))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.foldlM_eq_foldlM_toList : ∀ {α : Type u} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldlM f init t =
    List.foldlM (fun a b => f a b.1 b.2) init (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain_single : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α → β) (a : α) (m : M)
  (hif : Set.InjOn f (f ⁻¹' ↑(fun₀ | f a => m).support)), Finsupp.comapDomain f (fun₀ | f a => m) hif = fun₀ | a => m
-- Mathlib.Data.Finsupp.Single
Finsupp.update_self : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α), f.update a (f a) = f
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.exists_eq_spanSingleton_mul : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [IsDomain R₁] (I : FractionalIdeal (nonZeroDivisors R₁) K),
  ∃ a aI, a ≠ 0 ∧ I = FractionalIdeal.spanSingleton (nonZeroDivisors R₁) ((algebraMap R₁ K) a)⁻¹ * ↑aI
-- Init.Omega.Int
Lean.Omega.Int.ofNat_sub_sub : ∀ {a b c : ℕ}, ↑(a - b - c) = ↑(a - (b + c))
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.instInhabited : {M : Type u_1} →
  [inst : AddCommGroup M] → [inst_1 : LinearOrder M] → [inst_2 : IsOrderedAddMonoid M] → Inhabited (ArchimedeanClass M)
-- Mathlib.Order.LatticeIntervals
Set.Ico.coe_inf : ∀ {α : Type u_1} [inst : SemilatticeInf α] {a b : α} {x y : ↑(Set.Ico a b)}, ↑(x ⊓ y) = ↑x ⊓ ↑y
-- Mathlib.Lean.Meta.CongrTheorems
_private.Mathlib.Lean.Meta.CongrTheorems.0.Lean.Meta.mkRichHCongr.doubleTelescope.loop : {α : Type} →
  ℕ →
    Array Bool →
      (Array Lean.Expr → Array Lean.Expr → Array Bool → Lean.MetaM α) →
        ℕ → Lean.Expr → Lean.Expr → Array Lean.Expr → Array Lean.Expr → Array Bool → Lean.MetaM α
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Scheme.toSpecΓ_apply : ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X),
  X.toSpecΓ x = (AlgebraicGeometry.Spec.map (X.presheaf.Γgerm x)) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.index_elim : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {K V : Set G},
  IsCompact K →
    (interior V).Nonempty → ∃ t, K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V ∧ t.card = MeasureTheory.Measure.haar.index K V
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_filterMap : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.DHashMap.filterMap f m).getKey? k = (m.getKey? k).pfilter fun x_2 h' => (f x_2 (m.get x_2 ⋯)).isSome
-- Mathlib.LinearAlgebra.AffineSpace.Independent
AffineIndependent.injective_affineSpan_image : ∀ {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} [Nontrivial k] {p : ι → P},
  AffineIndependent k p → Function.Injective fun s => affineSpan k (p '' s)
-- Mathlib.Order.SuccPred.Basic
Order.Ioo_succ_right_eq_insert_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  a < b → ¬IsMax b → Set.Ioo a (Order.succ b) = insert b (Set.Ioo a b)
-- Mathlib.Topology.Subpath
/-- The subpath of `γ` from `0` to `1` is just `γ`, with a slightly different type.  -/
Path.subpath_zero_one : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b), γ.subpath 0 1 = γ.cast ⋯ ⋯
-- Mathlib.Algebra.Order.Field.Basic
mul_le_mul_of_mul_div_le : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b c d : α},
  a * (b / c) ≤ d → 0 < c → b * a ≤ d * c
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- A reproducing kernel Hilbert space is a Hilbert space with an
injection to functions mapping into another Hilbert space, such that point evaluation is continuous.
 -/
RKHS : (𝕜 : outParam (Type u_1)) →
  (H : Type u_2) →
    outParam (Type u_3) →
      (V : outParam (Type u_4)) →
        [inst : RCLike 𝕜] →
          [inst_1 : NormedAddCommGroup V] →
            [InnerProductSpace 𝕜 V] →
              [inst_3 : NormedAddCommGroup H] → [InnerProductSpace 𝕜 H] → Type (max (max u_2 u_3) u_4)
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.GCommMonoid.toGMonoid : {ι : Type u_1} →
  {A : ι → Type u_2} → {inst : AddCommMonoid ι} → [self : GradedMonoid.GCommMonoid A] → GradedMonoid.GMonoid A
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulMono.toPosMulReflectLT : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : LinearOrder α] [PosMulMono α], PosMulReflectLT α
-- Mathlib.LinearAlgebra.Projectivization.Basic
/-- Construct an element of the projectivization from a subspace of dimension 1.  -/
Projectivization.mk'' : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → (H : Submodule K V) → Module.finrank K ↥H = 1 → Projectivization K V
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_comp_inl : ∀ {R : Type u} (M : Type v) [inst : Zero M], TrivSqZeroExt.snd ∘ TrivSqZeroExt.inl = 0
-- Mathlib.Data.PFunctor.Multivariate.M
TypeVec.appendFun.eq_1 : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} (f : α.Arrow α') (g : β → β'),
  (f ::: g) = TypeVec.splitFun f g
-- Mathlib.GroupTheory.Finiteness
/-- A finitely generated monoid has a minimal generating set.  -/
Submonoid.exists_minimal_closure_eq_top : ∀ (M : Type u_1) [inst : Monoid M] [Monoid.FG M], ∃ S, Minimal (fun S => Submonoid.closure ↑S = ⊤) S
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonDocumentSymbolParams : Lean.FromJson Lean.Lsp.DocumentSymbolParams
-- Mathlib.GroupTheory.OrderOfElement
orderOf_eq_card_powers : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] [inst_1 : Fintype G] {x : G},
  orderOf x = Fintype.card ↥(Submonoid.powers x)
-- Mathlib.Topology.Algebra.Group.Basic
map_add_right_nhds : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (x y : G),
  Filter.map (fun x_1 => x_1 + x) (nhds y) = nhds (y + x)
-- Init.Data.Fin.Basic
/-- Multiplication modulo `n`, usually invoked via the `*` operator.

Examples:
* `(2 : Fin 10) * (2 : Fin 10) = (4 : Fin 10)`
* `(2 : Fin 10) * (7 : Fin 10) = (4 : Fin 10)`
* `(3 : Fin 10) * (7 : Fin 10) = (1 : Fin 10)`
 -/
Fin.mul : {n : ℕ} → Fin n → Fin n → Fin n
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.map_sup : ∀ {F : Type u_1} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] [inst_7 : IsScalarTower R A A] [inst_8 : SMulCommClass R A A]
  [inst_9 : IsScalarTower R B B] [inst_10 : SMulCommClass R B B] (f : F) (S T : NonUnitalSubalgebra R A),
  NonUnitalSubalgebra.map f (S ⊔ T) = NonUnitalSubalgebra.map f S ⊔ NonUnitalSubalgebra.map f T
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.refl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {F : Set X}, x ∈ F → JoinedIn F x x
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.lt_def : ∀ {α : Type u_1} [inst : LT α] {x y : WithZero α}, x < y ↔ (x = 0 ∧ ∃ b, y = ↑b) ∨ ∃ a b, a < b ∧ x = ↑a ∧ y = ↑b
-- Mathlib.Algebra.Group.Basic
rightInverse_neg : ∀ (G : Type u_3) [inst : InvolutiveNeg G], Function.RightInverse (fun a => -a) fun a => -a
-- Mathlib.Topology.Homotopy.HomotopyGroup
instInhabitedHomotopyGroup : {N : Type u_1} → {X : Type u_2} → [inst : TopologicalSpace X] → {x : X} → Inhabited (HomotopyGroup N X x)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.toAlgHom_id : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), (Algebra.Extension.Hom.id P).toAlgHom = AlgHom.id R P.Ring
-- Mathlib.RingTheory.Congruence.Basic
RingCon.comap_injective : ∀ {R : Type u_3} {R' : Type u_4} [inst : Add R] [inst_1 : Mul R] [inst_2 : Add R'] [inst_3 : Mul R'] {F : Type u_5}
  [inst_4 : FunLike F R' R] [inst_5 : MulHomClass F R' R] [inst_6 : AddHomClass F R' R] (f : F),
  Function.Surjective ⇑f → Function.Injective fun x => x.comap f
-- Init.Data.Dyadic.Basic
Dyadic.precision.eq_2 : ∀ (n k : ℤ) (hn : n % 2 = 1), (Dyadic.ofOdd n k hn).precision = some k
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.instInhabitedHoleIterator.default : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator
-- Mathlib.Algebra.Category.Grp.EpiMono
AddMonoidHom.ker_eq_bot_of_cancel : ∀ {A : Type u} {B : Type v} [inst : AddGroup A] [inst_1 : AddGroup B] {f : A →+ B},
  (∀ (u v : ↥f.ker →+ A), f.comp u = f.comp v → u = v) → f.ker = ⊥
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.instModuleOfIsScalarTower : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      (I : Ideal R) →
        (M : Type u_4) →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : Semiring S] →
                [inst_4 : SMul S R] → [inst_5 : Module S M] → [IsScalarTower S R M] → Module S (AdicCompletion I M)
-- Init.Data.BitVec.Lemmas
BitVec.eq_of_getLsbD_eq_iff : ∀ {w : ℕ} {x y : BitVec w}, x = y ↔ ∀ i < w, x.getLsbD i = y.getLsbD i
-- Init.While
/-- Pinning predicate for `repeatM.impl`: trivial unless `repeatM.body f` has a fixed point,
in which case `r` is logically pinned to that fixed point applied to `a`.  -/
_private.Init.While.0.repeatM.Pred : {α : Type u} → {m : Type u → Type v} → [Monad m] → {β : Type u} → (α → m (α ⊕ β)) → α → m β → Prop
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
/-- The name of the used lemma.  -/
Mathlib.Tactic.ClickSuggestions.ApplyAtKey.name : Mathlib.Tactic.ClickSuggestions.ApplyAtKey → String
-- Mathlib.Data.Fintype.Basic
/-- Induction principle to build a sequence, by adding one point at a time satisfying a given
symmetric relation with respect to all the previously chosen points.

More precisely, Assume that, for any finite set `s`, one can find another point satisfying
some relation `r` with respect to all the points in `s`. Then one may construct a
function `f : ℕ → α` such that `r (f m) (f n)` holds whenever `m ≠ n`.
We also ensure that all constructed points satisfy a given predicate `P`.  -/
exists_seq_of_forall_finset_exists' : ∀ {α : Type u_4} (P : α → Prop) (r : α → α → Prop) [Std.Symm r],
  (∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y) →
    ∃ f, (∀ (n : ℕ), P (f n)) ∧ Pairwise (Function.onFun r f)
-- Mathlib.Algebra.Homology.Augment
_private.Mathlib.Algebra.Homology.Augment.0.CochainComplex.augment.match_1.splitter : (motive : ℕ → ℕ → Sort u_1) →
  (x x_1 : ℕ) →
    (Unit → motive 0 1) →
      ((i j : ℕ) → motive i.succ j.succ) →
        ((x x_2 : ℕ) → (x = 0 → x_2 = 1 → False) → (∀ (i j : ℕ), x = i.succ → x_2 = j.succ → False) → motive x x_2) →
          motive x x_1
-- Init.Data.Sum.Lemmas
Sum.map_comp_map : ∀ {α' : Type u_1} {α'' : Type u_2} {β' : Type u_3} {β'' : Type u_4} {α : Type u_5} {β : Type u_6} (f' : α' → α'')
  (g' : β' → β'') (f : α → α') (g : β → β'), Sum.map f' g' ∘ Sum.map f g = Sum.map (f' ∘ f) (g' ∘ g)
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- A monotone decreasing convergence lemma for integrals of measures of thickenings:
`∫ t in (0, ‖f‖], μ (thickening ε {x | f(x) ≥ t}) dt` tends to
`∫ t in (0, ‖f‖], μ {x | f(x) ≥ t} dt` as `ε → 0`.  -/
MeasureTheory.tendsto_integral_meas_thickening_le : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoMetricSpace Ω] [OpensMeasurableSpace Ω]
  (f : BoundedContinuousFunction Ω ℝ) {A : Set ℝ},
  MeasureTheory.volume A ≠ ⊤ →
    ∀ (μ : MeasureTheory.ProbabilityMeasure Ω),
      Filter.Tendsto (fun ε => ∫ (t : ℝ) in A, (↑μ).real (Metric.thickening ε {a | t ≤ f a})) (nhdsWithin 0 (Set.Ioi 0))
        (nhds (∫ (t : ℝ) in A, (↑μ).real {a | t ≤ f a}))
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.RightLinear.mk : {D : Type u_1} →
  {D' : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] →
        {F : CategoryTheory.Functor D D'} →
          {C : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.MonoidalCategory C] →
                [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] →
                  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] →
                    [toLaxRightLinear : F.LaxRightLinear C] →
                      [toOplaxRightLinear : F.OplaxRightLinear C] →
                        (∀ (d : D) (c : C),
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c)
                                (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c) =
                              CategoryTheory.CategoryStruct.id
                                (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c)) →
                          (∀ (d : D) (c : C),
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c)
                                  (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c) =
                                CategoryTheory.CategoryStruct.id
                                  (F.obj (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c))) →
                            F.RightLinear C
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ)
  (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc)
  (hkf : CategoryTheory.Limits.IsLimit kf) {Z : C} (h : kf.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hS.cokerIsoKer' k hk cc kf hcc hkf).inv
      (CategoryTheory.CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf) h) =
    h
-- Mathlib.Algebra.Homology.Factorizations.Basic
CochainComplex.instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  CochainComplex.degreewiseEpiWithInjectiveKernel.IsMultiplicative
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_5 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w l r : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr l)
  (rhs : Std.Tactic.BVDecide.BVExpr r) (h : w = l + r) (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhs.append rhs h with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_5 w l r lhs rhs h
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.neighborSet_map_equiv : ∀ {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (e : V ≃ W) (w : W),
  (SimpleGraph.map (⇑e) G).neighborSet w = ⇑e.symm ⁻¹' G.neighborSet (e.symm w)