mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.beq.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : Batteries.AssocList α β → Batteries.AssocList α β → Sort u_3) (key : α)
  (value : β) (tail : Batteries.AssocList α β) (h_1 : Unit → motive Batteries.AssocList.nil Batteries.AssocList.nil)
  (h_2 :
    (key : α) →
      (value : β) →
        (tail : Batteries.AssocList α β) → motive (Batteries.AssocList.cons key value tail) Batteries.AssocList.nil)
  (h_3 :
    (key : α) →
      (value : β) →
        (tail : Batteries.AssocList α β) → motive Batteries.AssocList.nil (Batteries.AssocList.cons key value tail))
  (h_4 :
    (a : α) →
      (b : β) →
        (t : Batteries.AssocList α β) →
          (a' : α) →
            (b' : β) →
              (t' : Batteries.AssocList α β) →
                motive (Batteries.AssocList.cons a b t) (Batteries.AssocList.cons a' b' t')),
  (match Batteries.AssocList.nil, Batteries.AssocList.cons key value tail with
    | Batteries.AssocList.nil, Batteries.AssocList.nil => h_1 ()
    | Batteries.AssocList.cons key value tail, Batteries.AssocList.nil => h_2 key value tail
    | Batteries.AssocList.nil, Batteries.AssocList.cons key value tail => h_3 key value tail
    | Batteries.AssocList.cons a b t, Batteries.AssocList.cons a' b' t' => h_4 a b t a' b' t') =
    h_3 key value tail
-- Mathlib.Topology.Algebra.SeparationQuotient.Hom
/-- The lift of an additive monoid hom from `M` to an additive monoid hom from
`SeparationQuotient M`.  -/
SeparationQuotient.liftContinuousAddMonoidHom : {M : Type u_1} →
  {N : Type u_2} →
    [inst : TopologicalSpace M] →
      [inst_1 : TopologicalSpace N] →
        [inst_2 : AddCommMonoid M] →
          [inst_3 : ContinuousAdd M] →
            [inst_4 : AddCommMonoid N] →
              (f : M →ₜ+ N) → (∀ (x y : M), Inseparable x y → f x = f y) → SeparationQuotient M →ₜ+ N
-- Mathlib.Logic.Basic
/-- A 'ite' producing a `Pi` type `Π a, σ a`, applied to a value `a : α` is a `ite` that applies
either branch to `a`.  -/
ite_apply : ∀ {α : Sort u_1} {σ : α → Sort u_2} (P : Prop) [inst : Decidable P] (f g : (a : α) → σ a) (a : α),
  (if P then f else g) a = if P then f a else g a
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.smulFamily_toFun : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_4} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  [inst_2 : AddCommMonoid V] [inst_3 : SMulWithZero R V] (f : α → R) (s : HahnSeries.SummableFamily Γ V α) (a : α),
  (HahnSeries.SummableFamily.smulFamily f s) a = f a • s a
-- Mathlib.Analysis.Normed.Group.InfiniteSum
HasSum.enorm_le_of_bounded : ∀ {ι : Type u_1} {ε : Type u_5} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddCommMonoid ε] {f : ι → ε}
  {g : ι → ENNReal} {a : ε} {b : ENNReal}, HasSum f a → HasSum g b → (∀ (i : ι), ‖f i‖ₑ ≤ g i) → ‖a‖ₑ ≤ b
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.isClosed' : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] (self : ClosedSubmodule R M), IsClosed (↑self).carrier
-- Mathlib.Algebra.Group.Units.Equiv
toAddUnits_symm_apply : ∀ {G : Type u_5} [inst : AddGroup G] (x : AddUnits G), toAddUnits.symm x = ↑x
-- Mathlib.RingTheory.DiscreteValuationRing.TFAE
IsLocalRing.finrank_CotangentSpace_eq_one : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R],
  Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) = 1
-- Mathlib.CategoryTheory.Sums.Associator
/-- The inverse associator functor `C ⊕ (D ⊕ E) ⥤ (C ⊕ D) ⊕ E` for sums of categories.
 -/
CategoryTheory.sum.inverseAssociator : (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] → CategoryTheory.Functor (C ⊕ D ⊕ E) ((C ⊕ D) ⊕ E)
-- Mathlib.Data.DFinsupp.Submonoid
dfinsuppSumAddHom_mem : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] {S : Type u_1} [inst_3 : SetLike S γ] [AddSubmonoidClass S γ] (s : S) (f : Π₀ (i : ι), β i)
  (g : (i : ι) → β i →+ γ), (∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ s) → (DFinsupp.sumAddHom g) f ∈ s
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
CategoryTheory.Presieve.isSheaf_of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w))
  {J₁ J₂ : CategoryTheory.GrothendieckTopology C},
  J₁ ≤ J₂ → CategoryTheory.Presieve.IsSheaf J₂ P → CategoryTheory.Presieve.IsSheaf J₁ P
-- Mathlib.Data.Nat.Order.Lemmas
Nat.Subtype.semilatticeSup : (p : ℕ → Prop) → SemilatticeSup (Subtype p)
-- Std.Net.Addr
Std.Net.IPAddr.v4.inj : ∀ {addr addr_1 : Std.Net.IPv4Addr}, Std.Net.IPAddr.v4 addr = Std.Net.IPAddr.v4 addr_1 → addr = addr_1
-- Mathlib.Algebra.Group.EvenFunction
Function.Even.mul_odd : ∀ {α : Type u_1} [inst : Neg α] {R : Type u_3} [inst_1 : Mul R] {f g : α → R} [inst_2 : HasDistribNeg R],
  Function.Even f → Function.Odd g → Function.Odd (f * g)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_insert : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ)
  (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  k ≥ 0 →
    p.NonnegCoeffs →
      Lean.Grind.CommRing.Poly.denoteS ctx (Lean.Grind.CommRing.Poly.insert k m p) =
        ↑k.toNat * Lean.Grind.CommRing.Mon.denote ctx m + Lean.Grind.CommRing.Poly.denoteS ctx p
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instReflVeq : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R], Std.Refl fun x1 x2 => x1 =ᵥ x2
-- Std.Time.DateTime
/-- Getter for the `Minute` inside of a `DateTime`
 -/
Std.Time.DateTime.minute : Std.Time.DateTime → Std.Time.Minute.Ordinal
-- Batteries.Recycling.RBTree.Basic
RBTree.RBSet.instUnion : {α : Type u_1} → {cmp : α → α → Ordering} → Union (RBTree.RBSet α cmp)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} {φ φ' : D₁ ⟶ D₂}, φ = φ' ↔ ∀ (i : ι), φ.hom i = φ'.hom i
-- Mathlib.Data.Multiset.Fintype
Multiset.consEquiv_symm_none : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} {v : α},
  Multiset.consEquiv.symm none = ⟨v, ⟨Multiset.count v m, ⋯⟩⟩
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
SymmetricAlgebra.equivMvPolynomial_symm_X : ∀ {κ : Type uκ} {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis κ R M) (i : κ),
  (SymmetricAlgebra.equivMvPolynomial b).symm (MvPolynomial.X i) = (SymmetricAlgebra.ι R M) (b i)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_union_of_not_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (∀ a ∈ m₁, a ∉ m₂) → (m₁ ∪ m₂).size = m₁.size + m₂.size
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.LiftStruct.unop_l : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} (l : sq.LiftStruct), l.unop.l = l.l.unop
-- Mathlib.FieldTheory.KummerExtension
/-- Suppose `L/K` is the splitting field of `Xⁿ - a`, and `ζ` is an `n`-th primitive root of unity
in `K`, then `Gal(L/K)` is isomorphic to `ZMod n`.  -/
autEquivZmod : {K : Type u} →
  [inst : Field K] →
    {n : ℕ} →
      {a : K} →
        Irreducible (Polynomial.X ^ n - Polynomial.C a) →
          (L : Type u_1) →
            [inst_1 : Field L] →
              [inst_2 : Algebra K L] →
                [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] →
                  [NeZero n] → {ζ : K} → IsPrimitiveRoot ζ n → Gal(L/K) ≃* Multiplicative (ZMod n)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : Inhabited α] {a : α}, ∅.getKey! a = default
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.aleph0.eq_1 : Cardinal.aleph0 = Cardinal.lift.{u, 0} (Cardinal.mk ℕ)
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.vadd_def : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M}
  {α : Type u_1} [inst_2 : VAdd M α] (g : ↥p) (m : α), g +ᵥ m = ↑g +ᵥ m
-- Mathlib.Data.Finset.Lattice.Basic
Finset.instLattice : {α : Type u_1} → [DecidableEq α] → Lattice (Finset α)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.ofIso_vadd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {M : C} [inst_4 : CategoryTheory.AddMonObj M] {X : D} {N : C} [inst_5 : CategoryTheory.AddMonObj N] (e₁ : M ≅ N)
  [inst_6 : CategoryTheory.IsAddMonHom e₁.hom] {Y : D} (e₂ : X ≅ Y) [inst_7 : CategoryTheory.AddModObj M X],
  CategoryTheory.AddModObj.vadd =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom e₁.inv e₂.inv)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd e₂.hom)
-- Init.Data.SInt.Lemmas
Int16.toInt_le_iSizeMaxValue : ∀ (x : Int16), x.toInt ≤ ISize.maxValue.toInt
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.singleton_eq_univ : ∀ {α : Type u_1} [inst : Fintype α] [Subsingleton α] (a : α), {a} = Finset.univ
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.differentiable_aeval : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R 𝕜]
  (q : Polynomial R), Differentiable 𝕜 fun x => (Polynomial.aeval x) q
-- Mathlib.GroupTheory.Congruence.Hom
/-- A specialization of 'the smallest congruence relation containing a congruence relation `c`
equals `c`'.  -/
Con.mapOfSurjective_eq_mapGen : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_4} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [inst_3 : MulHomClass F M N] {c : Con M} {f : F} (h : Con.ker f ≤ c) (hf : Function.Surjective ⇑f),
  Con.mapGen ⇑f = Con.mapOfSurjective f h hf
-- Mathlib.Data.Nat.Init
Nat.leRec.eq_2 : ∀ {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯)
  (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) (m : ℕ) (H : n ≤ m + 1),
  Nat.leRec refl le_succ_of_le H =
    ⋯.by_cases (fun h => le_succ_of_le h (Nat.leRec refl le_succ_of_le h)) fun h =>
      Eq.ndrec (motive := fun {n} =>
        {motive : (m : ℕ) → n ≤ m → Sort u_1} →
          motive n ⋯ → (⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) → (H : n ≤ m + 1) → motive (m + 1) H)
        (fun {motive} refl le_succ_of_le H => refl) ⋯ refl le_succ_of_le H
-- Std.Time.Time.HourMarker
/-- `HourMarker` represents the two 12-hour periods of the day: `am` for hours between 12:00 AM and
11:59 AM, and `pm` for hours between 12:00 PM and 11:59 PM.
 -/
Std.Time.HourMarker : Type
-- Lean.Parser.Extra
Lean.Parser.commandParser.parenthesizer : optParam ℕ 0 → Lean.PrettyPrinter.Parenthesizer
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.maxEntry_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t₁.isEmpty = false} (h : t₁.Equiv t₂), t₁.maxEntry he = t₂.maxEntry ⋯
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.addVal_eq_top_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {a : R},
  (IsDiscreteValuationRing.addVal R) a = ⊤ ↔ a = 0
-- Aesop.RuleTac.Basic
Aesop.instInhabitedRuleTacOutput.default : Aesop.RuleTacOutput
-- Mathlib.Combinatorics.Matroid.Basic
/-- For finite `E`, finitely many matroids have ground set `E`.  -/
Matroid.finite_setOfPred_matroid' : ∀ {α : Type u_1} {E : Set α}, E.Finite → {M | M.E = E}.Finite
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionOptions.triggerCharacters? : Lean.Lsp.CompletionOptions → Option (Array String)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_empty : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.empty.maxKey? = none
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.map_eq_zero_iff : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M},
  e x = 0 ↔ x = 0
-- Mathlib.Algebra.Order.AddTorsor
instIsOrderedVAddOfIsOrderedAddMonoid : ∀ {G : Type u_1} [inst : AddCommMonoid G] [inst_1 : Preorder G] [IsOrderedAddMonoid G], IsOrderedVAdd G G
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.instBEqPolyCnstr : BEq Nat.Internal.Linear.PolyCnstr
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
_private.Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation.0.Real.integrableOn_rpowIntegrand₀₁_Ioi_one : ∀ {p x : ℝ},
  p ∈ Set.Ioo 0 1 →
    0 ≤ x → MeasureTheory.IntegrableOn (fun x_1 => p.rpowIntegrand₀₁ x_1 x) (Set.Ioi 1) MeasureTheory.volume
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- A sufficient condition for a linear map taking values in a TVS to have closed range is that
there exists a finite-codimension subspace of the domain whose image is closed.  -/
LinearMap.isClosed_range_of_isClosed_map_of_finiteDimensional_quotient : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup F]
  [inst_3 : TopologicalSpace F] [IsTopologicalAddGroup F] [inst_5 : Module 𝕜 F] [ContinuousSMul 𝕜 F] {E : Type u_4}
  [inst_7 : AddCommGroup E] [inst_8 : Module 𝕜 E] {f : E →ₗ[𝕜] F} {s : Submodule 𝕜 E} [s.CoFG],
  IsClosed ↑(Submodule.map f s) → IsClosed ↑f.range
-- Init.Sym.DSimp.DSimprocDSL
/-- Apply `a`, then apply `b` to the result.  -/
Lean.Parser.Sym.DSimp.andThen : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
_private.Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries.0.Pentagonal.multipliable_one_sub_X_pow : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : TopologicalSpace R] (k : ℕ),
  Multipliable fun n => 1 - PowerSeries.X ^ (n + k + 1)
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDeriv_fun_add : ∀ {𝕜 : 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] {n : ℕ}
  {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {x : E},
  DifferentiableAt 𝕜 ω₁ x → DifferentiableAt 𝕜 ω₂ x → extDeriv (fun x => ω₁ x + ω₂ x) x = extDeriv ω₁ x + extDeriv ω₂ x
-- Init.Data.Nat.Basic
Nat.eq_or_lt_of_not_lt : ∀ {a b : ℕ}, ¬a < b → a = b ∨ b < a
-- Mathlib.SetTheory.Cardinal.SchroederBernstein
/-- **The Schröder-Bernstein Theorem**: Given embeddings `α ↪ β` and `β ↪ α`, there exists an
equivalence `α ≃ β`.  -/
Function.Embedding.antisymm : ∀ {α : Type u} {β : Type v} (a : α ↪ β) (a : β ↪ α), Nonempty (α ≃ β)
-- Mathlib.Condensed.Light.TopCatAdjunction
_private.Mathlib.Condensed.Light.TopCatAdjunction.0.LightCondSet.coinducingCoprod.match_1.eq_1 : ∀ (X : LightCondSet) (motive : (i : (S : LightProfinite) × X.obj.obj (Opposite.op S)) × ↑i.fst.toTop → Sort u_2)
  (fst : LightProfinite) (i : X.obj.obj (Opposite.op fst)) (s : ↑⟨fst, i⟩.fst.toTop)
  (h_1 : (fst : LightProfinite) → (i : X.obj.obj (Opposite.op fst)) → (s : ↑⟨fst, i⟩.fst.toTop) → motive ⟨⟨fst, i⟩, s⟩),
  (match ⟨⟨fst, i⟩, s⟩ with
    | ⟨⟨fst, i⟩, s⟩ => h_1 fst i s) =
    h_1 fst i s
-- Mathlib.Tactic.CasesM
/-- Common implementation of `cases_type` and `cases_type!`.  -/
Mathlib.Tactic.elabCasesType : Array Lean.Ident → optParam Bool false → optParam Bool true → Lean.Elab.Tactic.TacticM Unit
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpoint.mk.injEq : ∀ (ref : Lean.Syntax) (term? : Option Lean.Term) (fixpointType : Lean.Elab.PartialFixpointType) (ref_1 : Lean.Syntax)
  (term?_1 : Option Lean.Term) (fixpointType_1 : Lean.Elab.PartialFixpointType),
  ({ ref := ref, term? := term?, fixpointType := fixpointType } =
      { ref := ref_1, term? := term?_1, fixpointType := fixpointType_1 }) =
    (ref = ref_1 ∧ term? = term?_1 ∧ fixpointType = fixpointType_1)
-- Init.Data.List.Sublist
List.isPrefixOf_iff_prefix : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ : List α}, l₁.isPrefixOf l₂ = true ↔ l₁ <+: l₂
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_comm : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommMonoid α] (s t : Finset α), s.mulEnergy t = t.mulEnergy s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
DifferentiableOn.ccos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E},
  DifferentiableOn ℂ f s → DifferentiableOn ℂ (fun x => Complex.cos (f x)) s
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.isPositive_covarianceOperator : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E} [inst_4 : CompleteSpace E],
  (↑(ProbabilityTheory.covarianceOperator μ)).IsPositive
-- Mathlib.Algebra.Field.Defs
DivisionSemiring.toSemiring : {K : Type u_2} → [self : DivisionSemiring K] → Semiring K
-- Init.Data.Vector.Attach
/-- If we fold over `l.attach` with a function that ignores the membership predicate,
we get the same results as folding over `l` directly.

This is useful when we need to use `attach` to show termination.

Unfortunately this can't be applied by `simp` because of the higher order unification problem,
and even when rewriting we need to specify the function explicitly.
See however `foldr_subtype` below.
 -/
Vector.foldr_attach : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → β → β} {b : β},
  Vector.foldr (fun t acc => f (↑t) acc) b xs.attach = Vector.foldr f b xs
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects : ∀ {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.IsCofibrant X.obj
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instIsUniformAddGroup : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F], IsUniformAddGroup (E →SWOT[σ] F)
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.instIsPushout_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (R' : Type u_4)
  (S' : Type u_5) [inst_3 : CommRing S'] [FaithfulSMul R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S]
  [inst_6 : Algebra S S'] [IsFractionRing S S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R S S']
  [inst_10 : CommRing R'] [inst_11 : Algebra R R'] [IsFractionRing R R'] [inst_13 : Algebra R' S']
  [inst_14 : IsScalarTower R R' S'], Algebra.IsPushout R S R' S'
-- Init.Data.String.Lemmas.Basic
String.Slice.cast_pos : ∀ {s t : String.Slice} {p : String.Pos.Raw} {h : String.Pos.Raw.IsValidForSlice s p} {h' : s.copy = t.copy}
  {h'' : String.Pos.Raw.IsValidForSlice t p}, (s.pos p h).cast h' = t.pos p h''
-- Init.System.IOError
IO.Error.otherError.sizeOf_spec : ∀ (osCode : UInt32) (details : String), sizeOf (IO.Error.otherError osCode details) = 1 + sizeOf osCode + sizeOf details
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.Trace.noConfusionType : Sort v✝ → Lean.Lsp.Trace → Lean.Lsp.Trace → Sort v✝
-- Mathlib.Data.Multiset.Replicate
Multiset.mem_replicate : ∀ {α : Type u_1} {a b : α} {n : ℕ}, b ∈ Multiset.replicate n a ↔ n ≠ 0 ∧ b = a
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₂_ne_zero : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥), RatFunc.Luroth.Q₂✝ h ≠ 0
-- Mathlib.Topology.Baire.BaireMeasurable
/-- The preimage of a meager set under a continuous open map is meager.  -/
IsMeagre.preimage_of_isOpenMap : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Continuous f → IsOpenMap f → ∀ {s : Set β}, IsMeagre s → IsMeagre (f ⁻¹' s)
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeAddMonoid.equivWithZeroFreeAddSemigroup_apply : ∀ {α : Type u_1} (a : FreeAddMonoid α),
  FreeAddMonoid.equivWithZeroFreeAddSemigroup a = (FreeAddMonoid.lift fun x => ↑(FreeAddSemigroup.of x)) a
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tendsto_atTop_zero_of_tsum_ne_top : ∀ {f : ℕ → ENNReal}, ∑' (x : ℕ), f x ≠ ⊤ → Filter.Tendsto f Filter.atTop (nhds 0)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Sums of measurable spaces are symmetric.  -/
MeasurableEquiv.sumCongr : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {δ : Type u_4} →
        [inst : MeasurableSpace α] →
          [inst_1 : MeasurableSpace β] →
            [inst_2 : MeasurableSpace γ] → [inst_3 : MeasurableSpace δ] → α ≃ᵐ β → γ ≃ᵐ δ → α ⊕ γ ≃ᵐ β ⊕ δ
-- Mathlib.LinearAlgebra.Transvection.Basic
/-- The set of transvections in the group of linear equivalences  -/
LinearEquiv.transvections : (R : Type u_1) → (V : Type u_2) → [inst : Ring R] → [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → Set (V ≃ₗ[R] V)
-- Mathlib.Order.SetNotation
/-- Delaborator for indexed supremum.  -/
iSup_delab : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Http.Protocol.H1
/-- Processes fixed-length body data when buffered user bytes are present.

Enforces exact-length semantics (no overflow), writes up to remaining length,
and updates writer state for any bytes still pending.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processFixedBufferedBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → ℕ → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Data.List.Permutation
List.Perm.permutations' : ∀ {α : Type u_1} {s t : List α}, s.Perm t → s.permutations'.Perm t.permutations'
-- Mathlib.RingTheory.HopfAlgebra.Basic
HopfAlgebra.counit_antipode : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] (a : A),
  CoalgebraStruct.counit ((HopfAlgebraStruct.antipode R) a) = CoalgebraStruct.counit a
-- Mathlib.Dynamics.Ergodic.Action.Basic
ErgodicVAdd.mk : ∀ {G : Type u_1} {α : Type u_2} [inst : VAdd G α] {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [toVAddInvariantMeasure : MeasureTheory.VAddInvariantMeasure G α μ],
  (∀ {s : Set α},
      MeasurableSet s → (∀ (g : G), (fun x => g +ᵥ x) ⁻¹' s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)) →
    ErgodicVAdd G α μ
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.apply_skipSuffixWhile_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {h : s.skipSuffixWhile P ≠ s.startPos},
  ¬P (((s.skipSuffixWhile P).prev h).get ⋯)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsIsoFunctorTruncGELTToLTGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : ℤ),
  CategoryTheory.IsIso (t.truncGELTToLTGE a b)