mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Data.Body.Basic
/-- Transforms into a `ByteArray`.
 -/
Std.Http.Body.ToByteArray.toByteArray : {α : Type} → [self : Std.Http.Body.ToByteArray α] → α → ByteArray
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- `Fintype.prod_equiv` is a specialization of `Finset.prod_bij` that
automatically fills in most arguments.

See `Equiv.prod_comp` for a version without `h`.
 -/
Fintype.prod_equiv : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid M]
  (e : ι ≃ κ) (f : ι → M) (g : κ → M), (∀ (x : ι), f x = g (e x)) → ∏ x, f x = ∏ x, g x
-- Lean.Elab.InfoTree.Types
Lean.Elab.ElabInfo.mk.sizeOf_spec : ∀ (elaborator : Lean.Name) (stx : Lean.Syntax),
  sizeOf { elaborator := elaborator, stx := stx } = 1 + sizeOf elaborator + sizeOf stx
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.toSubtype_π_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p) {Z : C}
  (h : Subtype.restrict p f j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f ↑j) h
-- Mathlib.LinearAlgebra.Semisimple
Module.End.IsSemisimple.aeval : ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f : Module.End K M}
  [FiniteDimensional K M], f.IsSemisimple → ∀ (p : Polynomial K), ((Polynomial.aeval f) p).IsSemisimple
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_stringSliceFrom : ∀ {s : String} {p : s.Pos} {q : String.Pos.Raw},
  String.Pos.Raw.IsValidForSlice (s.sliceFrom p) q ↔ String.Pos.Raw.IsValid s (q.offsetBy p.offset)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  (t t_1 : Std.ExtDTreeMap α β cmp), t = t_1 → ∀ (a a_1 : α), a = a_1 → t.getKey! a = t_1.getKey! a_1
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDerivAux.eq_1 : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ) (a : α) (x : γ),
  κ.rnDerivAux η a x =
    if hα : Countable α then ((κ a).rnDeriv (η a) x).toReal else (κ.map fun a => (a, ())).density η a x Set.univ
-- Mathlib.RingTheory.LocalProperties.Exactness
surjective_of_isLocalization_isMaximal : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3) [inst_3 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)]
  [inst_4 : (p : Ideal R) → [inst_4 : p.IsMaximal] → Algebra R (Rₚ p)] (Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4)
  [inst_5 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)]
  [inst_6 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)]
  [inst_7 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)]
  [inst_8 : (p : Ideal R) → [inst_8 : p.IsMaximal] → Algebra R (Sₚ p)]
  [∀ (p : Ideal R) [inst_9 : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)]
  [inst_10 : ∀ (p : Ideal R) [inst_10 : p.IsMaximal], IsScalarTower R S (Sₚ p)]
  [∀ (p : Ideal R) [inst_11 : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p]
  [∀ (p : Ideal R) [inst_12 : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))],
  (∀ (p : Ideal R) [inst : p.IsMaximal], Function.Surjective ⇑(algebraMap (Rₚ p) (Sₚ p))) →
    Function.Surjective ⇑(algebraMap R S)
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.subAt_pullSub : ∀ {A : Type u_1} (T : ↥(Descriptive.tree A)) (x : List A), Descriptive.Tree.subAt (Descriptive.Tree.pullSub T x) x = T
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.models_sentence_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {φ ψ : L.Sentence} {M : Type u_2} [Nonempty M] [inst : L.Structure M]
  [M ⊨ T], T.Iff φ ψ → (M ⊨ φ ↔ M ⊨ ψ)
-- Init.Data.Int.Order
Int.ofNat_natAbs_of_nonneg : ∀ {a : ℤ}, 0 ≤ a → ↑a.natAbs = a
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instLieModule : ∀ (R : Type u_1) (L : Type u_2) (M : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule R L (LieDerivation R L M)
-- Mathlib.Algebra.Homology.CochainComplexPlus
/-- The property of cochain complexes that are bounded below.  -/
CochainComplex.plus : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ObjectProperty (CochainComplex C ℤ)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
ContinuousInf.measurableInf₂ : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] {mγ : MeasurableSpace γ} [BorelSpace γ] [SecondCountableTopology γ]
  [inst_3 : Min γ] [ContinuousInf γ], MeasurableInf₂ γ
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabAddDeclDoc : Lean.Elab.Command.CommandElab
-- Lean.Meta.Tactic.Simp.LoopProtection
Lean.Meta.Simp.mkLoopWarningMsg : Lean.Meta.SimpTheorem → Lean.Meta.SimpM Lean.MessageData
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.Hom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] {M N : CategoryTheory.AddMod D A} (hom : M.X ⟶ N.X)
  [isAddModHom : CategoryTheory.IsAddModHom A hom] (hom_1 : M.X ⟶ N.X)
  (isAddModHom_1 : CategoryTheory.IsAddModHom A hom_1),
  ({ hom := hom, isAddModHom := isAddModHom } = { hom := hom_1, isAddModHom := isAddModHom_1 }) = (hom = hom_1)
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
/-- Constructor for isomorphisms in the category `LaxMonoidalFunctor C D`.  -/
CategoryTheory.LaxMonoidalFunctor.isoMk : {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] →
            {F G : CategoryTheory.LaxMonoidalFunctor C D} →
              (e : F.toFunctor ≅ G.toFunctor) → [CategoryTheory.NatTrans.IsMonoidal e.hom] → F ≅ G
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.σ_naturality_apply : ∀ {S T : SSet} (f : S ⟶ T) {n : ℕ} (i : Fin (n + 1)) (x : S.obj (Opposite.op { len := n })),
  (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n + 1 })))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S i)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ T i))
      ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.comp_id : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂), f.comp AffineIsometry.id = f
-- Mathlib.Algebra.Category.Ring.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
RingCat.Hom.Simps.hom : (R S : RingCat) → R.Hom S → ↑R →+* ↑S
-- Mathlib.Data.List.ToFinsupp
List.toFinsupp_support : ∀ {M : Type u_1} [inst : Zero M] (l : List M) [inst_1 : DecidablePred fun x => l.getD x 0 ≠ 0],
  l.toFinsupp.support = {i ∈ Finset.range l.length | l.getD i 0 ≠ 0}
-- Mathlib.Topology.Semicontinuity.Defs
/-- A function `f : α → Set β` is lower hemicontinuous at `x` if, whenever `t` is an open set
intersecting `f x`, then `t` also intersects `f x'` for all `x'` sufficiently close to `x`.  -/
LowerHemicontinuousAt : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [TopologicalSpace β] → (α → Set β) → α → Prop
-- Mathlib.Algebra.Polynomial.Div
Polynomial.pow_rootMultiplicity_dvd : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R) (a : R),
  (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p ∣ p
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.Hom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {A B : CategoryTheory.Mon C} →
        {M N : Bimod A B} →
          (hom : M.X ⟶ N.X) →
            autoParam
                (CategoryTheory.CategoryStruct.comp M.actLeft hom =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X hom)
                    N.actLeft)
                Bimod.Hom.left_act_hom._autoParam →
              autoParam
                  (CategoryTheory.CategoryStruct.comp M.actRight hom =
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight hom B.X)
                      N.actRight)
                  Bimod.Hom.right_act_hom._autoParam →
                M.Hom N
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.head?_toList : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] [Std.Iterators.Finite α Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β}, it.toList.head? = it.first?
-- Mathlib.LinearAlgebra.Finsupp.SumProd
Finsupp.snd_sumFinsuppLEquivProdFinsupp : ∀ {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_7}
  {β : Type u_8} (f : α ⊕ β →₀ M) (y : β), ((Finsupp.sumFinsuppLEquivProdFinsupp R) f).2 y = f (Sum.inr y)
-- Mathlib.Util.CompileInductive
/-- `compile_def% Foo.foo` adds compiled code for the definition `Foo.foo`.
This can be used for type class projections or definitions like `List._sizeOf_1`,
for which Lean does not generate compiled code by default
(since it is not used 99% of the time).
 -/
Mathlib.Util.«commandCompile_def%_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.Hom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {A B : T.Algebra} →
        (f : A.A ⟶ B.A) →
          autoParam (CategoryTheory.CategoryStruct.comp (T.map f) B.a = CategoryTheory.CategoryStruct.comp A.a f)
              CategoryTheory.Monad.Algebra.Hom.h._autoParam →
            A.Hom B
-- Init.Data.List.Count
List.count_eq_zero_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, a ∉ l → List.count a l = 0
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedRefInfo.kind : WantedRefInfo✝ → WantedRefKind✝
-- Init.Data.Nat.Bitwise.Lemmas
_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.eq_0_of_lt_one : ∀ (x : ℕ), x < 1 ↔ x = 0
-- Mathlib.Topology.Algebra.GroupWithZero
Homeomorph.coe_mulLeft₀ : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : GroupWithZero α] [inst_2 : SeparatelyContinuousMul α] (c : α)
  (hc : c ≠ 0), ⇑(Homeomorph.mulLeft₀ c hc) = fun x => c * x
-- Mathlib.Algebra.Group.WithOne.Map
WithOne.map₂_bot_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithOne α), WithOne.map₂ f a 1 = 1
-- Mathlib.Topology.Order.LiminfLimsup
limsInf_nhds : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] (a : α),
  (nhds a).limsInf = a
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
_private.Mathlib.LinearAlgebra.CliffordAlgebra.Even.0.CliffordAlgebra.even.lift.fst_fFold_fFold : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A] (f : CliffordAlgebra.EvenHom Q A)
  (m₁ m₂ : M) (x : A × ↥(CliffordAlgebra.even.lift.S✝ f)),
  (((CliffordAlgebra.even.lift.fFold✝ f) m₁) (((CliffordAlgebra.even.lift.fFold✝ f) m₂) x)).1 = (f.bilin m₁) m₂ * x.1
-- Mathlib.Order.SupIndep
iSupIndep.injOn_iInf : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {β : ι → Type u_5} (t : (i : ι) → β i → α),
  (∀ (i : ι), iSupIndep (t i)) → Set.InjOn (fun b => ⨅ i, t i (b i)) {b | ⨅ i, t i (b i) ≠ ⊥}
-- Init.Data.Array.Basic
/-- We claim this unsafe implementation is correct because an array cannot have more than `USize.size` elements in our runtime.

This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies `as.size < USize.size` to true.  -/
Array.forIn'Unsafe : {α : Type u} →
  {β : Type v} → {m : Type v → Type w} → [Monad m] → (as : Array α) → β → ((a : α) → a ∈ as → β → m (ForInStep β)) → m β
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.compare_maxKey?_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {km kmm : α} (hkm : t.maxKey? = some km), (t.modify k f).maxKey?.get ⋯ = kmm → cmp kmm km = Ordering.eq
-- Mathlib.Algebra.Order.Archimedean.Class
/-- The `MulArchimedeanClass.subsemigroup` associated to an upper set in
`FiniteMulArchimedeanClass M` is a subgroup.  -/
FiniteMulArchimedeanClass.subgroup : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedMonoid M] → UpperSet (FiniteMulArchimedeanClass M) → Subgroup M
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.LimitOfShape.prop_diag_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C} (self : P.LimitOfShape J X) (j : J), P (self.diag.obj j)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorHom_comp_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) (h : V ⟶ W),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f h)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight g W) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f g) h
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.const.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (declName : Lean.Name) (us : List Lean.Level)
  (args : Array (Lean.Compiler.LCNF.Arg pu))
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.LetValue._auto_3) (declName_1 : Lean.Name)
  (us_1 : List Lean.Level) (args_1 : Array (Lean.Compiler.LCNF.Arg pu))
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.LetValue._auto_3),
  (Lean.Compiler.LCNF.LetValue.const declName us args h =
      Lean.Compiler.LCNF.LetValue.const declName_1 us_1 args_1 h_1) =
    (declName = declName_1 ∧ us = us_1 ∧ args = args_1)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stmts₁.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (a : Turing.Dir) (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.stmts₁ (Turing.TM1.Stmt.move a q) = insert (Turing.TM1.Stmt.move a q) (Turing.TM1.stmts₁ q)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Tries with and without the minimal indexable subexpression condition, if both produce the
same pattern, use the one `minIndexable := false` since it is more compact.
 -/
Lean.Meta.Grind.MinIndexableMode.both : Lean.Meta.Grind.MinIndexableMode
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_le_maxKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {k : α} {v : β k}, (cmp t.maxKey! (t.insert k v).maxKey!).isLE = true
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_add_preimage_subset : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Add α] [inst_1 : Add β] [inst_2 : FunLike F α β]
  [AddHomClass F α β] (m : F) {s t : Set β}, ⇑m ⁻¹' s + ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s + t)
-- Mathlib.Probability.Decision.BayesEstimator
ProbabilityTheory.IsArgminEstimator.measurable : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [inst : StandardBorelSpace Θ]
  [inst_1 : Nonempty Θ] {𝓨 : Type u_4} [inst_2 : MeasurableSpace 𝓨] {ℓ : Θ → 𝓨 → ENNReal}
  {P : ProbabilityTheory.Kernel Θ 𝓧} [inst_3 : ProbabilityTheory.IsFiniteKernel P] {π : MeasureTheory.Measure Θ}
  [inst_4 : MeasureTheory.IsFiniteMeasure π] {f : 𝓧 → 𝓨}, ProbabilityTheory.IsArgminEstimator ℓ P π f → Measurable f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.tan.eq_1 : ∀ (θ : Real.Angle), θ.tan = θ.sin / θ.cos
-- Mathlib.Analysis.Asymptotics.Defs
/-- This version of the Landau notation `IsBigOWith C l f g` where `f` and `g` are two functions on
a type `α` and `l` is a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by `C * ‖g‖`.
In other words, `‖f‖ / ‖g‖` is eventually bounded by `C`, modulo division by zero issues that are
avoided by this definition. Probably you want to use `IsBigO` instead of this relation.  -/
Asymptotics.IsBigOWith : {α : Type u_18} → {E : Type u_19} → {F : Type u_20} → [Norm E] → [Norm F] → ℝ → Filter α → (α → E) → (α → F) → Prop
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.measure_mutuallySingularSetSlice : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (a : α),
  (η a) (κ.mutuallySingularSetSlice η a) = 0
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.prod_eq_top_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] [Nonempty M] [Nonempty N] {s : Subsemigroup M}
  {t : Subsemigroup N}, s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulETransformLeft.fst_mul_snd_subset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Group α] (e : α) (x : Finset α × Finset α),
  (Finset.mulETransformLeft e x).1 * (Finset.mulETransformLeft e x).2 ⊆ x.1 * x.2
-- Lean.Parser.Extension
Lean.Parser.ParserAliasInfo.mk : Lean.Name → Option ℕ → Bool → Lean.Parser.ParserAliasInfo
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.finsupport.eq_1 : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X),
  ρ.finsupport x₀ = ⋯.toFinset
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instMulOneClassOfMulOpposite : {M : Type u_1} → [MulOneClass Mᵐᵒᵖ] → MulOneClass Mᵈᵐᵃ
-- Lean.Server.Rpc.Basic
Lean.Lsp.RpcWireFormat.noConfusionType : Sort v✝ → Lean.Lsp.RpcWireFormat → Lean.Lsp.RpcWireFormat → Sort v✝
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.det_matrixOfPolynomials : ∀ {R : Type v} [inst : CommRing R] {n : ℕ} (p : Fin n → Polynomial R),
  (∀ (i : Fin n), (p i).natDegree = ↑i) → (∀ (i : Fin n), (p i).Monic) → (Matrix.of fun i j => (p j).coeff ↑i).det = 1
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.saveState : Lean.Elab.TermElabM Lean.Elab.Term.SavedState
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.nontrivialTopology : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NontrivialTopology X]
  (h : X ≃ₜ Y), NontrivialTopology Y
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Reify.0.Lean.Meta.Grind.Arith.Linear.reify?.toTopVar : Bool → ℕ → Lean.Expr → Lean.Meta.Grind.Arith.Linear.LinearM (Option Lean.Meta.Grind.Arith.Linear.LinExpr)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addCHaar.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G),
  MeasureTheory.Measure.haar.addCHaar K₀ K = Classical.choose ⋯ K
-- Lean.Data.Json.Parser
Lean.Json.Parser.finishSurrogatePair : UInt16 → Std.Internal.Parsec.String.Parser Char
-- Mathlib.Logic.Encodable.Basic
Encodable.instAntisymmPreimageNatCoeEmbeddingEncode'Le : ∀ {α : Type u_1} [inst : Encodable α], Std.Antisymm (⇑(Encodable.encode' α) ⁻¹'o fun x1 x2 => x1 ≤ x2)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.lt_veblen_invVeblen₁ : ∀ (x : Ordinal.{u_1}), x < Ordinal.veblen x.invVeblen₁ x
-- Mathlib.RingTheory.Artinian.Module
/-- **Alias** of `IsArtinianRing.setOfPred_isPrime_finite`. -/
IsArtinianRing.setOf_isPrime_finite : ∀ (R : Type u_1) [inst : CommRing R] [IsArtinianRing R], {I | I.IsPrime}.Finite
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasDerivWithinAt.rpow_const : ∀ {f : ℝ → ℝ} {f' x p : ℝ} {s : Set ℝ},
  HasDerivWithinAt f f' s x → f x ≠ 0 ∨ 1 ≤ p → HasDerivWithinAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) s x
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.instPartialOrder : {H : Type u} →
  [inst : NormedAddCommGroup H] →
    [inst_1 : InnerProductSpace ℂ H] → [inst_2 : CompleteSpace H] → PartialOrder (VonNeumannAlgebra H)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigOWith.right_le_sub_of_lt_one : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {c : ℝ} {l : Filter α} {f₁ f₂ : α → E'},
  Asymptotics.IsBigOWith c l f₁ f₂ → c < 1 → Asymptotics.IsBigOWith (1 / (1 - c)) l f₂ fun x => f₂ x - f₁ x
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.mem_degrees : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {i : σ},
  i ∈ p.degrees ↔ ∃ d, MvPolynomial.coeff d p ≠ 0 ∧ i ∈ d.support
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.NonlinearRightInverse.mk.injEq : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {f : E →SL[σ] F} (toFun : F → E) (nnnorm : NNReal)
  (bound' : ∀ (y : F), ‖toFun y‖ ≤ ↑nnnorm * ‖y‖) (right_inv' : ∀ (y : F), f (toFun y) = y) (toFun_1 : F → E)
  (nnnorm_1 : NNReal) (bound'_1 : ∀ (y : F), ‖toFun_1 y‖ ≤ ↑nnnorm_1 * ‖y‖)
  (right_inv'_1 : ∀ (y : F), f (toFun_1 y) = y),
  ({ toFun := toFun, nnnorm := nnnorm, bound' := bound', right_inv' := right_inv' } =
      { toFun := toFun_1, nnnorm := nnnorm_1, bound' := bound'_1, right_inv' := right_inv'_1 }) =
    (toFun = toFun_1 ∧ nnnorm = nnnorm_1)
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The composition of the isomorphism `pullbackSpecIso R S T` (from the pullback of
`Spec S ⟶ Spec R` and `Spec T ⟶ Spec R` to `Spec (S ⊗[R] T)`) with the morphism
`Spec (S ⊗[R] T) ⟶ Spec S` obtained by applying `Spec.map` to the ring morphism `s ↦ s ⊗ₜ[R] 1`
is the first projection.
 -/
AlgebraicGeometry.pullbackSpecIso_hom_fst : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).hom
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) =
    CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))
-- Mathlib.GroupTheory.ArchimedeanDensely
WithZero.denselyOrdered_iff : ∀ {M : Type u_3} [inst : Preorder M] [NoMinOrder M], DenselyOrdered (WithZero M) ↔ DenselyOrdered M
-- Mathlib.Data.Multiset.ZeroCons
Multiset.coe_eq_singleton : ∀ {α : Type u_1} {l : List α} {a : α}, ↑l = {a} ↔ l = [a]
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.zero_lt_getElem!_toList_ric_iff : ∀ {n i : ℕ}, 0 < (*...=n).toList[i]! ↔ i ≤ n ∧ 0 < i