mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLT : ∀ {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) (X : C) (a b : ℤ) [t.IsLE X b], t.IsLE ((t.truncLT a).obj X) b
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.proofWidgetsJsxElement.quot : Lean.ParserDescr
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_uInt32ToNat : ∀ (n : UInt32) (h : n.toNat < UInt16.size), UInt16.ofNatLT n.toNat h = n.toUInt16
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.Arrow.isoMk.congr_simp : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (l l_1 : f.left ≅ g.left)
  (e_l : l = l_1) (r r_1 : f.right ≅ g.right) (e_r : r = r_1)
  (h : CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom),
  CategoryTheory.Arrow.isoMk l r h = CategoryTheory.Arrow.isoMk l_1 r_1 ⋯
-- Mathlib.Order.Filter.Map
Set.RightInvOn.filter_map_Iic : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} {g : β → α},
  Set.RightInvOn g f t → Set.RightInvOn (Filter.map g) (Filter.map f) (Set.Iic (Filter.principal t))
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_toUSize : ∀ (n : UInt8), n.toUSize.toUInt16 = n.toUInt16
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ ∪ t₂ → k ∉ t₂ → k ∈ t₁
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.natDegree_hasseDeriv_le : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (n : ℕ),
  ((Polynomial.hasseDeriv n) p).natDegree ≤ p.natDegree - n
-- Mathlib.Order.Hom.Lattice
/-- `id` as a `LatticeHom`.  -/
LatticeHom.id : (α : Type u_2) → [inst : Lattice α] → LatticeHom α α
-- Mathlib.Algebra.BigOperators.Finprod
finsum_cond_ne : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) (a : α) [inst_1 : DecidableEq α]
  (hf : Function.HasFiniteSupport f), ∑ᶠ (i : α) (_ : i ≠ a), f i = ∑ i ∈ (Set.Finite.toFinset hf).erase a, f i
-- Mathlib.Data.Subtype
Subtype.coind_injective : ∀ {α : Sort u_4} {β : Sort u_5} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)),
  Function.Injective f → Function.Injective (Subtype.coind f h)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.append_left : ∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)}, FreeGroup.Red.Step L₂ L₃ → FreeGroup.Red.Step (L₁ ++ L₂) (L₁ ++ L₃)
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.Integrable.comp_smul : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure]
  {f : E → F}, MeasureTheory.Integrable f μ → ∀ {R : ℝ}, R ≠ 0 → MeasureTheory.Integrable (fun x => f (R • x)) μ
-- Init.Data.List.Basic
List.dropLast.eq_1 : ∀ {α : Type u_1}, [].dropLast = []
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integralSum.eq_1 : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} (f : (ι → ℝ) → E)
  (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤) (π : BoxIntegral.TaggedPrepartition I),
  BoxIntegral.integralSum f vol π = ∑ J ∈ π.boxes, (vol J) (f (π.tag J))
-- Mathlib.Algebra.Free
Magma.AssocQuotient.eq_1 : ∀ (α : Type u) [inst : Mul α], Magma.AssocQuotient α = Quot (Magma.AssocRel α)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddZeroClass.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddZeroClass M] [inst_2 : ContinuousAdd M],
  SeparationQuotient.instAddZeroClass =
    { toZero := SeparationQuotient.instZero, toAdd := SeparationQuotient.instAdd, zero_add := ⋯, add_zero := ⋯ }
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonWaitForDiagnostics : Lean.FromJson Lean.Lsp.WaitForDiagnostics
-- Mathlib.Order.Max
IsTop.isMax : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsTop a → IsMax a
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero : ∀ {z : ℂ},
  z.re < 0 →
    z.im = 0 → Filter.Tendsto Complex.log (nhdsWithin z {z | z.im < 0}) (nhds (↑(Real.log ‖z‖) - ↑Real.pi * Complex.I))
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.get!.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited β] (a : α) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.Const.get! ⟨{ size := size, buckets := buckets }, hm⟩ a =
    Std.DHashMap.Internal.AssocList.get! a buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))]
-- Mathlib.Data.Real.Basic
Real.le_mk_of_forall_le : ∀ {x : ℝ} {f : CauSeq ℚ abs}, (∃ i, ∀ j ≥ i, x ≤ ↑(↑f j)) → x ≤ Real.mk f
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_zero_size : ∀ {b : ByteArray}, b.extract 0 b.size = b
-- Mathlib.Order.UpperLower.Basic
isLowerSet_iff_Iio_subset : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α}, IsLowerSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Set.Iio a ⊆ s
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.merge.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (xs : List α) (h_1 : (ys : List α) → motive [] ys)
  (h_2 : (xs : List α) → motive xs [])
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (xs = [] → False) →
    (match xs, [] with
      | [], ys => h_1 ys
      | xs, [] => h_2 xs
      | x :: xs, y :: ys => h_3 x xs y ys) =
      h_2 xs
-- Batteries.Tactic.PrintDependents
Batteries.Tactic.CollectDependents.State.mk.injEq : ∀ (otherAxiom : Bool) (result : Lean.NameMap Bool) (otherAxiom_1 : Bool) (result_1 : Lean.NameMap Bool),
  ({ otherAxiom := otherAxiom, result := result } = { otherAxiom := otherAxiom_1, result := result_1 }) =
    (otherAxiom = otherAxiom_1 ∧ result = result_1)
-- Init.Data.List.Basic
List.zipWithAll_nil : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {as : List α},
  List.zipWithAll f as [] = List.map (fun a => f (some a) none) as
-- Mathlib.Analysis.Convex.Approximation
ConvexOn.exists_affine_le_real : ∀ {s : Set ℝ} {f : ℝ → ℝ}, IsClosed s → LowerSemicontinuousOn f s → ConvexOn ℝ s f → ∃ c c', ∀ x ∈ s, c * x + c' ≤ f x
-- Mathlib.Data.Finite.Prod
Set.fintypeOffDiag : {α : Type u_1} → (s : Set α) → [Fintype ↑s] → Fintype ↑s.offDiag
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_zero_apply : ∀ {R : Type u} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₂] (f : R →+* S₂)
  (p : MvPolynomial σ R), MvPolynomial.eval₂ f 0 p = f (MvPolynomial.constantCoeff p)
-- Lean.DocString.Extension
Lean.ElabInline.deferred.injEq : ∀ (index index_1 : ℕ), (Lean.ElabInline.deferred index = Lean.ElabInline.deferred index_1) = (index = index_1)
-- Mathlib.Algebra.Field.Defs
Semifield.toCommSemiring : {K : Type u_2} → [self : Semifield K] → CommSemiring K
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Valuation.vlt_iff_lt : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_2} [inst_2 : LinearOrderedCommMonoidWithZero Γ₀]
  (v : Valuation R Γ₀) [v.Compatible] {x y : R}, x <ᵥ y ↔ v x < v y
-- Mathlib.RingTheory.Artinian.Module
RingEquiv.isArtinianRing : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* S) [IsArtinianRing R],
  IsArtinianRing S
-- Init.Core
And.symm : ∀ {a b : Prop}, a ∧ b → b ∧ a
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.unpackSign.eq_1 : ∀ {spec : Float.Model.Format} (b : BitVec spec.numBits),
  Float.Model.UnpackedFloat.unpackSign b =
    BitVec.cast ⋯
      (BitVec.extractLsb (spec.mantissaBitsWithoutImplicit + spec.exponentBits)
        (spec.mantissaBitsWithoutImplicit + spec.exponentBits) b)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.Precylinder.op_p₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A),
  P.op.p₀ = P.i₀.op
-- Mathlib.Order.Defs.Unbundled
RelUpperSet.mk.inj : ∀ {α : Type u_1} {inst : LE α} {P : α → Prop} {carrier : Set α} {isRelUpperSet' : IsRelUpperSet carrier P}
  {carrier_1 : Set α} {isRelUpperSet'_1 : IsRelUpperSet carrier_1 P},
  { carrier := carrier, isRelUpperSet' := isRelUpperSet' } =
      { carrier := carrier_1, isRelUpperSet' := isRelUpperSet'_1 } →
    carrier = carrier_1
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.costructuredArrowObj_iff : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {T : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} T] (L : CategoryTheory.Functor A T)
  {W : CategoryTheory.MorphismProperty T} {X : T} (Y : CategoryTheory.CostructuredArrow L X),
  CategoryTheory.MorphismProperty.costructuredArrowObj L W Y ↔ W Y.hom
-- Mathlib.Topology.Category.Locale
Locale.instFrameCarrierUnopFrm : (X : Locale) → Order.Frame ↑(Opposite.unop X)
-- Mathlib.Algebra.Star.MonoidHom
/-- Reinterpret a star monoid equivalence as a `MulEquiv` by forgetting the interaction with the
star operation.  -/
StarMulEquiv.toMulEquiv : {A : Type u_6} →
  {B : Type u_7} → [inst : Mul A] → [inst_1 : Mul B] → [inst_2 : Star A] → [inst_3 : Star B] → (A ≃⋆* B) → A ≃* B
-- Mathlib.RepresentationTheory.Basic
/-- When `G` is a group, a `k`-linear representation of `G` on `V` can be thought of as
a group homomorphism from `G` into the invertible `k`-linear endomorphisms of `V`.
 -/
Representation.asGroupHom : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → Representation k G V → G →* (V →ₗ[k] V)ˣ
-- Init.Data.Range.Polymorphic.UInt
USize.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable USize
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_5 : HAdd Std.Time.Nanosecond.Offset Std.Time.Week.Offset Std.Time.Nanosecond.Offset
-- Mathlib.Algebra.Ring.ULift
ULift.ring : {R : Type u} → [Ring R] → Ring (ULift.{u_1, u} R)
-- Mathlib.SetTheory.ZFC.PSet
_private.Mathlib.SetTheory.ZFC.PSet.0.PSet.mem_wf_aux : ∀ {x y : PSet.{u}}, x.Equiv y → Acc (fun x1 x2 => x1 ∈ x2) y
-- Init.Data.SInt.Lemmas
Int16.cast_toNatClampNeg : ∀ (x : Int16), 0 ≤ x → ↑x.toNatClampNeg = x.toInt
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.minpolyX_aeval_X : ∀ {K : Type u_1} [inst : Field K] (f : RatFunc K), (Polynomial.aeval RatFunc.X) (f.minpolyX ↥K⟮f⟯) = 0
-- Mathlib.Data.FunLike.Graded
Graded.equiv_apply : ∀ {E : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [inst : SetLike σ A]
  [inst_1 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_2 : EquivLike E A B] [inst_3 : GradedEquivLike E 𝒜 ℬ] (e : E)
  (i : ι) (x : ↥(𝒜 i)), (Graded.equiv e i) x = Graded.subtypeMap e i x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Returns occurrences of `x`.  -/
Lean.Meta.Grind.Arith.Cutsat.getOccursOf : Int.Internal.Linear.Var → Lean.Meta.Grind.GoalM Lean.Meta.Grind.Arith.Cutsat.VarSet
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
/-- The additive equivalence between `FreeAbelianGroup X` and `(X →₀ ℤ)`.  -/
FreeAbelianGroup.equivFinsupp : (X : Type u_1) → FreeAbelianGroup X ≃+ (X →₀ ℤ)
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
/-- `Type` version of `exists_isTranscendenceBasis`.  -/
exists_isTranscendenceBasis' : ∀ (R : Type u_1) (A : Type w) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [FaithfulSMul R A],
  ∃ ι x, IsTranscendenceBasis R x
-- Lean.Meta.ReduceEval
_private.Lean.Meta.ReduceEval.0.Lean.Meta.throwFailedToEval : {α : Type} → Lean.Expr → Lean.MetaM α
-- Init.Data.BitVec.Lemmas
BitVec.sshiftRight_eq' : ∀ {w w_1 : ℕ} {y : BitVec w_1} (x : BitVec w), x.sshiftRight' y = x.sshiftRight y.toNat
-- Mathlib.Data.Nat.Digits.Defs
Nat.digitsAux0.eq_1 : Nat.digitsAux0 0 = []
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.map_contract : ∀ {R : Type u} [inst : CommSemiring R] {S : Type v} [inst_1 : CommSemiring S] {p : ℕ},
  p ≠ 0 →
    ∀ {f : R →+* S} {q : Polynomial R},
      Polynomial.map f (Polynomial.contract p q) = Polynomial.contract p (Polynomial.map f q)
-- Mathlib.Data.Finsupp.Single
Finsupp.single_apply_ne_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a x : α} {b : M}, (fun₀ | a => b) x ≠ 0 ↔ x = a ∧ b ≠ 0
-- Std.Time.Time.Unit.Nanosecond
/-- `Offset` represents a time offset in nanoseconds.
 -/
Std.Time.Nanosecond.Offset : Type
-- Init.Grind.ToInt
Lean.Grind.IntInterval.wrap_mem : ∀ (i : Lean.Grind.IntInterval), i.nonEmpty = true → ∀ (x : ℤ), i.wrap x ∈ i
-- Mathlib.Topology.ContinuousMap.Polynomial
/-- The subalgebra of polynomial functions in `C(X, R)`, for `X` a subset of some topological semiring
`R`.
 -/
polynomialFunctions : {R : Type u_1} →
  [inst : CommSemiring R] →
    [inst_1 : TopologicalSpace R] → [inst_2 : IsTopologicalSemiring R] → (X : Set R) → Subalgebra R C(↑X, R)
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientMapOfLE_apply_mk : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (h : s ≤ t) (g : α), Subgroup.quotientMapOfLE h ↑g = ↑g
-- Mathlib.Order.Hom.CompleteLattice
/-- Composition of `CompleteLatticeHom`s as a `CompleteLatticeHom`.  -/
CompleteLatticeHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : CompleteLattice α] →
        [inst_1 : CompleteLattice β] →
          [inst_2 : CompleteLattice γ] → CompleteLatticeHom β γ → CompleteLatticeHom α β → CompleteLatticeHom α γ
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod_η_snd : ∀ {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 D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E] {C' : Type u₁'}
  [inst_6 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor E C')
  [inst_7 : CategoryTheory.MonoidalCategory C'] [inst_8 : F.OplaxMonoidal] [inst_9 : G.OplaxMonoidal],
  (CategoryTheory.Functor.OplaxMonoidal.η (F.prod G)).2 = CategoryTheory.Functor.OplaxMonoidal.η G
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.iUnion_mk : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (f : BoxIntegral.Box ι → ι → ℝ)
  (h : ∀ (J : BoxIntegral.Box ι), f J ∈ BoxIntegral.Box.Icc I),
  { toPrepartition := π, tag := f, tag_mem_Icc := h }.iUnion = π.iUnion
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonTextDocumentEdit.fromJson : Lean.Json → Except String Lean.Lsp.TextDocumentEdit
-- Init.Data.Array.Count
Array.countP_eq_size : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, Array.countP p xs = xs.size ↔ ∀ a ∈ xs, p a = true
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : 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 → (m.insertMany l).getKey? k' = some k
-- Mathlib.Topology.Algebra.MulAction
Set.univ_smul_nhds_zero : ∀ {G₀ : Type u_5} {X : Type u_6} [inst : GroupWithZero G₀] [inst_1 : Zero X] [inst_2 : MulActionWithZero G₀ X]
  [inst_3 : TopologicalSpace G₀] [(nhdsWithin 0 {0}ᶜ).NeBot] [inst_5 : TopologicalSpace X] [ContinuousSMul G₀ X]
  {s : Set X}, s ∈ nhds 0 → Set.univ • s = Set.univ
-- Mathlib.Algebra.BigOperators.Group.List.Defs
List.prod_map_one : ∀ {ι : Type u_1} {M : Type u_2} [inst : MulOneClass M] {l : List ι}, (List.map (fun x => 1) l).prod = 1
-- Std.Internal.Parsec.Basic
/-- Parses zero or more chars with `p` into a string.
 -/
Std.Internal.Parsec.manyChars : {ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] →
      [Std.Internal.Parsec.Input ι elem idx] → Std.Internal.Parsec ι Char → Std.Internal.Parsec ι String
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.instBEqState : {dir : Std.Http.Protocol.H1.Direction} → BEq (Std.Http.Protocol.H1.Reader.State dir)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.XClass_ne_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [Nontrivial R] (x : R),
  WeierstrassCurve.Affine.CoordinateRing.XClass W' x ≠ 0
-- Mathlib.Order.Antichain
IsStrongAntichain.insert : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
  IsStrongAntichain r s → (∀ ⦃b : α⦄, b ∈ s → a ≠ b → ∀ (c : α), ¬r a c ∨ ¬r b c) → IsStrongAntichain r (insert a s)
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.copy : ∀ {P P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q Q' : AlgebraicGeometry.AffineTargetMorphismProperty} [AlgebraicGeometry.HasAffineProperty P Q],
  P = P' → Q = Q' → AlgebraicGeometry.HasAffineProperty P' Q'
-- Mathlib.Data.Nat.Init
Nat.leRec_succ : ∀ {m 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) ⋯) (h1 : n ≤ m) {h2 : n ≤ m + 1},
  Nat.leRec refl le_succ_of_le h2 = le_succ_of_le h1 (Nat.leRec refl le_succ_of_le h1)
-- Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
/-- In a fiber bundle, the preimage under the projection of a set with unique differentials
in the base has unique differentials in the bundle.  -/
UniqueMDiffOn.bundle_preimage : ∀ {𝕜 : 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] {s : Set M} {F : Type u_9} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] (Z : M → Type u_10) [inst_8 : TopologicalSpace (Bundle.TotalSpace F Z)]
  [inst_9 : (b : M) → TopologicalSpace (Z b)] [inst_10 : FiberBundle F Z],
  UniqueMDiff[s] → UniqueMDiff[Bundle.TotalSpace.proj ⁻¹' s]
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.instIsCancelAdd : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [IsCancelAdd R], IsCancelAdd (MonoidAlgebra R M)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.integral_sub_inv_smul_sub_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (c w : ℂ) (R : ℝ),
  ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z = ∮ (z : ℂ) in C(c, R), f z
-- Mathlib.Algebra.Order.Positive.Field
Positive.instPowSubtypeLtOfNatInt_mathlib : {K : Type u_1} → [inst : Field K] → [inst_1 : LinearOrder K] → [IsStrictOrderedRing K] → Pow { x // 0 < x } ℤ
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.conductor_zpow_dvd : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) (m : ℤ),
  (χ ^ m).conductor ∣ χ.conductor
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m.erase k).getKey? k = none
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.primrec_rfind' : Primrec Nat.Partrec.Code.rfind'
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropy_biUnion_le : ∀ {X : Type u_1} {ι : Type u_2} [inst : UniformSpace X] (s : Set ι) (T : X → X) (F : ι → Set X),
  ⨆ i ∈ s, Dynamics.coverEntropy T (F i) ≤ Dynamics.coverEntropy T (⋃ i ∈ s, F i)
-- Mathlib.CategoryTheory.Limits.Presentation
/-- If `F` preserves limits of shape `J`, it maps limit presentations of `X` to
limit presentations of `F(X)`.  -/
CategoryTheory.Limits.LimitPresentation.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} →
          CategoryTheory.Limits.LimitPresentation J X →
            {D : Type u_1} →
              [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
                (F : CategoryTheory.Functor C D) →
                  [CategoryTheory.Limits.PreservesLimitsOfShape J F] →
                    CategoryTheory.Limits.LimitPresentation J (F.obj X)
-- Mathlib.Topology.Constructions
continuous_uliftDown : ∀ {X : Type u} [inst : TopologicalSpace X], Continuous ULift.down
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
/-- The short complex in `ModuleCat` obtained from two linear map with composition equal to zero.  -/
ModuleCat.shortComplexOfCompEqZero : {R : Type u} →
  [inst : Ring R] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {N : Type v} →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] →
                {L : Type v} →
                  [inst_5 : AddCommGroup L] →
                    [inst_6 : Module R L] →
                      (f : M →ₗ[R] N) → (g : N →ₗ[R] L) → g ∘ₗ f = 0 → CategoryTheory.ShortComplex (ModuleCat R)
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstOfNatInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Subfunctor.Basic
/-- The inclusion of a subfunctor to the original functor.  -/
CategoryTheory.Subfunctor.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C (Type w)} → (G : CategoryTheory.Subfunctor F) → G.toFunctor ⟶ F
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.instEpiπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData), CategoryTheory.Epi h.π
-- Lean.Meta.Basic
Lean.Meta.withConfigWithKey : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Lean.Meta.ConfigWithKey → n α → n α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_alter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)},
  k' ∈ m.alter k f ↔ if (k == k') = true then (f (m.get? k)).isSome = true else k' ∈ m
-- Mathlib.Order.Category.BoolAlg
BoolAlg.Hom.ext_iff : ∀ {X Y : BoolAlg} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoShortComplexH2_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupCohomology.isoShortComplexH2 A).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.homMk (groupCohomology.cochainsIso₁ A).inv (groupCohomology.cochainsIso₂ A).inv
        (groupCohomology.cochainsIso₃ A).inv ⋯ ⋯)
      ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.up ℕ) 1 2 3 groupCohomology.isoShortComplexH2._proof_1
              groupCohomology.isoShortComplexH2._proof_2).inv.app
        (groupCohomology.inhomogeneousCochains A))
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Adds a simp theorem to a simp extension
 -/
Lean.Meta.addSimpTheorem : Lean.Meta.SimpExtension → Lean.Name → Bool → Bool → Lean.AttributeKind → ℕ → Lean.MetaM Unit
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max!_erase_le_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, t.erase k ≠ ∅ → (cmp (t.erase k).max! t.max!).isLE = true
-- Mathlib.Order.SetNotation
/-- Class for the `sSup` operator  -/
SupSet : Type u_1 → Type u_1
-- Lean.Meta.Match.SimpH
/-- Like `simpH?`, but works directly on a goal corresponding to the unsimplified equational theorem
hypothesis, and either closes it or returns a residual goal whose type is the simplified equational
theorem hypothesis.
 -/
Lean.Meta.Match.simpH : Lean.MVarId → ℕ → Lean.MetaM (Option Lean.MVarId)