mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Action.Continuous
/-- Continuous version of `Equivalence.mapAction`.  -/
CategoryTheory.Equivalence.mapContAction : {V : Type u_5} →
  {W : Type u_6} →
    [inst : CategoryTheory.Category.{v_2, u_5} V] →
      {FV : V → V → Type u_7} →
        {CV : V → Type u_8} →
          [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory V FV] →
              [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
                [inst_4 : CategoryTheory.Category.{v_3, u_6} W] →
                  {FW : W → W → Type u_9} →
                    {CW : W → Type u_10} →
                      [inst_5 : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] →
                        [inst_6 : CategoryTheory.ConcreteCategory W FW] →
                          [inst_7 : CategoryTheory.HasForget₂ W TopCat] →
                            (G : Type u_11) →
                              [inst_8 : Monoid G] →
                                [inst_9 : TopologicalSpace G] →
                                  (E : V ≌ W) →
                                    (∀ (X : ContAction V G), ((E.functor.mapAction G).obj X.obj).IsContinuous) →
                                      (∀ (X : ContAction W G), ((E.inverse.mapAction G).obj X.obj).IsContinuous) →
                                        (ContAction V G ≌ ContAction W G)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.tensorObj.zero_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} [inst_3 : CategoryTheory.AddMonObj M]
  [inst_4 : CategoryTheory.AddMonObj N],
  CategoryTheory.AddMonObj.zero =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero CategoryTheory.AddMonObj.zero)
-- Mathlib.RingTheory.EuclideanDomain
isCoprime_div_gcd_div_gcd : ∀ {R : Type u_1} [inst : EuclideanDomain R] [inst_1 : GCDMonoid R] {p q : R},
  q ≠ 0 → IsCoprime (p / gcd p q) (q / gcd p q)
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.instFreeOfSubsingleton : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M] [Subsingleton (CommRing.Pic R)], Module.Free R M
-- Mathlib.GroupTheory.Finiteness
AddGroup.FG.mk : ∀ {H : Type u_4} [inst : AddGroup H], ⊤.FG → AddGroup.FG H
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit'.match_3.eq_6 : ∀ (motive : Lean.Expr → Sort u_1) (u : Lean.Level)
  (h_1 : (name : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const name us))
  (h_2 : (f x : Lean.Expr) → motive (f.app x))
  (h_3 :
    (binderName : Lean.Name) →
      (ty body : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName ty body binderInfo))
  (h_4 : Unit → motive (Lean.Expr.sort Lean.Level.zero)) (h_5 : (a : Lean.Level) → motive (Lean.Expr.sort a.succ))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (x : Lean.Expr) → motive x),
  (u = Lean.Level.zero → False) →
    (∀ (a : Lean.Level), u = a.succ → False) →
      (match Lean.Expr.sort u with
        | Lean.Expr.const name us => h_1 name us
        | f.app x => h_2 f x
        | Lean.Expr.forallE binderName ty body binderInfo => h_3 binderName ty body binderInfo
        | Lean.Expr.sort Lean.Level.zero => h_4 ()
        | Lean.Expr.sort a.succ => h_5 a
        | Lean.Expr.sort u => h_6 u
        | x => h_7 x) =
        h_6 u
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.logMap_expMap : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.realSpace K},
  NumberField.mixedEmbedding.norm
        (NumberField.mixedEmbedding.mixedSpaceOfRealSpace (↑NumberField.mixedEmbedding.fundamentalCone.expMap x)) =
      1 →
    NumberField.mixedEmbedding.logMap
        (NumberField.mixedEmbedding.mixedSpaceOfRealSpace (↑NumberField.mixedEmbedding.fundamentalCone.expMap x)) =
      fun w => x ↑w
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.completeBipartiteGraph_Adj : ∀ (V : Type u_1) (W : Type u_2) (v w : V ⊕ W),
  (Digraph.completeBipartiteGraph V W).Adj v w =
    (v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_congr : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F),
  (∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) →
    MeasureTheory.FinMeasAdditive μ T →
      ∀ {f g : ↥(α →₁ₛ[μ] E)},
        ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) =ᵐ[μ] ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc g) →
          MeasureTheory.L1.SimpleFunc.setToL1S T f = MeasureTheory.L1.SimpleFunc.setToL1S T g
-- Mathlib.Data.Int.Init
Int.natCast_div : ∀ (m n : ℕ), ↑(m / n) = ↑m / ↑n
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
/-- The explicit coequalizer cofork of locally ringed spaces.  -/
AlgebraicGeometry.LocallyRingedSpace.coequalizerCofork : {X Y : AlgebraicGeometry.LocallyRingedSpace} → (f g : X ⟶ Y) → CategoryTheory.Limits.Cofork f g
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_hom : ∀ {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (s : Multiset M) {F : Type u_8}
  [inst_2 : FunLike F M N] [AddMonoidHomClass F M N] (f : F), (Multiset.map (⇑f) s).sum = f s.sum
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.spanSingleton_div_spanSingleton : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] (x y : K),
  FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x / FractionalIdeal.spanSingleton (nonZeroDivisors R₁) y =
    FractionalIdeal.spanSingleton (nonZeroDivisors R₁) (x / y)
-- Init.Data.SInt.Lemmas
ISize.toBitVec_ofBitVec : ∀ (b : BitVec System.Platform.numBits), (ISize.ofBitVec b).toBitVec = b
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_ker : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (K : Subgroup G) (f : G →* G'),
  f.ker.relIndex K = Nat.card ↥(Subgroup.map f K)
-- Lean.Data.Lsp.Internal
Lean.Lsp.ImportInfo.mk.injEq : ∀ (module : String) (isPrivate isAll isMeta : Bool) (module_1 : String) (isPrivate_1 isAll_1 isMeta_1 : Bool),
  ({ module := module, isPrivate := isPrivate, isAll := isAll, isMeta := isMeta } =
      { module := module_1, isPrivate := isPrivate_1, isAll := isAll_1, isMeta := isMeta_1 }) =
    (module = module_1 ∧ isPrivate = isPrivate_1 ∧ isAll = isAll_1 ∧ isMeta = isMeta_1)
-- Init.Data.Array.Range
Array.count_range' : ∀ {a s n step : ℕ},
  autoParam (0 < step) Array.count_range'._auto_1 →
    Array.count a (Array.range' s n step) = if ∃ i < n, a = s + step * i then 1 else 0
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.rewrites_reverse_comm : ∀ {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N} {u v : List (Symbol T N)},
  r.reverse.Rewrites u v ↔ r.Rewrites u.reverse v.reverse
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.medial_reindex : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] [inst_6 : CharZero k]
  (s : Affine.Simplex k P n) (e : Fin (n + 1) ≃ Fin (m + 1)), (s.reindex e).medial = s.medial.reindex e
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Splitting.coe_mk : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} (s : G →* E) (hs : Function.RightInverse ⇑s ⇑S.rightHom),
  ⇑{ toMonoidHom := s, rightInverse_rightHom := hs } = ⇑s
-- Mathlib.Combinatorics.SetFamily.Compression.UV
UV.compress_disjoint : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {s : Finset α} {u v : α} [inst_3 : DecidableEq α],
  Disjoint ({a ∈ s | UV.compress u v a ∈ s}) ({a ∈ Finset.image (UV.compress u v) s | a ∉ s})
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- A choice of isomorphism `T₁ ≅ T₂` between two distinguished triangles
when we are given two isomorphisms `e₁ : T₁.obj₁ ≅ T₂.obj₁` and `e₂ : T₁.obj₂ ≅ T₂.obj₂`.  -/
CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [hC : CategoryTheory.Pretriangulated C] →
              (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C) →
                T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
                  T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
                    (e₁ : T₁.obj₁ ≅ T₂.obj₁) →
                      (e₂ : T₁.obj₂ ≅ T₂.obj₂) →
                        CategoryTheory.CategoryStruct.comp T₁.mor₁ e₂.hom =
                            CategoryTheory.CategoryStruct.comp e₁.hom T₂.mor₁ →
                          (T₁ ≅ T₂)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Bundled right-exact functors.  -/
CategoryTheory.RightExactFunctor : (C : Type u₁) →
  [CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [CategoryTheory.Category.{v₂, u₂} D] → Type (max (max (max u₁ u₂) v₁) v₂)
-- Init.Prelude
/-- Sequences the effects of two terms, discarding the value of the second. This function is usually
invoked via the `<*` operator.

Given `x : f α` and `y : f β`, `x <* y` runs `x`, then runs `y`, and finally returns the result of
`x`.

The evaluation of the second argument is delayed by wrapping it in a function, enabling
“short-circuiting” behavior from `f`.


Conventions for notations in identifiers:

 * The recommended spelling of `<*` in identifiers is `seqLeft`. -/
SeqLeft.seqLeft : {f : Type u → Type v} → [self : SeqLeft f] → {α β : Type u} → f α → (Unit → f β) → f α
-- Init.Data.Array.Find
Array.getElem_zero_flatten : ∀ {α : Type u_1} {xss : Array (Array α)} (h : 0 < xss.flatten.size),
  xss.flatten[0] = (Array.findSome? (fun xs => xs[0]?) xss).get ⋯
-- Mathlib.Algebra.MvPolynomial.Expand
/-- Expansion is injective.  -/
MvPolynomial.expand_injective : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {n : ℕ}, 0 < n → Function.Injective ⇑(MvPolynomial.expand n)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.map_id : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S), WithAbs.map v v (RingHom.id R) = RingHom.id (WithAbs v)
-- Mathlib.Topology.Closure
subset_interior_iff_isOpen : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s ⊆ interior s ↔ IsOpen s
-- Mathlib.Data.Seq.Basic
Stream'.Seq.take_all : ∀ {α : Type u} {s : Stream'.Seq α} {p : α → Prop}, (∀ x ∈ s, p x) → ∀ {n : ℕ} {x : α}, x ∈ Stream'.Seq.take n s → p x
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] {ι_1 : Type u_5} {p : ι_1 → Prop} {b : ι_1 → Set F},
  (nhds 0).HasBasis p b →
    (nhds 0).HasBasis (fun Si => Bornology.IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si => {f | Set.MapsTo (⇑f) Si.1 (b Si.2)}
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.readyForRatAdd_ofArray : ∀ {α : outParam (Type u)} {β : outParam (Type v)} {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w}
  {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (arr : Array (Option β)),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.ofArray arr)
-- Std.Time.Format
/-- Formats a `PlainDateTime` value into a date time format string.
 -/
Std.Time.PlainDateTime.toDateTimeString : Std.Time.PlainDateTime → String
-- Mathlib.Computability.EpsilonNFA
εNFA.εClosure_univ : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ), M.εClosure Set.univ = Set.univ
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.prod_top : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (s : AddSubmonoid M),
  s.prod ⊤ = AddSubmonoid.comap (AddMonoidHom.fst M N) s
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousOn_iInf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {ι : Sort u_4} {δ : Type u_5} [inst_1 : CompleteLinearOrder δ]
  {f : ι → α → δ}, (∀ (i : ι), UpperSemicontinuousOn (f i) s) → UpperSemicontinuousOn (fun x' => ⨅ i, f i x') s
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_7} {n : ℕ} {x : 𝕜} {f : ι → 𝕜 → F} {I : Finset ι},
  (∀ i ∈ I, ContDiffAt 𝕜 (↑n) (f i) x) → iteratedDeriv n (∑ i ∈ I, f i) x = ∑ i ∈ I, iteratedDeriv n (f i) x
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.Limits.pushoutIsoUnopPullback f g).hom =
    (CategoryTheory.Limits.pullback.snd f.op g.op).unop
-- Std.Http.Data.Status
Std.Http.Status.seeOther.sizeOf_spec : sizeOf Std.Http.Status.seeOther = 1
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanPrepareModuleHierarchyParams.mk.sizeOf_spec : ∀ (textDocument : Lean.Lsp.TextDocumentIdentifier), sizeOf { textDocument := textDocument } = 1 + sizeOf textDocument
-- Mathlib.Topology.Irreducible
IrreducibleSpace.toNonempty : ∀ {X : Type u_3} {inst : TopologicalSpace X} [self : IrreducibleSpace X], Nonempty X
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.algHom_ext_iff : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_4}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f g : DividedPowerAlgebra R M →ₐ[R] A},
  f = g ↔ ∀ (n : ℕ) (m : M), f (DividedPowerAlgebra.dp R n m) = g (DividedPowerAlgebra.dp R n m)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.WeakLimitCone.mk.inj : ∀ {J : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} J} {C : Type u_3}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} C} {F : CategoryTheory.Functor J C} {cone : CategoryTheory.Limits.Cone F}
  {isWeakLimit : CategoryTheory.Limits.IsWeakLimit cone} {cone_1 : CategoryTheory.Limits.Cone F}
  {isWeakLimit_1 : CategoryTheory.Limits.IsWeakLimit cone_1},
  { cone := cone, isWeakLimit := isWeakLimit } = { cone := cone_1, isWeakLimit := isWeakLimit_1 } →
    cone = cone_1 ∧ isWeakLimit ≍ isWeakLimit_1
-- Std.Time.DateTime.WallTime
_private.Std.Time.DateTime.WallTime.0.Std.Time.WallTime.mk.inj : ∀ {val val_1 : Std.Time.Duration}, { val := val } = { val := val_1 } → val = val_1
-- Mathlib.Data.Nat.Init
/-- Recursion starting at a non-zero number: given a map `C k → C (k + 1)` for each `k`,
there is a map from `C n` to each `C m`, `n ≤ m`. For a version where the assumption is only made
when `k ≥ n`, see `Nat.leRec`.  -/
Nat.leRecOn : {C : ℕ → Sort u_1} → {n m : ℕ} → n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m
-- Mathlib.RingTheory.Norm.Basic
/-- Given `pb : PowerBasis R S`, then the norm of `pb.gen` is
`((minpoly R pb.gen).aroots F).prod`.  -/
Algebra.PowerBasis.norm_gen_eq_prod_roots : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {F : Type u_6}
  [inst_3 : Field F] [inst_4 : Algebra R F] (pb : PowerBasis R S),
  (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits →
    (algebraMap R F) ((Algebra.norm R) pb.gen) = ((minpoly R pb.gen).aroots F).prod
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- The Radon-Nikodym derivative of `f ν` with respect to `ν` is `f`.  -/
MeasureTheory.Measure.rnDeriv_withDensity₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite ν] {f : α → ENNReal},
  AEMeasurable f ν → (ν.withDensity f).rnDeriv ν =ᵐ[ν] f
-- Mathlib.Analysis.Asymptotics.Defs
/-- Eta-expanded form of `Asymptotics.IsBigOWith.sum` -/
Asymptotics.IsBigOWith.fun_sum : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {ι : Type u_18} {A : ι → α → E'} {C : ι → ℝ} {s : Finset ι},
  (∀ i ∈ s, Asymptotics.IsBigOWith (C i) l (A i) g) →
    Asymptotics.IsBigOWith (∑ i ∈ s, C i) l (fun a => ∑ c ∈ s, A c a) g
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- The bipartite double cover of `G` has twice the number of edges as `G`.  -/
SimpleGraph.card_edgeFinset_bipartiteDoubleCover : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj],
  G.bipartiteDoubleCover.edgeFinset.card = 2 * G.edgeFinset.card
-- Lean.Parser.Basic
Lean.Parser.trailingNodeAux : Lean.SyntaxNodeKind → Lean.Parser.Parser → Lean.Parser.TrailingParser
-- Batteries.Recycling.RBTree.Basic
/-- Fold a function on the values from right to left (in decreasing order).  -/
RBTree.RBNode.Stream.foldr : {α : Type u_1} → {σ : Sort u_2} → (α → σ → σ) → RBTree.RBNode.Stream α → σ → σ
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  k ∈ m → (m.insertMany l).get? k = m.get? k
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.monotone_approx : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : SemilatticeSup β] [inst_2 : OrderBot β]
  [inst_3 : Zero β] (i : ℕ → β) (f : α → β), Monotone (MeasureTheory.SimpleFunc.approx i f)
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The isomorphism between `incl ⋙ lift F _ _` with `F`.  -/
CategoryTheory.WithInitial.inclLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {Z : D} →
          (F : CategoryTheory.Functor C D) →
            (M : (x : C) → Z ⟶ F.obj x) →
              (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) →
                CategoryTheory.WithInitial.incl.comp (CategoryTheory.WithInitial.lift F M hM) ≅ F
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.insertMany_nil : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.insertMany [] = m
-- Mathlib.Order.Lattice
Subtype.mk_sup_mk : ∀ {α : Type u} [inst : SemilatticeSup α] {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)) {x y : α} (hx : P x)
  (hy : P y), ⟨x, hx⟩ ⊔ ⟨y, hy⟩ = ⟨x ⊔ y, ⋯⟩
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.gc_map_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F),
  GaloisConnection (AddSubmonoid.map f) (AddSubmonoid.comap f)
-- Mathlib.Data.TwoPointing
instDecidableEqTwoPointing.decEq : {α : Type u_3} → [DecidableEq α] → (x x_1 : TwoPointing α) → Decidable (x = x_1)
-- Mathlib.Data.List.Sigma
List.NodupKeys.map₂ : ∀ {α : Type u} {β : α → Type u_1} {β' : α → Type u_2} (f : (a : α) → β a → β' a) (l : List ((a : α) × β a)),
  l.NodupKeys → (List.map (Sigma.map id f) l).NodupKeys
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- Some glue, verifying that the structure presheaf valued in `CommRingCat` agrees
with the `Type`-valued structure presheaf.  -/
AlgebraicGeometry.structurePresheafCompForget : (R : Type u) →
  [inst : CommRing R] →
    CategoryTheory.Functor.comp (AlgebraicGeometry.structurePresheafInCommRingCat R)
        (CategoryTheory.forget CommRingCat) ≅
      (AlgebraicGeometry.structureSheafInType R R).obj
-- Mathlib.Geometry.Diffeology.Basic
/-- Replaces the D-topology of a diffeology with another topology equal to it. Useful
to construct diffeologies with better definitional equalities.  -/
DiffeologicalSpace.replaceDTopology : {X : Type u_1} →
  (d : DiffeologicalSpace X) → (t : TopologicalSpace X) → DiffeologicalSpace.dTopology = t → DiffeologicalSpace X
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_leftUnitor_inv_snd : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {a b : B × C}
  (f : a ⟶ b), (CategoryTheory.Bicategory.leftUnitor f).inv.2 = (CategoryTheory.Bicategory.leftUnitor f.2).inv
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.continuous : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  (α : ODE.FunSpace t₀ x₀ L r), Continuous α.toFun
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁)
  {Z : F.obj b₀ ⟶ F.obj b₁}
  (h : CategoryTheory.CategoryStruct.comp (F.map f) (F.map (CategoryTheory.CategoryStruct.id b₁)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b₁).inv) h)
-- Mathlib.Order.Bounds.Basic
/-- When there is a global minimum, every set is bounded below.  -/
OrderBot.bddBelow : ∀ {α : Type u_1} [inst : Preorder α] [OrderBot α] (s : Set α), BddBelow s
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.stronglyAdapted : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [inst_3 : LE E],
  MeasureTheory.Submartingale f ℱ μ → MeasureTheory.StronglyAdapted ℱ f
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (X : ↑(F.obj a)),
  (α.naturality (CategoryTheory.CategoryStruct.comp f g)).hom.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((α.app c).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((α.naturality g).hom.toNatTrans.app ((F.map f).toFunctor.obj X))
        (CategoryTheory.CategoryStruct.comp ((G.map g).toFunctor.map ((α.naturality f).hom.toNatTrans.app X))
          ((G.mapComp f g).inv.toNatTrans.app ((α.app a).toFunctor.obj X))))
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The Ore condition bundled in a sigma type. This is useful in situations where we want to obtain
both witnesses and the condition for a given fraction.  -/
OreLocalization.oreCondition : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} → [OreLocalization.OreSet S] → (r : R) → (s : ↥S) → (r' : R) ×' (s' : ↥S) ×' ↑s' * r = r' * ↑s