mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- The adjunction between restriction to `Over x` and pushforward along `Over.star x`.  -/
SheafOfModules.overPushforwardOverAdj : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] →
      {J : CategoryTheory.GrothendieckTopology C} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (x : C) →
            SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id (R.over x)) ⊣
              SheafOfModules.pushforward (SheafOfModules.pushforwardOver x)
-- Mathlib.Topology.Convenient.Category
/-- The counit isomorphism of the equivalence `ContinuousGeneratedByCat.equivalence`.  -/
ContinuousGeneratedByCat.equivalenceCounitIso : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      ContinuousGeneratedByCat.toGeneratedByTopCat.comp ContinuousGeneratedByCat.fromGeneratedByTopCat ≅
        CategoryTheory.Functor.id (ContinuousGeneratedByCat X)
-- Mathlib.Data.Finset.Sort
List.toFinset_sort : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r] [inst_2 : Std.Antisymm r]
  [inst_3 : Std.Total r] [inst_4 : DecidableEq α] {l : List α}, l.Nodup → (l.toFinset.sort r = l ↔ List.Pairwise r l)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β} [inst : Inhabited β],
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → Std.DHashMap.Const.get! (Std.DHashMap.Const.ofList l) k' = v
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Set.toFinset_one : ∀ {α : Type u_2} [inst : One α], Set.toFinset 1 = 1
-- Mathlib.Analysis.LocallyConvex.WeakDual
/-- A linear functional `φ` is in the span of a collection of linear functionals if and only if `φ`
is continuous with respect to the topology induced by the collection of linear functionals. See
`LinearMap.mem_span_iff_continuous_of_finite` for a result about finite collections of linear
functionals.  -/
LinearMap.mem_span_iff_continuous : ∀ {ι : Type u_4} {𝕜 : Type u_5} {E : Type u_6} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜), φ ∈ Submodule.span 𝕜 (Set.range f) ↔ Continuous ⇑φ
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Functor.faithful_of_comp_cancel_zero_of_hasLeftCalculusOfFractions : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] {E : Type u_3}
  [inst_4 : CategoryTheory.Category.{v_3, u_3} E] (F : CategoryTheory.Functor D E) [W.HasLeftCalculusOfFractions]
  [inst_6 : CategoryTheory.Preadditive D] [inst_7 : CategoryTheory.Preadditive E] [L.Additive] [F.Additive],
  (∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0) → F.Faithful
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift_comp_lift_apply_eq_self : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : PerfectRing M p]
  [inst_6 : IsPRadical i p] [inst_7 : ExpChar L p] [inst_8 : IsPRadical j p] [inst_9 : PerfectRing L p] (x : L),
  (PerfectRing.lift j i p) ((PerfectRing.lift i j p) x) = x
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.abs_rpow_of_nonneg : ∀ {x y : ℝ}, 0 ≤ x → |x ^ y| = |x| ^ y
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!_erase_eq_of_not_compare_min!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, t.erase k ≠ ∅ → ¬cmp k t.min! = Ordering.eq → (t.erase k).min! = t.min!
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- Let `s` be a subset of an additive semigroup `M` such that the closure of `s` is the whole
semigroup.  Then `AddHom.ofDense` defines an additive homomorphism from `M` asking for a proof
of `f (x + y) = f x + f y` only for `y ∈ s`.  -/
AddHom.ofDense : {M : Type u_3} →
  {N : Type u_4} →
    [inst : AddSemigroup M] →
      [inst_1 : AddSemigroup N] →
        {s : Set M} →
          (f : M → N) → AddSubsemigroup.closure s = ⊤ → (∀ (x y : M), y ∈ s → f (x + y) = f x + f y) → M →ₙ+ N
-- Mathlib.CategoryTheory.Linear.FunctorCategory
CategoryTheory.NatTrans.app_smul : ∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Linear R D] {F G : CategoryTheory.Functor C D} (X : C) (r : R) (α : F ⟶ G),
  (r • α).app X = r • α.app X
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.integral_cauchyPDFReal_eq_one : ∀ (x₀ : ℝ) {γ : NNReal}, γ ≠ 0 → ∫ (x : ℝ), ProbabilityTheory.cauchyPDFReal x₀ γ x = 1
-- Init.Control.StateRef
StateRefT'.instMonadStateOfOfMonadLiftTST : {ω σ : Type} → {m : Type → Type} → [MonadLiftT (ST ω) m] → MonadStateOf σ (StateRefT' ω σ m)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.smul_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.IsCofiltered C] [inst_3 : CategoryTheory.InitiallySmall C]
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R}
  (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf}
  (hcM : CategoryTheory.Limits.IsColimit cM) {U : Cᵒᵖ} (r : ↑(R.obj U)) (m : ↑(M.obj U)),
  (PresheafOfModules.ModuleColimit.ιR cR) r • PresheafOfModules.ModuleColimit.ιM m =
    PresheafOfModules.ModuleColimit.ιM (r • m)
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.range_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (p : F' ⟶ F)
  (U : C), (CategoryTheory.Subfunctor.range p).obj U = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (p.app U))
-- Mathlib.MeasureTheory.Measure.DiracProba
MeasureTheory.diracProba.eq_1 : ∀ {X : Type u_1} [inst : MeasurableSpace X] (x : X), MeasureTheory.diracProba x = ⟨MeasureTheory.Measure.dirac x, ⋯⟩
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.CompStruct.map_simplex : ∀ {X Y : SSet.Truncated 2}
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
  (h : e₀₁.CompStruct e₁₂ e₀₂) (f : X ⟶ Y),
  (h.map f).simplex =
    (CategoryTheory.ConcreteCategory.hom
        (f.app (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.Edge.CompStruct._proof_1 })))
      h.simplex
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
MeasureTheory.lintegral_map' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {f : β → ENNReal} {g : α → β},
  AEMeasurable f (MeasureTheory.Measure.map g μ) →
    AEMeasurable g μ → ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_le_size_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β}, m.size - 1 ≤ (Std.ExtDHashMap.Const.alter m k f).size
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.of_carrier : ∀ (R : RingCat), RingCat.of ↑R = R
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiffOn.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_11} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_12}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {f : M → M'} {s : Set M} {n : WithTop ℕ∞} {g : N → N'} {r : Set N},
  ContMDiffOn I I' n f s → ContMDiffOn J J' n g r → ContMDiffOn (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r)
-- Mathlib.Analysis.LocallyConvex.Basic
balanced_iUnion₂ : ∀ {𝕜 : Type u_1} {E : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E]
  {f : (i : ι) → κ i → Set E}, (∀ (i : ι) (j : κ i), Balanced 𝕜 (f i j)) → Balanced 𝕜 (⋃ i, ⋃ j, f i j)
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.mem_sup : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R} {x : R},
  x ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_eq_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited α] {k : α}, t.contains k = true → t.get! k = k
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isDetecting_iff_isSeparating : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Balanced C], P.IsDetecting ↔ P.IsSeparating
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_inv : ∀ {R : Type u} {M : Type v} [inst : Neg M] [inst_1 : Inv R] [inst_2 : SMul Rᵐᵒᵖ M] [inst_3 : SMul R M]
  (x : TrivSqZeroExt R M), x⁻¹.fst = x.fst⁻¹
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Further restricting the functor
`restrictedYoneda : Over A ⥤ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v` along the forgetful
functor in the first argument recovers the Yoneda embedding
`CostructuredArrow yoneda A ⥤ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v`. This basically follows
from the fact that the Yoneda embedding on `C` is fully faithful.  -/
CategoryTheory.OverPresheafAux.toOverYonedaCompRestrictedYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).comp
          (CategoryTheory.OverPresheafAux.restrictedYoneda A) ≅
        CategoryTheory.yoneda
-- Mathlib.Probability.Independence.Kernel.IndepFun
/-- Two random variables `f, g` are independent given a kernel `κ` and a measure `μ` iff
`μ ⊗ₘ κ.map (fun ω ↦ (f ω, g ω)) = μ ⊗ₘ (κ.map f ×ₖ κ.map g)`.  -/
ProbabilityTheory.Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map : ∀ {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {γ : Type u_6} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] {f : Ω → β} {g : Ω → γ},
  Measurable f →
    Measurable g →
      (ProbabilityTheory.Kernel.IndepFun f g κ μ ↔
        μ.compProd (κ.map fun ω => (f ω, g ω)) = μ.compProd ((κ.map f).prod (κ.map g)))
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.instMonoIntι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)],
  CategoryTheory.Mono (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι✝ f n₀)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instHasFramePureTrue : ∀ {φ : Prop} (σs : List (Type u_1)), Std.Do.SPred.Tactic.HasFrame ⌜φ⌝ ⌜True⌝ φ
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The inverse of a bijective equivariant map is equivariant.  -/
MulActionHom.inverse : {M : Type u_2} →
  {X : Type u_5} →
    [inst : SMul M X] →
      {Y₁ : Type u_8} →
        [inst_1 : SMul M Y₁] →
          (f : X →ₑ[id] Y₁) → (g : Y₁ → X) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → Y₁ →ₑ[id] X
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainTop.congr_simp : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α α_1 : L → R),
  α = α_1 → ∀ (β β_1 : LieModule.Weight R L M), β = β_1 → LieModule.chainTop α β = LieModule.chainTop α_1 β_1
-- Mathlib.RingTheory.Valuation.Basic
Valuation.ltAddSubgroup_monotone : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀),
  Monotone v.ltAddSubgroup
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.reorder.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.reorder c) = 1 + sizeOf c
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_mul_left_one : ∀ {α : Type u_2} [inst : Group α] {a : α}, (fun x => a * x) ⁻¹' 1 = {a⁻¹}
-- Lean.Elab.Tactic.Omega.OmegaM
Lean.Elab.Tactic.Omega.State.mk.injEq : ∀ (atoms atoms_1 : Std.HashMap Lean.Expr ℕ), ({ atoms := atoms } = { atoms := atoms_1 }) = (atoms = atoms_1)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.inter_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T)
  (F : CategoryTheory.PreZeroHypercover T)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (i : E.I₀ × F.1),
  (E.inter F).f i =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (E.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm i).fst)
        (F.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm i).snd))
      (E.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm i).fst)
-- Init.Data.Option.Lemmas
Option.pbind_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (o : Option α) (f : α → β)
  (g : (x : β) → Option.map f o = some x → Option γ), (Option.map f o).pbind g = o.pbind fun x h => g (f x) ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- A strong monomorphism `f` is a monomorphism which has the right lifting property
with respect to epimorphisms.  -/
CategoryTheory.StrongMono : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {P Q : C} → (P ⟶ Q) → Prop
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} [hi : Inhabited (β k')] {f : β k → β k},
  (t.modify k f).get! k' =
    if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).get! else t.get! k'
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryLED : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → (a : α) × β a → (a : α) × β a
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.iInf_toSubalgebra : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Sort u_3}
  (S : ι → IntermediateField F E), (iInf S).toSubalgebra = ⨅ i, (S i).toSubalgebra
-- Mathlib.MeasureTheory.Integral.CircleIntegral
ContinuousOn.circleIntegrable' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} {R : ℝ},
  ContinuousOn f (Metric.sphere c |R|) → CircleIntegrable f c R
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the smallest element of the tree set, panicking if the set is empty.
 -/
Std.ExtTreeSet.min! : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeSet α cmp → α
-- Init.Data.Array.Find
Array.idxOf_append : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs ys : Array α} {a : α},
  Array.idxOf a (xs ++ ys) = if a ∈ xs then Array.idxOf a xs else Array.idxOf a ys + xs.size
-- Mathlib.Order.Filter.Pointwise
Filter.smulCommClass_filter'' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α γ] [inst_1 : SMul β γ] [SMulCommClass α β γ],
  SMulCommClass (Filter α) β (Filter γ)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftId_hom_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  (X : CategoryTheory.MorphismProperty.Comma L R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftId L R).hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_inter_mul_sdiff : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set α} (t : Set α),
  s.Finite → (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s \ t), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.coeSubmodule_span_singleton : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R),
  IsLocalization.coeSubmodule S (Ideal.span {x}) = R ∙ (algebraMap R S) x
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.ne_natCast : ∀ (z : UpperHalfPlane) (n : ℕ), ↑z ≠ ↑n
-- Mathlib.Order.Filter.Extr
IsMaxOn.sub : ∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] {f g : α → β}
  {a : α} {s : Set α}, IsMaxOn f s a → IsMinOn g s a → IsMaxOn (fun x => f x - g x) s a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.nil_map_iff : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} {p : G.Walk u v},
  (SimpleGraph.Walk.map f p).Nil ↔ p.Nil
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_le_degree_of_support_subset : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {p q : MvPolynomial σ R},
  p.support ⊆ q.support → m.toSyn (m.degree p) ≤ m.toSyn (m.degree q)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- The `ℕ`-algebra equivalence between `Subsemiring.closure s` and `Algebra.adjoin ℕ s` given
by the identity map.  -/
Subsemiring.closureEquivAdjoinNat : {R : Type u_1} → [inst : Semiring R] → (s : Set R) → ↥(Subsemiring.closure s) ≃ₐ[ℕ] ↥(Algebra.adjoin ℕ s)
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.foldWithLeadingToken.go : {α : Type} →
  (α → Option Lean.Syntax → Lean.Syntax → α) →
    [Inhabited α] → Option Lean.Syntax → α → Lean.Syntax → Option Lean.Syntax × α
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.widePullbackShapeEquivObj.match_1.eq_1 : ∀ {J : Type u_1} (motive : CategoryTheory.Limits.WidePullbackShape J → Sort u_2) (x : J)
  (h_1 : (x : J) → motive (some x)) (h_2 : Unit → motive none),
  (match some x with
    | some x => h_1 x
    | none => h_2 ()) =
    h_1 x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.hasDerivAt_arctan : ∀ (x : ℝ), HasDerivAt Real.arctan (1 / (1 + x ^ 2)) x
-- Init.Data.Int.DivMod.Lemmas
Int.mul_sub_ediv_left : ∀ (b : ℤ) {a : ℤ} (c : ℤ), a ≠ 0 → (a * b - c) / a = b + -c / a
-- Mathlib.LinearAlgebra.StdBasis
Pi.basisFun_repr : ∀ (R : Type u_2) (η : Type u_4) [inst : Semiring R] [inst_1 : Finite η] (x : η → R) (i : η),
  ((Pi.basisFun R η).repr x) i = x i
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.coe_comp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] [inst_4 : NonUnitalNonAssocSemiring C] [inst_5 : Star C]
  (f : B →⋆ₙ+* C) (g : A →⋆ₙ+* B), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_univ_le_one : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν → ∀ᵐ (ω' : Ω') ∂ν, (κ ω') Set.univ ≤ 1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentHighlightKind : Lean.ToJson Lean.Lsp.DocumentHighlightKind
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.skipSuffix?_prop_eq_skipSuffix?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.skipSuffix? p = s.skipSuffix? fun x => decide (p x)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryCoproductColimit_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w))
  (s : CategoryTheory.Limits.BinaryCofan F G),
  (CategoryTheory.FunctorToTypes.binaryCoproductColimit F G).desc s =
    CategoryTheory.FunctorToTypes.coprod.desc s.inl s.inr
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.get?.eq_1 : ∀ {α : Type u} (s : Stream'.WSeq α) (n : ℕ), s.get? n = (s.drop n).head
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.BifibrantObject.instIsFibrantObjBifibrantObjects : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.BifibrantObject C),
  HomotopicalAlgebra.IsFibrant X.obj
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.link2.match_5.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.Balanced → Sort u_3)
  (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (h_1 :
    (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf → motive Std.DTreeMap.Internal.Impl.leaf hr)
  (h_2 :
    (szr : ℕ) →
      (k'' : α) →
        (v'' : β k'') →
          (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced) →
              Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'' →
                motive (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'') hr),
  (match hr' : Std.DTreeMap.Internal.Impl.leaf, hr with
    | Std.DTreeMap.Internal.Impl.leaf, hr => h_1 hr hr'
    | Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'', hr => h_2 szr k'' v'' l'' r'' hr hr') =
    h_1 hr ⋯
-- Mathlib.Data.List.Range
List.isChain_range_succ : ∀ (r : ℕ → ℕ → Prop) (n : ℕ), List.IsChain r (List.range n.succ) ↔ ∀ m < n, r m m.succ