mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.isLink_mono : ∀ {α : Type u_1} {β : Type u_2} {H G : Graph α β}, H.IsSubgraph G → ∀ ⦃e : β⦄ ⦃x y : α⦄, H.IsLink e x y → G.IsLink e x y
-- Mathlib.Probability.Process.Predictable
_private.Mathlib.Probability.Process.Predictable.0.MeasureTheory.IsStronglyPredictable.of_measurable_add_one.match_1_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nullMeasurableSet_le : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [SecondCountableTopology α] [OrderClosedTopology α]
  {μ : MeasureTheory.Measure δ} {f g : δ → α},
  AEMeasurable f μ → AEMeasurable g μ → MeasureTheory.NullMeasurableSet {a | f a ≤ g a} μ
-- Mathlib.CategoryTheory.Shift.Localization
/-- This is the commutation of a functor `G` to shifts by an additive monoid `M` when
`e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G` is an isomorphism, `Φ` is a localizer morphism and
`L₁` is a localization functor. We assume that all categories involved
are equipped with shifts and that `L₁`, `L₂` and `Φ.functor` commute to them.  -/
CategoryTheory.LocalizerMorphism.commShift : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
              (M : Type u_3) →
                [inst_2 : AddMonoid M] →
                  [inst_3 : CategoryTheory.HasShift C₁ M] →
                    [inst_4 : CategoryTheory.HasShift C₂ M] →
                      [Φ.functor.CommShift M] →
                        {D₁ : Type u_4} →
                          {D₂ : Type u_5} →
                            [inst_6 : CategoryTheory.Category.{v_3, u_4} D₁] →
                              [inst_7 : CategoryTheory.Category.{v_4, u_5} D₂] →
                                (L₁ : CategoryTheory.Functor C₁ D₁) →
                                  [L₁.IsLocalization W₁] →
                                    (L₂ : CategoryTheory.Functor C₂ D₂) →
                                      [inst_9 : CategoryTheory.HasShift D₁ M] →
                                        [inst_10 : CategoryTheory.HasShift D₂ M] →
                                          [L₁.CommShift M] →
                                            [L₂.CommShift M] →
                                              (G : CategoryTheory.Functor D₁ D₂) →
                                                (Φ.functor.comp L₂ ≅ L₁.comp G) → G.CommShift M
-- Mathlib.Analysis.Calculus.Rademacher
/-- *Rademacher's theorem*: a function between finite-dimensional real vector spaces which is
Lipschitz on a set is differentiable almost everywhere in this set.  -/
LipschitzOnWith.ae_differentiableWithinAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F] {C : NNReal} {s : Set E}
  {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [μ.IsAddHaarMeasure] {f : E → F},
  LipschitzOnWith C f s → MeasurableSet s → ∀ᵐ (x : E) ∂μ.restrict s, DifferentiableWithinAt ℝ f s x
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.mem_specialOrthogonalGroup_iff : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {A : Matrix n n R},
  A ∈ Matrix.specialOrthogonalGroup n R ↔ A ∈ Matrix.orthogonalGroup n R ∧ A.det = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_insert_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m.WF → ∀ {k : α} {v : β}, Std.DHashMap.Raw.Const.get! (m.insert k v) k = v
-- Mathlib.RingTheory.KrullDimension.Polynomial
Polynomial.ringKrullDim_le : ∀ {R : Type u_1} [inst : CommRing R], ringKrullDim (Polynomial R) ≤ 2 * ringKrullDim R + 1
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_apply_ite_of_false : ∀ {ι : Type u_1} {M : Type u_3} {γ : Type u_5} {s : Finset ι} [inst : AddCommMonoid M] {p : ι → Prop}
  [inst_1 : DecidablePred p] (f g : ι → γ) (k : γ → M),
  (∀ x ∈ s, ¬p x) → ∑ x ∈ s, k (if p x then f x else g x) = ∑ x ∈ s, k (g x)
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
/-- The spectral object attached to an object `X : C` in a category
equipped with a t-structure, as a functor `C ⥤ SpectralObject C EInt`.  -/
CategoryTheory.Triangulated.TStructure.spectralObjectFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C →
                [CategoryTheory.IsTriangulated C] →
                  CategoryTheory.Functor C (CategoryTheory.Triangulated.SpectralObject C EInt)
-- Lean.Elab.DeclModifiers
Lean.Elab.instInhabitedComputeKind : Inhabited Lean.Elab.ComputeKind
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is disjoint to `t`.  -/
SimpleGraph.isBipartiteWith_neighborFinset_disjoint' : ∀ {V : Type u_1} {w : V} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype ↑(G.neighborSet w)],
  G.IsBipartiteWith ↑s ↑t → w ∈ t → Disjoint (G.neighborFinset w) t
-- Batteries.Data.List.Basic
List.sections_eq_sectionsTR : @List.sections = @List.sectionsTR
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafAdjunction_homEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : CategoryTheory.Functor Cᵒᵖ A} {M : A}
  (f : P ⟶ Φ.skyscraperPresheaf M),
  (Φ.skyscraperPresheafAdjunction.homEquiv P M).symm f = Φ.skyscraperPresheafHomEquiv.symm f
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.rangeS_le : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  (algebraMap R A).rangeS ≤ S.toSubsemiring
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.mk.injEq : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Ring : Type w)
  [commRing : CommRing Ring] [algebra₁ : Algebra R Ring] [algebra₂ : Algebra Ring S]
  [isScalarTower : IsScalarTower R Ring S] (σ : S → Ring) (algebraMap_σ : ∀ (x : S), (algebraMap Ring S) (σ x) = x)
  (Ring_1 : Type w) (commRing_1 : CommRing Ring_1) (algebra₁_1 : Algebra R Ring_1) (algebra₂_1 : Algebra Ring_1 S)
  (isScalarTower_1 : IsScalarTower R Ring_1 S) (σ_1 : S → Ring_1)
  (algebraMap_σ_1 : ∀ (x : S), (algebraMap Ring_1 S) (σ_1 x) = x),
  ({ Ring := Ring, commRing := commRing, algebra₁ := algebra₁, algebra₂ := algebra₂, isScalarTower := isScalarTower,
        σ := σ, algebraMap_σ := algebraMap_σ } =
      { Ring := Ring_1, commRing := commRing_1, algebra₁ := algebra₁_1, algebra₂ := algebra₂_1,
        isScalarTower := isScalarTower_1, σ := σ_1, algebraMap_σ := algebraMap_σ_1 }) =
    (Ring = Ring_1 ∧ commRing ≍ commRing_1 ∧ algebra₁ ≍ algebra₁_1 ∧ algebra₂ ≍ algebra₂_1 ∧ σ ≍ σ_1)
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.PInfty_f_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℕ)
  {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n })) (AlgebraicTopology.DoldKan.PInfty.f n) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (f.app (Opposite.op { len := n }))
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- A class of objects which have a left dual.  -/
CategoryTheory.HasLeftDual : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.MonoidalCategory C] → C → Type (max u₁ v₁)
-- Init.Data.SInt.Basic
instModInt8 : Mod Int8
-- Mathlib.Data.EReal.Basic
EReal.natCast_ne_top : ∀ (n : ℕ), ↑n ≠ ⊤
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.decompAffineEquiv.eq_1 : ∀ (R : Type u_1) (S : Type u_2) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [inst : Ring S] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : IsTopologicalAddGroup V]
  [inst_6 : AddCommGroup W] [inst_7 : Module R W] [inst_8 : TopologicalSpace W] [inst_9 : Module S W]
  [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : AddTorsor W Q]
  [inst_13 : TopologicalSpace Q] [inst_14 : IsTopologicalAddGroup W] [inst_15 : IsTopologicalAddTorsor Q],
  ContinuousAffineMap.decompAffineEquiv R S V Q =
    { toEquiv := ContinuousAffineMap.decompEquiv R V Q, linear := ContinuousAffineMap.decompLinearEquiv R S V W,
      map_vadd' := ⋯ }
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- The affine homeomorphism given by reflection about the point `x`.
This is `Equiv.pointReflection` as a `ContinuousAffineEquiv`.  -/
ContinuousAffineEquiv.pointReflection : (k : Type u_1) →
  {P₁ : Type u_2} →
    {V₁ : Type u_6} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] →
          [inst_2 : Module k V₁] →
            [inst_3 : AddTorsor V₁ P₁] →
              [inst_4 : TopologicalSpace P₁] →
                [inst_5 : TopologicalSpace V₁] → [IsTopologicalAddTorsor P₁] → P₁ → P₁ ≃ᴬ[k] P₁
-- Std.Data.TreeMap.Basic
Std.TreeMap.instLawfulSingletonProd : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, LawfulSingleton (α × β) (Std.TreeMap α β cmp)
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.objEquiv.eq_1 : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C),
  CategoryTheory.Localization.Construction.objEquiv W =
    { toFun := W.Q.obj, invFun := fun X => X.as.obj, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.basisOfBasisLeft_apply : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  (H : A.LinearDisjoint ↥B) (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤) {ι : Type u_1} (b : Module.Basis ι F ↥A) (i : ι),
  (H.basisOfBasisLeft H' b) i = (algebraMap (↥A) E) (b i)
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
/-- A typeclass carrying a choice of lift of a 1-morphism from `B` to `FreeBicategory B`.  -/
Mathlib.Tactic.BicategoryCoherence.LiftHom : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b : B} → (a ⟶ b) → Type (max u v)
-- Mathlib.Data.Seq.Defs
Stream'.Seq.ofList_nil : ∀ {α : Type u}, ↑[] = Stream'.Seq.nil
-- Init.Data.UInt.Bitwise
USize.toUInt8_shiftLeft_mod : ∀ (a b : USize), (a <<< (b % 8)).toUInt8 = a.toUInt8 <<< b.toUInt8
-- Mathlib.GroupTheory.Congruence.Defs
Con.one : {M : Type u_1} → [inst : Mul M] → [One M] → (c : Con M) → One c.Quotient
-- Mathlib.Probability.Kernel.Defs
/-- A constant `C : ℝ≥0∞` such that `C < ∞` for a finite kernel
(`ProbabilityTheory.IsFiniteKernel.bound_lt_top κ`) and for all `a : α` and `s : Set β`,
`κ a s ≤ C` (`ProbabilityTheory.Kernel.measure_le_bound κ a s`).  -/
ProbabilityTheory.Kernel.bound : {α : Type u_1} →
  {β : Type u_2} → {mα : MeasurableSpace α} → {mβ : MeasurableSpace β} → ProbabilityTheory.Kernel α β → ENNReal
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_awayMap_eq_aux : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {e : ι} {f g : A} (hg : g ∈ 𝒜 e) {x : A} (hx : x = f * g)
  (a : HomogeneousLocalization.Away 𝒜 f),
  HomogeneousLocalization.val ((HomogeneousLocalization.awayMap 𝒜 hg hx) a) =
    (HomogeneousLocalization.awayMapAux✝ 𝒜 ⋯) a
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.Forall₂.sum_le_sum : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddRightMono M] [AddLeftMono M] {l₁ l₂ : List M},
  List.Forall₂ (fun x1 x2 => x1 ≤ x2) l₁ l₂ → l₁.sum ≤ l₂.sum
-- Mathlib.Algebra.Module.Torsion.Basic
Module.instQuotientIdealSpanSubmoduleHSMulSetTop : {R : Type u_1} →
  (M : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (s : Set R) → Module (R ⧸ Ideal.span s) (M ⧸ s • ⊤)
-- Init.Data.SInt.Bitwise
Int64.not_neg_one : ~~~(-1) = 0
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Ordinal.cof_eq_one_iff`. -/
Ordinal.cof_eq_one_iff_is_succ : ∀ {o : Ordinal.{u_1}}, o.cof = 1 ↔ o ∈ Set.range Order.succ
-- Mathlib.Order.Bounded
Set.unbounded_lt_Ioi : ∀ {α : Type u_1} [inst : SemilatticeSup α] [NoMaxOrder α] (a : α), Set.Unbounded (fun x1 x2 => x1 < x2) (Set.Ioi a)
-- Mathlib.NumberTheory.Divisors
Nat.prod_properDivisors_prime_pow : ∀ {α : Type u_1} [inst : CommMonoid α] {k p : ℕ} {f : ℕ → α},
  Nat.Prime p → ∏ x ∈ (p ^ k).properDivisors, f x = ∏ x ∈ Finset.range k, f (p ^ x)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.MultispanIndex.toLinearOrderMultispanIso.match_1.splitter : {ι : Type u_1} →
  [inst : LinearOrder ι] →
    (motive :
        CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι) → Sort u_2) →
      (i : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι)) →
        ((a : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).L) →
            motive (CategoryTheory.Limits.WalkingMultispan.left a)) →
          ((a : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).R) →
              motive (CategoryTheory.Limits.WalkingMultispan.right a)) →
            motive i
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryGT? : {α : Type u} → {β : Type v} → [Ord α] → α → (Std.DTreeMap.Internal.Impl α fun x => β) → Option (α × β)
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.bijective_restrictDomain : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E]
  (R : Type u_1) (L : Type u_2) [inst_4 : CommSemiring R] [inst_5 : Algebra R F] [inst_6 : Algebra R E]
  [inst_7 : Field L] [PerfectField L] [inst_9 : Algebra R L] [inst_10 : IsScalarTower R F E],
  Function.Bijective (AlgHom.domRestrict F)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.apply_inf_eq_inf_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : OrderTop α]
  [inst_2 : SemilatticeInf γ] [inst_3 : OrderTop γ] {s : Finset β} {f : β → α} (g : α → γ),
  (∀ (x y : α), g (x ⊓ y) = g x ⊓ g y) → g ⊤ = ⊤ → g (s.inf f) = s.inf (g ∘ f)
-- Mathlib.Data.PFun
PFun.compl_dom_subset_core : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β), f.Domᶜ ⊆ f.core s
-- Mathlib.CategoryTheory.Preadditive.FunctorCategory
CategoryTheory.NatTrans.app_sum : ∀ {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 D]
  {F G : CategoryTheory.Functor C D} {ι : Type u_3} (s : Finset ι) (X : C) (α : ι → (F ⟶ G)),
  (∑ i ∈ s, α i).app X = ∑ i ∈ s, (α i).app X
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.isScalar : Lean.IR.IRType → Bool
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Functoriality of `OverArrows η s` in `η`.  -/
CategoryTheory.OverPresheafAux.OverArrows.map₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A F G : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {η : F ⟶ A} →
        {μ : G ⟶ A} →
          {X : C} →
            {s : CategoryTheory.yoneda.obj X ⟶ A} →
              CategoryTheory.OverPresheafAux.OverArrows η s →
                (ε : F ⟶ G) → CategoryTheory.CategoryStruct.comp ε μ = η → CategoryTheory.OverPresheafAux.OverArrows μ s
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.quot_mk_eq_coe : ∀ {α : Type u_1} {β : Type u_2} (l : Filter α) (f : α → β), Quot.mk (⇑(l.germSetoid β)) f = ↑f
-- Mathlib.Logic.Function.Basic
Function.instIsPartialOrderSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [IsPartialOrder α r], IsPartialOrder α (Function.swap r)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.eval_or : ∀ {w : ℕ}, Std.Tactic.BVDecide.BVBinOp.or.eval = fun x1 x2 => x1 ||| x2
-- Lean.ResolveName
Lean.AliasEntry : Type
-- Mathlib.Topology.Separation.Basic
nhds_injective : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X], Function.Injective nhds
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_inl : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β], UniformContinuous Sum.inl
-- Mathlib.Logic.IsEmpty.Basic
Function.Bijective.of_isEmpty : ∀ {α : Type u_4} {β : Type u_5} (f : α → β) [IsEmpty β], Function.Bijective f
-- Init.Data.Int.DivMod.Bootstrap
Int.dvd_of_emod_eq_zero : ∀ {a b : ℤ}, b % a = 0 → a ∣ b
-- Mathlib.RingTheory.Ideal.Maps
/-- If `f : R ≃+* S` is a ring isomorphism and `I : Ideal R`, then `map f I = comap f.symm I`.  -/
Ideal.map_comap_of_equiv : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R} (f : R ≃+* S),
  Ideal.map (↑f) I = Ideal.comap f.symm I
-- Lean.Data.Json.Parser
Lean.Json.Parser.any : Std.Internal.Parsec.String.Parser Lean.Json
-- Mathlib.Algebra.Group.End
Equiv.Perm.sumCongr_swap_one : ∀ {α : Type u_7} {β : Type u_8} [inst : DecidableEq α] [inst_1 : DecidableEq β] (i j : α),
  (Equiv.swap i j).sumCongr 1 = Equiv.swap (Sum.inl i) (Sum.inl j)
-- Mathlib.Algebra.Prime.Lemmas
Prime.pow_dvd_of_dvd_mul_left : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p a b : M},
  Prime p → ∀ (n : ℕ), ¬p ∣ a → p ^ n ∣ a * b → p ^ n ∣ b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget.rhs : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {w : ℕ} →
          (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget aig w) → aig.RefVec self.n
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.tensor : {C : Type u} → {W X Y Z : CategoryTheory.FreeMonoidalCategory C} → W.Hom Y → X.Hom Z → (W.tensor X).Hom (Y.tensor Z)
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxi.Iterator.instIteratorLoop.loop_eq_wf : ∀ {α : Type u} {n : Type u → Type u_1} [inst : Std.PRange.UpwardEnumerable α]
  [inst_1 : Std.PRange.LawfulUpwardEnumerable α] [inst_2 : Monad n] [LawfulMonad n] {γ : Type u}
  {LargeEnough : α → Prop} {hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b}
  {next : α} {hn : LargeEnough next} {acc : γ} (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxi.Iterator α) Id Pl)
  (f : (out : α) → LargeEnough out → (c : γ) → n (Subtype (Pl out c))),
  Std.Rxi.Iterator.instIteratorLoop.loop γ Pl LargeEnough hl acc next hn f =
    Std.Rxi.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl acc next hn f
-- Mathlib.Data.ENat.Basic
ENat.top_sub_natCast : ∀ (a : ℕ), ⊤ - ↑a = ⊤
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- Given an invariant measure then it gives the same mass to measurable sets with
compact closure as any other invariant measure, up to the scalar `addHaarScalarFactor μ' μ`.

Auxiliary lemma in the proof of the more general
`measure_isAddInvariant_eq_smul_of_isCompact_closure`, which removes the
measurability assumption.  -/
MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure_of_measurableSet : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsAddLeftInvariant]
  {s : Set G}, MeasurableSet s → IsCompact (closure s) → μ' s = μ'.addHaarScalarFactor μ • μ s
-- Mathlib.GroupTheory.Coxeter.Basic
_private.Mathlib.GroupTheory.Coxeter.Basic.0.CoxeterSystem.restrictUnit.congr_simp : ∀ {B : Type u_1} {M M_1 : CoxeterMatrix B} (e_M : M = M_1) {G : Type u_5} [inst : Monoid G] {f f_1 : B → G}
  (e_f : f = f_1) (hf : M.IsLiftable f) (i i_1 : B),
  i = i_1 → CoxeterSystem.restrictUnit✝ hf i = CoxeterSystem.restrictUnit✝ ⋯ i_1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → γ a} {k : α}, k ∈ Std.ExtDHashMap.map f m ↔ k ∈ m
-- Mathlib.Algebra.Order.Hom.Basic
NonnegHomClass.mk : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : Zero β] [inst_1 : LE β]
  [inst_2 : FunLike F α β], (∀ (f : F) (a : α), 0 ≤ f a) → NonnegHomClass F α β
-- Mathlib.RingTheory.EuclideanDomain
EuclideanDomain.dvd_or_coprime : ∀ {α : Type u_1} [inst : EuclideanDomain α] (x y : α), Irreducible x → x ∣ y ∨ IsCoprime x y
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.mem_posFittingCompOf : ∀ (R : Type u_2) {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (x : L) (m : M),
  m ∈ LieModule.posFittingCompOf R M x ↔ ∀ (k : ℕ), ∃ n, ((LieModule.toEnd R L M) x ^ k) n = m
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressEnd.mk.inj : ∀ {kind : String} {message? : Option String} {kind_1 : String} {message?_1 : Option String},
  { kind := kind, message? := message? } = { kind := kind_1, message? := message?_1 } →
    kind = kind_1 ∧ message? = message?_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.find?_toArray_eq_none_iff_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, Array.find? (fun x => cmp x.1 k == Ordering.eq) (Std.DTreeMap.Raw.Const.toArray t) = none ↔ k ∉ t
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- If `F` preserves the limit of the pair `(A, B)`, then the binary fan given by
`(F.map fst A B, F.map (snd A B))` is a limit cone.  -/
CategoryTheory.CartesianMonoidalCategory.isLimitCartesianMonoidalCategoryOfPreservesLimits : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          (F : CategoryTheory.Functor C D) →
            (A B : C) →
              [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F] →
                CategoryTheory.Limits.IsLimit
                  (CategoryTheory.Limits.BinaryFan.mk (F.map (CategoryTheory.SemiCartesianMonoidalCategory.fst A B))
                    (F.map (CategoryTheory.SemiCartesianMonoidalCategory.snd A B)))
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S.eq_2 : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.S R 1 = Polynomial.X