mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (U : TopologicalSpace.Opens ↑X.toTopCat) {Z : CommRingCat}
  (h :
    ((TopCat.Presheaf.pushforward CommRingCat f.base).obj X.presheaf).obj
        (Opposite.op ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).obj U)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f U)
      (CategoryTheory.CategoryStruct.comp
        (f.c.app (Opposite.op ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).obj U))) h) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯)) h
-- Mathlib.Data.Nat.Choose.Bounds
Nat.choose_lt_pow_div : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {n k : ℕ},
  n ≠ 0 → 2 ≤ k → ↑(n.choose k) < ↑n ^ k / ↑k.factorial
-- Mathlib.Order.CompleteLattice.Basic
sInf_sdiff_singleton_top : ∀ {α : Type u_1} [inst : CompleteLattice α] (s : Set α), sInf (s \ {⊤}) = sInf s
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.UniversallyClosed.of_comp_surjective : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.UniversallyClosed (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.Surjective f],
  AlgebraicGeometry.UniversallyClosed g
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- A family of power series converges iff it converges coefficientwise  -/
PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : Semiring R] {ι : Type u_2} (f : ι → PowerSeries R) (u : Filter ι)
  (g : PowerSeries R),
  Filter.Tendsto f u (nhds g) ↔
    ∀ (d : ℕ), Filter.Tendsto (fun i => (PowerSeries.coeff d) (f i)) u (nhds ((PowerSeries.coeff d) g))
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Cfg.mk : {K : Type u_1} →
  {Γ : K → Type u_2} → {Λ : Type u_3} → {σ : Type u_4} → Option Λ → σ → ((k : K) → List (Γ k)) → Turing.TM2.Cfg Γ Λ σ
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.comp_lift_id_right : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {a b c : 𝒳} {S T : 𝒮} (f : S ⟶ T) (φ : a ⟶ b) [p.IsHomLift f φ] (ψ : b ⟶ c)
  [p.IsHomLift (CategoryTheory.CategoryStruct.id T) ψ], p.IsHomLift f (CategoryTheory.CategoryStruct.comp φ ψ)
-- Init.Data.BitVec.Bitblast
BitVec.DivModArgs.mk.sizeOf_spec : ∀ {w : ℕ} (n d : BitVec w), sizeOf { n := n, d := d } = 1 + sizeOf n + sizeOf d
-- Init.WF
WellFounded.Nat.fix_eq : ∀ {α : Sort u} {motive : α → Sort v} (h : α → ℕ)
  (F : (x : α) → ((y : α) → InvImage (fun x1 x2 => x1 < x2) h y x → motive y) → motive x) (x : α),
  WellFounded.Nat.fix h F x = F x fun y x => WellFounded.Nat.fix h F y
-- Mathlib.Data.Part
Part.div_get_eq : ∀ {α : Type u_1} [inst : Div α] (a b : Part α) (hab : (a / b).Dom), (a / b).get hab = a.get ⋯ / b.get ⋯
-- Mathlib.Order.Hom.Bounded
BotHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : Bot β] {f g : BotHom α β}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.instFaithfulGrpForget₂Grp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], (CategoryTheory.CommGrp.forget₂Grp C).Faithful
-- Mathlib.Logic.Equiv.Basic
Equiv.ofFiberEquiv_symm_apply : ∀ {α : Type u_13} {β : Type u_14} {γ : Type u_15} {f : α → γ} {g : β → γ}
  (e : (c : γ) → { a // f a = c } ≃ { b // g b = c }) (a : β),
  (Equiv.ofFiberEquiv e).symm a = ↑((Equiv.sigmaCongrRight e).symm ((Equiv.sigmaFiberEquiv g).symm a)).snd
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.zpow_apply_mem_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {n : ℤ} {x : α},
  (f ^ n) x ∈ f.support ↔ x ∈ f.support
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- If a monoidal functor `F` is an equivalence of categories then its inverse is also monoidal.  -/
CategoryTheory.Equivalence.inverseMonoidal : {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] → (e : C ≌ D) → [e.functor.Monoidal] → e.inverse.Monoidal
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
Std.Sat.CNF.Clause.eval.eq_1 : ∀ {α : Type u_1} (a : α → Bool) (c : Std.Sat.CNF.Clause α),
  Std.Sat.CNF.Clause.eval a c =
    List.any c fun x =>
      match x with
      | (i, n) => a i == n
-- Init.Data.Int.Bitwise.Lemmas
Int.instNeZeroHShiftLeftNat : ∀ {a : ℤ} {n : ℕ} [NeZero a], NeZero (a <<< n)
-- Mathlib.RingTheory.WittVector.Defs
WittVector.pow_coeff : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (m : ℕ) (x : WittVector p R) (n : ℕ),
  (x ^ m).coeff n = WittVector.peval (WittVector.wittPow p m n) ![x.coeff]
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.toTopHom : {α : Type u_6} →
  {β : Type u_7} → [inst : Min α] → [inst_1 : Min β] → [inst_2 : Top α] → [inst_3 : Top β] → InfTopHom α β → TopHom α β
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.snd_map_prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {X : α → β} {Y : α → γ} {μ : MeasureTheory.Measure α},
  Measurable X → (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).snd = MeasureTheory.Measure.map Y μ
-- Init.Data.Array.Lemmas
Array.getD_eq_getD_getElem? : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {d : α}, xs.getD i d = xs[i]?.getD d
-- Mathlib.Topology.Inseparable
/-- Push-forward of the neighborhood of a point along the projection to the separation quotient
is the neighborhood of its equivalence class.  -/
SeparationQuotient.map_mk_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X},
  Filter.map SeparationQuotient.mk (nhds x) = nhds (SeparationQuotient.mk x)
-- Mathlib.GroupTheory.Finiteness
/-- A monoid is finitely generated if it is finitely generated as a submonoid of itself.  -/
Monoid.FG : (M : Type u_1) → [Monoid M] → Prop
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Any common divisor of both elements is a divisor of the GCD.  -/
GCDMonoid.dvd_gcd : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : GCDMonoid α] {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetsExtEntry.global.injEq : ∀ (n n_1 : Lean.Name),
  (Lean.Widget.PanelWidgetsExtEntry.global n = Lean.Widget.PanelWidgetsExtEntry.global n_1) = (n = n_1)
-- Init.Notation
/-- The less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. -/
«term_<_» : Lean.TrailingParserDescr
-- Init.Data.Int.Cooper
/-- Left Cooper resolution of an upper and lower bound with divisibility constraint.
 -/
Int.cooper_resolution_dvd_left : ∀ {a b c d s p q : ℤ},
  0 < a →
    0 < b →
      0 < d →
        ((∃ x, p ≤ a * x ∧ b * x ≤ q ∧ d ∣ c * x + s) ↔
          ∃ k,
            0 ≤ k ∧
              k < ↑(a.lcm (a * d / ↑((a * d).gcd c))) ∧
                b * k + b * p ≤ a * q ∧ a ∣ k + p ∧ a * d ∣ c * k + c * p + a * s)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.notMem_singleton : ∀ {x y : ZFSet.{u}}, x ∉ {y} ↔ x ≠ y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- The proposition that a square
```
  Z ---f---> X
  |          |
  g         inl
  |          |
  v          v
  Y --inr--> P

```
is a pushout square. (Also known as a fiber coproduct or co-Cartesian square.)
 -/
CategoryTheory.IsPushout : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {Z X Y P : C} → (Z ⟶ X) → (Z ⟶ Y) → (X ⟶ P) → (Y ⟶ P) → Prop
-- Batteries.Tactic.Lint.Frontend
Batteries.Tactic.Lint.instDecidableEqLintVerbosity : DecidableEq Batteries.Tactic.Lint.LintVerbosity
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.instHashableTag.hash : Mathlib.CrossRef.Tag → UInt64
-- Mathlib.Topology.Compactness.Compact
isCompact_iff_ultrafilter_le_nhds' : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s ↔ ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ nhds x
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.zeros_append_toFun : ∀ {m : Tactic.ComputeAsymptotics.UnitMonomial} {left right : Tactic.ComputeAsymptotics.Basis},
  (List.replicate (List.length left) 0 ++ m).toFun (left ++ right) = m.toFun right
-- Mathlib.Logic.IsEmpty.Defs
/-- Eliminate out of a type that `IsEmpty` (without using projection notation).  -/
isEmptyElim : {α : Sort u} → [IsEmpty α] → {p : α → Sort v} → (a : α) → p a
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.restrictScalars_lift : ∀ {R : Type uR} {R' : Type u_1} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra S C] [inst_11 : Algebra R C] [inst_12 : IsScalarTower R S C] [inst_13 : CommSemiring R']
  [inst_14 : Algebra R R'] [inst_15 : Algebra R' S] [inst_16 : Algebra R' A] [inst_17 : IsScalarTower R R' A]
  [inst_18 : IsScalarTower R' S A] [inst_19 : Algebra R' C] [inst_20 : IsScalarTower R R' C]
  [inst_21 : IsScalarTower R' S C] (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ (x : A) (y : B), Commute (f x) (g y)),
  AlgHom.restrictScalars R' (Algebra.TensorProduct.lift f g hfg) =
    Algebra.TensorProduct.lift (AlgHom.restrictScalars R' f) g hfg
-- Mathlib.Combinatorics.Quiver.Path.Weight
_private.Mathlib.Combinatorics.Quiver.Path.Weight.0.Quiver.Path.weight.match_1.eq_2 : ∀ {V : Type u_2} [inst : Quiver V] (motive : (x x_1 : V) → Quiver.Path x x_1 → Sort u_3) (a x b : V)
  (p : Quiver.Path a b) (e : b ⟶ x) (h_1 : (a : V) → motive a a Quiver.Path.nil)
  (h_2 : (a x b : V) → (p : Quiver.Path a b) → (e : b ⟶ x) → motive a x (p.cons e)),
  (match a, x, p.cons e with
    | a, .(a), Quiver.Path.nil => h_1 a
    | a, x, p.cons e => h_2 a x b p e) =
    h_2 a x b p e
-- Mathlib.RingTheory.Idempotents
Subsemigroup.corner.eq_1 : ∀ {R : Type u_1} (e : R) [inst : Semigroup R],
  Subsemigroup.corner e = { carrier := Set.range fun x => e * x * e, mul_mem' := ⋯ }
-- Mathlib.Data.Finset.Card
Multiset.toFinset_card_eq_card_iff_nodup : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α}, m.toFinset.card = m.card ↔ m.Nodup
-- Mathlib.Topology.Separation.Basic
t1Space_iff_disjoint_pure_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X], T1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (nhds y)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_swap : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') (v : ι → M)
  [inst_5 : DecidableEq ι] {i j : ι}, i ≠ j → g (v ∘ ⇑(Equiv.swap i j)) = -g v
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- The volume form is invariant under pullback by a positively-oriented isometric automorphism.  -/
Orientation.volumeForm_comp_linearIsometryEquiv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) (φ : E ≃ₗᵢ[ℝ] E),
  0 < LinearMap.det ↑φ.toLinearEquiv → ∀ (x : Fin n → E), o.volumeForm (⇑φ ∘ x) = o.volumeForm x
-- Mathlib.Order.Interval.Set.Infinite
Set.Icc.infinite : ∀ {α : Type u_1} [inst : Preorder α] [DenselyOrdered α] {a b : α}, a < b → Infinite ↑(Set.Icc a b)
-- Std.Http.Data.Method
Std.Http.Method.acl.sizeOf_spec : sizeOf Std.Http.Method.acl = 1
-- Mathlib.Analysis.CStarAlgebra.Classes
/-- The class of non-unital commutative (complex) C⋆-algebras.  -/
NonUnitalCommCStarAlgebra : Type u_1 → Type u_1
-- Std.Sync.Broadcast
/-- A receiver for a `Broadcast` channel that can asynchronously receive messages.
Each receiver gets a copy of every message sent to the broadcast channel after
the receiver was created. Multiple receivers can exist for the same broadcast,
and each will receive all messages independently.
 -/
Std.Broadcast.Receiver : Type → Type
-- Mathlib.MeasureTheory.Integral.Prod
/-- The Bochner integral is measurable. This shows that the integrand of (the right-hand-side of)
the symmetric version of Fubini's theorem is measurable.
This version has `f` in curried form.  -/
MeasureTheory.StronglyMeasurable.integral_prod_left : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [MeasureTheory.SFinite μ]
  ⦃f : α → β → E⦄,
  MeasureTheory.StronglyMeasurable (Function.uncurry f) → MeasureTheory.StronglyMeasurable fun y => ∫ (x : α), f x y ∂μ
-- Mathlib.Data.Finset.Card
Finset.card_sub_card_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), t.card - s.card = (t \ s).card - (s \ t).card
-- Mathlib.Tactic.Peel
/-- Peel off a single quantifier from an `↔`.  -/
Mathlib.Tactic.Peel.peelIffAux : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.RingTheory.FiniteType
/-- An algebra morphism `A →ₐ[R] B` is of `FiniteType` if it is of finite type as ring morphism.
In other words, if `B` is finitely generated as `A`-algebra.  -/
AlgHom.FiniteType : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → Prop
-- Mathlib.Algebra.Group.Action.Defs
instIsCancelSMul : ∀ (G : Type u_9) [inst : CancelMonoid G], IsCancelSMul G G
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- This lemma is superseded by `MeasureTheory.MemLp.eLpNorm_indicator_le` which does not require
measurability on `f`.  -/
MeasureTheory.MemLp.eLpNorm_indicator_le_of_meas : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal} {f : α → β},
  1 ≤ p →
    p ≠ ⊤ →
      MeasureTheory.MemLp f p μ →
        MeasureTheory.StronglyMeasurable f →
          ∀ {ε : ℝ},
            0 < ε →
              ∃ δ,
                ∃ (_ : 0 < δ),
                  ∀ (s : Set α),
                    MeasurableSet s →
                      μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instNonUnitalSemiring : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [NonUnitalSemiring β] → NonUnitalSemiring (MeasureTheory.SimpleFunc α β)
-- Batteries.Data.List.Lemmas
List.length_swap : ∀ {α : Type u_1} {i j : ℕ} {xs : List α}, (xs.swap i j).length = xs.length
-- Mathlib.Geometry.Euclidean.Angle.Bisector
/-- A point `p` is equidistant to two affine subspaces (typically lines, for this version of the
lemma) if and only if the oriented angles at a point `p'` in their intersection between `p` and
its orthogonal projections onto the subspaces are equal.  -/
EuclideanGeometry.dist_orthogonalProjection_eq_iff_oangle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [inst_4 : Fact (Module.finrank ℝ V = 2)] [inst_5 : Module.Oriented ℝ V (Fin 2)]
  {p p' : P} {s₁ s₂ : AffineSubspace ℝ P} (hp'₁ : p' ∈ s₁) (hp'₂ : p' ∈ s₂),
  ↑((EuclideanGeometry.orthogonalProjection s₁) p) ≠ ↑((EuclideanGeometry.orthogonalProjection s₂) p) →
    ↑((EuclideanGeometry.orthogonalProjection s₁) p) ≠ p' →
      ↑((EuclideanGeometry.orthogonalProjection s₂) p) ≠ p' →
        (dist p ↑((EuclideanGeometry.orthogonalProjection s₁) p) =
            dist p ↑((EuclideanGeometry.orthogonalProjection s₂) p) ↔
          EuclideanGeometry.oangle (↑((EuclideanGeometry.orthogonalProjection s₁) p)) p' p =
            EuclideanGeometry.oangle p p' ↑((EuclideanGeometry.orthogonalProjection s₂) p))
-- Mathlib.Data.Sum.Order
Sum.inl_le_inl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a b : α}, Sum.inl a ≤ Sum.inl b ↔ a ≤ b
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.prodMk : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Y' : Type u_5} {f : X → Y} {f' : X → Y'},
  IsLocallyConstant f → IsLocallyConstant f' → IsLocallyConstant fun x => (f x, f' x)
-- Init.Data.Bool
Bool.instMin : Min Bool
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] (M : Type u_3) [inst_4 : AddCommGroup M]
  [inst_5 : Module R M] [inst_6 : LieRingModule L M] [inst_7 : LieModule R L M] (α χ : ↥H → R) {x : L},
  x ∈ LieAlgebra.rootSpace H α →
    Set.MapsTo ⇑((LieModule.toEnd R L M) x) ↑(LieModule.genWeightSpace M χ) ↑(LieModule.genWeightSpace M (α + χ))
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.fillHolesFromWhereFinally : Lean.Name →
  Array Lean.Elab.Term.ExprWithHoles✝ →
    Lean.Elab.WhereFinallyView → Array Lean.Elab.Attribute → Lean.Elab.TermElabM PUnit.{1}
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey!_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ [inst_4 : Inhabited α] {k : α} {f : β → β},
      (Std.DHashMap.Internal.Raw₀.Const.modify m k f).getKey! k = if m.contains k = true then k else default
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.erase₀ : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size} {a : α}
  (a_1 : m.WF), Std.DHashMap.Raw.WF.below a_1 → motive m a_1 → Std.DHashMap.Raw.WF.below ⋯
-- Mathlib.Geometry.Euclidean.Volume.Measure
/-- The $n$-dimensional volume of an object in an $n$-dimensional space is equal to the integral
of the volume of $(n-d)$-dimensional cross-section along an orthogonal $d$-dimensional subspace.
This is an analogue to `MeasureTheory.Measure.prod_apply`.  -/
AffineSubspace.euclideanHausdorffMeasure_eq_lintegral : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [inst_5 : MetricSpace P]
  [inst_6 : MeasurableSpace P] [inst_7 : BorelSpace P] [inst_8 : NormedAddTorsor V P] (s : AffineSubspace ℝ P)
  [hs : Nonempty ↥s] {t : Set P},
  MeasurableSet t →
    (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V)) t =
      ∫⁻ (x : ↥s),
        (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ ↥s.directionᗮ))
          (t ∩
            ↑(AffineSubspace.mk' (↑x)
                s.directionᗮ)) ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ ↥s.direction)
-- Init.Data.SInt.Bitwise
instAssociativeInt64HAnd : Std.Associative fun x1 x2 => x1 &&& x2
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.map_add_right_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant]
  (g : G), MeasureTheory.Measure.map (fun x => x + g) μ = μ
-- Mathlib.Topology.Constructions
Continuous.quotient_lift : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Setoid X} {f : X → Y},
  Continuous f → ∀ (hs : ∀ (a b : X), a ≈ b → f a = f b), Continuous (Quotient.lift f hs)
-- Mathlib.Topology.Order.Lattice
Filter.Tendsto.finset_inf'_nhds_apply : ∀ {L : Type u_1} [inst : TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ι → α → L} {l : Filter α}
  {g : ι → L} [inst_1 : SemilatticeInf L] [ContinuousInf L] (hne : s.Nonempty),
  (∀ i ∈ s, Filter.Tendsto (f i) l (nhds (g i))) →
    Filter.Tendsto (fun a => s.inf' hne fun x => f x a) l (nhds (s.inf' hne g))
-- Mathlib.Analysis.Normed.Module.Ball.Action
continuousSMul_sphere_sphere : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {r : ℝ}, ContinuousSMul ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformity_basis_dist_inv_nat_succ : ∀ {α : Type u} [inst : PseudoMetricSpace α],
  (uniformity α).HasBasis (fun x => True) fun n => {p | dist p.1 p.2 < 1 / (↑n + 1)}
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.ne_top_iff : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] [Nontrivial Γ₀]
  (v : AddValuation K Γ₀) {x : K}, v x ≠ ⊤ ↔ x ≠ 0
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsIntegral.trans_isAlgebraic : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S]
  [Algebra.IsIntegral R S] [alg : Algebra.IsAlgebraic S A], Algebra.IsAlgebraic R A
-- Mathlib.Tactic.Push
/-- `#push_discr_tree X` shows the discrimination tree of all lemmas used by `push X`.
This can be helpful when you are constructing a set of `push` lemmas for the constant `X`.
 -/
Mathlib.Tactic.Push.pushTree : Lean.ParserDescr
-- Init.Data.Iterators.Combinators.Monadic.ULift
Std.Iterators.instMonadULiftT : {n : Type (max u v) → Type v'} → [Monad n] → Monad (Std.Iterators.ULiftT n)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.contMDiffOn_comp_diffeomorph_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {G : Type u_7} [inst_9 : TopologicalSpace G]
  {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9}
  [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H M] {M' : Type u_10} [inst_12 : TopologicalSpace M']
  [inst_13 : ChartedSpace H' M'] {N : Type u_11} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n m : WithTop ℕ∞} (h : Diffeomorph I J M N n) {f : N → M'} {s : Set M},
  m ≤ n → (ContMDiffOn I I' m (f ∘ ⇑h) s ↔ ContMDiffOn J I' m f (⇑h.symm ⁻¹' s))
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.Limits.mapPair.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C}
  (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.left })
  (g :
    F.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.right }),
  CategoryTheory.Limits.mapPair f g =
    {
      app := fun x =>
        match x with
        | { as := CategoryTheory.Limits.WalkingPair.left } => f
        | { as := CategoryTheory.Limits.WalkingPair.right } => g,
      naturality := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
/-- The regularized hypergeometric function `₀F₀` is the complex exponential.  -/
Complex.regularizedHGFun_zero_zero : Complex.regularizedHGFun 0 0 = Complex.exp
-- Mathlib.Probability.Kernel.Defs
/-- A kernel is finite if every measure in its image is finite, with a uniform bound.  -/
ProbabilityTheory.IsFiniteKernel : {α : Type u_1} →
  {β : Type u_2} → {mα : MeasurableSpace α} → {mβ : MeasurableSpace β} → ProbabilityTheory.Kernel α β → Prop