mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Real.Irrational
Irrational.ratCast_add : ∀ (q : ℚ) {x : ℝ}, Irrational x → Irrational (↑q + x)
-- Mathlib.Data.Set.Semiring
SetSemiring.instCanonicallyOrderedAdd : ∀ {α : Type u_1}, CanonicallyOrderedAdd (SetSemiring α)
-- Std.Net.Addr
Std.Net.instDecidableEqIPv4Addr : DecidableEq Std.Net.IPv4Addr
-- Mathlib.Algebra.DirectSum.Finsupp
finsuppLEquivDirectSum_single : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (ι : Type u_1)
  [inst_3 : DecidableEq ι] (i : ι) (m : M),
  ((finsuppLEquivDirectSum R M ι) fun₀ | i => m) = (DirectSum.lof R ι (fun i => M) i) m
-- Mathlib.Algebra.Homology.SingleHomology
/-- The computation of the homology of single complexes, as a natural isomorphism
`single C c j ⋙ homologyFunctor C c j ≅ 𝟭 C`.  -/
HomologicalComplex.homologyFunctorSingleIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {ι : Type u_1} →
          [inst_3 : DecidableEq ι] →
            (c : ComplexShape ι) →
              (j : ι) →
                [inst_4 : CategoryTheory.CategoryWithHomology C] →
                  (HomologicalComplex.single C c j).comp (HomologicalComplex.homologyFunctor C c j) ≅
                    CategoryTheory.Functor.id C
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.π_comp_cokernelIsoOfEq_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasCokernel g]
  (h : f = g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f)
      (CategoryTheory.Limits.cokernelIsoOfEq h).hom =
    CategoryTheory.Limits.cokernel.π g
-- Mathlib.Topology.Algebra.ClopenNhdofOne
/-- Any closed subgroup of a profinite group is the intersection of the open subgroups containing it.
See https://math.stackexchange.com/questions/5023433/closed-subgroups-of-a-compact-topological-group.
 -/
ProfiniteGrp.closedSubgroup_eq_sInf_open : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] (H : ClosedSubgroup G), ↑H = sInf {N | IsOpen ↑N ∧ ↑H ≤ N}
-- Init.Data.Nat.Coprime
Nat.Coprime.coprime_mul_right_right : ∀ {m n k : ℕ}, m.Coprime (n * k) → m.Coprime n
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_bot_le_of_injective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  {I : Ideal R} [inst_3 : RingHomClass F R S], Function.Injective ⇑f → Ideal.comap f ⊥ ≤ I
-- Aesop.Util.Basic
Aesop.PersistentHashSet.toList : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashSet α → List α
-- Lean.Elab.Tactic.Grind.Basic
_private.Lean.Elab.Tactic.Grind.Basic.0.Lean.Elab.Tactic.Grind.evalGrindTactic.eval : Lean.Syntax →
  Lean.Elab.Tactic.Grind.SavedState →
    List (Lean.KeyedDeclsAttribute.AttributeEntry Lean.Elab.Tactic.Grind.GrindTactic) →
      Array Lean.Elab.Tactic.Grind.EvalTacticFailure → Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Lean.Elab.PreDefinition.TerminationMeasure
Lean.Elab.instInhabitedTerminationMeasure.default : Lean.Elab.TerminationMeasure
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- Given two morphisms of sheaves of `R`-modules `f : free ι ⟶ free σ` and `g : free σ ⟶ M`
satisfying `H : f ≫ g = 0` and `IsColimit (CokernelCofork.ofπ g H)`, we obtain
generators of `Presentation M`.  -/
SheafOfModules.generatorsOfIsCokernelFree : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {ι σ : Type u} →
              {M : SheafOfModules R} →
                (f : SheafOfModules.free ι ⟶ SheafOfModules.free σ) →
                  (g : SheafOfModules.free σ ⟶ M) →
                    (H : CategoryTheory.CategoryStruct.comp f g = 0) →
                      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H) →
                        M.GeneratingSections
-- Init.Data.String.Slice
String.Slice.SplitIterator.instIteratorIdSubslice : {ρ : Type} →
  {σ : String.Slice → Type} →
    [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      {pat : ρ} →
        [inst : String.Slice.Pattern.ToForwardSearcher pat σ] →
          {s : String.Slice} → Std.Iterator (String.Slice.SplitIterator pat s) Id s.Subslice
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.haarContent_apply : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G),
  (MeasureTheory.Measure.haar.haarContent K₀) K =
    ↑(have this := ⟨MeasureTheory.Measure.haar.chaar K₀ K, ⋯⟩;
      this)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis.contract_isBasis_union_union : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α},
  M.IsBasis (J ∪ I) (X ∪ I) → Disjoint J I → Disjoint X I → (M.contract I).IsBasis J X
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.map_comp_assoc : ∀ {n : Type u} {S S' S'' : AlgebraicGeometry.Scheme} (f : S ⟶ S') (g : S' ⟶ S'') {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.AffineSpace n S'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.map n (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.map n f)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.map n g) h)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.snd_opProdIsoCoprod_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B] {Z : Cᵒᵖ} (h : Opposite.op A ⨿ Opposite.op B ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd.op
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h
-- Mathlib.Control.EquivFunctor
/-- An `EquivFunctor` is only functorial with respect to equivalences.

To construct an `EquivFunctor`, it suffices to supply just the function `f α → f β` from
an equivalence `α ≃ β`, and then prove the functor laws. It's then a consequence that
this function is part of an equivalence, provided by `EquivFunctor.mapEquiv`.
 -/
EquivFunctor : (Type u₀ → Type u₁) → Type (max (u₀ + 1) u₁)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- `ιInvApp` is the right inverse of `D.ι i` on `U`.  -/
AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasLimits C] (i j : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)),
  CategoryTheory.CategoryStruct.comp (D.diagramOverOpenπ U i)
      (CategoryTheory.CategoryStruct.comp (D.ιInvAppπEqMap U)
        (CategoryTheory.CategoryStruct.comp (D.ιInvApp U) (D.diagramOverOpenπ U j))) =
    D.diagramOverOpenπ U j
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeffLinearEquiv`.

---

Linear equivalence between `SkewMonoidAlgebra k G` and `G →₀ k`.  -/
SkewMonoidAlgebra.toFinsuppLinearEquiv : {k : Type u_1} →
  {G : Type u_2} →
    {S : Type u_3} →
      [inst : Semiring S] → [inst_1 : AddCommMonoid k] → [inst_2 : Module S k] → SkewMonoidAlgebra k G ≃ₗ[S] G →₀ k
-- Mathlib.Order.Hom.Bounded
TopHom.symm_dual_id : ∀ {α : Type u_2} [inst : LE α] [inst_1 : OrderTop α], TopHom.dual.symm (BotHom.id αᵒᵈ) = TopHom.id α
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.move_left_right : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (T : Turing.Tape Γ),
  Turing.Tape.move Turing.Dir.right (Turing.Tape.move Turing.Dir.left T) = T
-- Lean.Elab.Match
/-- Convert a (normalized) pattern encoded as an `Expr` into a `Pattern`.
This method assumes that `e` has been normalized and the explicit and implicit (i.e., metavariables) pattern variables have
already been abstracted and converted back into new free variables.
 -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.toPattern : Lean.Expr → Lean.MetaM Lean.Meta.Match.Pattern
-- Mathlib.Topology.Baire.BaireMeasurable
BaireMeasurableSet.iUnion : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Sort u_3} [Countable ι] {s : ι → Set α},
  (∀ (i : ι), BaireMeasurableSet (s i)) → BaireMeasurableSet (⋃ i, s i)
-- Mathlib.Order.UpperLower.CompleteLattice
/-- Upper sets are order-isomorphic to lower sets under complementation.  -/
upperSetIsoLowerSet : {α : Type u_1} → [inst : LE α] → UpperSet α ≃o LowerSet α
-- Mathlib.CategoryTheory.Subobject.Limits
/-- The underlying object of `kernelSubobject f` is (up to isomorphism!)
the same as the chosen object `kernel f`.  -/
CategoryTheory.Limits.kernelSubobjectIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f) ≅
              CategoryTheory.Limits.kernel f
-- Mathlib.Topology.Covering.Quotient
/-- The action of `G` restricted to the fiber.  -/
IsQuotientCoveringMap.mulActionFiber : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {f : E → X} →
          {G : Type u_3} →
            [inst_2 : Group G] →
              [inst_3 : MulAction G E] → IsQuotientCoveringMap f G → (x : X) → MulAction G ↑(f ⁻¹' {x})
-- Lean.Environment
Lean.instNonemptyEnvironment : Nonempty Lean.Environment
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
OrderIso.mulRight₀_symm_apply : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [inst_2 : MulPosReflectLT G₀] (a : G₀)
  (ha : 0 < a) (x : G₀), (RelIso.symm (OrderIso.mulRight₀ a ha)) x = x * a⁻¹
-- Mathlib.Topology.ContinuousMap.Polynomial
Polynomial.toContinuousMap.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R]
  (p p_1 : Polynomial R), p = p_1 → p.toContinuousMap = p_1.toContinuousMap
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.zero_apply : ∀ (G H : AddGrpCat) (g : ↑G), (CategoryTheory.ConcreteCategory.hom 0) g = 0
-- Init.Data.Vector.Lemmas
Vector.eraseIdx!.eq_1 : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (i : ℕ),
  xs.eraseIdx! i =
    if x : i < n then xs.eraseIdx i x
    else
      have this := { default := xs.pop };
      panicWithPosWithDecl "Init.Data.Vector.Basic" "Vector.eraseIdx!" 395 4 "index out of bounds"
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_injective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R], Function.Injective MonoidAlgebra.coeff
-- Mathlib.Data.Set.Lattice
Set.biInter_eq_iInter : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : (x : α) → x ∈ s → Set β), ⋂ x, ⋂ (h : x ∈ s), t x h = ⋂ x, t ↑x ⋯
-- Init.Data.Int.DivMod.Bootstrap
Int.emod_pos_of_not_dvd : ∀ {a b : ℤ}, ¬a ∣ b → a = 0 ∨ 0 < b % a
-- Mathlib.Probability.Distributions.Uniform
MeasureTheory.pdf.IsUniform.isProbabilityMeasure : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} {x : MeasurableSpace Ω}
  {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E},
  μ s ≠ 0 → μ s ≠ ⊤ → MeasureTheory.pdf.IsUniform X s ℙ μ → MeasureTheory.IsProbabilityMeasure ℙ
-- Mathlib.Order.Monotone.Defs
/-- A function `f` is antitone if `a ≤ b` implies `f b ≤ f a`.  -/
Antitone : {α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → Prop
-- Std.Time.Duration
/-- Nanosecond span that ranges from -999999999 and 999999999
 -/
Std.Time.Duration.nano : Std.Time.Duration → Std.Time.Nanosecond.Span
-- Mathlib.Algebra.Order.Quantale
AddQuantale.mk : {α : Type u_1} → [inst : AddSemigroup α] → [inst_1 : CompleteLattice α] → [inst_2 : IsAddQuantale α] → AddQuantale α
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getVar : Lean.Grind.Linarith.Var → Lean.Meta.Grind.Arith.Linear.LinearM Lean.Expr
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_univ_left : ∀ {G : Type u_1} [inst : Group G] {S : Set G}, Subgroup.IsComplement Set.univ S ↔ ∃ g, S = {g}
-- Init.Data.Int.DivMod.Bootstrap
Int.mul_ediv_self_le : ∀ {x k : ℤ}, k ≠ 0 → k * (x / k) ≤ x
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The maximum of a measurable function is greater than its integral.  -/
MeasureTheory.exists_lintegral_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal}
  [MeasureTheory.IsProbabilityMeasure μ], ∫⁻ (a : α), f a ∂μ ≠ ⊤ → ∃ x, ∫⁻ (a : α), f a ∂μ ≤ f x
-- Mathlib.Computability.Partrec
Partrec.eq_1 : ∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] (f : α →. σ),
  Partrec f = Nat.Partrec fun n => (↑(Encodable.decode n)).bind fun a => Part.map Encodable.encode (f a)
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_add_coeff_mul : ∀ {R : Type u} [inst : Semiring R] (f g : Polynomial R),
  (f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.coe_comp : ∀ {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X}
  (f' : G' →g G'') (f : G →g G'), ⇑(f'.comp f) = ⇑f' ∘ ⇑f
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.isSymm_dynEntourage : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {n : ℕ} [U.IsSymm], (Dynamics.dynEntourage T U n).IsSymm
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.functorExtension₂_obj_obj_X : ∀ (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] (X : CategoryTheory.Functor C D)
  (P : CategoryTheory.Idempotents.Karoubi C),
  (((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).obj P).X = X.obj P.X
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.succ_aleph0 : Order.succ Cardinal.aleph0 = Cardinal.aleph 1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.boundariesToCycles₂_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x : ↥(groupHomology.boundaries₂ A)),
  ↑((groupHomology.boundariesToCycles₂ A) x) = ↑x
-- Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
/-- The **Turán density** of a simple graph `H` is the limit of `extremalNumber n H / n.choose 2`
as `n` approaches `∞`.

See `SimpleGraph.tendsto_turanDensity` for proof of existence.  -/
SimpleGraph.turanDensity : {W : Type u_1} → SimpleGraph W → ℝ
-- Init.Data.SInt.Lemmas
ISize.toInt8_ofInt : ∀ {n : ℤ}, (ISize.ofInt n).toInt8 = Int8.ofInt n
-- Mathlib.Topology.Order.IntermediateValue
Continuous.image_Icc_of_strictMono : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ}, Continuous f → StrictMono f → f '' Set.Icc a b = Set.Icc (f a) (f b)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.stdSimplex.facePairIso.congr_simp : ∀ {n : ℕ} (i j : Fin (n + 1)) (hij : i < j), SSet.stdSimplex.facePairIso i j hij = SSet.stdSimplex.facePairIso i j hij
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toList_insert!_perm : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : BEq α]
  [Std.TransOrd α] [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {k : α} {v : β},
      (Std.DTreeMap.Internal.Impl.Const.toList (Std.DTreeMap.Internal.Impl.insert! k v t)).Perm
        ((k, v) :: List.filter (fun x => decide ¬(k == x.1) = true) (Std.DTreeMap.Internal.Impl.Const.toList t))
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- A monoid object as a bimodule over itself.  -/
Bimod.regular : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (A : CategoryTheory.Mon C) → Bimod A A
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
EisensteinSeries.eisensteinSeriesSIF.eq_1 : ∀ {N : ℕ} (a : Fin 2 → ZMod N) (k : ℤ),
  EisensteinSeries.eisensteinSeriesSIF a k = { toFun := eisensteinSeries a k, slash_action_eq' := ⋯ }
-- Init.Data.UInt.Lemmas
USize.toUInt8_mod_of_dvd : ∀ (a b : USize), b.toNat ∣ 256 → (a % b).toUInt8 = a.toUInt8 % b.toUInt8
-- Mathlib.LinearAlgebra.RootSystem.OfBilinear
/-- The root pairing given by all reflective vectors for a bilinear form.  -/
RootPairing.ofBilinear : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          [Module.IsReflexive R M] →
            (B : M →ₗ[R] M →ₗ[R] R) →
              B.Nondegenerate → B.IsSymm → IsRegular 2 → RootPairing (↑{x | B.IsReflective x}) R M (Module.Dual R M)
-- Mathlib.GroupTheory.Torsion
neg_one_mem_torsion : ∀ {M : Type u_3} [inst : CommMonoid M] [inst_1 : HasDistribNeg M], -1 ∈ CommMonoid.torsion M
-- Mathlib.Data.Nat.Bits
Nat.zero_bits : Nat.bits 0 = []
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.monoid.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Monoid G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffMul I' n G], ContMDiffMap.monoid = Function.Injective.monoid DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.χ`.

---

`h.χ m` is the characteristic map of monomorphism `m` given by the bijection `h.homEquiv`.  -/
CategoryTheory.Classifier.SubobjectRepresentableBy.χ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} → CategoryTheory.SubobjectRepresentableBy Ω → {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- the nondegenerate simplex  -/
SSet.prodStdSimplex.pairingCore.Type₁.x : {m : ℕ} →
  {k : Fin (m + 1)} →
    {n : ℕ} → SSet.prodStdSimplex.pairingCore.Type₁ k n → ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
_private.Mathlib.Combinatorics.SimpleGraph.Bipartite.0.SimpleGraph.bipartiteDoubleCover.match_1.eq_3 : ∀ {V : Type u_1} (motive : V ⊕ V → V ⊕ V → Sort u_2) (x x_1 : V ⊕ V)
  (h_1 : (v' w' : V) → motive (Sum.inl v') (Sum.inr w')) (h_2 : (v' w' : V) → motive (Sum.inr v') (Sum.inl w'))
  (h_3 : (x x_2 : V ⊕ V) → motive x x_2),
  (∀ (v' w' : V), x = Sum.inl v' → x_1 = Sum.inr w' → False) →
    (∀ (v' w' : V), x = Sum.inr v' → x_1 = Sum.inl w' → False) →
      (match x, x_1 with
        | Sum.inl v', Sum.inr w' => h_1 v' w'
        | Sum.inr v', Sum.inl w' => h_2 v' w'
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.mk_eq_one : ∀ {z : ℂ} (hz : ‖z‖ ≤ 1), Complex.UnitClosedDisc.mk z hz = 1 ↔ z = 1
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.insert : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α},
  MeasurableSet s → ∀ (a : α), MeasurableSet (insert a s)
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.instCoeQuotientAddSubgroup.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α},
  QuotientAddGroup.instCoeQuotientAddSubgroup = { coe := QuotientAddGroup.mk }
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → t.get! t.max! = t.max!
-- Mathlib.Order.KrullDimension
Order.height.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Order.height a = ⨆ p, ⨆ (_ : RelSeries.last p ≤ a), ↑p.length
-- Mathlib.Order.SetNotation
iInf.eq_1 : ∀ {α : Type u} {ι : Sort v} [inst : InfSet α] (s : ι → α), iInf s = sInf (Set.range s)
-- Mathlib.Topology.PartialHomeomorph.Defs
/-- Two partial homeomorphisms are equal when they have equal `toFun`, `invFun` and `source`.
It is not sufficient to have equal `toFun` and `source`, as this only determines `invFun` on
the target. This would only be true for a weaker notion of equality, arguably the right one,
called `EqOnSource`.  -/
PartialHomeomorph.ext : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e e' : PartialHomeomorph X Y),
  (∀ (x : X), ↑e x = ↑e' x) → (∀ (x : Y), ↑e.symm x = ↑e'.symm x) → e.source = e'.source → e = e'
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.instMonoidalUnmopFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → (CategoryTheory.unmopFunctor C).Monoidal
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If a set of functions is equicontinuous at some `x₀`, its closure for the product topology is
also equicontinuous at `x₀`.  -/
Set.EquicontinuousAt.closure : ∀ {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {A : Set (X → α)} {x₀ : X},
  A.EquicontinuousAt x₀ → (closure A).EquicontinuousAt x₀
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The discriminant `Δ` of a Weierstrass curve. If `R` is a field, then this polynomial vanishes
if and only if the cubic curve cut out by this equation is singular. Sometimes only defined up to
sign in the literature; we choose the sign used by the LMFDB. For more discussion, see
[the LMFDB page on discriminants](https://www.lmfdb.org/knowledge/show/ec.discriminant).  -/
WeierstrassCurve.Δ : {R : Type u} → [CommRing R] → WeierstrassCurve R → R
-- Mathlib.RingTheory.IsTensorProduct
/-- Given a bilinear map `f : M₁ →ₗ[R] M₂ →ₗ[R] M`, `IsTensorProduct f` means that
`M` is the tensor product of `M₁` and `M₂` via `f`.
This is defined by requiring the lift `M₁ ⊗[R] M₂ → M` to be bijective.
 -/
IsTensorProduct : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M₁ : Type u_2} →
      {M₂ : Type u_3} →
        {M : Type u_4} →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : Module R M₁] → [inst_5 : Module R M₂] → [inst_6 : Module R M] → (M₁ →ₗ[R] M₂ →ₗ[R] M) → Prop
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformly.piProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β]
  {F : ι → α → β} {f : α → β} {p : Filter ι} [inst_2 : UniformSpace γ] {G : ι → α → γ} {g : α → γ},
  TendstoLocallyUniformly F f p →
    TendstoLocallyUniformly G g p → TendstoLocallyUniformly (fun n => Function.prod (F n) (G n)) (Function.prod f g) p
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveHypothesisBundle.mk : Array String →
  Array Lean.FVarId →
    Lean.Widget.CodeWithInfos →
      Option Lean.Widget.CodeWithInfos →
        Option Bool → Option Bool → Option Bool → Option Bool → Lean.Widget.InteractiveHypothesisBundle
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.coe_sup : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : SemilatticeSup β]
  [inst_3 : ContinuousSup β] (f g : C(α, β)), ⇑(f ⊔ g) = ⇑f ⊔ ⇑g