mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GroupWithZero.Action.Center
/-- For a group with zero, the center of the units is the same as the units of the center.  -/
Subgroup.centerUnitsEquivUnitsCenter : (G₀ : Type u_1) → [inst : GroupWithZero G₀] → ↥(Subgroup.center G₀ˣ) ≃* (↥(Submonoid.center G₀))ˣ
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.left_hom_inv_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g)
  [inst_1 : CategoryTheory.IsIso sq],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq)
      (CategoryTheory.CategoryStruct.comp g.hom (CategoryTheory.inv (CategoryTheory.Arrow.Hom.right sq))) =
    f.hom
-- Mathlib.Analysis.Fourier.PoissonSummation
/-- **Poisson's summation formula**, assuming that both `f` and its Fourier transform decay as
`|x| ^ (-b)` for some `1 < b`. (This is the one-dimensional case of Corollary VII.2.6 of Stein and
Weiss, *Introduction to Fourier analysis on Euclidean spaces*.)  -/
Real.tsum_eq_tsum_fourier_of_rpow_decay : ∀ {f : ℝ → ℂ},
  Continuous f →
    ∀ {b : ℝ},
      1 < b →
        (f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) →
          (FourierTransform.fourier f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) →
            ∀ (x : ℝ), ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), FourierTransform.fourier f ↑n * (fourier n) ↑x
-- Mathlib.AlgebraicGeometry.Restrict
/-- If `U = V`, then `X ∣_ U` is isomorphic to `X ∣_ V`.  -/
AlgebraicGeometry.Scheme.isoOfEq : (X : AlgebraicGeometry.Scheme) → {U V : X.Opens} → U = V → (↑U ≅ ↑V)
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_self : ∀ (n : ℕ), n.choose n = 1
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.State.mk.injEq : ∀ (count : ℕ) (results : Std.HashMap Lean.ExprStructEq Lean.Meta.LetToHave.Result✝) (count_1 : ℕ)
  (results_1 : Std.HashMap Lean.ExprStructEq Lean.Meta.LetToHave.Result✝),
  ({ count := count, results := results } = { count := count_1, results := results_1 }) =
    (count = count_1 ∧ results = results_1)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.hasSeparator_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.HasSeparator Cᵒᵖ ↔ CategoryTheory.HasCoseparator C
-- Mathlib.Topology.UniformSpace.Compact
/-- Let `c : Set (Set α)` be an open cover of a compact set `s`. Then there exists an entourage
`n` such that for each `x ∈ s` its `n`-neighborhood is contained in some `t ∈ c`.  -/
lebesgue_number_lemma_sUnion : ∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {S : Set (Set α)},
  IsCompact K → (∀ s ∈ S, IsOpen s) → K ⊆ ⋃₀ S → ∃ V ∈ uniformity α, ∀ x ∈ K, ∃ s ∈ S, UniformSpace.ball x V ⊆ s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.minKey! = km ↔ km ∈ t ∧ ∀ k ∈ t, (compare km k).isLE = true
-- Mathlib.Data.Nat.Factorial.NatCast
IsUnit.natCast_factorial_iff_of_charP : ∀ {A : Type u_1} [inst : Ring A] (p : ℕ) [Fact (Nat.Prime p)] [CharP A p] {n : ℕ}, IsUnit ↑n.factorial ↔ n < p
-- Plausible.Testable
Plausible.Ne.printableProp : {α : Type u_1} → [Repr α] → {x y : α} → Plausible.PrintableProp (x ≠ y)
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.bicategory_rightUnitor_hom_unop2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : Bᵒᵖ} (f : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitor f).hom.unop2 = (CategoryTheory.Bicategory.leftUnitor f.unop).hom
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.isRightAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : G ⊣ F), F.IsRightAdjoint
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- `G.PreservesPointwiseLeftKanExtensions L` means that `G : B ⥤ D` preserves all pointwise left
Kan extensions along `L : A ⥤ C` of every functor `A ⥤ B`.  -/
CategoryTheory.Functor.PreservesPointwiseLeftKanExtensions : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                CategoryTheory.Functor B D → CategoryTheory.Functor A C → Prop
-- Mathlib.Tactic.Find
/-- `find` finds definitions and theorems whose result type matches the current goal exactly,
and prints them as info lines.
In other words, `find` lists definitions and theorems that are `apply`able against the current goal.
`find` will not affect the goal by itself and should be removed from the finished proof.

For a command or tactic that takes the type to search for as an argument, see `#find`.

Example:
```lean
example : True := by
  find
  -- True.intro: True
  -- trivial: True
  -- ...
```
 -/
Mathlib.Tactic.Find.tacticFind : Lean.ParserDescr
-- Mathlib.GroupTheory.Commutator.Basic
/-- If `N` is a normal additive subgroup of `G` and `H` a commutative additive
subgroup such that `H ⊔ N = ⊤`, then `N` contains `addCommutator G`.  -/
AddSubgroup.Normal.addCommutator_le_of_self_sup_commutative_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] {N : AddSubgroup G} [N.Normal] {H : AddSubgroup G},
  N ⊔ H = ⊤ → IsAddCommutative ↥H → addCommutator G ≤ N
-- Mathlib.LinearAlgebra.Finsupp.Pi
FunOnFinite.linearMap_piSingle : ∀ (R : Type u_5) (M : Type u_6) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {X : Type u_7}
  {Y : Type u_8} [inst_3 : Finite X] [inst_4 : Finite Y] [inst_5 : DecidableEq X] [inst_6 : DecidableEq Y] (f : X → Y)
  (x : X) (m : M), (FunOnFinite.linearMap R M f) (Pi.single x m) = Pi.single (f x) m
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
/-- The **spectral mapping theorem** for the continuous functional calculus.  -/
cfcHom_map_spectrum : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  (f : C(↑(spectrum R a), R)), spectrum R ((cfcHom ha) f) = Set.range ⇑f
-- Mathlib.Topology.EMetricSpace.Basic
/-- A version of `edist_le_Ico_sum_edist` with each intermediate distance replaced
with an upper estimate.  -/
edist_le_Ico_sum_of_edist_le : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : ℕ → α} {m n : ℕ},
  m ≤ n →
    ∀ {d : ℕ → ENNReal},
      (∀ {k : ℕ}, m ≤ k → k < n → edist (f k) (f (k + 1)) ≤ d k) → edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, d i
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.cancel_counitInv_right_assoc' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {W X X' Y Y' Z : D} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h (e.counitInv.app Z))) =
      CategoryTheory.CategoryStruct.comp f'
        (CategoryTheory.CategoryStruct.comp g' (CategoryTheory.CategoryStruct.comp h' (e.counitInv.app Z))) ↔
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) =
      CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h')
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
/-- The "μᵣ" morphism.  -/
CategoryTheory.Functor.LaxRightLinear.μᵣ : {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'} →
                    [self : F.LaxRightLinear C] →
                      (d : D) →
                        (c : C) →
                          CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c ⟶
                            F.obj (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ofRingEquiv_toEquiv : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {f : A₁ ≃+* A₂}
  (hf : ∀ (x : R), f ((algebraMap R A₁) x) = (algebraMap R A₂) x),
  ↑(AlgEquiv.ofRingEquiv hf) = { toFun := ⇑f, invFun := ⇑f.symm, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Order.Basic
le_update_self_iff : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)] {x : (i : ι) → π i}
  {i : ι} {a : π i}, x ≤ Function.update x i a ↔ x i ≤ a
-- Mathlib.Algebra.Group.End
AddAut.instInhabited.eq_1 : ∀ (M : Type u_2) [inst : Add M], AddAut.instInhabited M = { default := 0 }
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J],
  (∀ (X₁ X₂ : CategoryTheory.Functor J C) (c₁ : CategoryTheory.Limits.Cone X₁) (c₂ : CategoryTheory.Limits.Cone X₂)
      (x : CategoryTheory.Limits.IsLimit c₁) (h₂ : CategoryTheory.Limits.IsLimit c₂) (f : X₁ ⟶ X₂),
      W.functorCategory J f →
        ∀ (φ : c₁.pt ⟶ c₂.pt),
          (∀ (j : J),
              CategoryTheory.CategoryStruct.comp φ (c₂.π.app j) =
                CategoryTheory.CategoryStruct.comp (c₁.π.app j) (f.app j)) →
            W φ) →
    W.IsStableUnderLimitsOfShape J
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.nil_take_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ), (p.take n).Nil ↔ p.Nil ∨ n = 0
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.topEquiv.eq_1 : ∀ {M : Type u_5} [inst : AddZeroClass M],
  AddSubmonoid.topEquiv =
    { toFun := fun x => ↑x, invFun := fun x => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
/-- Generalization of `Finset.sum_comm` to the case when the inner `Finset`s depend on
the outer variable.  -/
Finset.sum_comm' : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] {s : Finset γ} {t : γ → Finset α}
  {t' : Finset α} {s' : α → Finset γ},
  (∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') →
    ∀ {f : γ → α → β}, ∑ x ∈ s, ∑ y ∈ t x, f x y = ∑ y ∈ t', ∑ x ∈ s' y, f x y
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_bound_eq : ∀ {Ω : Type u_1} {a b : ℝ} (f : ℕ → Ω → ℝ) (N : ℕ) (ω : Ω), a < b → MeasureTheory.upperCrossingTime a b f N N ω = N
-- Mathlib.Algebra.BigOperators.Finprod
/-- If `t` is a finite set of pairwise disjoint finite sets, then the product of `f a`
over `a ∈ ⋃₀ t` is the product over `s ∈ t` of the products of `f a` over `a ∈ s`.  -/
finprod_mem_sUnion : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {t : Set (Set α)},
  t.PairwiseDisjoint id →
    t.Finite →
      (∀ x ∈ t, x.Finite) → ∏ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a
-- Mathlib.Data.Nat.ModEq
Nat.modEq_mul_modulus_add_iff : ∀ {n a b c : ℕ}, a ≡ b * n + c [MOD n] ↔ a ≡ c [MOD n]
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- The wide coequalizer morphism in any colimit cocone is an epimorphism.  -/
CategoryTheory.Limits.epi_of_isColimit_parallelFamily : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J]
  {c : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.parallelFamily f)} (i : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.Epi (c.ι.app CategoryTheory.Limits.WalkingParallelFamily.one)
-- Lean.Parser.Extension
/-- Reference to a category.  -/
Lean.Parser.ParserResolution.category : Lean.Name → Lean.Parser.ParserResolution
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.natDegree_basisDivisor_self : ∀ {F : Type u_1} [inst : Field F] {x : F}, (Lagrange.basisDivisor x x).natDegree = 0
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The preimage of a subsemiring along a ring homomorphism is a subsemiring.  -/
Subsemiring.comap : {R : Type u} →
  {S : Type v} → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → (R →+* S) → Subsemiring S → Subsemiring R
-- Mathlib.Topology.Algebra.Group.OpenMapping
AddMonoidHom.isOpenMap_of_sigmaCompact : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] [SigmaCompactSpace G]
  {H : Type u_3} [inst_4 : AddGroup H] [inst_5 : TopologicalSpace H] [BaireSpace H] [T2Space H] [ContinuousAdd H]
  (f : G →+ H), Function.Surjective ⇑f → Continuous ⇑f → IsOpenMap ⇑f
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_compl : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
  MeasurableSet s → MeasureTheory.Integrable f μ → ∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.bicone_π : ∀ {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]
  (b : J), (CategoryTheory.Limits.biproduct.bicone f).π b = CategoryTheory.Limits.biproduct.π f b
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_zero`. -/
ENat.coe_zero : ↑0 = 0
-- Mathlib.Algebra.Order.Group.Defs
/-- Assuming `α` equipped with `LinearOrder` is `CancelCommMonoid` and `IsOrderedMonoid`, it is
also `IsOrderedCancelMonoid`.

TODO: make it an `instance`. To avoid slowdown, it was not an instance when it was submitted. See
https://github.com/leanprover-community/mathlib4/pull/32828.  -/
IsOrderedMonoid.toIsOrderedCancelMonoid' : ∀ {α : Type u} [inst : CancelCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedMonoid α], IsOrderedCancelMonoid α
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.containsThenInsert_snd_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α}
  {b : β a}, (m.containsThenInsert a b).2 = ↑(Std.DHashMap.Internal.Raw₀.containsThenInsert ⟨m, ⋯⟩ a b).2
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.inertiaEquiv_apply_smul : ∀ {M : Type u_1} [inst : Group M] {N : Type u_4} [inst_1 : Group N] {R : Type u_5} [inst_2 : Ring R]
  [inst_3 : MulSemiringAction M R] [inst_4 : MulSemiringAction N R] (I : Ideal R) (e : M ≃* N)
  (he : ∀ (m : M) (x : R), e m • x = m • x) (m : ↥(Ideal.inertia M I)) (x : R), (I.inertiaEquiv e he) m • x = m • x
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
Submodule.IsHomogeneous.mem_iff : ∀ {ιM : Type u_2} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A] [inst_1 : AddCommMonoid M]
  [inst_2 : Module A M] {p : Submodule A M} (ℳ : ιM → σM) [inst_3 : DecidableEq ιM] [inst_4 : SetLike σM M]
  [inst_5 : AddSubmonoidClass σM M] [inst_6 : DirectSum.Decomposition ℳ],
  p.IsHomogeneous ℳ → ∀ {x : M}, x ∈ p ↔ ∀ (i : ιM), ↑(((DirectSum.decompose ℳ) x) i) ∈ p
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator.mk : {α : Type w} →
  {m : Type w → Type w'} → {β : Type w} → ℕ → ℕ → Std.IterM m β → Std.Iterators.Types.StepSizeIterator α m β
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.map_isLeast : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  RightOrdContinuous f → ∀ {s : Set α} {x : α}, IsLeast s x → IsLeast (f '' s) (f x)
-- Init.Data.Bool
Bool.not_bne_self : ∀ (x : Bool), ((!x) != x) = true
-- Mathlib.Analysis.ODE.ExistUnique
/-- **Picard-Lindelöf (Cauchy-Lipschitz) theorem**, differential form. This version shows the
existence of a local flow.  -/
IsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E}
  {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal},
  IsPicardLindelof f t₀ x₀ a r L K →
    ∃ α,
      ∀ x ∈ Metric.closedBall x₀ ↑r,
        α x ↑t₀ = x ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Set.Icc tmin tmax) t
-- Batteries.Classes.Order
Std.LawfulLECmp.ne_gt_iff_le : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [inst : LE α] [Std.LawfulLECmp cmp], cmp x y ≠ Ordering.gt ↔ x ≤ y
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.instIsLocalizedEquivalenceOppositeOpOp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.IsLocalizedEquivalence],
  Φ.op.IsLocalizedEquivalence
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.containsₘ : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → α → Bool
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.instTensorAddUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.AddMonObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.pullbackIsoPullback_hom_fst : ∀ {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (p : CategoryTheory.Limits.pullback f g),
  (↑((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.pullbackIsoPullback f g).hom) p)).1 =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) p
-- Mathlib.Data.WSeq.Productive
Stream'.WSeq.Productive.get?_terminates : ∀ {α : Type u} {s : Stream'.WSeq α} [self : s.Productive] (n : ℕ), (s.get? n).Terminates
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- If `has_image g`, then `has_image (f ≫ g)` when `f` is an isomorphism.  -/
CategoryTheory.Limits.instHasImageCompOfIsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] (g : Y ⟶ Z)
  [CategoryTheory.Limits.HasImage g], CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)
-- Init.Data.Array.Basic
Array.instRepr : {α : Type u} → [Repr α] → Repr (Array α)
-- Mathlib.Algebra.Algebra.Operations
Submodule.comap_op_mul : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (M N : Submodule R Aᵐᵒᵖ),
  Submodule.comap (↑(MulOpposite.opLinearEquiv R)) (M * N) =
    Submodule.comap (↑(MulOpposite.opLinearEquiv R)) N * Submodule.comap (↑(MulOpposite.opLinearEquiv R)) M
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.le_max!_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, t.contains k = true → (cmp k t.max!).isLE = true
-- Mathlib.Analysis.Analytic.Inverse
_private.Mathlib.Analysis.Analytic.Inverse.0.FormalMultilinearSeries.leftInv.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((n : ℕ) → motive n.succ.succ) → motive x
-- Init.Data.BitVec.Lemmas
/-- A `(x : BitVec v)` set to a width `w ≥ v` equals `(w - v)` zeros, followed by `x`.
 -/
BitVec.setWidth_eq_append : ∀ {v : ℕ} {x : BitVec v} {w : ℕ} (h : v ≤ w), BitVec.setWidth w x = BitVec.cast ⋯ (0#(w - v) ++ x)
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.addOrderOf_div_of_gcd_eq_one : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)]
  {m n : ℕ}, 0 < n → m.gcd n = 1 → addOrderOf ↑(↑m / ↑n * p) = n
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- `QuadraticMap.polar` as a bilinear map  -/
QuadraticMap.polarBilin : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → QuadraticMap R M N → LinearMap.BilinMap R M N
-- Std.Data.HashMap.Lemmas
Std.HashMap.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₁ → k ∉ m₁ \ m₂
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
instIsContinuousOpensCarrierMapGrothendieckTopology : ∀ {X Y : TopCat} (f : X ⟶ Y),
  (TopologicalSpace.Opens.map f).IsContinuous (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
/-- The isomorphism expressing the commutation of the functor `unopUnop C : Cᵒᵖᵒᵖ ⥤ C`
with the shift by `n : ℤ`.  -/
CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (n : ℤ) →
        (CategoryTheory.shiftFunctor Cᵒᵖᵒᵖ n).comp (CategoryTheory.unopUnop C) ≅
          (CategoryTheory.unopUnop C).comp (CategoryTheory.shiftFunctor C n)
-- Lean.CoreM
Lean.Elab.async : Lean.Option Bool
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_le_mulIndicator_of_subset : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : One M] {s t : Set α} {f : α → M},
  s ⊆ t → 1 ≤ f → s.mulIndicator f ≤ t.mulIndicator f
-- Init.Prelude
/-- Gadget for marking semi output parameters in type classes.

Semi-output parameters influence the order in which arguments to type class
instances are processed.  Lean determines an order where all non-(semi-)output
parameters to the instance argument have to be figured out before attempting to
synthesize an argument (that is, they do not contain assignable metavariables
created during TC synthesis). This rules out instances such as `[Mul β] : Add
α` (because `β` could be anything). Marking a parameter as semi-output is a
promise that instances of the type class will always fill in a value for that
parameter.

For example, the `Coe` class is defined as:
```
class Coe (α : semiOutParam (Sort u)) (β : Sort v)
```
This means that all `Coe` instances should provide a concrete value for `α`
(i.e., not an assignable metavariable). An instance like `Coe Nat Int` or `Coe
α (Option α)` is fine, but `Coe α Nat` is not since it does not provide a value
for `α`.
 -/
semiOutParam : Sort u → Sort u
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.cm4a : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C] {A B X Y : C}
  (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.WeakEquivalence i]
  [HomotopicalAlgebra.Fibration p], CategoryTheory.HasLiftingProperty i p
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- We say that a set `H : Set (X → α)` of functions is uniformly equicontinuous if the family
`(↑) : ↥H → (X → α)` is uniformly equicontinuous.  -/
Set.UniformEquicontinuous : {α : Type u_6} → {β : Type u_8} → [uα : UniformSpace α] → [uβ : UniformSpace β] → Set (β → α) → Prop
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.instHopfAlgebraObjForgetBialgHomX : {R : Type u} →
  [inst : CommRing R] → {A : CommHopfAlgCat R} → HopfAlgebra R ((CategoryTheory.forget (CommHopfAlgCat R)).obj A)
-- Mathlib.Order.Hom.Lattice
OrderHomClass.coe_to_lattice_hom : ∀ {F : Type u_1} (α : Type u_2) (β : Type u_3) [inst : FunLike F α β] [inst_1 : LinearOrder α] [inst_2 : Lattice β]
  [inst_3 : OrderHomClass F α β] (f : F), ⇑(OrderHomClass.toLatticeHom α β f) = ⇑f