mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.linear : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_4 : AddCommMonoid F] [inst_5 : Module R F]
  [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)] [Bundle.Trivialization.IsLinear R e]
  {b : B}, b ∈ e.baseSet → IsLinearMap R fun y => (↑e ⟨b, y⟩).2
-- Mathlib.Algebra.Group.End
Equiv.mulRight_mul : ∀ {α : Type u_4} [inst : Group α] (a b : α), Equiv.mulRight (a * b) = Equiv.mulRight b * Equiv.mulRight a
-- Mathlib.RingTheory.PowerSeries.Inverse
/-- Two ways of removing the constant coefficient of a power series are the same.  -/
PowerSeries.sub_const_eq_shift_mul_X : ∀ {R : Type u_1} [inst : Ring R] (φ : PowerSeries R),
  φ - PowerSeries.C (PowerSeries.constantCoeff φ) =
    (PowerSeries.mk fun p => (PowerSeries.coeff (p + 1)) φ) * PowerSeries.X
-- Mathlib.Data.Sign.Defs
SignType.nonpos_iff : ∀ {a : SignType}, a ≤ 0 ↔ a = -1 ∨ a = 0
-- Mathlib.Combinatorics.SimpleGraph.Cayley
/-- The Cayley graph induced by an operation `[Add M]` with generators `s`  -/
SimpleGraph.addCayley : {M : Type u_1} → Set M → [Add M] → SimpleGraph M
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_mul_of_one_le_right' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α] [MulLeftMono α] {a b : α}, 1 ≤ b → a ≤ a * b
-- Mathlib.Topology.MetricSpace.HolderNorm
MemHolder.nnHolderNorm_add_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : NormedAddCommGroup Y] {r : NNReal} {f g : X → Y},
  MemHolder r f → MemHolder r g → nnHolderNorm r (f + g) ≤ nnHolderNorm r f + nnHolderNorm r g
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.log_exp : ∀ {M : Type u_4} [inst : AddMonoid M] (a : M), (WithZero.exp a).log = a
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.instInhabited : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (h₁ : S₁.RightHomologyData) →
            (h₂ : S₂.RightHomologyData) → Inhabited (CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- Typecheck a `LinearMap` as a morphism in `SemimoduleCat`.  -/
SemimoduleCat.ofHom : {R : Type u} →
  [inst : Semiring R] →
    {X Y : Type v} →
      [inst_1 : AddCommMonoid X] →
        [inst_2 : Module R X] →
          [inst_3 : AddCommMonoid Y] →
            [inst_4 : Module R Y] → (X →ₗ[R] Y) → (SemimoduleCat.of R X ⟶ SemimoduleCat.of R Y)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instMulCoeOfMulMemClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Mul (R i)] [inst_2 : ∀ (i : ι), MulMemClass (S i) (R i)],
  RestrictedProduct.instMulCoeOfMulMemClass R = { mul := fun x y => ⟨fun i => x i * y i, ⋯⟩ }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.find?_toList_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α} {v : β},
  List.find? (fun x => cmp x.1 k == Ordering.eq) t.toList = some (k', v) ↔ t.getKey? k = some k' ∧ t[k]? = some v
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ₀Iter_zero : ∀ (n : ℕ), SimplexCategory.σ₀Iter 0 ⋯ = CategoryTheory.CategoryStruct.id { len := n }
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_hom_inv_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f.hom)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom h f.inv) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id V))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom h (CategoryTheory.CategoryStruct.id V))
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ImportData.mk.injEq : ∀ (errors errors_1 : IO.Ref (Array Lean.Meta.LazyDiscrTree.ImportFailure)),
  ({ errors := errors } = { errors := errors_1 }) = (errors = errors_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.hom_ext : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {Z : C} (g h : Z ⟶ ⨁ f),
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biproduct.π f j) =
        CategoryTheory.CategoryStruct.comp h (CategoryTheory.Limits.biproduct.π f j)) →
    g = h
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.support_update : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M)
  [inst_1 : DecidableEq α] [inst_2 : DecidableEq M],
  (f.update a b).support = if b = 0 then f.support.erase a else insert a f.support
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.mem_prod : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N}
  {p : G × N}, p ∈ H.prod K ↔ p.1 ∈ H ∧ p.2 ∈ K
-- Mathlib.Computability.StateTransition
StateTransition.EvalsTo.evals_in_steps : ∀ {σ : Type u_1} {f : σ → Option σ} {a : σ} {b : Option σ} (self : StateTransition.EvalsTo f a b),
  (flip bind f)^[self.steps] (some a) = b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.ExtDHashMap.filterMap f m).contains k = Option.any (fun x => (f k x).isSome) (m.get? k)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffAt.neg_section : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s : (x : M) → V x} {x₀ : M},
  ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) x₀ →
    ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (-s) x⟩) x₀
-- Init.Data.Int.Order
Int.neg_add_lt_left_of_lt_add : ∀ {a b c : ℤ}, a < b + c → -b + a < c
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.of_smul : ∀ {α : Type u_1} {n : Type u_4} {R : Type u_5} [inst : Monoid R] [inst_1 : Star R] [inst_2 : Star α]
  [inst_3 : MulAction R α] [StarModule R α] {A : Matrix n n α} {k : R} [Invertible k],
  (k • A).IsHermitian → IsSelfAdjoint k → A.IsHermitian
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkPushforward.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C X) (x : ↑X),
  TopCat.Presheaf.stalkPushforward C f F x =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colim.map
        (CategoryTheory.Functor.whiskerRight
          (CategoryTheory.NatTrans.op (TopologicalSpace.OpenNhds.inclusionMapIso f x).inv) F))
      (CategoryTheory.Limits.colimit.pre
        (((CategoryTheory.Functor.whiskeringLeft (TopologicalSpace.OpenNhds x)ᵒᵖ (TopologicalSpace.Opens ↑X)ᵒᵖ C).obj
              (TopologicalSpace.OpenNhds.inclusion x).op).obj
          F)
        (TopologicalSpace.OpenNhds.map f x).op)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} {h' : k ∈ Std.DHashMap.Raw.map f m} (h : m.WF),
  (Std.DHashMap.Raw.map f m).get k h' = f k (m.get k ⋯)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instSMulOfSMulCommClass.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {X : Type u_4} {Y : Type u_5} {σ : M → N} [inst : SMul M X]
  [inst_1 : SMul N Y] [inst_2 : SMul R Y] [inst_3 : SMulCommClass N R Y],
  MulActionHom.instSMulOfSMulCommClass = { smul := fun h f => { toFun := h • ⇑f, map_smul' := ⋯ } }
-- Init.Data.BitVec.Bitblast
BitVec.aandRec.congr_simp : ∀ {w : ℕ} (x x_1 : BitVec w),
  x = x_1 →
    ∀ (y y_1 : BitVec w), y = y_1 → ∀ (s s_1 : ℕ) (e_s : s = s_1) (hs : s < w), x.aandRec y s hs = x_1.aandRec y_1 s_1 ⋯
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.univ_add : ∀ {α : Type u_2} [inst : AddGroup α] {t : Set α}, t.Nonempty → Set.univ + t = Set.univ
-- Init.Data.BitVec.Lemmas
BitVec.ne_intMin_of_msb_eq_false : ∀ {w : ℕ}, 0 < w → ∀ {n : BitVec w}, n.msb = false → n ≠ BitVec.intMin w
-- Lean.Environment
/-- Direct imports  -/
Lean.EnvironmentHeader.imports : Lean.EnvironmentHeader → Array Lean.Import
-- Mathlib.Order.RelClasses
/-- Inducts on a well-founded `>` relation.  -/
WellFoundedGT.induction : ∀ {α : Type u} [inst : LT α] [WellFoundedGT α] {motive : α → Prop} (a : α),
  (∀ (x : α), (∀ (y : α), x < y → motive y) → motive x) → motive a
-- Mathlib.Topology.Path
Path.extend_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), ⇑γ.symm.extend = fun x_1 => γ.extend (1 - x_1)
-- Mathlib.Tactic.NormDet
/-- reify a `BirdDet` call and normalize it using the certificate-chain evaluator  -/
_private.Mathlib.Tactic.NormDet.0.normalizeBirdDet : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.inf_arrow_factors_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {B : C}
  (X Y : CategoryTheory.Subobject B), X.Factors (X ⊓ Y).arrow
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The homology of a short complex is the `left.H` field of a chosen homology data.  -/
CategoryTheory.ShortComplex.homology : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (S : CategoryTheory.ShortComplex C) → [S.HasHomology] → C
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_congr : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k k' : α}, (k == k') = true → m.getKey! k = m.getKey! k'
-- Mathlib.Control.Functor.Multivariate
MvFunctor.map_map : ∀ {n : ℕ} {α β γ : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [inst : MvFunctor F] [LawfulMvFunctor F] (g : α.Arrow β)
  (h : β.Arrow γ) (x : F α), MvFunctor.map h (MvFunctor.map g x) = MvFunctor.map (TypeVec.comp h g) x
-- Mathlib.Data.WSeq.Productive
Stream'.WSeq.productive_iff : ∀ {α : Type u} (s : Stream'.WSeq α), s.Productive ↔ ∀ (n : ℕ), (s.get? n).Terminates
-- Mathlib.Algebra.Module.Torsion.Basic
/-- For a natural number `n`, the `n`-torsion subgroup of `A` is a `ZMod n` module.  -/
AddSubgroup.torsionBy.zmodModule : {A : Type u_3} → [inst : AddCommGroup A] → {n : ℕ} → Module (ZMod n) ↥(AddSubgroup.torsionBy A ↑n)
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.subset : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A₁ A₂ : Set α} {B₁ B₂ : Set β}
  {f : α → β} {n : ℕ}, A₁ ⊆ A₂ → IsAddFreimanHom n A₂ B₂ f → Set.MapsTo f A₁ B₁ → IsAddFreimanHom n A₁ B₁ f
-- Mathlib.Algebra.Group.Hom.Defs
/-- Copy of a `MulHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
MulHom.copy : {M : Type u_4} → {N : Type u_5} → [inst : Mul M] → [inst_1 : Mul N] → (f : M →ₙ* N) → (f' : M → N) → f' = ⇑f → M →ₙ* N
-- Lean.DocString.Markdown
Lean.Doc.MarkdownBlock.mk : {i : Type u} →
  {b : Type v} →
    ((Lean.Doc.Inline i → Lean.Doc.MarkdownM (Array String)) →
        (Lean.Doc.Block i b → Lean.Doc.MarkdownM (Array String)) →
          b → Array (Lean.Doc.Block i b) → Lean.Doc.MarkdownM (Array String)) →
      Lean.Doc.MarkdownBlock i b
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.toFun_sum : ∀ {α : Type u_1} {ι : Type u_3} {𝔖 : Set (Set α)} {β : Type u_4} [inst : AddCommMonoid β] {f : ι → α → β}
  (I : Finset ι), (UniformOnFun.toFun 𝔖) (∑ i ∈ I, f i) = ∑ i ∈ I, (UniformOnFun.toFun 𝔖) (f i)
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the smallest element that is less than the given element,
panicking if no such element exists.
 -/
Std.TreeSet.getLT! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet α cmp → α → α
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_fintype : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] [inst_2 : Fintype α]
  (f : α →₀ M) (g : α → M → N), (∀ (i : α), g i 0 = 1) → f.prod g = ∏ i, g i (f i)
-- Init.Data.ByteArray.Lemmas
ByteArray.toList.eq_1 : ∀ (bs : ByteArray), bs.toList = ByteArray.toList.loop bs 0 []
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. A measurable function is smaller than its mean on a set of positive
measure.  -/
MeasureTheory.measure_le_laverage_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal}
  [MeasureTheory.IsFiniteMeasure μ], μ ≠ 0 → AEMeasurable f μ → 0 < μ {x | f x ≤ ⨍⁻ (a : α), f a ∂μ}
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.foldM_eq_foldlM_keys : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : δ → α → m' δ} {init : δ},
  Std.DHashMap.Raw.foldM (fun d a x => f d a) init ↑m = List.foldlM f init (↑m).keys
-- Mathlib.Logic.Equiv.Option
/-- When `α` and `β` are in the same universe, this is the same as the result of
`EquivFunctor.mapEquiv`.  -/
Equiv.optionCongr_eq_equivFunctor_mapEquiv : ∀ {α β : Type u} (e : α ≃ β), e.optionCongr = EquivFunctor.mapEquiv Option e
-- Aesop.Script.ScriptM
Aesop.ScriptM : Type → Type
-- Init.Data.BitVec.Lemmas
BitVec.toFin_sdiv : ∀ {w : ℕ} {x y : BitVec w},
  (x.sdiv y).toFin =
    match x.msb, y.msb with
    | false, false => x.toFin / y.toFin
    | false, true => (-(x / -y)).toFin
    | true, false => (-(-x / y)).toFin
    | true, true => (-x).toFin / (-y).toFin
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.coe_J : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R],
  ↑(SymplecticGroup.symJ l R) = Matrix.J l R
-- Batteries.Data.List.Basic
List.tails_eq_tailsTR : @List.tails = @List.tailsTR
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.topologicalSpace : (B : Type u_1) →
  (F : Type u_2) →
    [t₁ : TopologicalSpace B] → [t₂ : TopologicalSpace F] → TopologicalSpace (Bundle.TotalSpace F (Bundle.Trivial B F))
-- Mathlib.Order.Zorn
zorn_le_nonempty_Ici₀ : ∀ {α : Type u_1} [inst : Preorder α] (a : α),
  (∀ c ⊆ Set.Ici a, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub) →
    ∀ (x : α), a ≤ x → ∃ m, x ≤ m ∧ IsMax m
-- Std.Data.DHashMap.RawDef
Std.DHashMap.Raw.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)] (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)),
  sizeOf { size := size, buckets := buckets } = 1 + sizeOf size + sizeOf buckets
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofSubmodule'_toLinearMap : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
  {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
  (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂),
  ↑(f.ofSubmodule' U) = LinearMap.codRestrict U ((↑f).domRestrict (Submodule.comap (↑f) U)) ⋯
-- Mathlib.NumberTheory.Padics.AddChar
PadicInt.continuous_addChar_of_value_at_one : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : NormedRing R] [inst_2 : Algebra ℤ_[p] R]
  [inst_3 : IsBoundedSMul ℤ_[p] R] [inst_4 : IsUltrametricDist R] [inst_5 : CompleteSpace R] {r : R}
  (hr : Filter.Tendsto (fun x => r ^ x) Filter.atTop (nhds 0)), Continuous ⇑(PadicInt.addChar_of_value_at_one r hr)
-- Init.Data.BitVec.Lemmas
BitVec.getElem_zero_ofNat_zero : ∀ {w : ℕ} (i : ℕ) (h : i < w), (0#w)[i] = false
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_η : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).functor =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.foldl_eq_foldl_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {δ : Type w} {f : δ → α → δ} {init : δ},
  Std.TreeSet.Raw.foldl f init t = Array.foldl f init t.toArray
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsRefl.eq_zero : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁]
  {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.IsRefl → ∀ {x y : M₁}, (B x) y = 0 → (B y) x = 0
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α] [inst_7 : SizeOf C]
  [inst_8 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W₁ x)] [inst_9 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W₂ x)]
  [inst_10 : SizeOf α] (deg : C → α)
  (lt₁ : ∀ {X Y : C} (f : X ⟶ Y), W₁ f → ¬CategoryTheory.MorphismProperty.identities C f → deg Y < deg X)
  (lt₂ : ∀ {X Y : C} (f : X ⟶ Y), W₂ f → ¬CategoryTheory.MorphismProperty.identities C f → deg X < deg Y)
  (nonempty_unique : ∀ {X Y : C} (f : X ⟶ Y), Nonempty (Unique (W₁.MapFactorizationData W₂ f))),
  sizeOf { deg := deg, lt₁ := lt₁, lt₂ := lt₂, nonempty_unique := nonempty_unique } = 1
-- Mathlib.Probability.Kernel.Deterministic
/-- A kernel is deterministic if copying then applying the kernel to the two copies is the same
as first applying the kernel then copying.  -/
ProbabilityTheory.IsDeterministic : {α : Type u_1} →
  {β : Type u_2} → {mα : MeasurableSpace α} → {mβ : MeasurableSpace β} → ProbabilityTheory.Kernel α β → Prop
-- Mathlib.Topology.Algebra.Order.Field
/-- The function `x ↦ x⁻¹` tends to `-∞` on the left of `0`.  -/
tendsto_inv_nhdsLT_zero : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜], Filter.Tendsto (fun x => x⁻¹) (nhdsWithin 0 (Set.Iio 0)) Filter.atBot
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.pow_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Monoid β]
  [inst_3 : ContinuousMul β] (f : C(α, β)) (n : ℕ) (x : α), (f ^ n) x = f x ^ n
-- Mathlib.Algebra.Group.Defs
CommMagma.ext_iff : ∀ {G : Type u} {x y : CommMagma G}, x = y ↔ Mul.mul = Mul.mul
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.IterM.step_takeWhile.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : false = true → motive true) (h_2 : false = false → motive false),
  (match hP : false with
    | true => h_1 hP
    | false => h_2 hP) =
    h_2 ⋯
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_smul : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι]
  [inst_5 : (i : ι) → SMul R (G i)] [inst_6 : SMul R C]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)]
  [∀ (i : ι), MulActionHomClass (H i) R (G i) C] (g : (i : ι) → H i)
  (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (r : R) (x : DirectLimit G f),
  DirectLimit.lift f (fun x => ⇑(g x)) h (r • x) = r • DirectLimit.lift f (fun x => ⇑(g x)) h x
-- Std.Data.TreeSet.Basic
Std.TreeSet.instInter : {α : Type u} → {cmp : α → α → Ordering} → Inter (Std.TreeSet α cmp)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.η_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {X Y : C}
  (f : X ⟶ Y) [inst_3 : F.OplaxMonoidal],
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.η F).app X)
      ((CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C C)).map f) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.η F).app X) f
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint16.injEq : ∀ (val val_1 : UInt16),
  (Lean.Compiler.LCNF.LitValue.uint16 val = Lean.Compiler.LCNF.LitValue.uint16 val_1) = (val = val_1)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Function.Injective.tsum_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {g : γ → β},
  Function.Injective g → ∀ {f : β → α}, Function.support f ⊆ Set.range g → ∑' (c : γ), f (g c) = ∑' (b : β), f b
-- Mathlib.Data.Nat.Choose.Sum
/-- A version of the **binomial theorem** for commuting elements in noncommutative semirings.  -/
Commute.add_pow : ∀ {R : Type u_1} [inst : Semiring R] {x y : R},
  Commute x y → ∀ (n : ℕ), (x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
-- Lean.Server.AsyncList
Lean.AsyncList.delayed.sizeOf_spec : ∀ {ε : Type u} {α : Type v} [inst : SizeOf ε] [inst_1 : SizeOf α]
  (tl : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α))), sizeOf (Lean.AsyncList.delayed tl) = 1 + sizeOf tl
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Hom.ext_iff : ∀ {X Y : PartOrdEmb} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.quotTensorEquivQuotSMul_symm_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  (x : M), (TensorProduct.quotTensorEquivQuotSMul M I).symm (Submodule.Quotient.mk x) = 1 ⊗ₜ[R] x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mem_inv : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] {s : Finset α} {x : α}, x ∈ s⁻¹ ↔ ∃ y ∈ s, y⁻¹ = x
-- Mathlib.GroupTheory.Congruence.Hom
/-- Homomorphisms on the quotient of an `AddMonoid` by an additive
congruence relation `c` are equal if their compositions with `c.mk'` are equal.  -/
AddCon.hom_ext : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M}
  {f g : c.Quotient →+ P}, f.comp c.mk' = g.comp c.mk' → f = g
-- Init.Data.List.Lemmas
List.getLast!_cons_eq_getLastD : ∀ {α : Type u_1} {a : α} {l : List α} [inst : Inhabited α], (a :: l).getLast! = l.getLastD a