mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.forget_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.AddMon.forget C).Faithful
-- Mathlib.Data.Rat.Lemmas
Rat.coe_pnatDen : ∀ (x : ℚ), ↑x.pnatDen = x.den
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_neg : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.Chebyshev.C R (-n) = Polynomial.Chebyshev.C R n
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.hom_ext_iff : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} {f g : X ⟶ Y},
  f = g ↔ f.left = g.left ∧ f.right = g.right
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
/-- A concrete category with strong epi mono factorizations and such that
the forget functor preserves mono and epi admits functorial surjective/injective
factorizations.  -/
CategoryTheory.ConcreteCategory.functorialSurjectiveInjectiveFactorizationData : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] →
              [(CategoryTheory.forget C).PreservesMonomorphisms] →
                [(CategoryTheory.forget C).PreservesEpimorphisms] →
                  CategoryTheory.ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData C
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.isChain_dartAdj_cons_darts : ∀ {V : Type u} {G : SimpleGraph V} {d : G.Dart} {v w : V},
  d.toProd.2 = v → ∀ (p : G.Walk v w), List.IsChain G.DartAdj (d :: p.darts)
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.coe_id : ∀ {X : AddCommGrpCat}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- The hom-types in a `Cat`-enriched ordinary category are equivalent to the types underlying the
hom-categories.  -/
CategoryTheory.CatEnrichedOrdinary.homEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] →
      {a b : CategoryTheory.CatEnrichedOrdinary C} → (a ⟶ b) ≃ (a.toBase ⟶ b.toBase)
-- Init.Data.List.Find
/-- If `¬ p xs[j]` for all `j ≤ i`, then `i < xs.findIdx p`.  -/
List.lt_findIdx_of_not : ∀ {α : Type u_1} {p : α → Bool} {xs : List α} {i : ℕ} (h : i < xs.length),
  (∀ (j : ℕ) (hji : j ≤ i), ¬p xs[j] = true) → i < List.findIdx p xs
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addLeftMono : ∀ {α : Type u} [inst : Add α] [inst_1 : LE α] [AddLeftMono α], AddLeftMono (WithTop α)
-- Mathlib.Algebra.Group.Units.Equiv
Group.mulRight_bijective : ∀ {G : Type u_5} [inst : Group G] (a : G), Function.Bijective fun x => x * a
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_roo : ∀ {m n : ℤ} {i : ℕ}, (m<...n).toList[i]! = if i < (n - (m + 1)).toNat then m + 1 + ↑i else 0
-- Aesop.Search.Main
Aesop.traceTree : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q Unit
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- The yoneda embedding of `Grp C` into presheaves of groups.  -/
CategoryTheory.yonedaGrp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.Functor (CategoryTheory.Grp C) (CategoryTheory.Functor Cᵒᵖ GrpCat)
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.unop_d : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex Vᵒᵖ c) (i j : ι),
  X.unop.d i j = (X.d j i).unop
-- Mathlib.Data.Set.Disjoint
Set.disjoint_or_nonempty_inter : ∀ {α : Type u} (s t : Set α), Disjoint s t ∨ (s ∩ t).Nonempty
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T')
  {Y X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f_1 : Y ⟶ X),
  ((CategoryTheory.CostructuredArrow.map f).map f_1).right = CategoryTheory.CategoryStruct.id Y.right
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- The natural transformation `H ⟶ F` for an adjoint triple `F ⊣ G ⊣ H` with `G` fully faithful
is also equal to the inverse of the whiskered counit `H ⋙ G ⋙ F ⟶ H` of the first adjunction
followed by the whiskered counit `H ⋙ G ⋙ F ⟶ F` of the second.  -/
CategoryTheory.Adjunction.Triple.rightToLeft_eq_counits : ∀ {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}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful],
  t.rightToLeft =
    CategoryTheory.CategoryStruct.comp H.rightUnitor.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (H.whiskerLeft t.adj₁.counit))
        (CategoryTheory.CategoryStruct.comp (H.associator G F).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight t.adj₂.counit F) F.leftUnitor.hom)))
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.forallLTEqZero_supp_BddBelow : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] (f : Γ → R) (n : Γ),
  (∀ m < n, f m = 0) → BddBelow (Function.support f)
-- Lean.Declaration
Lean.DefinitionVal : Type
-- Init.Data.SInt.Lemmas
Int8.neg_inj : ∀ {a b : Int8}, -a = -b ↔ a = b
-- Init.Data.Order.Factories
/-- Creates a *total* `LE α` instance from an `LT α` instance.

This only makes sense for asymmetric `LT α` instances (see `Std.Asymm`).
 -/
LE.ofLT : (α : Type u) → [LT α] → LE α
-- Aesop.Tree.Tracing
Aesop.Rapp.traceMetadata : Aesop.Rapp → Aesop.TraceOption → Lean.MetaM Unit
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_subset_compl_diagSet : ∀ {V : Type u} (G : SimpleGraph V), G.edgeSet ⊆ Sym2.diagSetᶜ
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.strictMono_comap_prod_map : ∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal],
  StrictMono fun H => (AddSubgroup.comap N.subtype H, AddSubgroup.map (QuotientAddGroup.mk' N) H)
-- Init.Data.List.Int.Sum
List.min_le_sum_div_length_int : ∀ {xs : List ℤ} (h : xs ≠ []), xs.min h ≤ xs.sum / ↑xs.length
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonUnitalRing : {R : Type u_1} → {M : Type u_4} → [inst : Ring R] → [AddSemigroup M] → NonUnitalRing (AddMonoidAlgebra R M)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_ite : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f g : β → α}
  (p : β → Prop) [inst_2 : DecidablePred p],
  (s.sup fun i => if p i then f i else g i) = (Finset.filter p s).sup f ⊔ {i ∈ s | ¬p i}.sup g
-- Init.Data.UInt.Bitwise
UInt16.toUInt32_shiftLeft : ∀ (a b : UInt16), (a <<< b).toUInt32 = a.toUInt32 <<< (b % 16).toUInt32 % 65536
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.mulLECancellable_prod : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] [inst_1 : LE α] [MulLeftMono α] {s : Finset ι} {f : ι → α},
  MulLECancellable (∏ i ∈ s, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s → MulLECancellable (f i)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- The natural transformation `mapTrifunctor F I₁ I₂ I₃ ⟶ mapTrifunctor F' I₁ I₂ I₃`
induced by a natural transformation `F ⟶ F'` of trifunctors.  -/
CategoryTheory.GradedObject.mapTrifunctorMapNatTrans : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                {F F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))} →
                  (F ⟶ F') →
                    (I₁ : Type u_7) →
                      (I₂ : Type u_8) →
                        (I₃ : Type u_9) →
                          CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃ ⟶
                            CategoryTheory.GradedObject.mapTrifunctor F' I₁ I₂ I₃
-- Init.Data.Nat.Bitwise.Lemmas
Nat.or_div_two : ∀ {a b : ℕ}, (a ||| b) / 2 = a / 2 ||| b / 2
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent.0.termℂ_ℤ : Lean.ParserDescr
-- Mathlib.RingTheory.AdicCompletion.RingHom
IsAdicComplete.StrictMono.mk_liftRingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S) {a : ℕ → ℕ}
  (ha : StrictMono a) (f : (n : ℕ) → R →+* S ⧸ I ^ a n)
  (hf : ∀ {m : ℕ}, (Ideal.Quotient.factorPow I ⋯).comp (f (m + 1)) = f m) [inst_2 : IsAdicComplete I S] {n : ℕ} (x : R),
  (Ideal.Quotient.mk (I ^ a n)) ((IsAdicComplete.StrictMono.liftRingHom I ha f ⋯) x) = (f n) x
-- Mathlib.Util.Notation3
/-- A fold variable, use the fold state (but reverse the array).  -/
Mathlib.Notation3.BoundValueType.foldl : Mathlib.Notation3.BoundValueType
-- Mathlib.Data.Pi.Interval
Pi.card_Icc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) → α i),
  (Finset.Icc a b).card = ∏ i, (Finset.Icc (a i) (b i)).card
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.range_isMulCommutative : ∀ {G : Type u_7} [inst : Group G] [IsMulCommutative G] {N : Type u_8} [inst_2 : Group N] (f : G →* N),
  IsMulCommutative ↥f.range
-- Init.Data.ULift
instDecidableEqULift.decEq : {α : Type u_1} → [DecidableEq α] → (x x_1 : ULift.{u_2, u_1} α) → Decidable (x = x_1)
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.shiftFunctor₂XXIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (a b y b' : ℤ) (h : b' = b + y),
  K.shiftFunctor₂XXIso a b y b' h = K.shiftFunctor₂XXIso a b y b' h
-- Lean.Meta.Tactic.Grind.Util
Lean.Meta.Grind.getBinOp : Lean.Expr → Option Lean.Expr
-- Mathlib.Tactic.Algebra.Basic
/-- `ExBase BaseType sα e` stores the structure of a normalized expression `e`, which appears
as the base of an exponent expression `e^n`. The `sum` constructor is only used when the exponent
`n` is not a constant.  -/
Mathlib.Tactic.Algebra.ExBase : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} → {sR : Q(CommSemiring «$R»)} → {sA : Q(CommSemiring «$A»)} → Q(Algebra «$R» «$A») → Q(«$A») → Type
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeRightOpOfCone_ι : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.coconeRightOpOfCone c).ι = CategoryTheory.NatTrans.rightOp c.π
-- Mathlib.MeasureTheory.Function.EssSup
meas_lt_essInf : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLinearOrder β] {f : α → β} [inst_1 : TopologicalSpace β] [FirstCountableTopology β]
  [OrderTopology β],
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae μ) f) meas_lt_essInf._auto_1 →
    μ {y | f y < essInf f μ} = 0
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.uniqueHomFromTrivial.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.AddMon C),
  A.uniqueHomFromTrivial = { default := { hom := CategoryTheory.AddMonObj.zero, isAddMonHom_hom := ⋯ }, uniq := ⋯ }
-- Init.Control.Lawful.Basic
Id.run_pure : ∀ {α : Type u_1} (a : α), (pure a).run = a
-- Std.Data.DTreeMap.Internal.Cell
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Cell.Const.alter : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      [Std.OrientedOrd α] →
        {k : α} →
          (Option β → Option β) →
            Std.DTreeMap.Internal.Cell α (fun x => β) (compare k) →
              Std.DTreeMap.Internal.Cell α (fun x => β) (compare k)
-- Mathlib.Analysis.Distribution.TemperateGrowth
HasCompactSupport.hasTemperateGrowth : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F}, HasCompactSupport f → ContDiff ℝ (↑⊤) f → Function.HasTemperateGrowth f
-- Init.Data.UInt.Lemmas
UInt16.toNat_ofNat' : ∀ {n : ℕ}, (UInt16.ofNat n).toNat = n % 2 ^ 16
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.vadd_sphere : ∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [IsIsometricVAdd G X] (c : G) (x : X) (r : ℝ), c +ᵥ Metric.sphere x r = Metric.sphere (c +ᵥ x) r
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lmap_of : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {N : ι → Type u_1} [inst_3 : (i : ι) → AddCommMonoid (N i)]
  [inst_4 : (i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) [inst_5 : DecidableEq ι] (i : ι) (x : M i),
  (DirectSum.lmap f) ((DirectSum.of M i) x) = (DirectSum.of N i) ((f i) x)
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
List.prod_isUnit_iff : ∀ {M : Type u_8} [inst : CommMonoid M] {L : List M}, IsUnit L.prod ↔ ∀ m ∈ L, IsUnit m
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.neg_right : ∀ {R₁ : Type u_4} {M₁ : Type u_5} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B₁ : LinearMap.BilinForm R₁ M₁} (x y : M₁), (B₁ x) (-y) = -(B₁ x) y
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
sub_one_lt : ∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [AddLeftStrictMono R] (a : R),
  a - 1 < a
-- Mathlib.Topology.Algebra.Ring.Real
ENNReal.isOpenEmbedding_coe : Topology.IsOpenEmbedding ENNReal.ofNNReal
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.sum_add_tsum_subtype_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddCommGroup α] [IsUniformAddGroup α]
  [CompleteSpace α] [T2Space α] {f : β → α},
  Summable f → ∀ (s : Finset β), ∑ x ∈ s, f x + ∑' (x : { x // x ∉ s }), f ↑x = ∑' (x : β), f x
-- Batteries.Data.DList.Basic
Batteries.DList.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (apply : List α → List α) (invariant : ∀ (l : List α), apply l = apply [] ++ l),
  sizeOf { apply := apply, invariant := invariant } = 1
-- Mathlib.Data.Multiset.Filter
Multiset.filterMap_eq_filter : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p],
  Multiset.filterMap (Option.guard fun b => decide (p b)) = Multiset.filter p
-- Mathlib.RingTheory.RingHom.FaithfullyFlat
RingHom.FaithfullyFlat.isStableUnderBaseChange : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => RingHom.FaithfullyFlat
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.mul_def : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] (x y : GradedTensorProduct R 𝒜 ℬ), x * y = ((GradedTensorProduct.mulHom 𝒜 ℬ) x) y
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The map from ideals of `R` dividing `I` to the ideals of `A` dividing `J` induced by
a homomorphism `f : R/I →+* A/J`  -/
IsDedekindDomain.idealFactorsFunOfQuotHom : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [IsDedekindDomain A] →
          {I : Ideal R} →
            {J : Ideal A} → {f : R ⧸ I →+* A ⧸ J} → Function.Surjective ⇑f → { p // p ∣ I } →o { p // p ∣ J }
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse_map_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {X Y : CategoryTheory.Functor C (CategoryTheory.Mon D)} (α : X ⟶ Y)
  (X_1 : C), (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse.map α).hom.app X_1 = (α.app X_1).hom
-- Mathlib.Data.List.Cycle
Cycle.mem_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Cycle α}, b ∈ Cycle.map f s ↔ ∃ a ∈ s, f a = b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β},
  t₁.Equiv t₂ →
    ∀ {f : (a : α) → β a → γ a}, (Std.DTreeMap.Internal.Impl.map f t₁).Equiv (Std.DTreeMap.Internal.Impl.map f t₂)
-- Mathlib.Topology.Defs.Induced
Topology.IsCoinducing.mk : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
  tY = TopologicalSpace.coinduced f tX → Topology.IsCoinducing f
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.FormatError.mk.sizeOf_spec : ∀ (srcNat : ℕ) (srcEndPos : String.Pos.Raw) (fmtPos : ℕ) (msg : String) (length : ℕ) (srcStartPos : String.Pos.Raw),
  sizeOf
      { srcNat := srcNat, srcEndPos := srcEndPos, fmtPos := fmtPos, msg := msg, length := length,
        srcStartPos := srcStartPos } =
    1 + sizeOf srcNat + sizeOf srcEndPos + sizeOf fmtPos + sizeOf msg + sizeOf length + sizeOf srcStartPos
-- Init.Data.String.Basic
String.Slice.Pos.cast_endPos : ∀ {s t : String.Slice} {hst : s.copy = t.copy}, s.endPos.cast hst = t.endPos
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.LaxBraided.id : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (CategoryTheory.Functor.id C).LaxBraided
-- Mathlib.Logic.Equiv.Set
Equiv.Set.union_symm_apply_right : ∀ {α : Type u_3} {s t : Set α} [inst : DecidablePred fun x => x ∈ s] (H : Disjoint s t) (a : ↑t),
  (Equiv.Set.union H).symm (Sum.inr a) = ⟨↑a, ⋯⟩
-- Mathlib.Data.Multiset.Replicate
Multiset.le_replicate_iff : ∀ {α : Type u_1} {m : Multiset α} {a : α} {n : ℕ}, m ≤ Multiset.replicate n a ↔ ∃ k ≤ n, m = Multiset.replicate k a
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous.uniformContinuousOn : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α},
  UniformContinuous f → UniformContinuousOn f s
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.getElem_toList_eq : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {i : ℕ} {h : i < r.toList.length},
  r.toList[i] = (Std.PRange.succMany? (i + 1) r.lower).get ⋯
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (m.insertMany l).getD k' fallback = v
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.derives_reverse_comm : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)},
  g.reverse.Derives u v ↔ g.Derives u.reverse v.reverse
-- Mathlib.Data.Finset.Card
Finset.strongInduction.eq_def : ∀ {α : Type u_1} {p : Finset α → Sort u_4} (H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s) (x : Finset α),
  Finset.strongInduction H x =
    have s := x;
    H s fun t h =>
      have this := ⋯;
      Finset.strongInduction H t
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_eq_sum : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] {f : R →+* S} {x : S},
  Polynomial.eval₂ f x p = p.sum fun e a => f a * x ^ e
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Ico_add : ∀ {α : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid α] [inst_2 : PartialOrder α]
  [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [inst_5 : LocallyFiniteOrder α] (f : α → M) (a b c : α),
  ∑ x ∈ Finset.Ico a b, f (c + x) = ∑ x ∈ Finset.Ico (a + c) (b + c), f x
-- Mathlib.NumberTheory.Dioph
/-- Diophantine sets are closed under intersection.  -/
Dioph.«term_D∧_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.Hom.Basic
ZeroHom.instSub.eq_1 : ∀ {M : Type u_2} {N : Type u_3} [inst : Zero M] [inst_1 : SubtractionMonoid N],
  ZeroHom.instSub = { sub := fun f g => { toFun := fun m => f m - g m, map_zero' := ⋯ } }
-- Mathlib.Algebra.Field.Basic
/-- Constructs a `DivisionRing` structure on a `Ring` consisting only of units and 0.  -/
DivisionRing.ofIsUnitOrEqZero : {R : Type u_3} → [Nontrivial R] → [inst : Ring R] → (∀ (a : R), IsUnit a ∨ a = 0) → DivisionRing R
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.incl.sizeOf_spec : ∀ {R : Type u} [inst : SizeOf R] (x : R), sizeOf (Rack.PreEnvelGroup.incl x) = 1 + sizeOf x
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toSentence.eq_7 : FirstOrder.Field.FieldAxiom.existsInv.toSentence =
  ((((FirstOrder.Language.var ∘ Sum.inr) 0).bdEqual 0).not.imp
      (((FirstOrder.Language.var ∘ Sum.inr) 0 * (FirstOrder.Language.var ∘ Sum.inr) 1).bdEqual 1).ex).all
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening_iUnion : ∀ {ι : Sort u_1} {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (f : ι → Set α),
  Metric.thickening δ (⋃ i, f i) = ⋃ i, Metric.thickening δ (f i)
-- Std.Http.Protocol.H1.Reader
/-- Checks if the reader is in a closed state and cannot process more messages.
 -/
Std.Http.Protocol.H1.Reader.isClosed : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_containsKey_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.containsKey a (Std.Internal.List.eraseKey k l) = true → Std.Internal.List.containsKey a l = true
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.continuous_eval₂ : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : TopologicalSpace R] [IsTopologicalSemiring R]
  [inst_3 : Semiring S] (p : Polynomial S) (f : S →+* R), Continuous fun x => Polynomial.eval₂ f x p
-- Mathlib.Probability.Kernel.Composition.KernelLemmas
ProbabilityTheory.Kernel.parallelComp_id_left_comp_parallelComp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {T : Type u_4} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  {mZ : MeasurableSpace Z} {mT : MeasurableSpace T} {κ : ProbabilityTheory.Kernel X Y} {X' : Type u_5}
  {mX' : MeasurableSpace X'} {η : ProbabilityTheory.Kernel X' Z} [ProbabilityTheory.IsSFiniteKernel η]
  {ξ : ProbabilityTheory.Kernel Z T} [ProbabilityTheory.IsSFiniteKernel ξ],
  (ProbabilityTheory.Kernel.id.parallelComp ξ).comp (κ.parallelComp η) = κ.parallelComp (ξ.comp η)
-- Mathlib.Analysis.Normed.Lp.lpSpace
memℓp_zero_iff : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
  Memℓp f 0 ↔ {i | f i ≠ 0}.Finite