mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.End
/-- If the permutation `f` fixes the subtype `{x // p x}`, then this returns the permutation
on `{x // p x}` induced by `f`.  -/
Equiv.Perm.subtypePerm : {α : Type u_4} → {p : α → Prop} → (f : Equiv.Perm α) → (∀ (x : α), p (f x) ↔ p x) → Equiv.Perm { x // p x }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β} {hc : k' ∈ t.alter k f},
  (t.alter k f)[k'] = if heq : cmp k k' = Ordering.eq then (f t[k]?).get ⋯ else t[k']
-- Init.Data.UInt.Bitwise
UInt64.not_zero : ~~~0 = -1
-- Mathlib.Algebra.Free
FreeAddMagma.instLawfulMonad : LawfulMonad FreeAddMagma
-- Mathlib.Algebra.Order.Monoid.Submonoid
AddSubmonoid.nonneg.eq_1 : ∀ (M : Type u_1) [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : AddLeftMono M],
  AddSubmonoid.nonneg M = { carrier := Set.Ici 0, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Algebra.Lie.Cochain
/-- A Lie 2-cocycle is a 2-cochain that is annihilated by the coboundary map.  -/
LieModule.Cohomology.twoCocycle : (R : Type u_1) →
  [inst : CommRing R] →
    (L : Type u_2) →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          (M : Type u_3) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [LieModule R L M] → Submodule R ↥(LieModule.Cohomology.twoCochain R L M)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rcc_eq_none : ∀ {m n i : ℕ}, n + 1 ≤ i + m → (m...=n).toList[i]? = none
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.elim_path : ∀ {V : Type u} {G : SimpleGraph V} {p : Prop} {u v : V}, G.Reachable u v → (∀ (a : G.Path u v), p) → p
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {l : List α} {k fallback : α},
  k ∈ t → (t.insertMany l).getD k fallback = t.getD k fallback
-- Mathlib.Data.Rel
SetRel.isTrans_iff_comp_subset_self : ∀ {α : Type u_1} {R : SetRel α α}, R.IsTrans ↔ R.comp R ⊆ R
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.smulCommClass_right : ∀ {R' : Type u_1} {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring R'] [inst_1 : SMul α β] [inst_2 : SMul R' β]
  [SMulCommClass α R' β] (S : Subsemiring R'), SMulCommClass α (↥S) β
-- Mathlib.RingTheory.Congruence.Defs
RingConGen.Rel.symm : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} {x y : R},
  RingConGen.Rel r x y → RingConGen.Rel r y x
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y), Continuous ⇑h
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instHasLimits : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G], CategoryTheory.Limits.HasLimits (Rep.{w, u, v} k G)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.Monadic.isPlausibleStep_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] {it : Std.IterM Id α} {step : Std.IterStep (Std.IterM Id α) α},
  it.IsPlausibleStep step ↔ step = Std.Rxi.Iterator.Monadic.step it
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
/-- Left unitor for the vertical composition of lax natural transformations.  -/
CategoryTheory.Lax.LaxTrans.leftUnitor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          (η : F ⟶ G) → CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id F) η ≅ η
-- Init.Data.Iterators.Basic
/-- The constructor has been renamed.  -/
Std.Iterators.toIterM : {α : Type u_1} → {m : Type u_1 → Type u_2} → {β : Type u_1} → α → Std.IterM m β
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
/-- `F.mapAddHom` is an additive homomorphism whose underlying function is `F.map`.  -/
CategoryTheory.Functor.mapAddHom : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Preadditive D] →
            (F : CategoryTheory.Functor C D) → [F.Additive] → {X Y : C} → (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)
-- Mathlib.RingTheory.IsTensorProduct
/-- (Implementation) If `B = S ⊗[R] A`, this is the canonical `R`-isomorphism:
`B ⊗[A] M ≃ₗ[S] S ⊗[R] M`. See `IsPushout.cancelBaseChange` for the `S`-linear version.  -/
Algebra.IsPushout.cancelBaseChangeAux : (R : Type u_1) →
  (S : Type v₃) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (A : Type u_8) →
            (B : Type u_9) →
              [inst_3 : CommRing A] →
                [inst_4 : CommRing B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      [inst_7 : Algebra A B] →
                        [inst_8 : Algebra S B] →
                          [inst_9 : IsScalarTower R A B] →
                            [inst_10 : IsScalarTower R S B] →
                              [Algebra.IsPushout R S A B] →
                                (M : Type u_10) →
                                  [inst_12 : AddCommGroup M] →
                                    [inst_13 : Module R M] →
                                      [inst_14 : Module A M] →
                                        [IsScalarTower R A M] → TensorProduct A B M ≃ₗ[R] TensorProduct R S M
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_iff' : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {j' k' : ι'} (hj' : e.f j = j'),
  c.next j = k →
    c'.next j' = k' →
      ∀ (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)) (hcocone : CategoryTheory.Limits.IsColimit cocone)
        ⦃W : C⦄ (f' : cocone.pt ⟶ K.X k),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cocone) f' = K.d j k →
          ∀ (f'' : cocone.pt ⟶ (K.extend e).X k'),
            CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom
                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cocone) f'') =
                (K.extend e).d j' k' →
              ∀ (φ : W ⟶ cocone.pt),
                CategoryTheory.CategoryStruct.comp φ f' = 0 ↔ CategoryTheory.CategoryStruct.comp φ f'' = 0
-- Init.Data.BitVec.Lemmas
BitVec.reverse_append : ∀ {w v : ℕ} {x : BitVec w} {y : BitVec v}, (x ++ y).reverse = BitVec.cast ⋯ (y.reverse ++ x.reverse)
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.mk.congr_simp : ∀ {α : Sort u_1} {β : Sort u_2} (toFun toFun_1 : α → β) (e_toFun : toFun = toFun_1) (inj' : Function.Injective toFun),
  { toFun := toFun, inj' := inj' } = { toFun := toFun_1, inj' := ⋯ }
-- Mathlib.Data.Real.Sign
Real.sign.eq_1 : ∀ (r : ℝ), r.sign = if r < 0 then -1 else if 0 < r then 1 else 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.differentiableAt_arccos : ∀ {x : ℝ}, DifferentiableAt ℝ Real.arccos x ↔ x ≠ -1 ∧ x ≠ 1
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_comp_coe_symm : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), ↑e ∘SL ↑e.symm = ContinuousLinearMap.id R₂ M₂
-- Batteries.Data.List.Scan
List.getElem?_partialSums : ∀ {α : Type u_1} {i : ℕ} [inst : Add α] [inst_1 : Zero α] [Std.Associative fun x1 x2 => x1 + x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0] {l : List α},
  l.partialSums[i]? = if i ≤ l.length then some (List.take i l).sum else none
-- Mathlib.Data.Fin.Tuple.Basic
Fin.contractNth_apply_of_eq : ∀ {n : ℕ} {α : Sort u_1} (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n),
  ↑k = ↑j → j.contractNth op g k = op (g k.castSucc) (g k.succ)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
_private.Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.0.CategoryTheory.Limits.mapPair.match_1.eq_2 : ∀ (motive : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair → Sort u_1)
  (h_1 : Unit → motive { as := CategoryTheory.Limits.WalkingPair.left })
  (h_2 : Unit → motive { as := CategoryTheory.Limits.WalkingPair.right }),
  (match { as := CategoryTheory.Limits.WalkingPair.right } with
    | { as := CategoryTheory.Limits.WalkingPair.left } => h_1 ()
    | { as := CategoryTheory.Limits.WalkingPair.right } => h_2 ()) =
    h_2 ()
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.FTCFilter.pure : ∀ (a : ℝ), intervalIntegral.FTCFilter a (pure a) ⊥
-- Mathlib.Data.List.Pi
List.Pi.cons_map : ∀ {ι : Type u_1} [inst : DecidableEq ι] {α : ι → Sort u_2} {i : ι} {l : List ι} (a : α i) (f : (j : ι) → j ∈ l → α j)
  {α' : ι → Sort u_3} (φ : ⦃j : ι⦄ → α j → α' j),
  (List.Pi.cons i l (φ a) fun j hj => φ (f j hj)) = fun j hj => φ (List.Pi.cons i l a f j hj)
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instRepr : {α : Type u} → [Repr α] → Repr (WithOne α)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The union of all open cells of the subcomplex equals the subcomplex.  -/
Topology.RelCWComplex.Subcomplex.union' : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (self : Topology.RelCWComplex.Subcomplex C), D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = self.carrier
-- Mathlib.GroupTheory.Finiteness
Monoid.fg_of_finite : ∀ {M : Type u_1} [inst : Monoid M] [Finite M], Monoid.FG M
-- Init.Data.String.Basic
String.Pos.le_nextn : ∀ {s : String} {p : s.Pos} {n : ℕ}, p ≤ p.nextn n
-- Lean.ProjFns
Lean.addAuxParentProjectionInfo : Lean.Environment → Lean.Name → ℕ → Bool → Lean.Environment
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
/-- Any compactly supported continuous nonnegative `f` such that `f ≥ 1` on `K` gives an upper bound
on the content of `K`; namely `λ(K) ≤ Λ f`.  -/
rieszContentAux_le : ∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal)
  {K : TopologicalSpace.Compacts X} {f : CompactlySupportedContinuousMap X NNReal},
  (∀ x ∈ K, 1 ≤ f x) → rieszContentAux Λ K ≤ Λ f
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).π = CategoryTheory.CategoryStruct.id c.pt
-- Mathlib.Data.Finset.Slice
/-- **Alias** of the reverse direction of `Set.sized_union`. -/
Set.sized.union : ∀ {α : Type u_1} {A B : Set (Finset α)} {r : ℕ}, Set.Sized r A ∧ Set.Sized r B → Set.Sized r (A ∪ B)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_counitIso_hom_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (X : CategoryTheory.Comma (CategoryTheory.Functor.const C) (CategoryTheory.Functor.id (CategoryTheory.Functor C D))),
  (CategoryTheory.WithInitial.equivComma.counitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Analysis.Convex.Join
convexJoin_assoc_aux : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (s t u : Set E),
  convexJoin 𝕜 (convexJoin 𝕜 s t) u ⊆ convexJoin 𝕜 s (convexJoin 𝕜 t u)
-- Mathlib.Probability.ProbabilityMassFunction.Binomial
PMF.binomial_apply_of_le : ∀ {k b : ℕ},
  k ≤ b →
    ∀ {x : NNReal} (h : x ≤ 1),
      ENNReal.ofReal (↑(b.choose k) * ↑x ^ k * (1 - ↑x) ^ (b - k)) = (PMF.binomial x h b) (Fin.ofNat (b + 1) k)
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
/-- Exterior derivative of a differential form.

There are a few competing definitions of the exterior derivative of a differential form
that differ from each other by a normalization factor.
We use the following one:

$$
dω(x; v_0, \dots, v_n) = \sum_{i=0}^n (-1)^i D_x ω(x; v_0, \dots, \widehat{v_i}, \dots, v_n) · v_i
$$

where $\widehat{v_i}$ means that we omit this element of the tuple, see `extDeriv_apply`.
 -/
extDeriv : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → {n : ℕ} → (E → E [⋀^Fin n]→L[𝕜] F) → E → E [⋀^Fin (n + 1)]→L[𝕜] F
-- Mathlib.SetTheory.Cardinal.Ordinal
/-- **Alias** of `Ordinal.IsInitial.isPrincipal_add`. -/
Ordinal.IsInitial.principal_add : ∀ {o : Ordinal.{u_1}}, o.IsInitial → Ordinal.omega0 ≤ o → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o
-- Mathlib.Data.Finset.Density
Finset.dens_lt_dens : ∀ {α : Type u_2} [inst : Fintype α] {s t : Finset α}, s ⊂ t → s.dens < t.dens
-- Mathlib.Order.Filter.Pointwise
Filter.divisionCommMonoid.eq_1 : ∀ {α : Type u_2} [inst : DivisionCommMonoid α],
  Filter.divisionCommMonoid = { toDivisionMonoid := Filter.divisionMonoid, mul_comm := ⋯ }
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.mono : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, LeftOrdContinuous f → Monotone f
-- Mathlib.Analysis.MeanInequalities
/-- For `1 ≤ p`, the `p`-th power of the sum of `f i` is bounded above by a constant times the
sum of the `p`-th powers of `f i`. Version for sums over finite sets, with `ℝ≥0∞`-valued functions.
 -/
ENNReal.rpow_sum_le_const_mul_sum_rpow : ∀ {ι : Type u} (s : Finset ι) (f : ι → ENNReal) {p : ℝ},
  1 ≤ p → (∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
-- Init.Data.Vector.Lex
Vector.not_lt_iff_ge : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] {xs ys : Vector α n}, ¬xs < ys ↔ ys ≤ xs
-- Mathlib.Data.Multiset.Filter
/-- `Multiset.map f` preserves `count` if `f` is injective on the set of elements contained in
the multiset  -/
Multiset.count_map_eq_count : ∀ {α : Type u_1} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] (f : α → β) (s : Multiset α),
  Set.InjOn f {x | x ∈ s} → ∀ x ∈ s, Multiset.count (f x) (Multiset.map f s) = Multiset.count x s
-- Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_homEquiv_symm : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] {X Y : C} (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X ⟹ Y),
  (CategoryTheory.eHomEquiv C).symm g = CategoryTheory.MonoidalClosed.uncurry' g
-- Init.Core
if_pos : ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort u} {t e : α}, (if c then t else e) = t
-- Mathlib.RingTheory.Ideal.Operations
Ideal.le_span_singleton_mul_iff : ∀ {R : Type u} [inst : CommSemiring R] {x : R} {I J : Ideal R}, I ≤ Ideal.span {x} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.braiding_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (P Q : C),
  (CategoryTheory.Limits.biprod.braiding P Q).hom =
    CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.flattenList.toNatAux.match_1.eq_3 : ∀ {n : ℕ} (motive : List (BitVec n) → Sort u_1) (x y : BitVec n) (rest : List (BitVec n)) (h_1 : Unit → motive [])
  (h_2 : (x : BitVec n) → motive [x]) (h_3 : (x y : BitVec n) → (rest : List (BitVec n)) → motive (x :: y :: rest)),
  (match x :: y :: rest with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: y :: rest => h_3 x y rest) =
    h_3 x y rest
-- Init.Data.Range.Polymorphic.SInt
Int16.instRxoIsAlwaysFinite : Std.Rxo.IsAlwaysFinite Int16
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.restr_apply : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t), ↑h.restr = ↑e
-- Mathlib.Algebra.BigOperators.Finprod
/-- The torsion-free assumption makes sure that the result holds even when the support of `f` is
infinite. For a more usual version assuming `HasFiniteSupport f` instead, see `finsum_smul'`.  -/
finsum_smul : ∀ {ι : Sort u_6} {R : Type u_7} {M : Type u_8} [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.IsTorsionFree R M] (f : ι → R) (x : M), (∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.ofArrowIso_g₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'),
  (c.ofArrowIso e).g₂ = CategoryTheory.CategoryStruct.comp c.g₂ (CategoryTheory.Arrow.rightFunc.map e.hom)
-- Mathlib.Topology.Algebra.ConstMulAction
subset_interior_smul_right : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] {s : Set G} {t : Set α}, s • interior t ⊆ interior (s • t)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.summandAction : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} →
              [DecidableEq ι] → [(i : ι) → DecidableEq (G i)] → (i : ι) → MulAction (G i) (Monoid.PushoutI.NormalWord d)
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.candidates_dist_inl : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {f : GromovHausdorff.ProdSpaceFun✝ X Y},
  f ∈ GromovHausdorff.candidates X Y → ∀ (x y : X), f (Sum.inl x, Sum.inl y) = dist x y
-- Batteries.Data.Fin.Lemmas
Fin.find?_one : ∀ {p : Fin 1 → Bool}, Fin.find? p = if p 0 = true then some 0 else none
-- Mathlib.Algebra.Group.Units.Defs
/-- Units of a monoid have a unit  -/
Units.instOne : {α : Type u} → [inst : Monoid α] → One αˣ
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
slope_pos_iff : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {f : 𝕜 → 𝕜} {x₀ b : 𝕜},
  x₀ < b → (0 < slope f x₀ b ↔ f x₀ < f b)
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_apply_basisFun_self : ∀ {ι : Type u_2} {Ω : Type u_3} [inst : Fintype ι] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → ℝ},
  (∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) →
    ∀ (i : ι),
      ((ProbabilityTheory.covarianceBilin (MeasureTheory.Measure.map (fun ω => WithLp.toLp 2 fun x => X x ω) μ))
            ((EuclideanSpace.basisFun ι ℝ) i))
          ((EuclideanSpace.basisFun ι ℝ) i) =
        ProbabilityTheory.variance (X i) μ
-- Mathlib.Analysis.Normed.Module.Normalize
NormedSpace.norm_smul_normalize : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] (x : V), ‖x‖ • NormedSpace.normalize x = x
-- Mathlib.CategoryTheory.Limits.Cones
/-- Whiskering by an equivalence gives an equivalence between categories of cones.
 -/
CategoryTheory.Limits.Cone.whiskeringEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              (e : K ≌ J) → CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone (e.functor.comp F)
-- Mathlib.MeasureTheory.Measure.Content
/-- In a locally compact space, any measure constructed from a content is regular.  -/
MeasureTheory.Content.regular : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : R1Space G] [S : MeasurableSpace G]
  [inst_2 : BorelSpace G] [WeaklyLocallyCompactSpace G], μ.measure.Regular
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.id_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Functor.id C) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Functor.id C).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Init.Data.Array.InsertIdx
Array.getElem_insertIdx_self : ∀ {α : Type u} {xs : Array α} {x : α} {i : ℕ} (w : i ≤ xs.size), (xs.insertIdx i x w)[i] = x
-- Mathlib.Data.Finset.Sigma
Finset.inf_sigma : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : (i : ι) × α i → β)
  [inst : SemilatticeInf β] [inst_1 : OrderTop β], (s.sigma t).inf f = s.inf fun i => (t i).inf fun b => f ⟨i, b⟩
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.instCSLiftValLift : ∀ {α β : Type u_2} [inst : Mathlib.Tactic.Ring.CSLift α β] (a : α),
  Mathlib.Tactic.Ring.CSLiftVal a (Mathlib.Tactic.Ring.CSLift.lift a)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The type of objects in the fibered category associated to a contravariant
pseudofunctor from a 1-category to Cat.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat → Type (max u₁ u₂)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.uncurry_ofArrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} (Y : ι → C) (f : (i : ι) → Y i ⟶ X),
  (CategoryTheory.Presieve.ofArrows Y f).uncurry = Set.range fun i => ⟨Y i, f i⟩
-- Init.Data.Order.Lemmas
Std.instLawfulOrderLeftLeaningMax : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α], Std.LawfulOrderLeftLeaningMax α
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.subst_into_addg : ∀ {α : Type u_1} [inst : AddCommGroup α] (l r tl tr t : α), l = tl → r = tr → tl + tr = t → l + r = t
-- Aesop.Forward.SlotIndex
Aesop.instHAddSlotIndexNat : HAdd Aesop.SlotIndex ℕ Aesop.SlotIndex
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.le_Φ_coeff_natDegree_natDegree : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → (RatFunc.Luroth.g✝ E).natDegree ≤ ((RatFunc.Luroth.Φ✝ E).coeff (RatFunc.Luroth.φ✝ E).natDegree).natDegree
-- Mathlib.Order.Basic
Prod.GCongr.mk_le_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] {a₁ a₂ : α} {b₁ b₂ : β},
  a₁ ≤ a₂ → b₁ ≤ b₂ → (a₁, b₁) ≤ (a₂, b₂)
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Quot.isGeneratedBy`. -/
Quot.deltaGeneratedSpace : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  [Topology.IsGeneratedBy X Y] {r : Y → Y → Prop}, Topology.IsGeneratedBy X (Quot r)
-- Init.Data.Int.OfNat
Int.Nonneg.num_cert.eq_1 : ∀ (a : ℤ), Int.Nonneg.num_cert a = decide (a ≥ 0)
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.one_le_coverMincard_iff : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X) (n : ℕ), 1 ≤ Dynamics.coverMincard T F U n ↔ F.Nonempty
-- Init.Data.UInt.Lemmas
USize.ofNatLT_uInt8ToNat : ∀ (n : UInt8), USize.ofNatLT n.toNat ⋯ = n.toUSize