mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_1.eq_2 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      (b : Bool) → motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b)))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  (match Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty with
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) => h_3 l b
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) =
    h_2 ()
-- Mathlib.Data.Int.Bitwise
_private.Mathlib.Data.Int.Bitwise.0.Int.testBit.match_1.eq_1 : ∀ (motive : ℤ → ℕ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) n)
  (h_2 : (m n : ℕ) → motive (Int.negSucc m) n),
  (match Int.ofNat m, n with
    | Int.ofNat m, n => h_1 m n
    | Int.negSucc m, n => h_2 m n) =
    h_1 m n
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- Reverse version of `point_vsub_centroid_eq_smul_vsub`.  -/
Affine.Simplex.centroid_vsub_point_eq_smul_vsub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.centroid -ᵥ s.points i = ↑n • (s.faceOppositeCentroid i -ᵥ s.centroid)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {f : α → β → Option γ} {k : α},
  (Std.ExtHashMap.filterMap f m).getKey! k = ((m.getKey? k).pfilter fun x_2 h' => (f x_2 m[x_2]).isSome).get!
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
CFC.one_le_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  (a : A), autoParam (p a) CFC.one_le_iff._auto_1 → (1 ≤ a ↔ ∀ x ∈ spectrum R a, 1 ≤ x)
-- Init.Data.AC
Lean.Data.AC.Context.toList_nonEmpty : ∀ (e : Lean.Data.AC.Expr), e.toList ≠ []
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.eqFunDecl : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.FunDecl pu → Lean.Compiler.LCNF.FunDecl pu → Bool
-- Aesop.Stats.Basic
Aesop.instMonadStatsStateRefT' : {m : Type → Type} → {ω σ : Type} → [Aesop.MonadStats m] → Aesop.MonadStats (StateRefT' ω σ m)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instOneOfMulOpposite : {M : Type u_1} → [One Mᵐᵒᵖ] → One Mᵈᵐᵃ
-- Mathlib.RingTheory.AdicCompletion.Basic
IsPrecomplete.bot : ∀ {R : Type u_1} [inst : CommRing R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M], IsPrecomplete ⊥ M
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.pow_eq_one_iff' : ∀ {β : Type u_3} [Finite β] {f : Equiv.Perm β}, f.IsCycle → ∀ {n : ℕ} {x : β}, f x ≠ x → (f ^ n = 1 ↔ (f ^ n) x = x)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.IsOver.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [inst : X.Over S] [inst_1 : Y.Over S]
  (f : X.PartialMap Y), AlgebraicGeometry.Scheme.PartialMap.IsOver S f = AlgebraicGeometry.Scheme.Hom.IsOver f.hom S
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- Given two morphisms of complexes `φ₁ φ₂ : F ⟶ G`, the datum of a homotopy between `φ₁` and
`φ₂` is equivalent to the datum of a `1`-cochain `z` such that `δ (-1) 0 z` is the difference
of the zero cochains associated to `φ₂` and `φ₁`.  -/
CochainComplex.HomComplex.Cochain.equivHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ₁ φ₂ : F ⟶ G) →
          Homotopy φ₁ φ₂ ≃
            { z //
              CochainComplex.HomComplex.Cochain.ofHom φ₁ =
                CochainComplex.HomComplex.δ (-1) 0 z + CochainComplex.HomComplex.Cochain.ofHom φ₂ }
-- Init.Omega.IntList
/-- Implementation of negation on `IntList`.  -/
Lean.Omega.IntList.neg : Lean.Omega.IntList → Lean.Omega.IntList
-- Init.Data.List.Find
List.getLast_filter : ∀ {α : Type u_1} {p : α → Bool} {l : List α} (h : List.filter p l ≠ []),
  (List.filter p l).getLast h = (List.find? p l.reverse).get ⋯
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsKolmogorovProcess.q_pos : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {X : T → Ω → E} {P : MeasureTheory.Measure Ω} {p q : ℝ} {M : NNReal},
  ProbabilityTheory.IsKolmogorovProcess X P p q M → 0 < q
-- Mathlib.Data.Set.Lattice
Set.sInter_eq_biInter : ∀ {α : Type u_1} {s : Set (Set α)}, ⋂₀ s = ⋂ i ∈ s, i
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
Antitone.const_mul_of_nonpos : ∀ {R : Type u} {α : Type u_1} [inst : Semiring R] [inst_1 : Preorder R] {a : R} [inst_2 : Preorder α] {f : α → R}
  [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R],
  Antitone f → a ≤ 0 → Monotone fun x => a * f x
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_lt_ediv_of_lt_of_neg : ∀ {a b c : ℤ}, b < a → c ∣ a → c < 0 → a / c < b / c
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.setLIntegral_rnDeriv_le : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] {κ η : ProbabilityTheory.Kernel α γ}
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {a : α} {s : Set γ},
  MeasurableSet s → ∫⁻ (c : γ) in s, κ.rnDeriv η a c ∂η a ≤ (κ a) s
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, panicking if the map is
empty.
 -/
Std.DTreeMap.Raw.minEntry! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited ((a : α) × β a)] → Std.DTreeMap.Raw α β cmp → (a : α) × β a
-- Mathlib.Analysis.Meromorphic.Basic
/-- If `f` is meromorphic at `x`, then `f + g` is meromorphic at `x` if and only if `g` is meromorphic
at `x`.
 -/
MeromorphicAt.meromorphicAt_add_iff_meromorphicAt₁ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E}, MeromorphicAt f x → (MeromorphicAt (f + g) x ↔ MeromorphicAt g x)
-- Std.Http.Data.Body.Any
Std.Http.Body.Any.mk : Std.Async.Async (Option Std.Http.Chunk) →
  Std.Async.Async Unit →
    Std.Async.Async Bool →
      Std.Async.Selector (Option Std.Http.Chunk) →
        Std.Async.Async (Option (Option Std.Http.Chunk)) →
          Std.Async.Async (Option Std.Http.Body.Length) →
            (Option Std.Http.Body.Length → Std.Async.Async Unit) → Std.Http.Body.Any
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.prun_bind : ∀ {m : Type w → Type w'} {α : Type u} {β : Type v} {γ : Type w} [inst : Monad m] [LawfulMonad m]
  {x : Std.Iterators.HetT m α} {f : α → Std.Iterators.HetT m β} {g : (b : β) → (x.bind f).Property b → m γ},
  (x.bind f).prun g = x.prun fun a ha => (f a).prun fun b hb => g b ⋯
-- Init.Data.SInt.Lemmas
ISize.sub_left_inj : ∀ {a b : ISize} (c : ISize), a - c = b - c ↔ a = b
-- Mathlib.Order.Partition.Equipartition
/-- Given a finset equipartitioned into `k` parts, its elements can be enumerated such that
elements in the same part have congruent indices modulo `k`.  -/
Finpartition.IsEquipartition.exists_partPreservingEquiv : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {P : Finpartition s},
  P.IsEquipartition → ∃ f, ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ ↑(f a) % P.parts.card = ↑(f b) % P.parts.card
-- Mathlib.Data.Nat.Init
/-- Decreasing induction: if `P (k+1)` implies `P k` for all `k < n`, then `P n` implies `P m` for
all `m ≤ n`.
Also works for functions to `Sort*`.

For a version also assuming `m ≤ k`, see `Nat.decreasingInduction'`.  -/
Nat.decreasingInduction : {n : ℕ} →
  {motive : (m : ℕ) → m ≤ n → Sort u_1} →
    ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → {m : ℕ} → (mn : m ≤ n) → motive m mn
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- When the second map `S.g` is zero, this is the homology data on `S` given
by any colimit cokernel cofork of `S.f`  -/
CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        S.g = 0 → (c : CategoryTheory.Limits.CokernelCofork S.f) → CategoryTheory.Limits.IsColimit c → S.HomologyData
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.functorialityCompFunctoriality.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₅, u₅} E] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D)
  (H : CategoryTheory.Functor D E),
  CategoryTheory.Limits.Cone.functorialityCompFunctoriality F G H =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          (((CategoryTheory.Limits.Cone.functoriality F G).comp
                (CategoryTheory.Limits.Cone.functoriality (F.comp G) H)).obj
            x))
      ⋯
-- Lean.Server.CodeActions.Provider
Lean.CodeAction.FindTacticResult.tacticSeq.inj : ∀ {preferred : Bool} {insertIdx : ℕ} {a : Lean.Syntax.Stack} {preferred_1 : Bool} {insertIdx_1 : ℕ}
  {a_1 : Lean.Syntax.Stack},
  Lean.CodeAction.FindTacticResult.tacticSeq preferred insertIdx a =
      Lean.CodeAction.FindTacticResult.tacticSeq preferred_1 insertIdx_1 a_1 →
    preferred = preferred_1 ∧ insertIdx = insertIdx_1 ∧ a = a_1
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.copy_eq : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) (F : Set X) (hF : F = ↑E)
  (J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (hJ : J = E.I), E.copy F hF J hJ = E
-- ImportGraph.Tools.FindHome
GoToModuleLinkProps.modName : GoToModuleLinkProps → Lean.Name
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map : ∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → β}
  {g : Ω → β'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [MeasureTheory.IsFiniteMeasure μ],
  AEMeasurable f μ →
    AEMeasurable g μ →
      (ProbabilityTheory.IndepFun f g μ ↔
        MeasureTheory.Measure.map (fun ω => (f ω, g ω)) μ =
          (MeasureTheory.Measure.map f μ).prod (MeasureTheory.Measure.map g μ))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_insertManyIfNewUnit!_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α],
  t.WF →
    ∀ {l : List α}, (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.Adjunction.isContinuous_of_isCocontinuous : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) [F.IsCocontinuous J K], G.IsContinuous K J
-- Mathlib.Algebra.BigOperators.Expect
Fintype.expect_one : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : Semiring M] [inst_2 : Module ℚ≥0 M] [Nonempty ι],
  (Finset.univ.expect fun _i => 1) = 1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.Walk.setOfPred_length_eq_add_one : ∀ {V : Type u} (G : SimpleGraph V) (u v : V) (n : ℕ),
  {p | p.length = n + 1} = ⋃ w, ⋃ (h : G.Adj u w), SimpleGraph.Walk.cons h '' {p' | p'.length = n}
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.ElementarilyEquivalent.nonempty_iff : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.ElementarilyEquivalent M N → (Nonempty M ↔ Nonempty N)
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
/-- rank-nullity theorem : the dimensions of the kernel and the range of a linear map add up to
the dimension of the source space.  -/
LinearMap.finrank_range_add_finrank_ker : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [FiniteDimensional K V] (f : V →ₗ[K] V₂),
  Module.finrank K ↥f.range + Module.finrank K ↥f.ker = Module.finrank K V
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.conj_id : ∀ {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [inst : CommSemiring R₁']
  [inst_1 : CommSemiring R₂'] [inst_2 : AddCommMonoid M₁'] [inst_3 : AddCommMonoid M₂'] [inst_4 : Module R₁' M₁']
  [inst_5 : Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [inst_6 : RingHomInvPair σ₁'₂' σ₂'₁']
  [inst_7 : RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] M₂'), e.conj LinearMap.id = LinearMap.id
-- Mathlib.MeasureTheory.Group.Arithmetic
measurable_const_vadd_iff : ∀ {β : Type u_5} {α : Type u_6} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace α] {f : α → β} {G : Type u_7}
  [inst_2 : AddGroup G] [inst_3 : AddAction G β] [MeasurableConstVAdd G β] (c : G),
  (Measurable fun x => c +ᵥ f x) ↔ Measurable f
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.limitAddCommMonoid : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) →
          [inst_2 : Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] →
            AddCommMonoid
              (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (ModuleCat R)))).pt
-- Lean.Compiler.IR.CompilerM
Lean.IR.Log.format : Lean.IR.Log → Std.Format
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_2 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] (X Y : C)
  [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m m' n : M),
  CategoryTheory.Localization.HasSmallLocalizedHom W
    ((CategoryTheory.shiftFunctor C m').obj ((CategoryTheory.shiftFunctor C m).obj X))
    ((CategoryTheory.shiftFunctor C n).obj Y)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.const_add_eq_map : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Add β] (f : MeasureTheory.SimpleFunc α β) (b : β),
  MeasureTheory.SimpleFunc.const α b + f = MeasureTheory.SimpleFunc.map (fun a => b + a) f
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_add : ∀ {R : Type u_1} [inst : Semiring R] (x y : R) (p q : Polynomial (Polynomial R)),
  Polynomial.evalEval x y (p + q) = Polynomial.evalEval x y p + Polynomial.evalEval x y q
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ext₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cochain F G 0),
  (∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯) → z₁ = z₂
-- Lean.Server.Utils
Lean.Server.mkApplyWorkspaceEditRequest : Lean.Lsp.ApplyWorkspaceEditParams → Lean.JsonRpc.Request Lean.Lsp.ApplyWorkspaceEditParams
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.eigenvectorUnitary_transpose_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian) (j : n), (↑hA.eigenvectorUnitary).transpose j = (hA.eigenvectorBasis j).ofLp
-- Mathlib.Data.List.Basic
List.map_bijective_iff : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Bijective (List.map f) ↔ Function.Bijective f
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
CategoryTheory.Limits.HasWeakKernels.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  autoParam (∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasWeakKernel f)
      CategoryTheory.Limits.HasWeakKernels.hasWeakLimit._autoParam →
    CategoryTheory.Limits.HasWeakKernels C
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.inter_cylinder : ∀ {ι : Type u_1} {α : ι → Type u_2} (s₁ s₂ : Finset ι) (S₁ : Set ((i : ↥s₁) → α ↑i)) (S₂ : Set ((i : ↥s₂) → α ↑i))
  [inst : DecidableEq ι],
  MeasureTheory.cylinder s₁ S₁ ∩ MeasureTheory.cylinder s₂ S₂ =
    MeasureTheory.cylinder (s₁ ∪ s₂) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ Finset.restrict₂ ⋯ ⁻¹' S₂)
-- Mathlib.Topology.ContinuousMap.LocallyConvex
ContinuousMap.instLocallyConvexSpace : ∀ {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : TopologicalSpace X] [inst_1 : Semiring 𝕜]
  [inst_2 : PartialOrder 𝕜] [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : TopologicalSpace E]
  [LocallyConvexSpace 𝕜 E] [inst_7 : IsTopologicalAddGroup E] [inst_8 : ContinuousConstSMul 𝕜 E],
  LocallyConvexSpace 𝕜 C(X, E)
-- Mathlib.MeasureTheory.Measure.Complex
MeasureTheory.SignedMeasure.re_toComplexMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} (s t : MeasureTheory.SignedMeasure α),
  MeasureTheory.ComplexMeasure.re (s.toComplexMeasure t) = s
-- Init.Data.List.BasicAux
List.sizeOf_get : ∀ {α : Type u_1} [inst : SizeOf α] (as : List α) (i : Fin as.length), sizeOf (as.get i) < sizeOf as
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_injective : ∀ {R : Type u_1} (n : ℕ) [inst : Semiring R], Function.Injective ⇑(SkewPolynomial.monomial n)
-- Mathlib.Data.NNRat.Defs
Rat.le_toNNRat_iff_coe_le : ∀ {p : ℚ} {q : ℚ≥0}, 0 ≤ p → (q ≤ p.toNNRat ↔ ↑q ≤ p)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `TensorProduct.leftComm`  -/
TensorProduct.AlgebraTensorModule.leftComm : (R : Type uR) →
  (A : Type uA) →
    (M : Type uM) →
      (P : Type uP) →
        (Q : Type uQ) →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring A] →
              [inst_2 : Algebra R A] →
                [inst_3 : AddCommMonoid M] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module A M] →
                      [inst_6 : IsScalarTower R A M] →
                        [inst_7 : AddCommMonoid P] →
                          [inst_8 : Module A P] →
                            [inst_9 : AddCommMonoid Q] →
                              [inst_10 : Module R Q] →
                                [inst_11 : Module R P] →
                                  [inst_12 : IsScalarTower R A P] →
                                    TensorProduct A M (TensorProduct R P Q) ≃ₗ[A]
                                      TensorProduct A P (TensorProduct R M Q)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.sPolynomial_self : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f : MvPolynomial σ R), m.sPolynomial f f = 0
-- Mathlib.Topology.Instances.AddCircle.Real
ZMod.toAddCircle_natCast : ∀ {N : ℕ} [inst : NeZero N] (j : ℕ), ZMod.toAddCircle ↑j = ↑(↑j / ↑N)
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- Given generators `R[xᵢ] → S` and an injective map `σ → ι`, this is the
composition `I/I² → ⊕ S dxᵢ → ⊕ S dxᵢ` where the second `i` only runs over `σ`.  -/
Algebra.Generators.cotangentRestrict : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type w} →
            (P : Algebra.Generators R S ι) →
              {σ : Type u_1} → {u : σ → ι} → Function.Injective u → P.toExtension.Cotangent →ₗ[S] σ →₀ S
-- Init.Data.Slice.Array.Lemmas
Subarray.getElem_eq_getElem_toList : ∀ {α : Type u_1} {i : ℕ} {xs : Subarray α} {h : i < Std.Slice.size xs}, xs[i] = (Std.Slice.toList xs)[i]
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.instZPow.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : MulOneClass M] [inst_1 : CommGroup N],
  MonoidHom.instZPow = { pow := fun f n => { toFun := ⇑f ^ n, map_one' := ⋯, map_mul' := ⋯ } }
-- Lean.Meta.Tactic.LibrarySearch
/-- Sequentially invokes a tactic `act` on each value in candidates on the current state.

The tactic `act` should return a list of meta-variables that still need to be resolved.
If this list is empty, then no variables remain to be solved, and `tryOnEach` returns
`none` with the environment set so each goal is resolved (unless `collectAll` is true,
in which case it continues searching and collects complete solutions in the array).

If the action throws an internal exception with the `abortSpeculationId` id then
further computation is stopped and intermediate results returned. If any other
exception is thrown, then it is silently discarded.
 -/
Lean.Meta.LibrarySearch.tryOnEach : (Lean.Meta.LibrarySearch.Candidate → Lean.MetaM (List Lean.MVarId)) →
  Array Lean.Meta.LibrarySearch.Candidate →
    optParam Bool false → Lean.MetaM (Option (Array (List Lean.MVarId × Lean.MetavarContext)))
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (x : ↑(X.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app hU.fromSpec U)) x =
    (CategoryTheory.ConcreteCategory.hom
        ((AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).presheaf.map (CategoryTheory.eqToHom ⋯)))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv) x)
-- Mathlib.MeasureTheory.Integral.Layercake
/-- The layer cake formula / **Cavalieri's principle** / tail probability formula:

Let `f` be a non-negative measurable function on a measure space. Let `G` be an
increasing absolutely continuous function on the positive real line, vanishing at the origin,
with derivative `G' = g`. Then the integral of the composition `G ∘ f` can be written as
the integral over the positive real line of the "tail measures" `μ {ω | f(ω) ≥ t}` of `f`
weighted by `g`.

Roughly speaking, the statement is: `∫⁻ (G ∘ f) ∂μ = ∫⁻ t in 0..∞, g(t) * μ {ω | f(ω) ≥ t}`.

See `MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul` for a version with sets of the form
`{ω | f(ω) > t}` instead.  -/
MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : MeasureTheory.Measure α),
  0 ≤ᵐ[μ] f →
    AEMeasurable f μ →
      (∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t) →
        (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), 0 ≤ g t) →
          ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
            ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)