mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.Prod
/-- A variant of `hasDerivAtFilter_finCons` where the derivative variables are free on the RHS
instead.  -/
hasDerivAtFilter_finCons' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {F' : Fin n.succ → Type u_1}
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : 𝕜 → F' 0} {φs : 𝕜 → (i : Fin n) → F' i.succ} {φ' : F' 0} {φs' : (i : Fin n) → F' i.succ} {l : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter (fun x => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') l ↔
    HasDerivAtFilter φ φ' l ∧ HasDerivAtFilter φs φs' l
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapWhiskerLeft_id : ∀ {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] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (H : CategoryTheory.Functor C E) (Fᵣ : CategoryTheory.Functor D E'),
  CategoryTheory.Join.mapWhiskerLeft H (CategoryTheory.CategoryStruct.id Fᵣ) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Join.mapPair H Fᵣ)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_subset_Ioo_right : ∀ {α : Type u_2} {a b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  b₁ ≤ b₂ → Finset.Ioo a b₁ ⊆ Finset.Ioo a b₂
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.ιColimitType_eq_of_map_eq_map : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w₀)) {j j' : J}
  (x : F.obj j) (y : F.obj j') {k : J} (f : j ⟶ k) (f' : j' ⟶ k),
  (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f')) y →
    F.ιColimitType j x = F.ιColimitType j' y
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.exists_insert_of_not_isBase : ∀ {α : Type u_1} {M : Matroid α} {B I : Set α}, M.Indep I → ¬M.IsBase I → M.IsBase B → ∃ e ∈ B \ I, M.Indep (insert e I)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- Auxiliary definition for `extFunctor`.  -/
CategoryTheory.Abelian.extFunctorObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → [CategoryTheory.HasExt C] → C → ℕ → CategoryTheory.Functor C AddCommGrpCat
-- Std.Time.Format.Modifier
Std.Time.instReprExtendedDayPeriod : Repr Std.Time.ExtendedDayPeriod
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.orbitEquivQuotientStabilizer.eq_1 : ∀ (G : Type u) {X : Type v} [inst : AddGroup G] [inst_1 : AddAction G X] (b : X),
  AddAction.orbitEquivQuotientStabilizer G b =
    (Equiv.ofBijective (fun g => ⟨AddAction.ofQuotientStabilizer G b g, ⋯⟩) ⋯).symm
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumInl_onRelation : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ℕ) (val : L.Relations _n),
  FirstOrder.Language.LHom.sumInl.onRelation val = Sum.inl val
-- Mathlib.Algebra.Lie.CartanSubalgebra
/-- A nilpotent Lie algebra is its own Cartan subalgebra.  -/
LieAlgebra.top_isCartanSubalgebra_of_nilpotent : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [LieRing.IsNilpotent L],
  ⊤.IsCartanSubalgebra
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} (x : ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).base) x =
    (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f)) x
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.mul` -/
MeromorphicOn.fun_mul : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {s t : 𝕜 → 𝕜'} {U : Set 𝕜},
  MeromorphicOn s U → MeromorphicOn t U → MeromorphicOn (fun i => s i * t i) U
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.op_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} {E' : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  [inst_3 : CategoryTheory.Category.{v_2, u_2} E'] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E}
  {H : CategoryTheory.Functor E E'},
  CategoryTheory.NatIso.op (F.associator G H) =
    F.opComp (G.comp H) ≪≫
      F.op.isoWhiskerLeft (G.opComp H) ≪≫
        (F.op.associator G.op H.op).symm ≪≫
          CategoryTheory.Functor.isoWhiskerRight (F.opComp G).symm H.op ≪≫ ((F.comp G).opComp H).symm
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  k ∈ m.insertMany l ↔ k ∈ m ∨ l.contains k = true
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.dual.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β],
  SupBotHom.dual =
    { toFun := fun f => { toInfHom := SupHom.dual f.toSupHom, map_top' := ⋯ },
      invFun := fun f => { toSupHom := SupHom.dual.symm f.toInfHom, map_bot' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Vector.Lemmas
Vector.mk_isEqv_mk : ∀ {α : Type u_1} {n : ℕ} {r : α → α → Bool} {xs ys : Array α} (h : xs.size = n) (h' : ys.size = n),
  (Vector.mk xs h).isEqv (Vector.mk ys h') r = xs.isEqv ys r
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAt.deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜}, HasDerivAt f f' x → deriv f x = f'
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Pos.find?_prop_eq_none_iff : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String} {pos : s.Pos},
  pos.find? p = none ↔ ∀ (pos' : s.Pos), pos ≤ pos' → ∀ (h : pos' ≠ s.endPos), ¬p (pos'.get h)
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.integral_map_cast_poissonMeasure' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {R : Type u_2} [inst_1 : NatCast R] [inst_2 : MeasurableSpace R]
  [inst_3 : NormedSpace ℝ E] [CompleteSpace E] [Countable R] [MeasurableSingletonClass R] {r : NNReal} {f : R → E},
  MeasureTheory.Integrable f (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r)) →
    ∫ (x : R), f x ∂MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r) =
      ∑' (n : ℕ), (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) • f ↑n
-- Mathlib.Util.Superscript
/-- A bidirectional character mapping.  -/
Mathlib.Tactic.Superscript.Mapping : Type
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.const.sizeOf_spec : ∀ (moduleName identName : String),
  sizeOf (Lean.Lsp.RefIdent.const moduleName identName) = 1 + sizeOf moduleName + sizeOf identName
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.coe_subtype : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), ⇑H.subtype = Subtype.val
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.comp_linearEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} [inst_7 : AddCommMonoid N₁] [inst_8 : Module R N₁],
  IsTensorProduct f → ∀ (e₁ : N₁ ≃ₗ[R] M₁), IsTensorProduct (f ∘ₗ ↑e₁)
-- Mathlib.Algebra.Order.Module.Defs
nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulStrictMono α β] {a : α} {b : β}, 0 ≤ a • b → 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
-- Lean.DocString.Syntax
/-- Link targets, which may be URLs or named references  -/
Lean.Parser.Category.link_target : Lean.Parser.Category
-- Mathlib.Algebra.Group.Submonoid.Defs
SubmonoidClass.toCommMonoid.eq_1 : ∀ {M : Type u_5} [inst : CommMonoid M] {A : Type u_4} [inst_1 : SetLike A M] [inst_2 : SubmonoidClass A M] (S : A),
  SubmonoidClass.toCommMonoid S = { toMonoid := SubmonoidClass.toMonoid S, mul_comm := ⋯ }
-- Init.Data.UInt.Bitwise
USize.ofFin_shiftRight : ∀ (a b : Fin USize.size), ↑b < System.Platform.numBits → USize.ofFin (a >>> b) = USize.ofFin a >>> USize.ofFin b
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.sInf_le_sSup : ∀ (s : Set ℝ), BddBelow s → BddAbove s → sInf s ≤ sSup s
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.term_ : Lean.ParserDescr
-- Init.Data.UInt.Lemmas
UInt32.lt_of_le_of_lt : ∀ {a b c : UInt32}, a ≤ b → b < c → a < c
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.hom_ext_iff : ∀ {X Y : TopCat} {f g : X ⟶ Y}, f = g ↔ TopCat.Hom.hom f = TopCat.Hom.hom g
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Multiset.prod_map_nonneg : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulMono R]
  {α : Type u_2} {s : Multiset α} {f : α → R}, (∀ a ∈ s, 0 ≤ f a) → 0 ≤ (Multiset.map f s).prod
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isEmpty_takeEndWhile_dropEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, ((s.dropEndWhile pat).takeEndWhile pat).isEmpty = true
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.jointly_surjective₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.IsCofiltered C] [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} (r₁ r₂ : ↑cR.pt)
  (m : PresheafOfModules.ModuleColimit hcR hcM),
  ∃ U a₁ a₂ x,
    (PresheafOfModules.ModuleColimit.ιR cR) a₁ = r₁ ∧
      (PresheafOfModules.ModuleColimit.ιR cR) a₂ = r₂ ∧ PresheafOfModules.ModuleColimit.ιM x = m
-- Init.Data.List.Basic
List.isEqv_cons_nil : ∀ {α : Type u} {a : α} {as : List α} {eqv : α → α → Bool}, (a :: as).isEqv [] eqv = false
-- Mathlib.Topology.Algebra.UniformConvergence
instNegUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg β], instNegUniformFun = { neg := instNegUniformFun._aux_1 }
-- Init.Data.Float.Model.Unpacked.Basic
/-- An inductive type representing a floating-point number with constructors for signed infinity,
not-a-number without payload, signed zero, and finite floats with a sign, positive natural
mantissa and integral exponent.

Finite floats do not have a unique representation in this format: multiplying the
mantissa by two and decreasing the exponent by one yields a finite float that represents the
same rational number.

For a given `Format`, we say that an unpacked float is in canonical form if the exponent
is equal to the `targetExponent` according to that format. Some operations on `UnpackedFloat`,
such as `compare`, assume that the input(s) are all in canonical form for the same format.

Note that an unpacked float in canonical form for a given format may not actually be
representable in that format as the exponent is too large to fit. In this case, the `pack`
function will overflow the float to infinity.

This type exists solely for the purpose of supporting `Float.Model` and `Float32.Model`. It is not
a goal of this development to serve as the basis for a general-purpose floating-point library or
to have any direct lemmas written about it at all. Rather, users interested in a library about
floating-point numbers should develop such a library completely separately, and users interested in
proving properties of their programs involving `Float` should prove that the operations defined
here are equivalent to the operations defined in the separate library and then transfer lemmas from
the library to the `Float` and `Float32` types.
 -/
Float.Model.UnpackedFloat : Type
-- Mathlib.Analysis.Normed.MulAction
NormSMulClass.of_nnnorm_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedRing α] [inst_1 : SeminormedAddGroup β] [inst_2 : SMul α β],
  (∀ (r : α) (x : β), ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊) → NormSMulClass α β
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsAffine X]
  [AlgebraicGeometry.IsAffine Y], P f ↔ Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f))
-- Mathlib.Order.GaloisConnection.Basic
/-- Makes a Galois connection from an order-preserving bijection.  -/
OrderIso.to_galoisConnection : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β), GaloisConnection ⇑e ⇑e.symm
-- Mathlib.Topology.Sets.CompactOpenCovered
IsCompactOpenCovered.of_biUnion_eq_of_isCompact : ∀ {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [inst : (i : ι) → TopologicalSpace (X i)]
  [inst_1 : TopologicalSpace S] {U : Set S},
  IsCompact U →
    ∀ (s : Set (TopologicalSpace.Opens S)),
      ⋃ t ∈ s, ↑t = U → (∀ t ∈ s, IsCompactOpenCovered f ↑t) → IsCompactOpenCovered f U
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.isSymm_comp_iff : ∀ {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix m m (Matrix n n α)},
  ((Matrix.comp m m n n α) A).IsSymm ↔ A.transpose = A.map fun x => x.transpose
-- Mathlib.Tactic.Positivity.Core
/-- Read a `positivity` extension from a declaration of the right type.  -/
Mathlib.Meta.Positivity.mkPositivityExt : Lean.Name → Lean.ImportM Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_neg : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : NegZeroClass α] (d : n → α),
  -Matrix.diagonal d = Matrix.diagonal fun i => -d i
-- Mathlib.Algebra.Order.Field.Basic
le_iff_forall_one_lt_le_mul₀ : ∀ {α : Type u_4} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  0 ≤ b → (a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.continuousWithinAt_leftLim : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [CompleteSpace E] [T3Space E] {f : α → E},
  BoundedVariationOn f Set.univ → ∀ {x : α}, ContinuousWithinAt (Function.leftLim f) (Set.Iic x) x
-- Mathlib.LinearAlgebra.Projection
Submodule.coe_isComplEquivProj_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p : Submodule R E)
  (q : { q // IsCompl p q }), ↑(p.isComplEquivProj q) = p.projectionOnto ↑q ⋯
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.mk.sizeOf_spec : ∀ {R : Type u_14} {S : Type u_15} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R}
  [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {M : Type u_16} {M₂ : Type u_17}
  [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M] [inst_7 : Module S M₂]
  [inst_8 : SizeOf R] [inst_9 : SizeOf S] [inst_10 : SizeOf M] [inst_11 : SizeOf M₂] (toLinearMap : M →ₛₗ[σ] M₂)
  (invFun : M₂ → M) (left_inv : autoParam (Function.LeftInverse invFun toLinearMap.toFun) Equiv.left_inv._autoParam)
  (right_inv : autoParam (Function.RightInverse invFun toLinearMap.toFun) Equiv.right_inv._autoParam),
  sizeOf { toLinearMap := toLinearMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
    1 + sizeOf toLinearMap
-- Mathlib.Order.Lattice
ofDual_inf : ∀ {α : Type u} [inst : Max α] (a b : αᵒᵈ), OrderDual.ofDual (a ⊓ b) = OrderDual.ofDual a ⊔ OrderDual.ofDual b
-- Lean.Level
/-- Short for `LevelMVarId`  -/
Lean.LMVarId : Type
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.forM_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} {m : Type w → Type w'} [Std.TransCmp cmp]
  [inst : Monad m] [LawfulMonad m] {f : α → m PUnit.{w + 1}}, t₁.Equiv t₂ → forM t₁ f = forM t₂ f
-- Init.Data.List.Nat.Erase
List.getElem?_eraseIdx_of_ge : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, i ≤ j → (l.eraseIdx i)[j]? = l[j + 1]?
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_of_contains_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {k a : α} {v : β}, (m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true
-- Mathlib.Algebra.Group.Defs
CommGroup.toDivisionCommMonoid : {G : Type u_1} → [CommGroup G] → DivisionCommMonoid G
-- Mathlib.Data.WSeq.Productive
Stream'.WSeq.productive_ofSeq : ∀ {α : Type u} (s : Stream'.Seq α), (↑s).Productive
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The sum of two `C^n` functions on a domain is `C^n`.  -/
ContDiffOn.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {s : Set E} {f g : E → F}, ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n g s → ContDiffOn 𝕜 n (fun x => f x + g x) s
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- Supporting class for coercions `xₖ : R[x₁, ..., xₙ]`.  -/
Algebra.CoeAdjoinAux : {α : Type u_1} → α → Set α → Prop
-- Mathlib.Topology.Instances.CantorSet
/-- Given `x ∈ [0, 1/3] ∪ [2/3, 1]` (i.e. a level of the Cantor set),
this function rescales the interval containing `x` back to `[0, 1]`.
Used to iteratively extract the ternary representation of `x`.  -/
cantorStep : ℝ → ℝ
-- Plausible.Gen
Plausible.instReprGenError.repr : Plausible.GenError → ℕ → Std.Format
-- Init.Data.String.Search
/-- Interprets a string as the decimal representation of an integer, returning it. Returns `none`
if the string does not contain a decimal integer.

A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
and optionally `-` in front. Leading `+` characters are not allowed.

Use `String.isInt` to check whether `String.toInt?`
would return `some`. `String.toInt!` is an
alternative that panics instead of returning `none` when the string is not an integer.

Examples:

* `"".toInt? = none`

* `"-".toInt? = none`

* `"0".toInt? = some 0`

* `"5".toInt? = some 5`

* `"-5".toInt? = some (-5)`

* `"587".toInt? = some 587`

* `"-587".toInt? = some (-587)`

* `" 5".toInt? = none`

* `"2-3".toInt? = none`

* `"0xff".toInt? = none`
 -/
String.toInt? : String → Option ℤ
-- Mathlib.Tactic.WLOG
/-- The implementation of `wlog` and `wlog!`  -/
Mathlib.Tactic.wlogCore : Lean.TSyntax `Lean.binderIdent →
  Lean.Term →
    Option (Lean.TSyntaxArray `ident) →
      Option (Lean.TSyntax `ident) →
        optParam (Option (Lean.TSyntax `Lean.Parser.Tactic.optConfig)) none → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instInhabitedContMDiffMonoidMorphism.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Monoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {H' : Type u_5}
  [inst_7 : TopologicalSpace H'] {E' : Type u_6} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [inst_10 : Monoid G'] [inst_11 : TopologicalSpace G']
  [inst_12 : ChartedSpace H' G'], instInhabitedContMDiffMonoidMorphism = { default := 1 }
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
pos_of_mul_neg_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R]
  [AddRightReflectLE R] {a b : R}, a * b < 0 → a ≤ 0 → 0 < b
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Limits.PreservesColimit₂.mk : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} {G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)},
  (∀ {c₁ : CategoryTheory.Limits.Cocone K₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁)
      {c₂ : CategoryTheory.Limits.Cocone K₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂),
      Nonempty (CategoryTheory.Limits.IsColimit (G.mapCocone₂ c₁ c₂))) →
    CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G
-- Lean.Structure
/-- Gets the name of the auxiliary definition that would have the default value for the structure field if it exists.
 -/
Lean.mkDefaultFnOfProjFn : Lean.Name → Lean.Name
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f f₁ : E → F}
  {f' : F} {x v : E}, HasLineDerivAt 𝕜 f f' x v → f₁ =ᶠ[nhds x] f → HasLineDerivAt 𝕜 f₁ f' x v
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.toSpanSingletonLIE_symm_apply : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 →L[𝕜] E), (ContinuousLinearMap.toSpanSingletonLIE 𝕜 E).symm f = f 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  k ∈ Std.ExtDTreeMap.Const.insertMany t l ↔ k ∈ t ∨ (List.map Prod.fst l).contains k = true
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- `F.mapCocone c` being colimiting is the same as the induced cofan being colimiting.  -/
CategoryTheory.Limits.Cofan.isColimitMapCoconeEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          {ι : Type u_1} →
            (X : ι → C) →
              (c : CategoryTheory.Limits.Cofan X) →
                CategoryTheory.Limits.IsColimit (F.mapCocone c) ≃
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (F.obj c.pt) fun i => F.map (c.inj i))
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mem_coe : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  {x : L}, x ∈ ↑L' ↔ x ∈ L'
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
AddCommGrpCat.instBraidedCategory : CategoryTheory.BraidedCategory AddCommGrpCat
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.typein_lt_fin : ∀ {n : ℕ} (x : Fin n), (Ordinal.typein LT.lt).toRelEmbedding x = ↑↑x
-- Lean.Server.InfoUtils
_private.Lean.Server.InfoUtils.0.Lean.Elab.Info.fmtHover?.fmtModule? : Lean.Name → Lean.MetaM (Option Std.Format)
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Splitting.instAddMonoidHomClass : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  (S : AddGroupExtension N E G), AddMonoidHomClass S.Splitting G E
-- Mathlib.GroupTheory.Torsion
/-- Torsion additive submonoids of a torsion additive submonoid are
isomorphic to the additive submonoid.  -/
AddCommMonoid.Torsion.ofTorsion : (G : Type u_1) →
  [inst : AddCommMonoid G] → ↥(AddCommMonoid.addTorsion ↥(AddCommMonoid.addTorsion G)) ≃+ ↥(AddCommMonoid.addTorsion G)
-- Lean.Meta.Basic
Lean.Meta.State.mctx : Lean.Meta.State → Lean.MetavarContext