mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.seminorm_eq_bot_of_gt : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {i : ℕ},
  n < ↑i → ContDiffMapSupportedIn.seminorm 𝕜 E F n K i = ⊥
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- The instance `Algebra k (SkewMonoidAlgebra A G)` whenever we have `Algebra k A`.
In particular this provides the instance `Algebra k (SkewMonoidAlgebra k G)`.  -/
SkewMonoidAlgebra.instAlgebraOfSMulCommClass : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Monoid G] →
      [inst_1 : CommSemiring k] →
        {A : Type u_3} →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra k A] →
              [inst_4 : MulSemiringAction G A] → [SMulCommClass G k A] → Algebra k (SkewMonoidAlgebra A G)
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.of_lt_right : ∀ {α : Type u_1} {a b b' : α} [inst : LinearOrder α], a < b → b = b' → ¬b' ≤ a
-- Init.Data.List.Basic
/-- Treats the list as an association list that maps keys to values, returning the first value whose key
is equal to the specified key.

`O(|l|)`.

Examples:
* `[(1, "one"), (3, "three"), (3, "other")].lookup 3 = some "three"`
* `[(1, "one"), (3, "three"), (3, "other")].lookup 2 = none`
 -/
List.lookup : {α : Type u} → {β : Type v} → [BEq α] → α → List (α × β) → Option β
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.instOne : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : Zero ι] → [GradedMonoid.GOne A] → [inst : (i : ι) → AddCommMonoid (A i)] → One (DirectSum ι fun i => A i)
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- The left homotopy relation is transitive.
 -/
SSet.Truncated.HomotopicL.trans : ∀ {X : SSet.Truncated 2} [X.Quasicategory₂]
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f g h : SSet.Truncated.Edge x y},
  SSet.Truncated.HomotopicL f g → SSet.Truncated.HomotopicL g h → SSet.Truncated.HomotopicL f h
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
/-- The lift (as a continuous linear map) of `f` with `f x = f y` for `Inseparable x y`.  -/
SeparationQuotient.liftCLM : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ContinuousAdd M] →
                  [inst_5 : ContinuousConstSMul R M] →
                    [inst_6 : Semiring S] →
                      [inst_7 : AddCommMonoid N] →
                        [inst_8 : Module S N] →
                          [inst_9 : TopologicalSpace N] →
                            {σ : R →+* S} →
                              (f : M →SL[σ] N) →
                                (∀ (x y : M), Inseparable x y → f x = f y) → SeparationQuotient M →SL[σ] N
-- Aesop.Index.Basic
Aesop.instInhabitedIndexMatchLocation.default : Aesop.IndexMatchLocation
-- Lean.Expr
Lean.Expr.lit.sizeOf_spec : ∀ (a : Lean.Literal), sizeOf (Lean.Expr.lit a) = 1 + sizeOf a
-- Mathlib.Geometry.Euclidean.MongePoint
/-- For any three points in an orthocentric system generated by
triangle `t`, there is a point in the subspace spanned by the triangle
from which the distance of all those three points equals the circumradius.  -/
EuclideanGeometry.exists_dist_eq_circumradius_of_subset_insert_orthocenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {t : Affine.Triangle ℝ P},
  t.orthocenter ∉ Set.range t.points →
    ∀ {p : Fin 3 → P},
      Set.range p ⊆ insert t.orthocenter (Set.range t.points) →
        Function.Injective p →
          ∃ c ∈ affineSpan ℝ (Set.range t.points), ∀ p₁ ∈ Set.range p, dist p₁ c = Affine.Simplex.circumradius t
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.vadd_Lp_add : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f g : ↥(MeasureTheory.Lp E p μ)), c +ᵥ f + g = (c +ᵥ f) + (c +ᵥ g)
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_four : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  Nat.card α = 4 → ∀ (S : Sylow 2 ↥(alternatingGroup α)), ↑S = alternatingGroup.kleinFour α
-- Mathlib.GroupTheory.Complement
Subgroup.instInhabitedRightTransversal : {G : Type u_1} → [inst : Group G] → {H : Subgroup G} → Inhabited H.RightTransversal
-- Mathlib.Logic.Unique
/-- Every provable proposition is unique, as all proofs are equal.  -/
uniqueProp : {p : Prop} → p → Unique p
-- Mathlib.Topology.UniformSpace.CompactConvergence
Filter.HasBasis.compactConvergenceUniformity_of_compact : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] [CompactSpace α] {ι : Sort u_1}
  {p : ι → Prop} {V : ι → Set (β × β)},
  (uniformity β).HasBasis p V → (uniformity C(α, β)).HasBasis p fun i => {fg | ∀ (x : α), (fg.1 x, fg.2 x) ∈ V i}
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.nu_lt_one_of_prime : ∀ (self : BoundingSieve) (p : ℕ), Nat.Prime p → p ∣ self.prodPrimes → self.nu p < 1
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- An explicit pullback cone over `cospan f g` if `f` is an open immersion.  -/
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullbackConeOfLeft : {X Y Z : AlgebraicGeometry.LocallyRingedSpace} →
  (f : X ⟶ Z) →
    (g : Y ⟶ Z) → [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] → CategoryTheory.Limits.PullbackCone f g
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
Homeomorph.isSimplyConnected_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X ≃ₜ Y) {s : Set Y},
  IsSimplyConnected (⇑f ⁻¹' s) ↔ IsSimplyConnected s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isSome_getElem?_iff_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m[a]?.isSome = true ↔ a ∈ m
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Naturality of the lax functoriality constraint, on the right.  -/
CategoryTheory.LaxFunctor.mapComp_naturality_right_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat)
  {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (X : ↑(self.obj a)) {Z : ↑(self.obj c)}
  (h : (self.map (CategoryTheory.CategoryStruct.comp f g')).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)).toNatTrans.app X)
        h) =
    CategoryTheory.CategoryStruct.comp ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((self.mapComp f g').toNatTrans.app X) h)
-- Mathlib.Order.Hom.Bounded
/-- A `TopHomClass` morphism preserves the top element.  -/
TopHomClass.map_top : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : Top α} {inst_1 : Top β}
  {inst_2 : FunLike F α β} [self : TopHomClass F α β] (f : F), f ⊤ = ⊤
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- If `μ 1 ≤ 1` and `∀ y : R, μ (x * y) = μ x * μ y`, then `smoothingFun μ x = μ x`.  -/
smoothingFun_apply_of_map_mul_eq_mul : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R),
  μ 1 ≤ 1 → ∀ {x : R}, (∀ (y : R), μ (x * y) = μ x * μ y) → smoothingFun μ x = μ x
-- Init.Data.Format.Basic
Std.Format.align.injEq : ∀ (force force_1 : Bool), (Std.Format.align force = Std.Format.align force_1) = (force = force_1)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_sub_right : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Sub α] [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] (s t : Finset α) (f : α → β), (s - t).sup f = t.sup fun y => s.sup fun x => f (x - y)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_toArray_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {k : α} {v : β k}, m.WF → (⟨k, v⟩ ∈ m.toArray ↔ m.get? k = some v)
-- Lean.Meta.Basic
/-- Return `some mvarDecl` where `mvarDecl` is `mvarId` declaration in the current metavariable context.
Return `none` if `mvarId` has no declaration in the current metavariable context.
 -/
Lean.MVarId.findDecl? : Lean.MVarId → Lean.MetaM (Option Lean.MetavarDecl)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {km : α}, t.maxKey? = some km → t.getKey! km = km
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_insert : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF →
    ∀ {k a : α} {v : β},
      Std.DHashMap.Raw.Const.get! (m.insert k v) a = if (k == a) = true then v else Std.DHashMap.Raw.Const.get! m a
-- Mathlib.Order.CompleteLattice.Lemmas
Monotone.iSup_nat_add : ∀ {α : Type u_1} [inst : CompleteLattice α] {f : ℕ → α}, Monotone f → ∀ (k : ℕ), ⨆ n, f (n + k) = ⨆ n, f n
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_left_unitor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom =
    CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a).hom (self.map f))
        (CategoryTheory.Bicategory.leftUnitor (self.map f)).hom)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVLogicalExpr.eval_gate : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {g : Std.Tactic.BVDecide.Gate}
  {x y : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred},
  Std.Tactic.BVDecide.BVLogicalExpr.eval assign (Std.Tactic.BVDecide.BoolExpr.gate g x y) =
    g.eval (Std.Tactic.BVDecide.BVLogicalExpr.eval assign x) (Std.Tactic.BVDecide.BVLogicalExpr.eval assign y)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.instIsScalarTowerHahnSeries : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid V] [inst_2 : Zero R]
  {S : Type u_6} [inst_3 : Zero S] [inst_4 : SMul R S] [inst_5 : SMulWithZero R V] [inst_6 : SMulWithZero S V]
  [IsScalarTower R S V], IsScalarTower R S (HahnSeries Γ V)
-- Std.Data.DHashMap.Internal.Defs
Std.DHashMap.Internal.Raw.WFImp.mk : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β},
  Std.DHashMap.Internal.IsHashSelf m.buckets →
    m.size = (Std.DHashMap.Internal.toListModel m.buckets).length →
      Std.Internal.List.DistinctKeys (Std.DHashMap.Internal.toListModel m.buckets) → Std.DHashMap.Internal.Raw.WFImp m
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {fallback : α},
  ∅.minKeyD fallback = fallback
-- Mathlib.Topology.Connected.Basic
IsConnected.nonempty : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsConnected s → s.Nonempty
-- Mathlib.Logic.Function.Iterate
Function.LeftInverse.iterate : ∀ {α : Type u} {f g : α → α}, Function.LeftInverse g f → ∀ (n : ℕ), Function.LeftInverse g^[n] f^[n]
-- Mathlib.Data.List.Basic
List.mem_head?_append_of_mem_head? : ∀ {α : Type u} {s t : List α} {x : α}, x ∈ s.head? → x ∈ (s ++ t).head?
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty D) (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y),
  P.inverseImage F f ↔ P (F.map f)
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (f : α →ₙ+* β), (NonUnitalRingHom.id β).comp f = f
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- Continuous alternating maps themselves form a normed group with respect to the operator norm.  -/
ContinuousAlternatingMap.instNormedAddCommGroup : {𝕜 : Type u} →
  {E : Type wE} →
    {F : Type wF} →
      {ι : Type v} →
        [Fintype ι] →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → NormedAddCommGroup (E [⋀^ι]→L[𝕜] F)
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_div_le : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), ‖a / b‖₊ ≤ ‖a‖₊ + ‖b‖₊
-- Init.Data.UInt.BasicAux
/-- Subtracts one word-sized-bit unsigned integer from another, wrapping around on underflow. Usually
accessed via the `-` operator.

This function is overridden at runtime with an efficient implementation.
 -/
USize.sub : USize → USize → USize
-- Mathlib.Control.Monad.Cont
StateT.goto_mkLabel : ∀ {m : Type u → Type v} {α β σ : Type u} (x : MonadCont.Label (α × σ) m (β × σ)) (i : α),
  MonadCont.goto (StateT.mkLabel x) i = StateT.mk fun s => MonadCont.goto x (i, s)
-- Init.Data.SInt.Basic
/-- The largest number that `Int8` can represent: `2^7 - 1 = 127`.  -/
Int8.maxValue : Int8
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_finsetSum_index : ∀ {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  {s : Finset ι} {g : ι → α →₀ M} {h : α → M → N},
  (∀ (a : α), h a 0 = 0) →
    (∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) → ∑ i ∈ s, (g i).sum h = (∑ i ∈ s, g i).sum h
-- Mathlib.LinearAlgebra.Prod
/-- **Vertical line test** for linear maps.

Let `f : G → H × I` be a linear (or semilinear) map to a product. Assume that `f` is surjective on
the first factor and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` at
most once. Then the image of `f` is the graph of some linear map `f' : H → I`.  -/
LinearMap.exists_range_eq_graph : ∀ {R : Type u_3} {S : Type u_4} {G : Type u_5} {H : Type u_6} {I : Type u_7} [inst : Semiring R] [inst_1 : Semiring S]
  {σ : R →+* S} [inst_2 : RingHomSurjective σ] [inst_3 : AddCommMonoid G] [inst_4 : Module R G]
  [inst_5 : AddCommMonoid H] [inst_6 : Module S H] [inst_7 : AddCommMonoid I] [inst_8 : Module S I]
  {f : G →ₛₗ[σ] H × I},
  Function.Surjective (Prod.fst ∘ ⇑f) →
    (∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) → ∃ f', f.range = f'.graph
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (X Y : C) (f g : X ⟶ Y),
  CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y f g =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
      (CategoryTheory.Limits.biprod.desc f g)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.nsmul_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {x : A}, x ∈ S → ∀ (n : ℕ), n • x ∈ S
-- Mathlib.Data.List.Cycle
/-- The unique empty cycle.  -/
Cycle.nil : {α : Type u_1} → Cycle α
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.Nontrivial.of_polynomial_ne : ∀ {R : Type u_1} [inst : Semiring R] {p q : SkewPolynomial R} [MulSemiringAction (Multiplicative ℕ) R],
  p ≠ q → Nontrivial R
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_congr₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} {f g : β → γ → α} {M : SummationFilter γ},
  (∀ (b : β) (c : γ), f b c = g b c) → ∑'[L] (b : β), ∑'[M] (c : γ), f b c = ∑'[L] (b : β), ∑'[M] (c : γ), g b c
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_map : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (n : σ →₀ ℕ)
  (φ : MvPowerSeries σ R), (MvPowerSeries.coeff n) ((MvPowerSeries.map f) φ) = f ((MvPowerSeries.coeff n) φ)
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.inertiaDeg_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [inst_3 : q.LiesOver p] [inst_4 : q.IsPrime] [inst_5 : p.IsPrime]
  [inst_6 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
  [inst_7 : Localization.AtPrime.IsLiesOverAlgebra p q], q.inertiaDeg R = Module.finrank p.ResidueField q.ResidueField
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.drop_cons_eq : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (n : ℕ) (hn : n ≠ 0),
  (SimpleGraph.Walk.cons h p).drop n = (p.drop (n - 1)).copy ⋯ ⋯
-- Init.Control.StateCps
StateCpsT.runK_get : ∀ {σ : Type u} {m : Type u → Type v} {β : Type u} (s : σ) (k : σ → σ → m β), get.runK s k = k s s
-- Mathlib.Algebra.Category.ModuleCat.Images
ModuleCat.image.fac : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H),
  CategoryTheory.CategoryStruct.comp (ModuleCat.factorThruImage f) (ModuleCat.image.ι f) = f
-- Mathlib.Data.Part
Part.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (o : Part α), Part.map f o = { Dom := o.Dom, get := f ∘ o.get }
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.sectL_mapId_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (c : C)
  (x : B),
  ((CategoryTheory.Bicategory.Prod.sectL B c).mapId x).inv =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x))
      (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id c))
-- Mathlib.CategoryTheory.Grothendieck
/-- If `F : C ⥤ Cat` and `x : Grothendieck F`, then every `C`-isomorphism `α : x.base ≅ c` induces
an isomorphism between `x` and its transport along `α`
 -/
CategoryTheory.Grothendieck.transportIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      (x : CategoryTheory.Grothendieck F) → {c : C} → (α : x.base ≅ c) → x.transport α.hom ≅ x
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.ofHoms_homFamily : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  CategoryTheory.MorphismProperty.ofHoms P.homFamily = P
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
/-- Given a family of opens `opensLeCoverCocone U` is essentially the natural cocone
associated to the sieve generated by the presieve associated to `U` with indexing
category changed using the above equivalence.  -/
TopCat.Presheaf.whiskerIsoMapGenerateCocone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : TopCat} →
      (F : TopCat.Presheaf C X) →
        {ι : Type u_2} →
          (U : ι → TopologicalSpace.Opens ↑X) →
            {Y : TopologicalSpace.Opens ↑X} →
              (hY : Y = iSup U) →
                CategoryTheory.Limits.Cone.whisker (TopCat.Presheaf.generateEquivalenceOpensLe U hY).op.functor
                    (CategoryTheory.Functor.mapCone F (TopCat.Presheaf.SheafCondition.opensLeCoverCocone U).op) ≅
                  CategoryTheory.Functor.mapCone F
                    (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows.cocone.op
-- Mathlib.GroupTheory.Sylow
Sylow.instSetLike : {p : ℕ} → {G : Type u_1} → [inst : Group G] → SetLike (Sylow p G) G
-- Init.Data.Int.DivMod.Bootstrap
Int.ediv.eq_1 : ∀ (m n : ℕ), (Int.ofNat m).ediv (Int.ofNat n) = Int.ofNat (m / n)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_emptyCollection : ∀ (α : Type u), Cardinal.mk ↑∅ = 0
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.range_val : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  S.val.range = S.toSubalgebra
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertList_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l1 l2 l3 l4 : List ((a : α) × β a)},
  l1.Perm l3 →
    l2.Perm l4 →
      Std.Internal.List.DistinctKeys l1 →
        Std.Internal.List.DistinctKeys l2 →
          Std.Internal.List.DistinctKeys l3 →
            (Std.Internal.List.insertList l1 l2).Perm (Std.Internal.List.insertList l3 l4)
-- Mathlib.CategoryTheory.Sites.Equivalence
/-- Transporting to a small model and sheafifying there is left adjoint to the underlying presheaf
functor
 -/
CategoryTheory.smallSheafificationAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₃) →
        [inst_1 : CategoryTheory.Category.{v₃, u₃} A] →
          [inst_2 : CategoryTheory.EssentiallySmall.{w, v₁, u₁} C] →
            [inst_3 : CategoryTheory.HasSheafify ((CategoryTheory.equivSmallModel C).inverse.inducedTopology J) A] →
              CategoryTheory.smallSheafify J A ⊣ CategoryTheory.sheafToPresheaf J A
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.rankAtStalk_baseChange : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  [Module.Finite R M] {S : Type u_1} [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : PrimeSpectrum S),
  Module.rankAtStalk (TensorProduct R S M) p = Module.rankAtStalk M (PrimeSpectrum.comap (algebraMap R S) p)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.comp_hasFDerivWithinAt_iff' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} {x : G}
  {f' : G →L[𝕜] F}, HasFDerivWithinAt (⇑iso ∘ f) f' s x ↔ HasFDerivWithinAt f (↑↑iso.symm ∘SL f') s x
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.UnifIntegrable.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : NormedAddCommGroup β] {x : MeasurableSpace α} (f : ι → α → β)
  (p : ENNReal) (μ : MeasureTheory.Measure α),
  MeasureTheory.UnifIntegrable f p μ =
    ∀ ⦃ε : ℝ⦄,
      0 < ε →
        ∃ δ,
          ∃ (_ : 0 < δ),
            ∀ (i : ι) (s : Set α),
              MeasurableSet s →
                μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
-- Mathlib.Order.OmegaCompletePartialOrder
Part.omegaCompletePartialOrder : {α : Type u_2} → OmegaCompletePartialOrder (Part α)
-- Mathlib.MeasureTheory.Group.Arithmetic
Multiset.aemeasurable_fun_sum : ∀ {M : Type u_2} {α : Type u_4} [inst : AddCommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Multiset (α → M)),
  (∀ f ∈ s, AEMeasurable f μ) → AEMeasurable (fun x => (Multiset.map (fun f => f x) s).sum) μ
-- Mathlib.SetTheory.Lists
/-- Hereditarily finite list, aka ZFA list. A ZFA list is either an "atom" (`b = false`),
corresponding to an element of `α`, or a "proper" ZFA list, inductively defined from the empty ZFA
list and from appending a ZFA list to a proper ZFA list.  -/
Lists : Type u_2 → Type (max 0 u_2)