mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_sdiff_neg_vadd : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ (s \ (-c +ᵥ t)) = μ ((c +ᵥ s) \ t)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instZero : {K : Type u} → [inst : CommRing K] → Zero (RatFunc K)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- Construct an element of `(F ⨿ G).obj a` from an element of `F.obj a`  -/
CategoryTheory.FunctorToTypes.coprodInl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C (Type w)} → {a : C} → F.obj a → (F ⨿ G).obj a
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instIsIsoAbApp : ∀ {X : AlgebraicGeometry.Scheme} {M N : X.Modules} {φ : M ⟶ N} {U : X.Opens} [CategoryTheory.IsIso φ],
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Modules.Hom.app φ U)
-- Mathlib.Analysis.Convex.Basic
Monotone.convex_gt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {f : E → β}, Monotone f → ∀ (r : β), Convex 𝕜 {x | f x ≤ r}
-- Mathlib.Analysis.Normed.Module.Extr
/-- If `f : α → E` is a function such that `norm ∘ f` has a local maximum on a set `s` at a point
`c` and `y` is a vector on the same ray as `f c`, then the function `fun x => ‖f x + y‖` has a local
maximum on `s` at `c`.  -/
IsLocalMaxOn.norm_add_sameRay : ∀ {X : Type u_2} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : TopologicalSpace X] {f : X → E} {s : Set X} {c : X} {y : E},
  IsLocalMaxOn (norm ∘ f) s c → SameRay ℝ (f c) y → IsLocalMaxOn (fun x => ‖f x + y‖) s c
-- Mathlib.Topology.Order
/-- A copy of a type equipped with the discrete topology.  -/
WithDiscreteTopology : Type u_1 → Type u_1
-- Mathlib.Data.Int.Sqrt
Int.sqrt_nonneg : ∀ (n : ℤ), 0 ≤ Int.sqrt n
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- Convergence of finite measures implies the convergence of their total masses.  -/
Filter.Tendsto.mass : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto μs F (nhds μ) → Filter.Tendsto (fun i => (μs i).mass) F (nhds μ.mass)
-- Aesop.Stats.Basic
Aesop.instInhabitedScriptGenerated : Inhabited Aesop.ScriptGenerated
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasIterationOfShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} (I : CategoryTheory.MorphismProperty C) {κ : Cardinal.{w}}
  {inst_1 : Fact κ.IsRegular} {inst_2 : OrderBot κ.ord.ToType} [self : I.IsCardinalForSmallObjectArgument κ],
  CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instCompl : {α : Type u_1} → [inst : TopologicalSpace α] → [CompactSpace α] → [T2Space α] → Compl (TopologicalSpace.CompactOpens α)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.KernelFork.map_condition_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.KernelFork f) (G : CategoryTheory.Functor C D)
  [G.PreservesZeroMorphisms] {Z : D} (h : G.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Fork.ι c))
      (CategoryTheory.CategoryStruct.comp (G.map f) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_eq_none : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, a ∉ m → m[a]? = none
-- Std.Time.Format.Basic
/-- Parses the input string into a `DateTime`.
 -/
Std.Time.GenericFormat.parse : {aw : Std.Time.Awareness} → Std.Time.GenericFormat aw → String → Except String Std.Time.DateTime
-- Mathlib.Data.String.Defs
/-- `String.mapTokens c f s` tokenizes `s : string` on `c : char`, maps `f` over each token, and
then reassembles the string by intercalating the separator token `c` over the mapped tokens.  -/
String.mapTokens : Char → (String → String) → String → String
-- Init.Data.List.Nat.Sublist
List.IsSuffix.getElem : ∀ {α : Type u_1} {xs ys : List α} (h : xs <:+ ys) {i : ℕ} (hn : i < xs.length), xs[i] = ys[ys.length - xs.length + i]
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffWithinAt.neg_section : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s : (x : M) → V x} {u : Set M} {x₀ : M},
  ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) u x₀ →
    ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (-s) x⟩) u x₀
-- Mathlib.Combinatorics.Quiver.Subquiver
/-- A wide subquiver viewed as a quiver on its own.  -/
WideSubquiver.quiver : {V : Type u_1} → [inst : Quiver V] → (H : WideSubquiver V) → Quiver (WideSubquiver.toType V H)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {f : α → ε} {s : Set α},
  MeasurableSet s → MeasureTheory.eLpNorm (s.indicator f) p μ = MeasureTheory.eLpNorm f p (μ.restrict s)
-- Mathlib.Data.Set.Lattice
Set.iUnion_eq_range_psigma : ∀ {β : Type u_2} {ι : Sort u_5} (s : ι → Set β), ⋃ i, s i = Set.range fun a => ↑a.snd
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a fallback : α},
  (t.insert k).getD a fallback = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getD a fallback
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instRxiHasSize : {n : ℕ} → Std.Rxi.HasSize (BitVec n)
-- Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
_private.Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy.0.CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.comm_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y} (H : CategoryTheory.SimplicialObject.Homotopy f g) (n : ℕ),
  f.app (Opposite.op { len := n + 1 }) =
    CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.alternatingFaceMapComplex C).obj X).d (n + 1) n)
          (CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom H n (n + 1)) +
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom H (n + 1) (n + 2))
          (((AlgebraicTopology.alternatingFaceMapComplex C).obj Y).d (n + 2) (n + 1)) +
      g.app (Opposite.op { len := n + 1 })
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.zmultiples_ne_bot : ∀ {G : Type u_1} [inst : AddGroup G] {g : G}, AddSubgroup.zmultiples g ≠ ⊥ ↔ g ≠ 0
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
PartOrdEmb.instIsClosedUnderColimitsOfShapeIsCardinalFilteredOfIsCardinalFiltered : ∀ (κ : Cardinal.{u}) [inst : Fact κ.IsRegular] (J : Type u) [inst_1 : CategoryTheory.SmallCategory J]
  [CategoryTheory.IsCardinalFiltered J κ], (PartOrdEmb.isCardinalFiltered κ).IsClosedUnderColimitsOfShape J
-- Mathlib.Tactic.TermCongr
/-- Does `CongrResult.mkDefault` but makes sure there are no lingering congruence holes.  -/
Mathlib.Tactic.TermCongr.CongrResult.mkDefault' : ℕ → Lean.Expr → Lean.Expr → Lean.MetaM Mathlib.Tactic.TermCongr.CongrResult
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Lambda subexpressions for each alternate.  -/
Lean.PrettyPrinter.Delaborator.AppMatchState.alts : Lean.PrettyPrinter.Delaborator.AppMatchState → Array Lean.SubExpr
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.coe_himp : ∀ {α : Type u_1} [inst : HeytingAlgebra α] (a b : Heyting.Regular α), ↑(a ⇨ b) = ↑a ⇨ ↑b
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivWithinAt.iterate : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {f : 𝕜 → 𝕜} {f' : 𝕜},
  HasDerivWithinAt f f' s x → f x = x → Set.MapsTo f s s → ∀ (n : ℕ), HasDerivWithinAt f^[n] (f' ^ n) s x
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.equivListRowLens_symm_apply : ∀ (ww : { w // w.SortedGE ∧ ∀ x ∈ w, 0 < x }), YoungDiagram.equivListRowLens.symm ww = YoungDiagram.ofRowLens ↑ww ⋯
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.le : ∀ {x y : ℝ*} {r s : ℝ}, x.IsSt r → y.IsSt s → x ≤ y → r ≤ s
-- Init.SimpLemmas
dite_cond_congr : ∀ {α : Sort u_1} {b c : Prop} {s : Decidable b} [inst : Decidable c] {x : b → α} {y : ¬b → α} (h₁ : b = c),
  dite b x y = if h : c then x ⋯ else y ⋯
-- Mathlib.Order.Filter.Pointwise
/-- An additive action of an additive monoid `α` on a type `β` gives an additive
action of `Filter α` on `Filter β`.  -/
Filter.addAction : {α : Type u_2} → {β : Type u_3} → [inst : AddMonoid α] → [AddAction α β] → AddAction (Filter α) (Filter β)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.prod_same_index_mono : ∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {ι : Type u_6} [inst : LinearOrder ι] {p : ι → Prop}
  {sa : ι → Set α} {sb : ι → Set β},
  la.HasBasis p sa →
    lb.HasBasis p sb → MonotoneOn sa {i | p i} → MonotoneOn sb {i | p i} → (la ×ˢ lb).HasBasis p fun i => sa i ×ˢ sb i
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.elabFixedTermElab : Lean.Elab.Term.TermElab
-- Mathlib.Tactic.DeriveTraversable
/-- The deriving handler for `LawfulTraversable`.  -/
Mathlib.Deriving.Traversable.lawfulTraversableDeriveHandler : Lean.Elab.DerivingHandler
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.snd_one : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : One α], (NonemptyInterval.toProd 1).2 = 1
-- Mathlib.Order.Fin.Tuple
/-- Note this lemma can only be written about non-dependent tuples as `insertNth (last n) = snoc` is
not a definitional equality.  -/
Fin.insertNthOrderIso_last : ∀ (n : ℕ) (α : Type u_2) [inst : LE α], Fin.insertNthOrderIso (fun x => α) (Fin.last n) = Fin.snocOrderIso fun x => α
-- Mathlib.Algebra.BigOperators.Finprod
finsum_def' : ∀ {M : Type u_7} {α : Sort u_8} [inst : AddCommMonoid M] (f : α → M),
  finsum f = if h : Function.HasFiniteSupport (f ∘ PLift.down) then ∑ i ∈ Set.Finite.toFinset h, f i.down else 0
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Surjective.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.Surjective
-- Mathlib.Data.Set.Basic
Set.right_eq_inter : ∀ {α : Type u} {s t : Set α}, t = s ∩ t ↔ t ⊆ s
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.instLawfulOrderLTOfLawfulUpwardEnumerableLT : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLE α],
  Std.LawfulOrderLT α
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_zero_right : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : Zero N] (f : α →₀ N),
  f.neLocus 0 = f.support
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.equiv_mk : ∀ {R : Type u_1} (K : Type u_2) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] (K' : Type u_3) [inst_5 : Field K'] [inst_6 : Algebra R K']
  [inst_7 : IsFractionRing R K'] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ),
  (ClassGroup.equiv K') ((ClassGroup.mk K) I) =
    (QuotientGroup.mk' (toPrincipalIdeal R K').range)
      ((Units.mapEquiv ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K K')) I)
-- Init.Data.SInt.Lemmas
Int8.toInt_minValue_lt_zero : Int8.minValue.toInt < 0
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2ComputableAux.mk.injEq : ∀ {Γ₀ Γ₁ : Type} (tm : Turing.FinTM2) (inputAlphabet : tm.Γ tm.k₀ ≃ Γ₀) (outputAlphabet : tm.Γ tm.k₁ ≃ Γ₁)
  (tm_1 : Turing.FinTM2) (inputAlphabet_1 : tm_1.Γ tm_1.k₀ ≃ Γ₀) (outputAlphabet_1 : tm_1.Γ tm_1.k₁ ≃ Γ₁),
  ({ tm := tm, inputAlphabet := inputAlphabet, outputAlphabet := outputAlphabet } =
      { tm := tm_1, inputAlphabet := inputAlphabet_1, outputAlphabet := outputAlphabet_1 }) =
    (tm = tm_1 ∧ inputAlphabet ≍ inputAlphabet_1 ∧ outputAlphabet ≍ outputAlphabet_1)
-- Mathlib.Analysis.Normed.Group.Ultra
/-- All triangles are isosceles in an ultrametric normed group.  -/
IsUltrametricDist.nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm : ∀ {S : Type u_1} [inst : SeminormedGroup S] [IsUltrametricDist S] {x y : S}, ‖x‖₊ ≠ ‖y‖₊ → ‖x * y‖₊ = max ‖x‖₊ ‖y‖₊
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_piecewise : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s t : Finset ι) (f g : ι → M),
  ∏ x ∈ s, t.piecewise f g x = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse_obj : ∀ {V : Type u'} [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {W : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} W] [inst_3 : CategoryTheory.MonoidalCategory W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.LaxMonoidal] (D : Type u) [inst_5 : CategoryTheory.EnrichedCategory V D]
  (e :
    (v : V) →
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v))
  (h :
    ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
      (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f))
  (X : CategoryTheory.ForgetEnrichment W (CategoryTheory.TransportEnrichment F D)),
  (CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse F D e h).obj X =
    CategoryTheory.ForgetEnrichment.of V (CategoryTheory.ForgetEnrichment.to W X)
-- Init.Data.Array.Count
Array.count_eq_size_filter : ∀ {α : Type u_1} [inst : BEq α] {a : α} {xs : Array α}, Array.count a xs = (Array.filter (fun x => x == a) xs).size
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_mulVec : ∀ {l : Type u_1} {m : Type u_2} {α : Type v} [inst : DecidableEq l] [inst_1 : Fintype m]
  [inst_2 : NonUnitalNonAssocSemiring α] (A : Matrix l m α) (i : l) (c v : m → α),
  (A.updateRow i c).mulVec v = Function.update (A.mulVec v) i (c ⬝ᵥ v)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instBot.eq_1 : ∀ {R : Type u} {M : Type v} [inst : SMul R M], SubMulAction.instBot = { bot := { carrier := ∅, smul_mem' := ⋯ } }
-- Mathlib.Order.Filter.SmallSets
Filter.Eventually.exists_mem_of_smallSets : ∀ {α : Type u_1} {l : Filter α} {p : Set α → Prop}, (∀ᶠ (t : Set α) in l.smallSets, p t) → ∃ s ∈ l, p s
-- Init.Data.Fin.Lemmas
Fin.lt_of_le_of_lt : ∀ {n : ℕ} {a b c : Fin n}, a ≤ b → b < c → a < c
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.maxEntryD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {fallback : (a : α) × β a}, t₁.maxEntryD fallback = t₂.maxEntryD fallback
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.coeff_expand_mul' : ∀ {R : Type u} [inst : CommSemiring R] {p : ℕ},
  0 < p → ∀ (f : Polynomial R) (n : ℕ), ((Polynomial.expand R p) f).coeff (p * n) = f.coeff n
-- Mathlib.Order.WithBot
WithTop.map₂.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3}, WithTop.map₂ = Option.map₂
-- Mathlib.Order.Category.BddDistLat
BddDistLat.id_apply : ∀ (X : BddDistLat) (x : ↑X.toDistLat), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.Topology.Order.OrderClosed
isClosed_le_prod' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α], IsClosed {p | p.2 ≤ p.1}
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instSubtractionMonoid.eq_1 : ∀ {α : Type u_1} [inst : SubtractionMonoid α],
  Lex.instSubtractionMonoid =
    { toSubNegMonoid := Lex.instSubNegAddMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.neg.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr},
  Lean.Meta.Grind.Arith.Linear.EqCnstrProof.neg c = Lean.Meta.Grind.Arith.Linear.EqCnstrProof.neg c_1 → c = c_1
-- Lean.Structure
Lean.StructureDescr.mk.sizeOf_spec : ∀ (structName : Lean.Name) (fields : Array Lean.StructureFieldInfo),
  sizeOf { structName := structName, fields := fields } = 1 + sizeOf structName + sizeOf fields
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.nonneg_of_mem_compactSet : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.realSpace K},
  x ∈ NumberField.mixedEmbedding.fundamentalCone.compactSet K → ∀ (w : NumberField.InfinitePlace K), 0 ≤ x w
-- Mathlib.NumberTheory.LSeries.Linearity
LSeriesSummable.sub : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (f - g) s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_alter!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {fallback : β} {f : Option β → Option β},
      Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.Const.alter! k f t) k fallback =
        (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback
-- Mathlib.Algebra.Ring.Basic
/-- A (not necessarily unital or associative) ring with no zero divisors has cancellative
multiplication on both sides. Since either left or right cancellative multiplication implies
the absence of zero divisors, the four conditions are equivalent to each other.  -/
noZeroDivisors_tfae : ∀ {R : Type u_3} [inst : NonUnitalNonAssocRing R],
  [NoZeroDivisors R, IsLeftCancelMulZero R, IsRightCancelMulZero R, IsCancelMulZero R].TFAE
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_of_mem_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α} {k : α}, l.contains k = false → k ∈ Std.DHashMap.Const.insertManyIfNewUnit m l → k ∈ m
-- Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject
CategoryTheory.InjectiveObject.instHasFiniteBiproductsOfHasFiniteProducts : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasFiniteProducts C],
  CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.InjectiveObject C)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.matrix_π_assoc : ∀ {J : Type} [inst : Finite J] {K : Type} [inst_1 : Finite K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C}
  {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (k : K) {Z : C} (h : g k ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π g k) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc fun j => m j k) h
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.mk : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        {Q : Type u_5} →
          [inst : Ring R] →
            [inst_1 : AddCommGroup V] →
              [inst_2 : Module R V] →
                [inst_3 : TopologicalSpace P] →
                  [inst_4 : AddTorsor V P] →
                    [inst_5 : AddCommGroup W] →
                      [inst_6 : Module R W] →
                        [inst_7 : TopologicalSpace Q] →
                          [inst_8 : AddTorsor W Q] →
                            (toAffineMap : P →ᵃ[R] Q) → Continuous toAffineMap.toFun → P →ᴬ[R] Q
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.lift'_mk : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M''] [inst_3 : Module R M] [inst_4 : Module R M''] (g : M →ₗ[R] M'')
  (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (m : M) (s : ↥S),
  LocalizedModule.lift' S g h (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (g m)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.casesOn_one : ∀ {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (one : motive 1)
  (of_mul : (x : α) → (xs : FreeMonoid α) → motive (FreeMonoid.of x * xs)), FreeMonoid.casesOn 1 one of_mul = one
-- Mathlib.Combinatorics.Colex
/-- Colex is an extension of the base order.  -/
Finset.Colex.singleton_lt_singleton : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, toColex {a} < toColex {b} ↔ a < b
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.mapEquiv_symm : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  (pkg' : AbstractCompletion.{vβ, uβ} β) (e : α ≃ᵤ β), (pkg.mapEquiv pkg' e).symm = pkg'.mapEquiv pkg e.symm
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condDistrib_comp_self : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β} (X : α → β) {f : β → Ω} (hf : Measurable f),
  ⇑(ProbabilityTheory.condDistrib (f ∘ X) X μ) =ᵐ[MeasureTheory.Measure.map X μ]
    ⇑(ProbabilityTheory.Kernel.deterministic f hf)
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.isSupported_iff : ∀ {ι : 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 : HomologicalComplex C c') (e : c.Embedding c'),
  K.IsSupported e ↔ ∀ (i' : ι'), (∀ (i : ι), e.f i ≠ i') → K.ExactAt i'
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.FixedTermElab.toFixedTermElabRefImpl : Lean.Elab.Term.FixedTermElab → Lean.Elab.Term.FixedTermElabRef
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.leftInverse_invFun : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}
  [inst_2 : Nonempty α] (hf : MeasurableEmbedding f), Function.LeftInverse hf.invFun f
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffWithinAt.continuousWithinAt_iteratedFDerivWithin : ∀ {𝕜 : 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] {s : Set E} {f : E → F} {x : E}
  {n : WithTop ℕ∞} {k : ℕ},
  ContDiffWithinAt 𝕜 n f s x → UniqueDiffOn 𝕜 s → ↑k ≤ n → x ∈ s → ContinuousWithinAt (iteratedFDerivWithin 𝕜 k f s) s x
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
hasFDerivAt_jacobiTheta₂_term : ∀ (n : ℤ) (z τ : ℂ), HasFDerivAt (fun p => jacobiTheta₂_term n p.1 p.2) (jacobiTheta₂_term_fderiv n z τ) (z, τ)