mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.swap_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C × D), (CategoryTheory.Prod.swap C D).obj X = (X.2, X.1)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.mk.injEq : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
  (lift : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt)
  (fac :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (j : J),
        CategoryTheory.CategoryStruct.comp (lift s) (t.π.app j) = s.π.app j)
      CategoryTheory.Limits.IsLimit.fac._autoParam)
  (uniq :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (m : s.pt ⟶ t.pt),
        (∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) → m = lift s)
      CategoryTheory.Limits.IsLimit.uniq._autoParam)
  (lift_1 : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt)
  (fac_1 :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (j : J),
        CategoryTheory.CategoryStruct.comp (lift_1 s) (t.π.app j) = s.π.app j)
      CategoryTheory.Limits.IsLimit.fac._autoParam)
  (uniq_1 :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (m : s.pt ⟶ t.pt),
        (∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) → m = lift_1 s)
      CategoryTheory.Limits.IsLimit.uniq._autoParam),
  ({ lift := lift, fac := fac, uniq := uniq } = { lift := lift_1, fac := fac_1, uniq := uniq_1 }) = (lift = lift_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
SSet.Subcomplex.Pairing.instFiniteSubtypeElemNIIAncestralRel : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (y : ↑P.II), Finite { x // P.AncestralRel x y }
-- Mathlib.Data.DFinsupp.Multiset
Multiset.toDFinsupp_replicate : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (n : ℕ), Multiset.toDFinsupp (Multiset.replicate n a) = fun₀ | a => n
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_blockDiagonal' : ∀ {p : Type u_4} {R : Type u_6} [inst : Fintype p] [inst_1 : AddCommMonoid R] [inst_2 : DecidableEq p]
  {m : p → Type u_8} [inst_3 : (i : p) → Fintype (m i)] (M : (i : p) → Matrix (m i) (m i) R),
  (Matrix.blockDiagonal' M).trace = ∑ i, (M i).trace
-- Mathlib.Order.Category.Lat
Lat.ofHom_id : ∀ {X : Type u} [inst : Lattice X], Lat.ofHom (LatticeHom.id X) = CategoryTheory.CategoryStruct.id (Lat.of X)
-- Mathlib.CategoryTheory.Action.Limits
Action.forget_linear : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V] {R : Type u_3} [inst_3 : Semiring R] [inst_4 : CategoryTheory.Linear R V],
  CategoryTheory.Functor.Linear R (Action.forget V G)
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter_containsKey_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)}
  {hl₁ : Std.Internal.List.DistinctKeys l₁} {k : α},
  Std.Internal.List.containsKey k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = true ↔
    Std.Internal.List.containsKey k l₁ = true ∧ Std.Internal.List.containsKey k l₂ = true
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Given a presieve on `X`, and a sieve on each domain of an arrow in the presieve, we can bind to
produce a sieve on `X`.
 -/
CategoryTheory.Sieve.bind : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      (S : CategoryTheory.Presieve X) → (⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Sieve Y) → CategoryTheory.Sieve X
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_monotoneOn : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  MonotoneOn MulArchimedeanClass.mk (Set.Iic 1)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.div_subset_div_left : ∀ {α : Type u_2} [inst : Div α] {s t₁ t₂ : Set α}, t₁ ⊆ t₂ → s / t₁ ⊆ s / t₂
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.Integrable.convergenceR_cond : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
  (h : BoxIntegral.Integrable I l f vol) (ε : ℝ) (c : NNReal), l.RCond (h.convergenceR ε c)
-- Std.Do.PostCond
Std.Do.ExceptConds.imp_intro : ∀ {ps : Std.Do.PostShape} {P Q R : Std.Do.ExceptConds ps}, (P ∧ₑ Q).entails R → P.entails (Q →ₑ R)
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.coe_add : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] (a b : { x // 0 ≤ x }),
  ↑(a + b) = ↑a + ↑b
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.num_scalar : ∀ (u : ℝˣ) (z : UpperHalfPlane), UpperHalfPlane.num ((Matrix.GeneralLinearGroup.scalar (Fin 2)) u) ↑z = ↑↑u * ↑z
-- Init.Data.Nat.Basic
Nat.succ_ne_self : ∀ (n : ℕ), n.succ ≠ n
-- Mathlib.GroupTheory.FinitelyPresentedGroup
Group.isFinitelyPresented_iff : ∀ (G : Type u_5) [inst : Group G],
  Group.IsFinitelyPresented G ↔ ∃ n φ, Function.Surjective ⇑φ ∧ φ.ker.IsFinitelyNormallyGenerated
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.mk.congr_simp : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (toLinearMap toLinearMap_1 : V →ₗ[A] W)
  (e_toLinearMap : toLinearMap = toLinearMap_1) (isIntertwining' : ∀ (g : G), toLinearMap ∘ₗ ρ g = σ g ∘ₗ toLinearMap),
  { toLinearMap := toLinearMap, isIntertwining' := isIntertwining' } =
    { toLinearMap := toLinearMap_1, isIntertwining' := ⋯ }
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.ι'.eq_1 : ∀ {I : Type u} [inst : DecidableEq I] (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)],
  LinearAlgebra.FreeProduct.ι' R A = (LinearAlgebra.FreeProduct.mkAlgHom R A).toLinearMap ∘ₗ TensorAlgebra.ι R
-- Mathlib.Order.Heyting.Basic
fst_hnot : ∀ {α : Type u_2} {β : Type u_3} [inst : HNot α] [inst_1 : HNot β] (a : α × β), (￢a).1 = ￢a.1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.IsCycle₂.eq_1 : ∀ {G : Type u_1} {A : Type u_2} [inst : Mul G] [inst_1 : Inv G] [inst_2 : AddCommGroup A] [inst_3 : SMul G A]
  (x : G × G →₀ A),
  groupHomology.IsCycle₂ x =
    ((x.sum fun g a => (fun₀ | g.2 => g.1⁻¹ • a) + fun₀ | g.1 => a) = x.sum fun g a => fun₀ | g.1 * g.2 => a)
-- Mathlib.CategoryTheory.Limits.Types.End
CategoryTheory.Limits.chosenEnd.π_apply : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))} (j : J)
  (x : CategoryTheory.Limits.Types.end_ F),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.chosenEnd.π F j)) x = ↑x j
-- Mathlib.Algebra.Polynomial.Lifts
Polynomial.exists_natDegree_eq_of_mem_lifts : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial S},
  p ∈ Polynomial.lifts f → ∃ q, Polynomial.map f q = p ∧ q.natDegree = p.natDegree
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_filter_not_contains_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α},
  l₁.isEmpty = true → (List.filter (fun p => !l₂.contains p.fst) l₁).isEmpty = true
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_insertMany_list_le : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {l : List (α × β)}, (Std.DTreeMap.Const.insertMany t l).size ≤ t.size + l.length
-- Mathlib.Topology.UniformSpace.Ultra.Basic
UniformSpace.nhds_basis_clopens : ∀ {X : Type u_1} [inst : UniformSpace X] [IsUltraUniformity X] (x : X),
  (nhds x).HasBasis (fun s => x ∈ s ∧ IsClopen s) id
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.dropInfix?.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (List α) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (s : List α) → motive (some s)),
  (match none with
    | none => h_1 ()
    | some s => h_2 s) =
    h_1 ()
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
_private.Mathlib.Data.Fin.Tuple.NatAntidiagonal.0.List.Nat.antidiagonalTuple.match_1.splitter : (motive : ℕ → ℕ → Sort u_1) →
  (x x_1 : ℕ) → (Unit → motive 0 0) → ((n : ℕ) → motive 0 n.succ) → ((k n : ℕ) → motive k.succ n) → motive x x_1
-- Mathlib.Control.ULift
PLift.instLawfulApplicative_mathlib : LawfulApplicative PLift
-- Init.Data.UInt.Lemmas
UInt64.lt_iff_toFin_lt : ∀ {a b : UInt64}, a < b ↔ a.toFin < b.toFin
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.fst : ∀ {α : Type u_4} {β : Type u_5} [inst : Monoid α] [inst_1 : Monoid β] {x : α × β}, IsOfFinOrder x → IsOfFinOrder x.1
-- Mathlib.RingTheory.Finiteness.Nilpotent
Matrix.isNilpotent_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_3} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  {A : Matrix ι ι R}, IsNilpotent A ↔ ∀ (v : ι → R), ∃ n, (A ^ n).mulVec v = 0
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- [Stacks Tag 00T7](https://stacks.math.columbia.edu/tag/00T7) ((3)) -/
Algebra.SubmersivePresentation.free_cotangent : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ),
  Module.Free S P.toExtension.Cotangent
-- Mathlib.Analysis.Calculus.DerivativeTest
deriv_pos_left_of_sign_deriv : ∀ {f : ℝ → ℝ} {x₀ : ℝ},
  (∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x₀ - x)) →
    ∀ᶠ (b : ℝ) in nhdsWithin x₀ (Set.Iio x₀), deriv f b > 0
-- Mathlib.RingTheory.PowerBasis
/-- `pb.equivOfMinpoly pb' h` is an equivalence of algebras with the same power basis,
where "the same" means that they have identical minimal polynomials.

See also `PowerBasis.equivOfRoot` which takes the hypothesis that each generator is a root of the
other basis' minimal polynomial; `PowerBasis.equivOfRoot` is more general if `A` is not a field.
 -/
PowerBasis.equivOfMinpoly : {S : Type u_2} →
  [inst : Ring S] →
    {A : Type u_4} →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra A S] →
          {S' : Type u_7} →
            [inst_3 : Ring S'] →
              [inst_4 : Algebra A S'] →
                (pb : PowerBasis A S) → (pb' : PowerBasis A S') → minpoly A pb.gen = minpoly A pb'.gen → S ≃ₐ[A] S'
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.forall_dual_apply_eq_zero_iff : ∀ {V : Type uV} [inst : AddCommMonoid V] (R : Type u_1) [inst_1 : Semiring R] [inst_2 : Module R V]
  [Module.Projective R V] (v : V), (∀ (φ : Module.Dual R V), φ v = 0) ↔ v = 0
-- Mathlib.Algebra.Group.Nat.Hom
ext_nat' : ∀ {A : Type u_2} {F : Type u_4} [inst : FunLike F ℕ A] [inst_1 : AddZeroClass A] [AddMonoidHomClass F ℕ A] (f g : F),
  f 1 = g 1 → f = g
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- A class that carries the non-Prop data required to define a left action of a
monoidal category `C` on a category `D`, to set up notations.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.MonoidalCategoryStruct C] → Type (max (max (max u_1 u_2) v_1) v_2)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- `ArchimedeanStrata.stratum` as a submodule of
`ArchimedeanStrata.baseDomain`.  -/
HahnEmbedding.ArchimedeanStrata.stratum' : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      (u : HahnEmbedding.ArchimedeanStrata K M) → FiniteArchimedeanClass M → Submodule K ↥u.baseDomain
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
/-- The sum to be bounded (`ℤ` version).  -/
HurwitzKernelBounds.F_int : ℕ → UnitAddCircle → ℝ → ℝ
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- The uniform bound we have given is summable, and remains so after multiplying by any fixed
power of `|n|` (we shall need this for `k = 0, 1, 2`).  -/
summable_pow_mul_jacobiTheta₂_term_bound : ∀ (S : ℝ) {T : ℝ}, 0 < T → ∀ (k : ℕ), Summable fun n => ↑|n| ^ k * Real.exp (-Real.pi * (T * ↑n ^ 2 - 2 * S * ↑|n|))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.containsThenInsertIfNew_snd : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.containsThenInsertIfNew k v).2 = t.insertIfNew k v
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.ι_ι_assoc : ∀ {n : ℕ} (i j : Fin (n + 2)) (hij : j ≠ i) {Z : SSet} (h : SSet.stdSimplex.obj { len := n + 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.horn.ι i j hij)
      (CategoryTheory.CategoryStruct.comp (SSet.horn (n + 1) i).ι h) =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) h
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.dTo_eq : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι}
  (r : c.Rel i j), C.dTo j = CategoryTheory.CategoryStruct.comp (C.xPrevIso r).hom (C.d i j)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H0_induction_on : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {C : ↑(groupCohomology.H0 A) → Prop}
  (x : ↑(groupCohomology.H0 A)),
  (∀ (x : ↥A.ρ.invariants), C ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H0Iso A).inv) x)) → C x
-- Mathlib.RingTheory.SimpleModule.Isotypic
instNontrivialSubtypeMemSubmoduleValSetIsotypicComponents : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (c : ↑(isotypicComponents R M)), Nontrivial ↥↑c
-- Aesop.RuleTac.RuleTerm
Aesop.RuleTerm.const : Lean.Name → Aesop.RuleTerm
-- Mathlib.NumberTheory.LSeries.Nonvanishing
DirichletCharacter.LFunctionTrivChar_isBigO_near_one_horizontal : ∀ {N : ℕ} [inst : NeZero N],
  (fun x => DirichletCharacter.LFunctionTrivChar N (1 + ↑x)) =O[nhdsWithin 0 (Set.Ioi 0)] fun x => 1 / ↑x
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.convex_range : ∀ {𝕜 : 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)
  [inst_4 : NormedSpace ℝ E], Convex ℝ (Set.range ↑I)
-- Mathlib.MeasureTheory.Group.AEStabilizer
MulAction.aestabilizer.congr_simp : ∀ (G : Type u_1) {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {x : MeasurableSpace α}
  (μ μ_1 : MeasureTheory.Measure α) (e_μ : μ = μ_1) [inst_2 : MeasureTheory.SMulInvariantMeasure G α μ] (s s_1 : Set α),
  s = s_1 → MulAction.aestabilizer G μ s = MulAction.aestabilizer G μ_1 s_1
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the reverse direction of `Equiv.Perm.sameCycle_symm_apply_right`. -/
Equiv.Perm.SameCycle.symm_apply_right : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → f.SameCycle x ((Equiv.symm f) y)
-- Mathlib.Algebra.Group.WithOne.Basic
MulEquiv.withOneCongr.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : Mul β] (e : α ≃* β),
  e.withOneCongr =
    { toFun := ⇑(WithOne.mapMulHom e.toMulHom), invFun := ⇑(WithOne.mapMulHom e.symm.toMulHom), left_inv := ⋯,
      right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_norm_transpose : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] (A : Matrix m n α), ‖A.transpose‖ = ‖A‖
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L] [FiniteDimensional K L]
  {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L]
  [LieModule.IsTriangularizable K (↥H) L] [CharZero K] {α : LieModule.Weight K (↥H) L},
  α.IsNonZero → ∃ h e f, IsSl2Triple h e f ∧ e ∈ LieAlgebra.rootSpace H ⇑α ∧ f ∈ LieAlgebra.rootSpace H (-⇑α)
-- Mathlib.Data.Set.Sups
Set.infs_singleton : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s : Set α} {b : α}, s ⊼ {b} = (fun a => a ⊓ b) '' s
-- Mathlib.Algebra.Category.AlgCat.Limits
/-- The flat sections of a functor into `AlgCat R` form a submodule of all sections.
 -/
AlgCat.sectionsSubalgebra : {R : Type u} →
  [inst : CommRing R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (AlgCat R)) → Subalgebra R ((j : J) → ↑(F.obj j))
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.coe_toMultiplicative_range : ∀ {A : Type u_7} {A' : Type u_8} [inst : AddGroup A] [inst_1 : AddGroup A'] (f : A →+ A'),
  (AddMonoidHom.toMultiplicative f).range = AddSubgroup.toSubgroup f.range
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.lTensor_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} (f : σ.IntertwiningMap τ) (v : V) (w : W),
  (Representation.IntertwiningMap.lTensor ρ f) (v ⊗ₜ[A] w) = v ⊗ₜ[A] f w
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.add.match_3.eq_3 : ∀ (motive : Dyadic → Dyadic → Sort u_1) (n₁ k₁ : ℤ) (hn₁ : n₁ % 2 = 1) (n₂ k₂ : ℤ) (hn₂ : n₂ % 2 = 1)
  (h_1 : (y : Dyadic) → motive Dyadic.zero y) (h_2 : (x : Dyadic) → motive x Dyadic.zero)
  (h_3 :
    (n₁ k₁ : ℤ) →
      (hn₁ : n₁ % 2 = 1) → (n₂ k₂ : ℤ) → (hn₂ : n₂ % 2 = 1) → motive (Dyadic.ofOdd n₁ k₁ hn₁) (Dyadic.ofOdd n₂ k₂ hn₂)),
  (match Dyadic.ofOdd n₁ k₁ hn₁, Dyadic.ofOdd n₂ k₂ hn₂ with
    | Dyadic.zero, y => h_1 y
    | x, Dyadic.zero => h_2 x
    | Dyadic.ofOdd n₁ k₁ hn₁, Dyadic.ofOdd n₂ k₂ hn₂ => h_3 n₁ k₁ hn₁ n₂ k₂ hn₂) =
    h_3 n₁ k₁ hn₁ n₂ k₂ hn₂
-- Init.Data.Option.Lemmas
Option.filter_some_neg : ∀ {α : Type u_1} {p : α → Bool} {a : α}, p a = false → Option.filter p (some a) = none
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_finset_of_infinite : ∀ (α : Type u) [Infinite α], Cardinal.mk (Finset α) = Cardinal.mk α
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.equivOfLe_apply : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {K K' : LieSubalgebra R L} (h : K ≤ K') (x : ↥K), (LieSubalgebra.equivOfLe h) x = ⟨(LieSubalgebra.inclusion h) x, ⋯⟩
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
/-- `liminf (c - xᵢ) = c - limsup xᵢ`.  -/
liminf_const_sub : ∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] (F : Filter ι) [F.NeBot] [inst_4 : AddCommSemigroup R] [inst_5 : Sub R] [ContinuousSub R]
  [OrderedSub R] [AddLeftMono R] (f : ι → R) (c : R),
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F f →
    Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f → Filter.liminf (fun i => c - f i) F = c - Filter.limsup f F
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.findGoalsAt? : Lean.Server.FileWorker.EditableDocument →
  String.Pos.Raw → Lean.Server.ServerTask (Option (List Lean.Elab.GoalsAtResult))
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_lt_nat : ∀ {m : ℕ∞} {n : ℕ}, ↑m < ↑n ↔ m < ↑n
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_bot : ∀ {M : Type u_2} [inst : AddZeroClass M], ⊥.op = ⊥
-- Mathlib.Data.Set.Image
/-- **Alias** of `Set.preimage_sdiff`. -/
Set.preimage_diff : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set β), f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.instAEval : (R : Type u_1) →
  (M : Type u_2) →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module A M] →
                [inst_5 : Module R M] → [inst_6 : IsScalarTower R A M] → (x : A) → Module R (Module.AEval R M x)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.SpecMap_awayMap_awayι_assoc : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A}
  (hx : x = f * g) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj 𝒜 ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx)))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 x ⋯ ⋯) h
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.instSMulCommClassSubtypeMem_1 : ∀ {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [inst : SetLike S α] [inst_1 : SMul M N] [inst_2 : SMul M α]
  [inst_3 : Monoid N] [inst_4 : MulAction N α] [inst_5 : SMulMemClass S N α] [inst_6 : IsScalarTower M N α] (s : S)
  [SMulCommClass M N α], SMulCommClass M N ↥s
-- Mathlib.Order.Hom.Lattice
SupHom.coe_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] [inst_2 : Bot β], ⇑⊥ = ⊥
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.dvdNotUnit_iff_lt : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {a b : Associates M}, DvdNotUnit a b ↔ a < b
-- Mathlib.Algebra.DualNumber
/-- The type of dual numbers, numbers of the form $a + bε$ where $ε^2 = 0$.
`R[ε]` is notation for `DualNumber R`.  -/
DualNumber.«term_[ε]» : Lean.TrailingParserDescr
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.get : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {len : ℕ} → aig.RefVec len → (idx : ℕ) → idx < len → aig.Ref
-- Init.Data.Vector.Attach
Vector.getElem_attach : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n), xs.attach[i] = ⟨xs[i], ⋯⟩
-- Mathlib.Algebra.GroupWithZero.Action.Hom
ZeroHom.instSMulZeroClass : {M : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} → [inst : Zero A] → [inst_1 : Zero B] → [SMulZeroClass M B] → SMulZeroClass M (ZeroHom A B)
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The cocone over the proposed colimit group.  -/
GrpCat.FilteredColimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → (F : CategoryTheory.Functor J GrpCat) → CategoryTheory.Limits.Cocone F
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.homEquivOfIsRightKanExtension_apply_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] (G : CategoryTheory.Functor D H) (β : G ⟶ F') (X : C),
  ((F'.homEquivOfIsRightKanExtension α G) β).app X = CategoryTheory.CategoryStruct.comp (β.app (L.obj X)) (α.app X)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
DifferentiableOn.csinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E},
  DifferentiableOn ℂ f s → DifferentiableOn ℂ (fun x => Complex.sinh (f x)) s