mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.HahnSeries.Valuation
HahnSeries.addVal_le_of_coeff_ne_zero : ∀ {Γ : Type u_1} {R : Type u_2} [inst : AddCancelCommMonoid Γ] [inst_1 : LinearOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : Ring R] [inst_4 : IsDomain R] {x : HahnSeries Γ R} {g : Γ},
  x.coeff g ≠ 0 → (HahnSeries.addVal Γ R) x ≤ ↑g
-- Init.Data.List.Zip
List.tail_zipWith : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {l : List α} {l' : List α_1},
  (List.zipWith f l l').tail = List.zipWith f l.tail l'.tail
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- This is a simple version of the **Unfolding Trick**: Given a subgroup `Γ` of a group `G`, the
integral of a function `f` on `G` with respect to a right-invariant measure `μ` is equal to the
integral over the quotient `G ⧸ Γ` of the automorphization of `f`.  -/
QuotientGroup.integral_eq_integral_automorphize : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G},
  MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ →
    ∀ [Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] {E : Type u_2}
      [inst_8 : NormedAddCommGroup E] [inst_9 : NormedSpace ℝ E] [μ.IsMulRightInvariant] {f : G → E},
      MeasureTheory.Integrable f μ →
        MeasureTheory.AEStronglyMeasurable (QuotientGroup.automorphize f)
            (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) →
          ∫ (x : G), f x ∂μ =
            ∫ (x : G ⧸ Γ), QuotientGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)
-- Std.Http.Data.Status
Std.Http.Status.gatewayTimeout.sizeOf_spec : sizeOf Std.Http.Status.gatewayTimeout = 1
-- Init.Data.String.Defs
List.utf8Encode_nil : [].utf8Encode = ByteArray.empty
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.hasIntScalar : (p n : ℕ) → (R : Type u_1) → [CommRing R] → [Fact (Nat.Prime p)] → SMul ℤ (TruncatedWittVector p n R)
-- Mathlib.Order.WellFounded
WellFounded.onFun : ∀ {α : Sort u_4} {β : Sort u_5} {r : β → β → Prop} {f : α → β}, WellFounded r → WellFounded (Function.onFun r f)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.map_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (b : Module.Basis ι R M) (f : M ≃ₗ[R] M')
  (i : ι), (b.map f) i = f (b i)
-- Mathlib.Combinatorics.SetFamily.LYM
Finset.slice_subset_falling : ∀ {α : Type u_2} [inst : DecidableEq α] (k : ℕ) (𝒜 : Finset (Finset α)), 𝒜.slice k ⊆ Finset.falling k 𝒜
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
/-- the data involved in a 1-cochain  -/
CategoryTheory.PresheafOfGroups.OneCochain.ev : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : CategoryTheory.Functor Cᵒᵖ GrpCat} →
      {I : Type w'} →
        {U : I → C} →
          CategoryTheory.PresheafOfGroups.OneCochain G U →
            (i j : I) → ⦃T : C⦄ → (T ⟶ U i) → (T ⟶ U j) → ↑(G.obj (Opposite.op T))
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.mkNatIso.congr_simp : ∀ {V : SSet.Truncated 2} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D]
  {F G : CategoryTheory.Functor V.HomotopyCategory D}
  (iso iso_1 :
    (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })) →
      F.obj (SSet.Truncated.HomotopyCategory.mk x) ≅ G.obj (SSet.Truncated.HomotopyCategory.mk x))
  (e_iso : iso = iso_1)
  (hiso :
    ∀ ⦃x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })⦄
      (e : SSet.Truncated.Edge x y),
      CategoryTheory.CategoryStruct.comp (F.map (SSet.Truncated.HomotopyCategory.homMk e)) (iso y).hom =
        CategoryTheory.CategoryStruct.comp (iso x).hom (G.map (SSet.Truncated.HomotopyCategory.homMk e))),
  SSet.Truncated.HomotopyCategory.mkNatIso iso hiso = SSet.Truncated.HomotopyCategory.mkNatIso iso_1 ⋯
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLE'Map_comp_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [inst_2 : e.IsTruncLE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : ∀ (i' : ι'), M.HasHomology i'] {Z : HomologicalComplex C c} (h : M.truncLE' e ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncLE'Map (CategoryTheory.CategoryStruct.comp φ φ') e) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncLE'Map φ e)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncLE'Map φ' e) h)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_le_maxKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β k} {fallback : α}, (cmp (t.maxKeyD fallback) ((t.insert k v).maxKeyD fallback)).isLE = true
-- Mathlib.Tactic.Have
Mathlib.Tactic.optBinderIdent.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- In the presence of zero morphisms, projections into a product are (split) epimorphisms.  -/
CategoryTheory.Limits.isSplitEpi_prod_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  [inst_2 : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)],
  CategoryTheory.IsSplitEpi CategoryTheory.Limits.prod.fst
-- Init.Data.String.Lemmas.Splits
String.Slice.copy_sliceTo_eq_iff_splits : ∀ {s : String.Slice} {p : s.Pos} {t₁ : String}, (s.sliceTo p).copy = t₁ ↔ p.Splits t₁ (s.sliceFrom p).copy
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.lift_comp_neg_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj B] (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f
        (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg))
      CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
      CategoryTheory.AddMonObj.zero
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} {I : CategoryTheory.InjectiveResolution Z} {Z' : C}
  {I' : CategoryTheory.InjectiveResolution Z'} {f : Z ⟶ Z'} [inst_3 : SizeOf C] (hom : I.cocomplex ⟶ I'.cocomplex)
  (ι_f_zero_comp_hom_f_zero :
    CategoryTheory.CategoryStruct.comp (I.ι.f 0) (hom.f 0) =
      CategoryTheory.CategoryStruct.comp (((CochainComplex.single₀ C).map f).f 0) (I'.ι.f 0)),
  sizeOf { hom := hom, ι_f_zero_comp_hom_f_zero := ι_f_zero_comp_hom_f_zero } =
    1 + sizeOf hom + sizeOf ι_f_zero_comp_hom_f_zero
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_ofNat_succ : ∀ {R : Type u} [inst : Semiring R] (a n : ℕ) [h : a.AtLeastTwo], (OfNat.ofNat a).coeff (n + 1) = 0
-- Mathlib.Data.Set.Sigma
Set.mk_preimage_sigma_eq_if : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} [inst : DecidablePred fun x => x ∈ s],
  Sigma.mk i ⁻¹' s.sigma t = if i ∈ s then t i else ∅
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
/-- The property of objects that are the point of a limit cone for a
functor `F : J ⥤ C` where all objects `F.obj j` satisfy `P`.  -/
CategoryTheory.ObjectProperty.limitsOfShape : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C →
      (J : Type u') → [CategoryTheory.Category.{v', u'} J] → CategoryTheory.ObjectProperty C
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.G.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J GrpCat),
  GrpCat.FilteredColimits.G F = MonCat.FilteredColimits.colimit (F.comp (CategoryTheory.forget₂ GrpCat MonCat))
-- Mathlib.MeasureTheory.Group.Convolution
/-- Convolution is associative.  -/
MeasureTheory.Measure.conv_assoc : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] (μ ν ρ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite ρ], (μ.conv ν).conv ρ = μ.conv (ν.conv ρ)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfpFamily_le_iff : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Small.{u, u_1} ι] {a b : Ordinal.{u}},
  Ordinal.nfpFamily f a ≤ b ↔ ∀ (l : List ι), List.foldr f a l ≤ b
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
/-- A family of 1-hypercovers consists of the data of a predicate on
`OneHypercover.{w} J X` for all `X`.  -/
CategoryTheory.GrothendieckTopology.OneHypercoverFamily : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C → Type (max (max u (w + 1)) v)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false → ∀ {k fallback : α}, (cmp (t.maxKeyD fallback) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Order.CompleteLattice.Basic
biInf_le : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} {s : Set ι} (f : ι → α) {i : ι}, i ∈ s → ⨅ i ∈ s, f i ≤ f i
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_insertManyIfNewUnit_emptyWithCapacity_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α} {k : α}
  {h :
    (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).contains
        k =
      true},
  Std.DHashMap.Internal.Raw₀.Const.get
      (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k h =
    ()
-- Mathlib.Algebra.Ring.GeomSum
geom_sum₂_mul : ∀ {R : Type u_1} [inst : CommRing R] (x y : R) (n : ℕ),
  (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
-- Mathlib.Order.Directed
/-- A monotone function on an upwards-directed type is directed.  -/
directed_of_isDirected_le : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [IsDirectedOrder α] {f : α → β} {r : β → β → Prop},
  (∀ ⦃i j : α⦄, i ≤ j → r (f i) (f j)) → Directed r f
-- Lean.Setup
Lean.instInhabitedImportArtifacts : Inhabited Lean.ImportArtifacts
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.lTensorHomToHomLTensor_apply : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {P : Type u_9}
  {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid N₂]
  [inst_5 : Module R₂ M₂] [inst_6 : Module R₂ N₂] [inst_7 : Module R P] (m₂ : M₂) (f : P →ₛₗ[σ₁₂] N₂) (p : P),
  ((TensorProduct.lTensorHomToHomLTensor σ₁₂ P M₂ N₂) (m₂ ⊗ₜ[R₂] f)) p = m₂ ⊗ₜ[R₂] f p
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- A seminorm on a group `G` is a function `f : G → ℝ` that sends one to zero, is submultiplicative
and such that `f x⁻¹ = f x` for all `x`.  -/
GroupSeminorm : (G : Type u_6) → [Group G] → Type u_6
-- Mathlib.Tactic.Core
/-- Returns the root directory which contains the package root file, e.g. `Mathlib.lean`.  -/
Mathlib.getPackageDir : String → IO System.FilePath
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instVAdd'.eq_1 : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α], OrderDual.instVAdd' = inst
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.prodμ_inverse_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A] (X : (A × D) × C × E),
  (CategoryTheory.prod.prodμ C D E A).inverse.obj X = ((X.1.1, X.2.1), X.1.2, X.2.2)
-- Mathlib.Data.Finset.Union
Finset.disjiUnion_disjUnion : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f g : α → Finset β} (hfg : ∀ (a : α), Disjoint (f a) (g a))
  (hfg' : (↑s).Pairwise fun a₁ a₂ => Disjoint (f a₁) (g a₂)) (hf : (↑s).PairwiseDisjoint f)
  (hg : (↑s).PairwiseDisjoint g),
  s.disjiUnion (fun a => (f a).disjUnion (g a) ⋯) ⋯ = (s.disjiUnion f hf).disjUnion (s.disjiUnion g hg) ⋯
-- Init.Data.Vector.Lemmas
Vector.replace_append : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {n m : ℕ} {a b : α} {xs : Vector α n} {ys : Vector α m},
  (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.curriedTensor_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (Y_1 : C),
  ((CategoryTheory.MonoidalCategory.curriedTensor C).map f).app Y_1 =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y_1
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.atIdxSlow?_eq_match.match_3.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` reflects limits of shape `Jᵒᵖ`, then `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects colimits
of shape `J`.  -/
CategoryTheory.Limits.reflectsColimitsOfShape_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ)
  [CategoryTheory.Limits.ReflectsLimitsOfShape Jᵒᵖ F.unop], CategoryTheory.Limits.ReflectsColimitsOfShape J F
-- Mathlib.GroupTheory.PGroup
IsPGroup.center_nontrivial : ∀ {p : ℕ} {G : Type u_1} [inst : Group G],
  IsPGroup p G → ∀ [hp : Fact (Nat.Prime p)] [Nontrivial G] [Finite G], Nontrivial ↥(Subgroup.center G)
-- Mathlib.Topology.UnitInterval
Set.Icc.coe_convexComb : ∀ {a b : ℝ} (x y : ↑(Set.Icc a b)) (t : ↑unitInterval), ↑(Set.Icc.convexComb x y t) = (1 - ↑t) * ↑x + ↑t * ↑y
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instInhabitedOffset : Inhabited Std.Time.Minute.Offset
-- Mathlib.Algebra.BigOperators.Fin
/-- Let `(g₀, g₁, ..., gₙ)` be a tuple of elements in `Gⁿ⁺¹`.
Then if `k < j`, this says `-(g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ) = gₖ`.
If `k = j`, it says `-(g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ + gₖ₊₁`.
If `k > j`, it says `-(g₀ + g₁ + ... + gₖ) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ₊₁.`
Useful for defining group cohomology.  -/
Fin.neg_partialSum_add_eq_contractNth : ∀ {n : ℕ} {G : Type u_3} [inst : AddGroup G] (g : Fin (n + 1) → G) (j : Fin (n + 1)) (k : Fin n),
  -Fin.partialSum g (j.succ.succAbove k.castSucc) + Fin.partialSum g (j.succAbove k).succ =
    j.contractNth (fun x1 x2 => x1 + x2) g k
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_right_cert.eq_1 : ∀ (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (d : ℤ) (n : ℕ),
  Int.Internal.Linear.cooper_dvd_right_cert p₁ p₂ p₃ d n =
    Int.Internal.Linear.Poly.casesOn p₁ (fun x => false) fun a x x_1 =>
      Int.Internal.Linear.Poly.casesOn p₂ (fun x => false) fun b y x_2 =>
        Int.Internal.Linear.Poly.casesOn p₃ (fun x => false) fun c z x_3 =>
          Nat.beq x y &&
            (Nat.beq x z &&
              (decide (a < 0) && (decide (b > 0) && (decide (d > 0) && n.beq (b.lcm (b * d / ↑((b * d).gcd c)))))))
-- Mathlib.Order.CompleteLattice.Basic
biSup_ge_eq_of_antitone : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : Preorder β] {f : β → α},
  Antitone f → ∀ (b : β), ⨆ b', ⨆ (_ : b ≤ b'), f b' = f b
-- Init.Data.Array.Find
Array.findIdx?_flatten : ∀ {α : Type u_1} {xss : Array (Array α)} {p : α → Bool},
  Array.findIdx? p xss.flatten =
    Option.map
      (fun i => (Array.map Array.size (xss.take i)).sum + (Option.map (fun xs => Array.findIdx p xs) xss[i]?).getD 0)
      (Array.findIdx? (fun x => x.any p) xss)
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.toLinearMap_ofIsTopCompl : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} {F : Type u_3} [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : TopologicalSpace F] [inst_6 : AddCommGroup F]
  [inst_7 : Module R F] [inst_8 : ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ : ↥p →L[R] F)
  (ψ : ↥q →L[R] F), ↑(ContinuousLinearMap.ofIsTopCompl h φ ψ) = LinearMap.ofIsCompl ⋯ ↑φ ↑ψ
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Real.sub_le_dist : ∀ (x y : ℝ), x - y ≤ dist x y
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.evariance_def' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Ω → ℝ},
  MeasureTheory.AEStronglyMeasurable X μ →
    ProbabilityTheory.evariance X μ = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.le_limsup_mul : ∀ {ι : Type u_4} {f : Filter ι} {u v : ι → ENNReal}, Filter.limsup u f * Filter.liminf v f ≤ Filter.limsup (u * v) f
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.noncommSum_mem : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {ι : Type u_3} {t : Finset ι} {f : ι → G}
  (comm : (↑t).Pairwise (Function.onFun AddCommute f)), (∀ c ∈ t, f c ∈ K) → t.noncommSum f comm ∈ K
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.buckets_empty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {i : ℕ} {h : i < ∅.inner.buckets.size},
  ∅.inner.buckets[i] = Std.DHashMap.Internal.AssocList.nil
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- Relation between `Λ s` and the Mellin transform of `f - f₀`, where the latter is defined.
(Compare `IsStrongFEPair.hasMellin` for a version without assumptions on `s.re` assuming the
FE-pair is strong.)  -/
WeakFEPair.hasMellin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) [CompleteSpace E] {s : ℂ},
  P.k < s.re → HasMellin (fun x => P.f x - P.f₀) s (P.Λ s)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The postcomposition of a cocycle with a morphism of cochain complexes.  -/
CochainComplex.HomComplex.Cocycle.postcomp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G K : CochainComplex C ℤ} →
        {n : ℤ} → CochainComplex.HomComplex.Cocycle F G n → (G ⟶ K) → CochainComplex.HomComplex.Cocycle F K n
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.lintegral_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν → ∫⁻ (x : α), μ.rnDeriv ν x ∂ν = μ Set.univ
-- Mathlib.MeasureTheory.Measure.Tight
/-- A set of measures `S` is tight if for all `0 < ε`, there exists a compact set `K` such that
for all `μ ∈ S`, `μ Kᶜ ≤ ε`.
This is formulated in terms of filters, and proven equivalent to the definition above
in `IsTightMeasureSet_iff_exists_isCompact_measure_compl_le`.  -/
MeasureTheory.IsTightMeasureSet : {𝓧 : Type u_1} → {m𝓧 : MeasurableSpace 𝓧} → [TopologicalSpace 𝓧] → Set (MeasureTheory.Measure 𝓧) → Prop
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → ∀ {h : k' ∈ Std.DHashMap.Const.ofList l}, (Std.DHashMap.Const.ofList l).getKey k' h = k
-- Lean.ResolveName
_private.Lean.ResolveName.0.Lean.resolveLocalName.loop : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadResolveName m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [Lean.MonadLog m] →
            [Lean.AddMessageContext m] →
              Lean.MacroScopesView →
                (Lean.MacroScopesView → Bool → Option Lean.LocalDecl) →
                  Lean.Name → List String → Bool → m (Option (Lean.Expr × List String))
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- The canonical basis of the free group over `X`.  -/
FreeGroupBasis.ofFreeGroup : (X : Type u_5) → FreeGroupBasis X (FreeGroup X)
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
/-- The commutator subgroup of the permutation group is the alternating group  -/
alternatingGroup.commutator_perm_eq : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α],
  5 ≤ Nat.card α → commutator (Equiv.Perm α) = alternatingGroup α
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isNone_getElem?_toList_rcc_eq : ∀ {m n : ℤ} {i : ℕ}, ((m...=n).toList[i]?.isNone = true) = ((n + 1 - m).toNat ≤ i)
-- Aesop.Script.Tactic
Aesop.Script.STactic.mk.sizeOf_spec : ∀ (numSubgoals : ℕ) (run : Array (Array Lean.Syntax.Tactic) → Lean.Syntax.Tactic),
  sizeOf { numSubgoals := numSubgoals, run := run } = 1 + sizeOf numSubgoals
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPower.beq_spec_2 : ∀ (x x_1 : Lean.Grind.CommRing.Power),
  (∀ (a : Lean.Grind.CommRing.Var) (a_1 : ℕ) (b : Lean.Grind.CommRing.Var) (b_1 : ℕ),
      x = { x := a, k := a_1 } → x_1 = { x := b, k := b_1 } → False) →
    (x == x_1) = false
-- Lean.Parser.Extra
Lean.Parser.withSetOption.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.List.MinMax
List.argmax_nil : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] (f : α → β), List.argmax f [] = none
-- Lean.Meta.Tactic.Grind.Proof
/-- Given `lhs` and `rhs` proof terms of the form `nestedProof p hp` and `nestedProof q hq`,
constructs a congruence proof for `nestedProof p hp ≍ nestedProof q hq`.
`p` and `q` are in the same equivalence class.
 -/
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkNestedProofCongr : Lean.Expr → Lean.Expr → Bool → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Algebra.Free
FreeAddMagma.recOnPure.eq_1 : ∀ {α : Type u} {C : FreeAddMagma α → Sort l} (x : FreeAddMagma α) (ih1 : (x : α) → C (pure x))
  (ih2 : (x y : FreeAddMagma α) → C x → C y → C (x + y)), x.recOnPure ih1 ih2 = x.recOnAdd ih1 ih2
-- Std.Http.Data.Status
/-- 414 URI Too Long
 -/
Std.Http.Status.uriTooLong : Std.Http.Status
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpoly_coeff_eq_zero_iff_of_basis : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ι' : Type u_6} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ : L →ₗ[R] Module.End R M) [inst_5 : Fintype ι] [inst_6 : Fintype ι'] [inst_7 : DecidableEq ι]
  [inst_8 : DecidableEq ι'] [inst_9 : Module.Free R M] [inst_10 : Module.Finite R M] (b : Module.Basis ι R L)
  (b' : Module.Basis ι' R L) (k : ℕ), (φ.polyCharpoly b).coeff k = 0 ↔ (φ.polyCharpoly b').coeff k = 0
-- Init.Data.List.Basic
List.dropLast.eq_3 : ∀ {α : Type u_1} (a : α) (as : List α), (as = [] → False) → (a :: as).dropLast = a :: as.dropLast
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary.ι_ι_assoc : ∀ {n : ℕ} (i : Fin (n + 2)) {Z : SSet} (h : SSet.stdSimplex.obj { len := n + 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.boundary.ι i)
      (CategoryTheory.CategoryStruct.comp (SSet.boundary (n + 1)).ι h) =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i) h
-- Plausible.Arbitrary
Plausible.UInt8.Arbitrary : Plausible.Arbitrary UInt8