mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (arrows : CategoryTheory.Presieve X)
  (downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (CategoryTheory.CategoryStruct.comp g f))
  (arrows_1 : CategoryTheory.Presieve X)
  (downward_closed_1 :
    ∀ {Y Z : C} {f : Y ⟶ X}, arrows_1 f → ∀ (g : Z ⟶ Y), arrows_1 (CategoryTheory.CategoryStruct.comp g f)),
  ({ arrows := arrows, downward_closed := downward_closed } =
      { arrows := arrows_1, downward_closed := downward_closed_1 }) =
    (arrows = arrows_1)
-- Mathlib.Data.List.Destutter
/-- `destutter'` on a relation like ≠ or <, whose negation is transitive, has length monotone
under a `¬R` changing of the first element.  -/
List.length_destutter'_cotrans_ge : ∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] {b : α} [i : IsTrans α Rᶜ] {a : α} {l : List α},
  ¬R b a → (List.destutter' R b l).length ≤ (List.destutter' R a l).length
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α} {fallback : β k},
  (Std.ExtDTreeMap.filter f t).getD k fallback = (Option.filter (f k) (t.get? k)).getD fallback
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.LeftHomotopyRel.refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (f : X ⟶ Y), HomotopicalAlgebra.LeftHomotopyRel f f
-- Mathlib.Data.List.Infix
List.infix_singleton_iff : ∀ {α : Type u_1} (xs : List α) (x : α), xs <:+: [x] ↔ xs = [] ∨ xs = [x]
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.triangleRotation_counitIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive],
  (CategoryTheory.Pretriangulated.triangleRotation C).counitIso = CategoryTheory.Pretriangulated.invRotCompRot
-- Mathlib.Topology.Maps.OpenQuotient
IsOpenQuotientMap.map_nhds_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenQuotientMap f → ∀ (x : X), Filter.map f (nhds x) = nhds (f x)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.indep_iff : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I ↔ ∃ B, M.IsBase B ∧ I ⊆ B
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
/-- [Stacks Tag 0310](https://stacks.math.columbia.edu/tag/0310) ((1)) -/
Module.associatedPrimes.mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {R' : Type u_2} [inst_1 : CommRing R'] [inst_2 : Algebra R R']
  [hSR' : IsLocalization S R'] {M : Type u_3} {M' : Type u_4} [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  [inst_5 : AddCommGroup M'] [inst_6 : Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] [inst_8 : Module R' M']
  [IsScalarTower R R' M'] (p : Ideal R'),
  Ideal.comap (algebraMap R R') p ∈ associatedPrimes R M → p ∈ associatedPrimes R' M'
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_insert : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF → ∀ {k : α} {v : β k}, (↑(m.insert k v)).size = if m.contains k = true then (↑m).size else (↑m).size + 1
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_add_const_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Integrable X μ →
    ∀ (c : ℝ), ProbabilityTheory.covariance (fun ω => X ω + c) Y μ = ProbabilityTheory.covariance X Y μ
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientKerEquivOfRightInverse_apply : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (φ : G →+ H) (ψ : H → G)
  (hφ : Function.RightInverse ψ ⇑φ) (a : G ⧸ φ.ker),
  (QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ hφ) a = (QuotientAddGroup.kerLift φ) a
-- Mathlib.Data.Sym.Basic
Sym.mem_fill_iff : ∀ {α : Type u_1} {n : ℕ} {a b : α} {i : Fin (n + 1)} {s : Sym α (n - ↑i)}, a ∈ Sym.fill b i s ↔ ↑i ≠ 0 ∧ a = b ∨ a ∈ s
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.liftOrderHom_mk : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {α : Type u_2}
  [inst_3 : PartialOrder α] (f : M → α)
  (h : ∀ (a b : M), MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b → f a ≤ f b) (a : M),
  (MulArchimedeanClass.liftOrderHom f h) (MulArchimedeanClass.mk a) = f a
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.countablySeparated_def : ∀ {α : Type u_1} [inst : MeasurableSpace α],
  MeasurableSpace.CountablySeparated α ↔ HasCountableSeparatingOn α MeasurableSet Set.univ
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.of_zeroHypercover_target : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [inst_1 : K.HasPullbacks] [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y}
  (𝒰 : K.ZeroHypercover Y) [𝒰.Small], (∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) → P f
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.subsingletonEquiv_symm_apply : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Subsingleton ι] (i₀ : ι) (x : s i₀),
  (PiTensorProduct.subsingletonEquiv i₀).symm x = ⨂ₜ[R] (i : ι), Function.update 0 i₀ x i
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.FunctorToTypes.hcomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (σ : F ⟶ G)
  {D : Type u'} [𝒟 : CategoryTheory.Category.{u', u'} D] (I J : CategoryTheory.Functor D C) (ρ : I ⟶ J) {W : D}
  (x : (I.comp F).obj W),
  (CategoryTheory.ConcreteCategory.hom ((ρ ◫ σ).app W)) x =
    (CategoryTheory.ConcreteCategory.hom (G.map (ρ.app W))) ((CategoryTheory.ConcreteCategory.hom (σ.app (I.obj W))) x)
-- Mathlib.Algebra.Algebra.Hom
AlgHom.ofLinearMap_toLinearMap : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) (map_one : φ.toLinearMap 1 = 1)
  (map_mul : ∀ (x y : A), φ.toLinearMap (x * y) = φ.toLinearMap x * φ.toLinearMap y),
  AlgHom.ofLinearMap φ.toLinearMap map_one map_mul = φ
-- Init.MetaTypes
Lean.Meta.Occurrences.pos.sizeOf_spec : ∀ (idxs : List ℕ), sizeOf (Lean.Meta.Occurrences.pos idxs) = 1 + sizeOf idxs
-- Mathlib.Order.SuccPred.WithBot
WithBot.succ_lt_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α] {x y : WithBot α} [NoMaxOrder α],
  x < y → x.succ < y.succ
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.combine.eq_def : ∀ {α : Type u_1} (le : α → α → Bool) (x : Batteries.PairingHeapImp.Heap α),
  Batteries.PairingHeapImp.Heap.combine le x =
    match x with
    | h₁@h_1:(Batteries.PairingHeapImp.Heap.node a child h₂@h:(Batteries.PairingHeapImp.Heap.node a_1 child_1 s)) =>
      Batteries.PairingHeapImp.Heap.merge le (Batteries.PairingHeapImp.Heap.merge le h₁ h₂)
        (Batteries.PairingHeapImp.Heap.combine le s)
    | h => h
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.id_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.Comon C), (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X
-- Mathlib.Tactic.Ring.Common
/-- Attempts to prove that a polynomial expression in `ℕ` is positive.

* `0 < 0` fails
* `0 < a + b` if `0 < a` or `0 < b`
 -/
Mathlib.Tactic.Ring.Common.ExSumNat.evalPos : {a : Q(ℕ)} → Mathlib.Tactic.Ring.Common.ExSumNat a → Option Q(0 < «$a»)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.mk.congr_simp : ∀ {α : Type u_4} [inst : TopologicalSpace α] (carrier carrier_1 : Set α) (e_carrier : carrier = carrier_1)
  (isClosed' : IsClosed carrier),
  { carrier := carrier, isClosed' := isClosed' } = { carrier := carrier_1, isClosed' := ⋯ }
-- Init.Prelude
Char.val_ne_of_ne : ∀ {c d : Char}, ¬c = d → ¬c.val = d.val
-- Init.Data.List.Basic
List.range'_zero : ∀ {s step : ℕ}, List.range' s 0 step = []
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- There is some split coequalizer  -/
CategoryTheory.HasSplitCoequalizer.splittable : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f g : X ⟶ Y}
  [self : CategoryTheory.HasSplitCoequalizer f g], ∃ Z h, Nonempty (CategoryTheory.IsSplitCoequalizer f g h)
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.instInhabited : {α : Type u_2} → [inst : MulZeroOneClass α] → Inhabited (α →*₀ α)
-- Lean.Parser.Term
Lean.Parser.Term.declName.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.UInt
USize.toFin_injective : Function.Injective USize.toFin
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Swapping the two vectors passed to `oangle` negates the angle.  -/
Orientation.oangle_rev : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), o.oangle y x = -o.oangle x y
-- Mathlib.Topology.Algebra.Group.Basic
ConjAct.units_continuousConstSMul : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M], ContinuousConstSMul (ConjAct Mˣ) M
-- Mathlib.CategoryTheory.MorphismProperty.RetractArgument
/-- If `i ≫ p = f`, and `f` has the right lifting property with respect to `i`,
then `f` is a retract of `p`.  -/
CategoryTheory.RetractArrow.ofRightLiftingProperty : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {i : X ⟶ Y} →
          {p : Y ⟶ Z} →
            CategoryTheory.CategoryStruct.comp i p = f →
              [CategoryTheory.HasLiftingProperty i f] → CategoryTheory.RetractArrow f p
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_min : ∀ (x y : ℝ), ENNReal.ofReal (min x y) = min (ENNReal.ofReal x) (ENNReal.ofReal y)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (next : Option α) (upperBound : α),
  sizeOf { next := next, upperBound := upperBound } = 1 + sizeOf next + sizeOf upperBound
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The underlying object of the base category.  -/
CategoryTheory.Kleisli.of : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {T : CategoryTheory.Monad C} → CategoryTheory.Kleisli T → C
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {v : β},
  (k, v) ∈ Std.DHashMap.Const.toList m ↔ m.getKey? k = some k ∧ Std.DHashMap.Const.get? m k = some v
-- Mathlib.RingTheory.Ideal.Operations
Submodule.smul_le_right : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : Ideal R}
  {N : Submodule R M}, I • N ≤ N
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
_private.Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification.0.NumberField.InfinitePlace.surjOn_embeddingConjugateIte : ∀ {K : Type u_4} (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K),
  Set.SurjOn (NumberField.InfinitePlace.embeddingConjugateIte✝ v) (NumberField.InfinitePlace.unramifiedPlacesOver L v)
    (NumberField.ComplexEmbedding.unmixedEmbeddingsOver L v.embedding)
-- Init.Data.List.Basic
/-- Removes the last element of the list, if one exists.

Examples:
* `[].dropLast = []`
* `["tea"].dropLast = []`
* `["tea", "coffee", "juice"].dropLast = ["tea", "coffee"]`
 -/
List.dropLast : {α : Type u_1} → List α → List α
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
/-- The t-structure induced on the full subcategory of `t`-bounded below objects.  -/
CategoryTheory.Triangulated.TStructure.onMinus : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} 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) →
                [CategoryTheory.IsTriangulated C] → CategoryTheory.Triangulated.TStructure t.minus.FullSubcategory
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the reverse direction of `lipschitzOnWith_inv_iff`. -/
LipschitzOnWith.inv : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal} {f : α → E}
  {s : Set α}, LipschitzOnWith K f s → LipschitzOnWith K f⁻¹ s
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.map_comp_lift : ∀ {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.Groupoid E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E),
  (CategoryTheory.FreeGroupoid.map F).comp (CategoryTheory.FreeGroupoid.lift G) =
    CategoryTheory.FreeGroupoid.lift (F.comp G)
-- Init.Data.Sum.Lemmas
Sum.isRight_eq_false : ∀ {α : Type u_1} {β : Type u_2} {x : α ⊕ β}, x.isRight = false ↔ x.isLeft = true
-- Mathlib.Logic.Function.Basic
Function.uncurry_update_update : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq α'] (f : α → α' → β)
  (a : α) (a' : α') (b : β),
  Function.uncurry (Function.update f a (Function.update (f a) a' b)) = Function.update (Function.uncurry f) (a, a') b
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.isLeftAdjoint_iff_rightAdjointObjIsDefined_eq_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D), F.IsLeftAdjoint ↔ F.rightAdjointObjIsDefined = ⊤
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem_mul : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m),
  0 < m →
    ∀
      (q :
        ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace)
      (a : A) {n : ℕ} (hn : a ∈ 𝒜 (n * m)),
      a ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q ↔
        HomogeneousLocalization.mk { deg := m * n, num := ⟨a, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (h : (↑m).WF) [Inhabited α] {k k' : α} {f : β → β}
  (hc : (Std.DHashMap.Internal.Raw₀.Const.modify m k f).contains k' = true),
  (Std.DHashMap.Internal.Raw₀.Const.modify m k f).getKey k' hc = if (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Laplacian for functions on real inner product spaces, with respect to a set `s`. Use `open
InnerProductSpace` to access the notation `Δ[s]` for `InnerProductSpace.LaplacianWithin`.
 -/
InnerProductSpace.laplacianWithin : {E : Type u_2} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      [FiniteDimensional ℝ E] →
        {F : Type u_3} → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → (E → F) → Set E → E → F
-- Batteries.Data.List.Lemmas
List.findIdxNth.go.eq_def : ∀ {α : Type u_1} (p : α → Bool) (xs : List α) (n s : ℕ),
  List.findIdxNth.go p xs n s =
    match xs, n, s with
    | [], x, s => s
    | a :: xs, 0, s => bif p a then s else List.findIdxNth.go p xs 0 (s + 1)
    | a :: xs, n.succ, s => bif !p a then List.findIdxNth.go p xs (n + 1) (s + 1) else List.findIdxNth.go p xs n (s + 1)
-- Mathlib.Analysis.Normed.Group.Basic
mem_closedBall_zero_iff : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a : E} {r : ℝ}, a ∈ Metric.closedBall 0 r ↔ ‖a‖ ≤ r
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.mem_trivChange_source : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (i j : ι)
  (p : B × F), p ∈ (Z.trivChange i j).source ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.isEmpty = true → t.contains a = false
-- Mathlib.Algebra.Notation.Prod
Prod.mk_sub_mk : ∀ {G : Type u_8} {H : Type u_9} [inst : Sub G] [inst_1 : Sub H] (x₁ x₂ : G) (y₁ y₂ : H),
  (x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂)
-- Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Finset.card_finsuppAntidiag_nat_eq_multichoose : ∀ {ι : Type u_1} [inst : DecidableEq ι] {s : Finset ι} (n : ℕ), (s.finsuppAntidiag n).card = s.card.multichoose n
-- Mathlib.NumberTheory.PythagoreanTriples
_private.Mathlib.NumberTheory.PythagoreanTriples.0.coprime_sq_sub_sq_add_of_odd_even : ∀ {m n : ℤ}, m.gcd n = 1 → m % 2 = 1 → n % 2 = 0 → (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.getUserConfig : Lean.Meta.SimpM Lean.Options
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.repr_eq_iff : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {b : Module.Basis ι R M} {f : M →ₗ[R] ι →₀ R}, ↑b.repr = f ↔ ∀ (i : ι), f (b i) = fun₀ | i => 1
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- The minimal subalgebra that includes `s`.  -/
Algebra.adjoin : (R : Type u) →
  {A : Type v} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Set A → Subalgebra R A
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.operation_eq_map_mk_operation : ∀ {α : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {x : Std.Iterators.PostconditionT m α},
  x.operation = (fun a => ⟨↑a, ⋯⟩) <$> x.operation
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_Ico_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)] (f : (i : ι) → α i)
  (i : ι) (a : α i), Function.update f i '' Set.Ico a (f i) = Set.Ico (Function.update f i a) f
-- Init.Data.Rat.Lemmas
Rat.le_iff_sub_nonneg : ∀ (a b : ℚ), a ≤ b ↔ 0 ≤ b - a
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.GeneratorNode : Type
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.monadLift_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α ε : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m α)
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)),
  ⦃(Std.Do.wp x).apply (fun a => Q.1 a, Q.2.2)⦄ MonadLift.monadLift x ⦃Q⦄
-- Mathlib.Algebra.Ring.Idempotent
IsIdempotentElem.sub_iff : ∀ {R : Type u_1} [inst : NonUnitalRing R] [IsAddTorsionFree R] {p q : R},
  IsIdempotentElem p → IsIdempotentElem q → (IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p)
-- Mathlib.Analysis.Convex.Strong
strongConvexOn_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {f : E → ℝ},
  StrongConvexOn s 0 f ↔ ConvexOn ℝ s f
-- Init.Data.List.Zip
List.unzip_zip : ∀ {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β}, l₁.length = l₂.length → (l₁.zip l₂).unzip = (l₁, l₂)
-- Std.Time.Date.Unit.Month
Std.Time.Month.instOrdOrdinal : Ord Std.Time.Month.Ordinal
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.Eqv.of_map : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] {i j : ι} (h : i ≤ j) (x : G i),
  Module.DirectLimit.Eqv f ((DirectSum.lof R ι G i) x) ((DirectSum.lof R ι G j) ((f i j h) x))
-- Mathlib.Algebra.MonoidAlgebra.Support
MonoidAlgebra.support_coeff_one_subset : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : One G], (MonoidAlgebra.coeff 1).support ⊆ 1
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.forget_createsLimitsOfSize.eq_1 : MonCat.forget_createsLimitsOfSize =
  { CreatesLimitsOfShape := fun {J} [CategoryTheory.Category.{w, v} J] => inferInstance }
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.map_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D), (sq.map F).X₁ = F.obj sq.X₁
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.OmissionReason.string.inj : ∀ {s s_1 : String},
  Lean.PrettyPrinter.Delaborator.OmissionReason.string s = Lean.PrettyPrinter.Delaborator.OmissionReason.string s_1 →
    s = s_1
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.coe_circle_smul : ∀ (z : Circle) (w : Complex.UnitClosedDisc), ↑(z • w) = ↑z * ↑w
-- Mathlib.Order.UpperLower.Basic
not_bddBelow_Iio : ∀ {α : Type u_1} [inst : Preorder α] (a : α) [NoMinOrder α], ¬BddBelow (Set.Iio a)
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.coe_pow : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] (x : ↑(Set.Ioc 0 1))
  (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Eta-expanded form of `MeasureTheory.StronglyMeasurable.const_vadd` -/
MeasureTheory.StronglyMeasurable.fun_const_vadd : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {𝕜 : Type u_5}
  [inst_1 : VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β],
  MeasureTheory.StronglyMeasurable f → ∀ (c : 𝕜), MeasureTheory.StronglyMeasurable fun i => c +ᵥ f i
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications `M` and `M₂` will be topological modules over the
topological semiring `R`.  -/
ContinuousLinearEquiv.continuous_invFun : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R}
  [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {M : Type u_3} [inst_4 : TopologicalSpace M]
  [inst_5 : AddCommMonoid M] {M₂ : Type u_4} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R M] [inst_9 : Module S M₂] (self : M ≃SL[σ] M₂), Continuous (↑self).invFun
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- Substitution `y = exp x` in integrals over `Ioi a`  -/
MeasureTheory.integral_comp_exp_Ioi : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : ℝ → E) (a : ℝ),
  ∫ (x : ℝ) in Set.Ioi a, Real.exp x • g (Real.exp x) = ∫ (y : ℝ) in Set.Ioi (Real.exp a), g y
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.trans_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃),
  (e.trans e').hom = CategoryTheory.CategoryStruct.comp e.hom e'.hom
-- Init.Data.Int.Order
Int.add_pos : ∀ {a b : ℤ}, 0 < a → 0 < b → 0 < a + b