mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X) {Z : C}
  (h :
    ((TopCat.Presheaf.pushforward C f.base).obj X.presheaf).obj
        (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj U)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f U)
      (CategoryTheory.CategoryStruct.comp
        (f.c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj U))) h) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯)) h
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- `Under.pushout` commutes with composition.  -/
CategoryTheory.MorphismProperty.Under.pushoutComp : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q : CategoryTheory.MorphismProperty T} →
      [inst_1 : Q.IsMultiplicative] →
        {X Y Z : T} →
          (f : X ⟶ Y) →
            (g : Y ⟶ Z) →
              [inst_2 : P.IsStableUnderCobaseChangeAlong f] →
                [inst_3 : P.IsStableUnderCobaseChangeAlong g] →
                  [inst_4 : P.HasPushoutsAlong f] →
                    [inst_5 : P.HasPushoutsAlong g] →
                      [Q.RespectsIso] →
                        [inst_7 : Q.IsStableUnderCobaseChange] →
                          (fg : optParam (X ⟶ Z) (CategoryTheory.CategoryStruct.comp f g)) →
                            (hfg :
                                autoParam (fg = CategoryTheory.CategoryStruct.comp f g)
                                  CategoryTheory.MorphismProperty.Under.pushoutComp._auto_1) →
                              CategoryTheory.MorphismProperty.Under.pushout P Q fg ≅
                                (CategoryTheory.MorphismProperty.Under.pushout P Q f).comp
                                  (CategoryTheory.MorphismProperty.Under.pushout P Q g)
-- Lean.Elab.Tactic.RCases
/-- Takes the number of fields of a single constructor and patterns to match its fields against
(not necessarily the same number). The returned lists each contain one element per field of the
constructor. The `name` is the name which will be used in the top-level `cases` tactic, and the
`rcases_patt` is the pattern which the field will be matched against by subsequent `cases`
tactics.
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.processConstructor : Lean.Syntax →
  Array Lean.Meta.ParamInfo →
    Bool → ℕ → List Lean.Elab.Tactic.RCases.RCasesPatt → List Lean.Name × List Lean.Elab.Tactic.RCases.RCasesPatt
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.nodalWeight_eq_eval_nodal_erase_inv : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι},
  Lagrange.nodalWeight s v i = (Polynomial.eval (v i) (Lagrange.nodal (s.erase i) v))⁻¹
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.instAddI : (G : Type u) → (H : Type v) → [Add G] → [Add H] → (b : Bool) → Add (I✝ G H b)
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.subset_of_mem_disjointOfDiffUnion : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : MeasureTheory.IsSetSemiring C) {I : Finset (Set α)} (hs : s ∈ C)
  (hI : ↑I ⊆ C), ∀ t ∈ ↑(hC.disjointOfDiffUnion hs hI), t ⊆ s
-- Init.Prelude
/-- `NonemptyType` is inhabited, because `PUnit` is a nonempty type.  -/
instInhabitedNonemptyType : Inhabited NonemptyType
-- Mathlib.Algebra.Homology.Augment
/-- We can "augment" a cochain complex by inserting an arbitrary object in degree zero
(shifting everything else up), along with a suitable differential.
 -/
CochainComplex.augment : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (C : CochainComplex V ℕ) →
        {X : V} → (f : X ⟶ C.X 0) → CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0 → CochainComplex V ℕ
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.comp`. -/
MeasureTheory.ProgMeasurable.comp : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : MeasurableSpace ι] {t : ι → Ω → ι}
  [inst_3 : TopologicalSpace ι] [BorelSpace ι] [TopologicalSpace.PseudoMetrizableSpace ι],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStronglyProgressive f t →
      (∀ (i : ι) (ω : Ω), t i ω ≤ i) → MeasureTheory.IsStronglyProgressive f fun i ω => u (t i ω) ω
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- A **right-uniform group** is a topological group endowed with the associated
right uniform structure: the uniformity filter `𝓤 G` is the inverse image of `𝓝 1` by the map
`(x, y) ↦ y * x⁻¹`.

In other words, we declare that two points `x` and `y` are infinitely close
precisely when `y * x⁻¹` is infinitely close to `1`.  -/
IsRightUniformGroup : (G : Type u_7) → [UniformSpace G] → [Group G] → Prop
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure.brecOn : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.multiplicativeClosure x → Prop} {X Y : C} {x : X ⟶ Y}
  (t : W.multiplicativeClosure x),
  (∀ ⦃X Y : C⦄ (x : X ⟶ Y) (t : W.multiplicativeClosure x),
      CategoryTheory.MorphismProperty.multiplicativeClosure.below t → motive x t) →
    motive x t
-- Mathlib.Topology.Compactness.Lindelof
/-- **Alias** of `Quotient.lindelofSpace`. -/
Quotient.LindelofSpace : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Setoid X} [LindelofSpace X], LindelofSpace (Quotient s)
-- Mathlib.CategoryTheory.Functor.OfSequence
/-- Constructor for natural transformations `F ⟶ G` in `ℕ ⥤ C` which takes as inputs
the morphisms `F.obj n ⟶ G.obj n` for all `n : ℕ` and the naturality condition only
for morphisms of the form `n ⟶ n + 1`.  -/
CategoryTheory.NatTrans.ofSequence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {F G : CategoryTheory.Functor ℕ C} →
      (app : (n : ℕ) → F.obj n ⟶ G.obj n) →
        (∀ (n : ℕ),
            CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) (app (n + 1)) =
              CategoryTheory.CategoryStruct.comp (app n) (G.map (CategoryTheory.homOfLE ⋯))) →
          (F ⟶ G)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.natCast_mul_lt_natCast_mul : ∀ {n : ℕ} {a b : Cardinal.{u_1}}, n ≠ 0 → (↑n * a < ↑n * b ↔ a < b)
-- Mathlib.Data.Finset.Union
Finset.pairwiseDisjoint_disjUnion : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f g : α → Finset β} (hfg : ∀ (a : α), Disjoint (f a) (g a)),
  ((↑s).Pairwise fun a₁ a₂ => Disjoint (f a₁) (g a₂)) →
    (↑s).PairwiseDisjoint f → (↑s).PairwiseDisjoint g → (↑s).PairwiseDisjoint fun a => (f a).disjUnion (g a) ⋯
-- Mathlib.Topology.Algebra.Order.Field
Filter.Tendsto.div_atTop : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {a : 𝕜},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x / g x) l (nhds 0)
-- Mathlib.AlgebraicGeometry.QuasiAffine
AlgebraicGeometry.Scheme.instIsQuasiAffineOfIsAffine : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X], X.IsQuasiAffine
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.approx_of_mem_C : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (n : ℕ) {x : X},
  x ∈ c.C → Urysohns.CU.approx n c x = 0
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.derivFamily_strictMono : ∀ {ι : Type u_1} [Small.{u, u_1} ι] (f : ι → Ordinal.{u} → Ordinal.{u}), StrictMono (Ordinal.derivFamily f)
-- Mathlib.Algebra.BigOperators.Fin
finSigmaFinEquiv_apply : ∀ {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
-- Mathlib.CategoryTheory.MorphismProperty.Local
/-- A property of morphisms `P` in `C` is local at the target with respect to the precoverage `K` if
it respects isomorphisms, and:
`P` holds for `f : X ⟶ Y` if and only if it holds for the restrictions of `f` to `Uᵢ` for a
`0`-hypercover `{Uᵢ}` of `Y` in the precoverage `K`.
 -/
CategoryTheory.MorphismProperty.IsLocalAtTarget : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.Precoverage C → Prop
-- Mathlib.Analysis.Normed.Ring.Units
/-- Maximal ideals in normed rings with summable geometric series are closed.  -/
Ideal.IsMaximal.isClosed : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] {I : Ideal R} [hI : I.IsMaximal], IsClosed ↑I
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instCompleteSpace : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3}, CompleteSpace (CStarMatrix m n A)
-- Mathlib.CategoryTheory.Abelian.CommSq
CategoryTheory.Abelian.mono_cokernel_map_of_isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X₁ X₂ X₃ X₄ : C}
  {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} (sq : CategoryTheory.IsPullback t l r b),
  CategoryTheory.Mono (CategoryTheory.Limits.cokernel.map t b l r ⋯)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Filter.isMeasurablyGenerated_top : ∀ {α : Type u_1} [inst : MeasurableSpace α], ⊤.IsMeasurablyGenerated
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succ_inj : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.InfinitelyUpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] {a b : α}, Std.PRange.succ a = Std.PRange.succ b ↔ a = b
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
CategoryTheory.TwoSquare.GuitartExact.instWhiskerHorizontalOfIsIsoFunctor : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] {T : CategoryTheory.Functor C₁ D₁} {L : CategoryTheory.Functor C₁ C₂}
  {R : CategoryTheory.Functor D₁ D₂} {B : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T L R B)
  {T' : CategoryTheory.Functor C₁ D₁} {B' : CategoryTheory.Functor C₂ D₂} [w.GuitartExact] (α : T' ⟶ T) (β : B ⟶ B')
  [CategoryTheory.IsIso α] [CategoryTheory.IsIso β], (w.whiskerHorizontal α β).GuitartExact
-- Mathlib.Tactic.ArithMult
/-- The `arith_mult` attribute used to tag `IsMultiplicative` statements for the
`arith_mult` tactic.  -/
ArithmeticFunction.attrArith_mult : Lean.ParserDescr
-- Mathlib.Algebra.BigOperators.ModEq
Int.prod_modEq_ite : ∀ {α : Type u_1} {n : ℤ} {f : α → ℤ} [inst : DecidableEq α] {s : Finset α} {a : α},
  (∀ x ∈ s, x ≠ a → f x ≡ 1 [ZMOD n]) → ∏ x ∈ s, f x ≡ if a ∈ s then f a else 1 [ZMOD n]
-- Mathlib.Logic.Small.Set
small_iUnion : ∀ {α : Type u1} {ι : Type u4} [Small.{u, u4} ι] (s : ι → Set α) [∀ (i : ι), Small.{u, u1} ↑(s i)],
  Small.{u, u1} ↑(⋃ i, s i)
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.leftAdjointObjIsDefined_of_adjunction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D} (adj : G ⊣ F) (X : C), F.leftAdjointObjIsDefined X
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.δ_comp_δ_whiskerRight_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X Y Z : C) {Z_1 : D}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (F.obj Z))
        h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv h)))
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.detectOffsets : Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Data.Options
Lean.Options.set : {α : Type} → [Lean.KVMap.Value α] → Lean.Options → Lean.Name → α → Lean.Options
-- Mathlib.ModelTheory.Syntax
/-- Applies a relation to terms as a bounded formula.  -/
FirstOrder.Language.Relations.boundedFormula : {L : FirstOrder.Language} →
  {α : Type u'} → {n l : ℕ} → L.Relations n → (Fin n → L.Term (α ⊕ Fin l)) → L.BoundedFormula α l
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instMulOneClassOfContinuousMul : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : MulOneClass β] → [ContinuousMul β] → MulOneClass C(α, β)
-- Mathlib.CategoryTheory.EssentiallySmall
/-- Any thin category is locally small.
 -/
CategoryTheory.locallySmall_of_thin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [Quiver.IsThin C], CategoryTheory.LocallySmall.{w, v, u} C
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHAddDuration : HAdd Std.Time.WallTime Std.Time.Duration Std.Time.WallTime
-- Aesop.RuleTac.Tactic
/-- Elaborates and runs the given tactic syntax `stx`. The syntax `stx` must be of
kind `tactic` or `tacticSeq`.
 -/
Aesop.RuleTac.tacticStx : Lean.Syntax → Aesop.RuleTac
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.CommShift.commShift_counit : ∀ {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} {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {adj : F ⊣ G} {A : Type u_3} {inst_2 : AddMonoid A} {inst_3 : CategoryTheory.HasShift C A}
  {inst_4 : CategoryTheory.HasShift D A} {inst_5 : F.CommShift A} {inst_6 : G.CommShift A} [self : adj.CommShift A],
  CategoryTheory.NatTrans.CommShift adj.counit A
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsKleinFour.inv_eq_self : ∀ {G : Type u_1} [inst : Group G] [IsKleinFour G] (x : G), x⁻¹ = x
-- Mathlib.Algebra.Field.Periodic
Function.Periodic.image_Ioc : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddCommGroup α] [inst_1 : LinearOrder α]
  [IsOrderedAddMonoid α] [Archimedean α],
  Function.Periodic f c → 0 < c → ∀ (a : α), f '' Set.Ioc a (a + c) = Set.range f
-- Mathlib.Order.SuccPred.Limit
Order.isSuccLimit_iff_of_orderBot : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : OrderBot α],
  Order.IsSuccLimit a ↔ a ≠ ⊥ ∧ Order.IsSuccPrelimit a
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
HomotopyCategory.instLinearIntUpShiftFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] (n : ℤ),
  CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n)
-- Mathlib.Order.CompleteLattice.Defs
Equiv.infSet_def : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : InfSet β] (s : Set α), sInf s = e.symm (⨅ a ∈ s, e a)
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_ne_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.natTrailingDegree ≠ 0 ↔ p ≠ 0 ∧ p.coeff 0 = 0
-- Init.Grind.Ring.Basic
/-- Multiplying by a numeral is consistently defined with respect to the canonical map from natural
numbers.
 -/
Lean.Grind.Semiring.nsmul_eq_natCast_mul : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (n : ℕ) (a : α), n • a = ↑n * a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sqrtTwoAddSeries_succ : ∀ (x : ℝ) (n : ℕ), x.sqrtTwoAddSeries (n + 1) = (√(2 + x)).sqrtTwoAddSeries n
-- Mathlib.Order.Cover
WithBot.coe_wcovBy_coe : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, ↑b ⩿ ↑a ↔ b ⩿ a
-- Init.Data.UInt.Lemmas
UInt8.neg_add_mul_eq_mul_not : ∀ {a b : UInt8}, -(a + a * b) = a * ~~~b
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Iic_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Iic a)), Subtype.val '' Set.Iio b = Set.Iio ↑b
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.subset_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  s ⊆ ↑(Submodule.span R s)
-- Mathlib.Combinatorics.SimpleGraph.DegreeSum
SimpleGraph.dart_card_eq_twice_card_edges : ∀ {V : Type u} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj],
  Fintype.card G.Dart = 2 * G.edgeFinset.card
-- Mathlib.Algebra.RingQuot
RingQuot.preLiftAlgHom_def : ∀ (S : Type u_1) [inst : CommSemiring S] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra S A] {B : Type u_3}
  [inst_3 : Semiring B] [inst_4 : Algebra S B] {s : A → A → Prop} {f : A →ₐ[S] B} (h : ∀ ⦃x y : A⦄, s x y → f x = f y),
  RingQuot.preLiftAlgHom S h =
    { toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
      commutes' := ⋯ }
-- Init.Data.UInt.Lemmas
UInt32.ofNatTruncate_toNat : ∀ (n : UInt32), UInt32.ofNatClamp n.toNat = n
-- Mathlib.Topology.UniformSpace.Basic
IsSymm_entourageProd : ∀ {α : Type ua} {β : Type ub} {u : SetRel α α} {v : SetRel β β} [u.IsSymm] [v.IsSymm], (entourageProd u v).IsSymm
-- Mathlib.Topology.Baire.BaireMeasurable
/-- Any Borel set differs from some open set by a meager set.  -/
MeasurableSet.residualEq_isOpen : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} [inst_1 : MeasurableSpace α] [BorelSpace α],
  MeasurableSet s → ∃ u, IsOpen u ∧ s =ᶠ[residual α] u
-- Aesop.RuleTac.RuleTerm
Aesop.RuleTerm.const.inj : ∀ {decl decl_1 : Lean.Name}, Aesop.RuleTerm.const decl = Aesop.RuleTerm.const decl_1 → decl = decl_1
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.State.equalLMVarIds : Aesop.EqualUpToIdsM.State → Std.HashMap Lean.LMVarId Lean.LMVarId
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.congr_apply : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C] [inst_13 : Semiring D]
  [inst_14 : Algebra R D] (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) (x : TensorProduct R A B),
  (Algebra.TensorProduct.congr f g) x = (Algebra.TensorProduct.map ↑f ↑g) x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_eq_back_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.maxKey he = t.keysArray.back ⋯
-- Mathlib.Logic.Equiv.Defs
/-- The sort of maps from a type that `IsEmpty` is equivalent to `PUnit`.  -/
Equiv.arrowPUnitOfIsEmpty : (α : Sort u_1) → (β : Sort u_2) → [IsEmpty α] → (α → β) ≃ PUnit.{u}
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.toEquiv_refl : ∀ {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₁],
  (↑(ContinuousAffineEquiv.refl k P₁)).toEquiv = Equiv.refl P₁
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The center is commutative.  -/
Subring.instCommRingSubtypeMemCenter : {R : Type u_1} → [inst : Ring R] → CommRing ↥(Subring.center R)
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
/-- **Alias** of `AlgebraicGeometry.Scheme.Hom.isEmbedding`.

---

**Alias** of `AlgebraicGeometry.IsPreimmersion.isEmbedding`. -/
AlgebraicGeometry.IsPreimmersion.base_embedding : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.IsPreimmersion f], Topology.IsEmbedding ⇑f
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
QuotientGroup.measurable_coe : ∀ {G : Type u_6} [inst : Group G] [inst_1 : MeasurableSpace G] {S : Subgroup G}, Measurable QuotientGroup.mk
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_eq_nhds_of_re_neg_of_im_pos : ∀ {x : ℂ}, x.re < 0 → 0 < x.im → Complex.arg =ᶠ[nhds x] fun x => Real.arcsin ((-x).im / ‖x‖) + Real.pi
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_fst_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.comapIso f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f I.subschemeι) h) =
    CategoryTheory.CategoryStruct.comp (I.comap f).subschemeι h
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_Icc_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (b : α i), Pi.single i '' Set.Icc 0 b = Set.Icc 0 (Pi.single i b)
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.if : ∀ {α : Type u_1} {β : Type u_2} {l₁ : Filter α} {l₂ : Filter β} {f g : α → β} {p : α → Prop}
  [inst : (x : α) → Decidable (p x)],
  Filter.Tendsto f (l₁ ⊓ Filter.principal {x | p x}) l₂ →
    Filter.Tendsto g (l₁ ⊓ Filter.principal {x | ¬p x}) l₂ → Filter.Tendsto (fun x => if p x then f x else g x) l₁ l₂
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.isSuccLimit_of_mem_frontier : ∀ {s : Set Ordinal.{u}} {a : Ordinal.{u}}, a ∈ frontier s → Order.IsSuccLimit a
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Subtype.image_eball`. -/
Subtype.image_emetricBall : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ENNReal),
  Subtype.val '' Metric.eball a r = Metric.eball (↑a) r ∩ {a | p a}
-- Mathlib.Analysis.Complex.Basic
Complex.isometry_ofReal : Isometry Complex.ofReal
-- Mathlib.Logic.Hydra
/-- A multiset is accessible under `CutExpand` if all its singleton subsets are,
assuming `r` is irreflexive.  -/
Relation.acc_of_singleton : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Irrefl r] {s : Multiset α},
  (∀ a ∈ s, Acc (Relation.CutExpand r) {a}) → Acc (Relation.CutExpand r) s
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
/-- From a dynamical cover `s` with entourage `U` and time `m`, we construct covers with entourage
`U ○ U` and any multiple `m * n` of `m` with controlled cardinality. This lemma is the first step
in a submultiplicative-like property of `coverMincard`, with consequences such as explicit bounds
for the topological entropy (`coverEntropyInfEntourage_le_card_div`) and an equality between
two notions of topological entropy (`coverEntropyInf_eq_coverEntropySup_of_inv`).  -/
Dynamics.IsDynCoverOf.iterate_le_pow : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} {m : ℕ},
  Set.MapsTo T F F →
    ∀ [U.IsSymm] (n : ℕ) {s : Finset X},
      Dynamics.IsDynCoverOf T F U m ↑s → ∃ t, Dynamics.IsDynCoverOf T F (U.comp U) (m * n) ↑t ∧ t.card ≤ s.card ^ n