mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Finsupp.Defs
Module.End.ringHomEndFinsupp_apply_apply : ∀ (ι : Type u_4) {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End (Module.End R M) M) (a : ι →₀ M),
  ((Module.End.ringHomEndFinsupp ι) f) a = (Finsupp.mapRange.addMonoidHom ↑f) a
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.forget₂_map_ofHom : ∀ {X Y : Type u} [inst : AddCommMonoid X] [inst_1 : AddCommMonoid Y] (f : X →+ Y),
  (CategoryTheory.forget₂ AddCommMonCat AddMonCat).map (AddCommMonCat.ofHom f) = AddMonCat.ofHom f
-- Mathlib.Order.Interval.Finset.Floor
Int.cast_mem_Iio_iff : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {b : α} {n : ℤ},
  ↑n ∈ Set.Iio b ↔ n ∈ Set.Iio ⌈b⌉
-- Mathlib.Tactic.Translate.ToAdditive
/-- We need to fix a few abbreviations after applying `nameDict`, i.e. replacing `ZeroLE` by `Nonneg`.
This dictionary contains these fixes.
The input should contain entries that is in `lowerCamelCase` (e.g. `ltzero`; the initial sequence
of capital letters should be lower-cased) and the output should be in `UpperCamelCase`
(e.g. `LTZero`).
When applying the dictionary, we lower-case the output if the input was also given in lower-case.
 -/
Mathlib.Tactic.ToAdditive.abbreviationDict : Std.HashMap String String
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RocSliceData.mk.inj : ∀ {α : Type u} {β : α → Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α β} {range : Std.Roc α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α β} {range_1 : Std.Roc α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Algebra.Field.Rat
NNRat.instDiv : Div ℚ≥0
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.mk.injEq : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (toFun : ↥g.cycleFactorsFinset → α)
  (mem_support_self' : ∀ (c : ↥g.cycleFactorsFinset), toFun c ∈ (↑c).support) (toFun_1 : ↥g.cycleFactorsFinset → α)
  (mem_support_self'_1 : ∀ (c : ↥g.cycleFactorsFinset), toFun_1 c ∈ (↑c).support),
  ({ toFun := toFun, mem_support_self' := mem_support_self' } =
      { toFun := toFun_1, mem_support_self' := mem_support_self'_1 }) =
    (toFun = toFun_1)
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_mod : ∀ {a b : USize} (h : System.Platform.numBits = 64), (a % b).toBitVec64 h = a.toBitVec64 h % b.toBitVec64 h
-- Init.Data.BitVec.Lemmas
BitVec.neg_toInt_neg : ∀ {w : ℕ} {x : BitVec w}, x.msb = false → -(-x).toInt = ↑x.toNat
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l l' : List ((a : α) × β a)} {fallback : α},
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → Std.Internal.List.minKeyD l fallback = Std.Internal.List.minKeyD l' fallback
-- Mathlib.Data.Finsupp.Basic
Finsupp.apply_eq_of_mem_graph : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {m : M} {f : α →₀ M}, (a, m) ∈ f.graph → f a = m
-- Mathlib.Algebra.GroupWithZero.Action.End
/-- The tautological action by `AddMonoid.End α` on `α`.

This generalizes `Function.End.applyMulAction`.  -/
AddMonoid.End.applyDistribMulAction : {α : Type u_4} → [inst : AddMonoid α] → DistribMulAction (AddMonoid.End α) α
-- Lean.Elab.PreDefinition.MkInhabitant
_private.Lean.Elab.PreDefinition.MkInhabitant.0.Lean.Elab.withInhabitedInstances.go.eq_def : ∀ {α : Type} (xs : Array Lean.Expr) (k : Array Lean.Expr → Lean.MetaM α) (i : ℕ) (insts : Array Lean.Expr),
  Lean.Elab.withInhabitedInstances.go✝ xs k i insts =
    if h : i < xs.size then
      have x := xs[i];
      do
      let xTy ← Lean.Meta.inferType x
      let u ← Lean.Meta.getLevel xTy
      have instTy : Lean.Expr := Lean.mkApp (Lean.Expr.const `Inhabited [u]) xTy
      have instVal : Lean.Expr := Lean.mkApp2 (Lean.Expr.const `Inhabited.mk [u]) xTy x
      Lean.Meta.withLetDecl `inst instTy instVal fun inst =>
          Lean.Elab.withInhabitedInstances.go✝ xs k (i + 1) (insts.push inst)
    else k insts
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk_surjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (f : CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y),
  ∃ z, f = CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk z
-- Mathlib.Data.Finset.Sigma
biSup_finsetSigma : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} [inst : CompleteLattice β] (s : Finset ι)
  (t : (i : ι) → Finset (α i)) (f : Sigma α → β), ⨆ ij ∈ s.sigma t, f ij = ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩
-- Mathlib.Computability.Encoding
Computability.Γ'.bra.sizeOf_spec : sizeOf Computability.Γ'.bra = 1
-- Mathlib.Order.Filter.AtTopBot.Monoid
/-- In an ordered cancellative multiplicative monoid, if `f x * C → +∞`, then `f x → +∞`.

Earlier, this name was used for a similar lemma about ordered rings,
which is now called `Filter.Tendsto.atTop_of_mul_const₀`.  -/
Filter.Tendsto.atTop_of_mul_const : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {l : Filter α}
  {f : α → M} (C : M), Filter.Tendsto (fun x => f x * C) l Filter.atTop → Filter.Tendsto f l Filter.atTop
-- Init.System.FilePath
/-- An absolute path starts at the root directory or a drive letter. Accessing files through an absolute
path does not depend on the current working directory.
 -/
System.FilePath.isAbsolute : System.FilePath → Bool
-- Init.Data.List.Lemmas
List.forall_mem_ne : ∀ {α : Type u_1} {a : α} {l : List α}, (∀ a' ∈ l, ¬a = a') ↔ a ∉ l
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instNonUnitalSemiring : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalSemiring A] →
          [inst_2 : Module R A] →
            [SMulCommClass R A A] →
              [IsScalarTower R A A] →
                [inst_5 : NonUnitalSemiring B] →
                  [inst_6 : Module R B] →
                    [SMulCommClass R B B] → [IsScalarTower R B B] → NonUnitalSemiring (TensorProduct R A B)
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Over.instHasColimitsOfShape : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {X : C} [CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.Over X)
-- Mathlib.Data.Num.Basic
Num.zero.sizeOf_spec : sizeOf Num.zero = 1
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.le_def : ∀ (C : Type u) [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.MorphismProperty C},
  P ≤ Q ↔ ∀ {X Y : C} (f : X ⟶ Y), P f → Q f
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.frequently_iff : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ {q : α → Prop}, (∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.algebraMap_pairingIn : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : P.IsValuedIn S] (i j : ι),
  (algebraMap S R) (P.pairingIn S i j) = P.pairing i j
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullback.hom_ext : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → objs j ⟶ B) [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C}
  (g1 g2 : X ⟶ CategoryTheory.Limits.widePullback B objs arrows),
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp g1 (CategoryTheory.Limits.WidePullback.π arrows j) =
        CategoryTheory.CategoryStruct.comp g2 (CategoryTheory.Limits.WidePullback.π arrows j)) →
    CategoryTheory.CategoryStruct.comp g1 (CategoryTheory.Limits.WidePullback.base arrows) =
        CategoryTheory.CategoryStruct.comp g2 (CategoryTheory.Limits.WidePullback.base arrows) →
      g1 = g2
-- Mathlib.Algebra.Homology.ComplexShape
/-- There is at most one nonzero differential from `X i`.  -/
ComplexShape.next_eq : ∀ {ι : Type u_1} (self : ComplexShape ι) {i j j' : ι}, self.Rel i j → self.Rel i j' → j = j'
-- Lean.Meta.Tactic.Grind.EMatch
/-- Constructs a proof of `lhs = rhs` (`lhs ≍ rhs` if `heq := true`) for a delayed
generalized-pattern equality. `lhs` is a term from the goal and has already been
internalized. `rhs` is the value the pattern was instantiated with; it is preprocessed,
and the equality is established using the e-graph. The instantiation fails if `lhs` and
`rhs` cannot be proved equal. `expectedType` is used for error messages only.

**Note**: `rhs` is an auxiliary term, and it is internalized inside
`withoutModifyingState`. The equality proof is also constructed there, before the state
is restored. `rhs` may contain metavariables corresponding to theorem parameters that
have not been assigned yet; they are abstracted at the end of `instantiateTheorem`. The
e-graph must not retain terms containing such metavariables: they become dangling
references when the `withNewMCtxDepth` at `instantiateTheorem` is exited. See issue
#13773.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.mkGeneralizedPatternEqProof : Lean.Expr →
  Lean.Expr →
    Lean.Meta.Grind.Origin →
      Lean.Expr → Bool → OptionT (StateT Lean.Meta.Grind.EMatch.Choice Lean.Meta.Grind.EMatch.M) Lean.Expr
-- Mathlib.CategoryTheory.Galois.Decomposition
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.mkSelfProdFib.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C),
  CategoryTheory.PreGaloisCategory.mkSelfProdFib✝ F X = CategoryTheory.PreGaloisCategory.mkSelfProdFib✝ F X
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterM.match_1.eq_2 : ∀ {β : Type u_1} {n : Type u_1 → Type u_2} {f : β → n (ULift.{u_1, 0} Bool)} [inst : MonadAttach n] (out : β)
  (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) (hf : MonadAttach.CanReturn (f out) { down := true })
  (h_1 : (hf : MonadAttach.CanReturn (f out) { down := false }) → motive ⟨{ down := false }, hf⟩)
  (h_2 : (hf : MonadAttach.CanReturn (f out) { down := true }) → motive ⟨{ down := true }, hf⟩),
  (match ⟨{ down := true }, hf⟩ with
    | ⟨{ down := false }, hf⟩ => h_1 hf
    | ⟨{ down := true }, hf⟩ => h_2 hf) =
    h_2 hf
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.max : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n : ℕ} →
      {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)} →
        {k k' : ℕ} →
          (hk : k < n) →
            (hk' : k' < n) →
              (X k hk).fst → (X k' hk').fst → CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep✝ n X
-- Mathlib.Order.Compare
Ordering.Compares.le_total : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} {o : Ordering}, o.Compares a b → a ≤ b ∨ b ≤ a
-- Mathlib.SetTheory.ZFC.Cardinal
ZFSet.card_insert : ∀ {x y : ZFSet.{u}}, x ∉ y → (insert x y).card = y.card + 1
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.Range.start : Lean.Lsp.Range → Lean.Lsp.Position
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- The function `Real.exp` is real analytic.  -/
analyticOnNhd_rexp : AnalyticOnNhd ℝ Real.exp Set.univ
-- Lean.Elab.Tactic.Omega.OmegaM
/-- If `groundNat? e = some n`, then `e` is definitionally equal to `OfNat.ofNat n`.
 -/
Lean.Elab.Tactic.Omega.groundNat? : Lean.Expr → Option ℕ
-- Mathlib.Order.Filter.Extr
IsMinFilter.comp_tendsto : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {l : Filter α} {g : δ → α} {l' : Filter δ}
  {b : δ}, IsMinFilter f l (g b) → Filter.Tendsto g l' l → IsMinFilter (f ∘ g) l' b
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.EquivEven.ι_eq_v_add_smul_e0 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M) (r : R),
  (CliffordAlgebra.ι (CliffordAlgebra.EquivEven.Q' Q)) (m, r) =
    (CliffordAlgebra.EquivEven.v Q) m + r • CliffordAlgebra.EquivEven.e0 Q
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂_compl₁₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₁' : Type u_8} {M₂' : Type u_9} {n : Type u_11} {m : Type u_12}
  {n' : Type u_13} {m' : Type u_14} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁]
  [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] [inst_5 : Fintype n] [inst_6 : Fintype m] [inst_7 : DecidableEq m]
  [inst_8 : DecidableEq n] (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂) [inst_9 : AddCommMonoid M₁']
  [inst_10 : Module R M₁'] [inst_11 : AddCommMonoid M₂'] [inst_12 : Module R M₂'] (b₁' : Module.Basis n' R M₁')
  (b₂' : Module.Basis m' R M₂') [inst_13 : Fintype n'] [inst_14 : Fintype m'] [inst_15 : DecidableEq n']
  [inst_16 : DecidableEq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (l : M₁' →ₗ[R] M₁) (r : M₂' →ₗ[R] M₂),
  (LinearMap.toMatrix₂ b₁' b₂') (B.compl₁₂ l r) =
    ((LinearMap.toMatrix b₁' b₁) l).transpose * (LinearMap.toMatrix₂ b₁ b₂) B * (LinearMap.toMatrix b₂' b₂) r
-- Mathlib.Data.Finset.Basic
Finset.attach_nonempty_iff : ∀ {α : Type u_1} {s : Finset α}, s.attach.Nonempty ↔ s.Nonempty
-- Mathlib.Order.Filter.Pointwise
Filter.prod_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] {l : Filter β}, l ×ˢ 0 = Filter.map (fun x => (x, 0)) l
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.normThreshold_zero : ∀ {a : ℝ}, ProbabilityTheory.Fernique.normThreshold a 0 = a
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_add_le_of_degree_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} {n : ℕ},
  p.natDegree ≤ n → q.natDegree ≤ n → (p + q).natDegree ≤ n
-- Lean.Parser.Extra
Lean.Parser.dbgTraceState.parenthesizer : String → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Heyting.Basic
Prod.instGeneralizedCoheytingAlgebra : {α : Type u_2} →
  {β : Type u_3} →
    [GeneralizedCoheytingAlgebra α] → [GeneralizedCoheytingAlgebra β] → GeneralizedCoheytingAlgebra (α × β)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_toHomeomorph : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), ⇑e.toHomeomorph = ⇑e
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.guard.inj : ∀ {origin origin_1 : Lean.Meta.Grind.Origin},
  Lean.Meta.Grind.SplitSource.guard origin = Lean.Meta.Grind.SplitSource.guard origin_1 → origin = origin_1
-- Mathlib.RingTheory.FinitePresentation
RingHom.FinitePresentation.of_bijective : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] {f : A →+* B},
  Function.Bijective ⇑f → f.FinitePresentation
-- Mathlib.Order.Concept
/-- See `Concept.ext` for a version using the extent.  -/
Concept.ext' : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r}, c.intent = d.intent → c = d
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.hom_ext₄_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 4}
  {φ φ' : f ⟶ g},
  φ = φ' ↔
    CategoryTheory.ComposableArrows.app' φ 0 _proof_361✝ = CategoryTheory.ComposableArrows.app' φ' 0 _proof_361✝ ∧
      CategoryTheory.ComposableArrows.app' φ 1 _proof_362✝ = CategoryTheory.ComposableArrows.app' φ' 1 _proof_362✝ ∧
        CategoryTheory.ComposableArrows.app' φ 2 _proof_363✝ = CategoryTheory.ComposableArrows.app' φ' 2 _proof_363✝ ∧
          CategoryTheory.ComposableArrows.app' φ 3 _proof_364✝ = CategoryTheory.ComposableArrows.app' φ' 3 _proof_364✝ ∧
            CategoryTheory.ComposableArrows.app' φ 4 _proof_365✝ = CategoryTheory.ComposableArrows.app' φ' 4 _proof_365✝
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.RepresentablyCoflat.comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.RepresentablyCoflat F] [CategoryTheory.RepresentablyCoflat G],
  CategoryTheory.RepresentablyCoflat (F.comp G)
-- Mathlib.GroupTheory.Solvable
Group.instIsSolvable : ∀ {G : Type u_3} [inst : CommGroup G], Group.IsSolvable G
-- Init.Grind.Offset
Lean.Grind.Nat.ro_lo_1 : ∀ (u w v k₁ k₂ : ℕ), u ≤ w + k₁ → w + k₂ ≤ v → u ≤ v + (k₁ - k₂)
-- Init.Data.Vector.Attach
Vector.map_attachWith : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {P : α → Prop} {H : ∀ a ∈ xs, P a} {f : { x // P x } → β},
  Vector.map f (xs.attachWith P H) =
    Vector.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => f ⟨x, ⋯⟩)
      xs.attach
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.fun_add : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α} {f g : α → M}
  [MeasurableAdd₂ M], Measurable f → Measurable g → Measurable fun i => f i + g i
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.touchpointWeights_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  [inst_8 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ (f : P →ᵃⁱ[ℝ] P₂), (s.map f.toAffineMap ⋯).touchpointWeights signs = s.touchpointWeights signs
-- Mathlib.Probability.Kernel.Disintegration.Basic
ProbabilityTheory.Kernel.condKernelCountable.instIsCondKernel : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} [inst : Countable α] (κCond : α → ProbabilityTheory.Kernel β Ω)
  [∀ (a : α), ProbabilityTheory.IsMarkovKernel (κCond a)]
  (h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y) (κ : ProbabilityTheory.Kernel α (β × Ω))
  [ProbabilityTheory.IsSFiniteKernel κ] [∀ (a : α), (κ a).IsCondKernel (κCond a)],
  κ.IsCondKernel (ProbabilityTheory.Kernel.condKernelCountable κCond h_atom)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.uniqueUpToIso_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {b : CategoryTheory.Limits.BinaryBicone X Y}
  (hb : b.IsBilimit),
  (CategoryTheory.Limits.biprod.uniqueUpToIso X Y hb).inv = CategoryTheory.Limits.biprod.desc b.inl b.inr
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.addCommutator.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (G : C)
  [inst_2 : CategoryTheory.AddGrpObj G],
  CategoryTheory.AddGrpObj.addCommutator G =
    CategoryTheory.SemiCartesianMonoidalCategory.fst G G + CategoryTheory.SemiCartesianMonoidalCategory.snd G G +
        -CategoryTheory.SemiCartesianMonoidalCategory.fst G G +
      -CategoryTheory.SemiCartesianMonoidalCategory.snd G G
-- Mathlib.RingTheory.HahnSeries.Binomial
HahnSeries.SummableFamily.binomialFamily_apply : ∀ {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : LinearOrder Γ] [inst_1 : AddCommMonoid Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : BinomialRing R] [inst_5 : CommRing A]
  [inst_6 : Algebra R A] {x : HahnSeries Γ A},
  0 < (x - 1).orderTop →
    ∀ (r : R) (n : ℕ), (HahnSeries.SummableFamily.binomialFamily x r) n = Ring.choose r n • (x - 1) ^ n
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.msgToInteractiveAux.pushEmbed : Lean.Widget.EmbedFmt✝ → Lean.Widget.MsgFmtM✝ ℕ
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.mkIso_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : CategoryTheory.AddGrp C} (e : G.X ≅ H.X)
  (zero_f :
    autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom = CategoryTheory.AddMonObj.zero)
      CategoryTheory.AddGrp.mkIso._auto_1)
  (add_f :
    autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
          CategoryTheory.AddMonObj.add)
      CategoryTheory.AddGrp.mkIso._auto_3),
  (CategoryTheory.AddGrp.mkIso e zero_f add_f).hom.hom.hom = e.hom
-- Mathlib.Logic.Encodable.Basic
/-- The lift of an encodable type is encodable.  -/
PLift.encodable : {α : Type u_1} → [Encodable α] → Encodable (PLift α)
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.unitsEquivSelf.eq_1 : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G), H.unitsEquivSelf = H.unitsEquivUnitsType.trans toUnits.symm
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.eq_6 : ∀ (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVUnOp.not)
  (h_2 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance))
  (h_3 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance))
  (h_4 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance))
  (h_5 : Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) (h_6 : Unit → motive Std.Tactic.BVDecide.BVUnOp.clz)
  (h_7 : Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop),
  (match Std.Tactic.BVDecide.BVUnOp.clz with
    | Std.Tactic.BVDecide.BVUnOp.not => h_1 ()
    | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance => h_2 distance
    | Std.Tactic.BVDecide.BVUnOp.rotateRight distance => h_3 distance
    | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance => h_4 distance
    | Std.Tactic.BVDecide.BVUnOp.reverse => h_5 ()
    | Std.Tactic.BVDecide.BVUnOp.clz => h_6 ()
    | Std.Tactic.BVDecide.BVUnOp.cpop => h_7 ()) =
    h_6 ()
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Limits.CoproductDisjoint.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C},
  (∀ {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) {i j : ι},
      i ≠ j →
        ∀ (s : CategoryTheory.Limits.PullbackCone (c.inj i) (c.inj j)) (a : CategoryTheory.Limits.IsLimit s),
          Nonempty (CategoryTheory.Limits.IsInitial s.pt)) →
    (∀ {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) (i : ι),
        CategoryTheory.Mono (c.inj i)) →
      CategoryTheory.Limits.CoproductDisjoint X