mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.compactSpace_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], CompactSpace (TopologicalSpace.NonemptyCompacts α) ↔ CompactSpace α
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The functor `SmallObject.functor f : Arrow C ⥤ Arrow C` that is part of
the small object argument for a family of morphisms `f`, on an object given
as a morphism `πX : X ⟶ S`.  -/
CategoryTheory.SmallObject.functorObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S X : C} →
            (πX : X ⟶ S) →
              [inst_1 :
                  CategoryTheory.Limits.HasColimitsOfShape
                    (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
                [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
                      (CategoryTheory.SmallObject.functorObjLeft f πX)] →
                  C
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_pos_iff : ∀ {ι : Type u_9} {M : Type u_10} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [CanonicallyOrderedAdd M]
  {f : ι → M} {s : Finset ι}, 0 < ∑ x ∈ s, f x ↔ ∃ x ∈ s, 0 < f x
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.isPWO_support_antidiagonal : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO}, {a | (Finset.antidiagonal hs ht a).Nonempty}.IsPWO
-- Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
MeasureTheory.Measure.mutuallySingular_compProd_right_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η]
  [MeasurableSpace.CountableOrCountablyGenerated α β] [MeasureTheory.SFinite μ],
  (μ.compProd κ).MutuallySingular (μ.compProd η) ↔ ∀ᵐ (a : α) ∂μ, (κ a).MutuallySingular (η a)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The iterated derivative of the sum of two functions is the sum of the iterated derivatives.
 -/
iteratedFDerivWithin_add_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {x : E} {i : ℕ} {f g : E → F},
  ContDiffWithinAt 𝕜 (↑i) f s x →
    ContDiffWithinAt 𝕜 (↑i) g s x →
      UniqueDiffOn 𝕜 s →
        x ∈ s → iteratedFDerivWithin 𝕜 i (f + g) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x
-- Mathlib.Algebra.Group.AddChar
AddChar.toAddMonoidHomEquiv_apply : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : AddChar A M) (a : A),
  (AddChar.toAddMonoidHomEquiv ψ) a = Additive.ofMul (ψ a)
-- Lean.Elab.SyntheticMVars
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.withSynthesizeLightImp : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Init.Data.Array.Attach
/-- “Attaches” individual proofs to an array of values that satisfy a predicate `P`, returning an array
of elements in the corresponding subtype `{ x // P x }`.

`O(1)`.
 -/
Array.attachWith : {α : Type u_1} → (xs : Array α) → (P : α → Prop) → (∀ x ∈ xs, P x) → Array { x // P x }
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.ZNum.zNeg.match_1.eq_1 : ∀ (motive : ZNum → Sort u_1) (h_1 : Unit → motive ZNum.zero) (h_2 : (a : PosNum) → motive (ZNum.pos a))
  (h_3 : (a : PosNum) → motive (ZNum.neg a)),
  (match ZNum.zero with
    | ZNum.zero => h_1 ()
    | ZNum.pos a => h_2 a
    | ZNum.neg a => h_3 a) =
    h_1 ()
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH1_τ₂ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  (groupHomology.mapShortComplexH1 f φ).τ₂ = groupHomology.chainsMap₁ f φ
-- Mathlib.Order.Ideal
Order.mem_idealOfCofinals : ∀ {P : Type u_1} [inst : Preorder P] (p : P) {ι : Type u_2} [inst_1 : Encodable ι] (𝒟 : ι → Order.Cofinal P),
  p ∈ Order.idealOfCofinals p 𝒟
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_succ_uIcc : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.succ (Finset.uIcc i j) = Finset.uIcc i.succ j.succ
-- Init.Data.Option.Lemmas
Option.pelim_none' : ∀ {α : Type u_1} {x : Option α} {α_1 : Sort u_2} {b : α_1} {f : (a : α) → x = some a → α_1}, x = none → x.pelim b f = b
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Commuting a functor that preserves right Kan extensions with the `ran` functor.  -/
CategoryTheory.Functor.ranCompIsoOfPreserves : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (G : CategoryTheory.Functor B D) →
                  (L : CategoryTheory.Functor A C) →
                    [G.PreservesRightKanExtensions L] →
                      [inst_5 : ∀ (F : CategoryTheory.Functor A B), L.HasRightKanExtension F] →
                        [inst_6 : ∀ (F : CategoryTheory.Functor A D), L.HasRightKanExtension F] →
                          L.ran.comp ((CategoryTheory.Functor.whiskeringRight C B D).obj G) ≅
                            ((CategoryTheory.Functor.whiskeringRight A B D).obj G).comp L.ran
-- Mathlib.Data.List.Cycle
_private.Mathlib.Data.List.Cycle.0.List.nextOr.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → α → α → Sort u_2) (y z : α) (xs : List α) (x default : α)
  (h_1 : (x default : α) → motive [] x default) (h_2 : (head x default : α) → motive [head] x default)
  (h_3 : (y z : α) → (xs : List α) → (x default : α) → motive (y :: z :: xs) x default),
  (match y :: z :: xs, x, default with
    | [], x, default => h_1 x default
    | [head], x, default => h_2 head x default
    | y :: z :: xs, x, default => h_3 y z xs x default) =
    h_3 y z xs x default
-- Mathlib.Data.NNRat.Defs
NNRat.coe_one : ↑1 = 1
-- Mathlib.Analysis.Normed.Group.Continuity
SeminormedAddGroup.tendstoUniformlyOn_zero : ∀ {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [inst : SeminormedAddGroup G] {f : ι → κ → G} {s : Set κ} {l : Filter ι},
  TendstoUniformlyOn f 0 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.instIsClosedUnderIsomorphismsFunctorRightExactFunctor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.rightExactFunctor C D).IsClosedUnderIsomorphisms
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- The root of `T`, except its type is `G` instead of the type synonym `T`.  -/
_private.Mathlib.GroupTheory.FreeGroup.NielsenSchreier.0.IsFreeGroupoid.SpanningTree.root' : {G : Type u} →
  [inst : CategoryTheory.Groupoid G] →
    [inst_1 : IsFreeGroupoid G] →
      (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) →
        [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] → G
-- Std.Http.Data.Response
/-- Builds and returns the final HTTP Response with an empty body (`{}`).
Requires an `EmptyCollection` instance for the response body type.
 -/
Std.Http.Response.Builder.build : {t : Type} → [EmptyCollection t] → Std.Http.Response.Builder → Std.Http.Response t
-- Init.PropLemmas
/-- Transfer decidability of `a` to decidability of `b`, if the propositions are equivalent.
**Important**: this function should be used instead of `rw` on `Decidable b`, because the
kernel will get stuck reducing the usage of `propext` otherwise,
and `decide` will not work.  -/
decidable_of_iff : {b : Prop} → (a : Prop) → (a ↔ b) → [Decidable a] → Decidable b
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalSubalgebra.starClosure_mono : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : IsScalarTower R A A]
  [inst_7 : SMulCommClass R A A], Monotone NonUnitalSubalgebra.starClosure
-- Mathlib.Algebra.Group.Hom.Basic
/-- Define a morphism of additive groups given a map which respects ratios.  -/
MonoidHom.ofMapDiv : {G : Type u_5} →
  [inst : Group G] → {H : Type u_8} → [inst_1 : Group H] → (f : G → H) → (∀ (x y : G), f (x / y) = f x / f y) → G →* H
-- Init.Core
USize.ofBitVec.inj : ∀ {toBitVec toBitVec_1 : BitVec System.Platform.numBits},
  { toBitVec := toBitVec } = { toBitVec := toBitVec_1 } → toBitVec = toBitVec_1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Function.Periodic.lift.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {f f_1 : α → β} (e_f : f = f_1) {c : α} [inst : AddGroup α] (h : Function.Periodic f c)
  (x x_1 : α ⧸ AddSubgroup.zmultiples c), x = x_1 → h.lift x = ⋯.lift x_1
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_le_iff : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A}
  {S : Subalgebra R A}, Algebra.adjoin R s ≤ S ↔ s ⊆ ↑S
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.fundCircuit_subset_insert : ∀ {α : Type u_1} (M : Matroid α) (e : α) (I : Set α), M.fundCircuit e I ⊆ insert e I
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.SubgoalsResult.mk : List Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.SynthInstance.SubgoalsResult
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.preComp_b : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X X' : CategoryTheory.SimplicialObject C} {n : ℕ}
  {Z : C} (f : AlgebraicTopology.DoldKan.MorphComponents X n Z) (g : X' ⟶ X) (i : Fin (n + 1)),
  (f.preComp g).b i = CategoryTheory.CategoryStruct.comp (g.app (Opposite.op { len := n })) (f.b i)
-- Mathlib.RingTheory.AdjoinRoot
/-- The canonical algebraic homomorphism from `AdjoinRoot f` to `AdjoinRoot g`, where
the polynomial `g : S[X]` divides `f`.  -/
AdjoinRoot.algHomOfDvd : (R : Type u_1) →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (f g : Polynomial S) → g ∣ f → AdjoinRoot f →ₐ[R] AdjoinRoot g
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.atIdxSlow?_eq_match.match_3.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Topology.Constructions
denseRange_inclusion_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X} (hst : s ⊆ t), DenseRange (Set.inclusion hst) ↔ t ⊆ closure s
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Regular epimorphisms are preserved by isomorphisms in the arrow category.  -/
CategoryTheory.RegularEpi.ofArrowIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y X' Y' : C} →
      {f : X ⟶ Y} →
        {g : X' ⟶ Y'} →
          (CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g) →
            CategoryTheory.RegularEpi f → CategoryTheory.RegularEpi g
-- Init.Data.UInt.Lemmas
UInt16.succ_mul : ∀ {a b : UInt16}, (a + 1) * b = a * b + b
-- Mathlib.Data.List.Basic
_private.Mathlib.Data.List.Basic.0.List.getLast?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Aesop.Search.ExpandSafePrefix
Aesop.SafeExpansionM.State.mk : ℕ → Aesop.SafeExpansionM.State
-- Mathlib.CategoryTheory.Monad.EquivMon
/-- Passing from `Monad C` to `Mon (C ⥤ C)` is functorial.  -/
CategoryTheory.Monad.monadToMon : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.Monad C) (CategoryTheory.Mon (CategoryTheory.Functor C C))
-- Lean.AuxRecursor
Lean.noConfusionExt : Lean.MapDeclarationExtension Lean.NoConfusionInfo
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The **Lusin separation theorem**: if two analytic sets are disjoint, then they are contained in
disjoint Borel sets.  -/
MeasureTheory.AnalyticSet.measurablySeparable : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α] [inst_2 : MeasurableSpace α] [OpensMeasurableSpace α]
  {s t : Set α},
  MeasureTheory.AnalyticSet s → MeasureTheory.AnalyticSet t → Disjoint s t → MeasureTheory.MeasurablySeparable s t
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
CategoryTheory.Square.IsPushout.map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {sq : CategoryTheory.Square C},
  sq.IsPushout →
    ∀ (F : CategoryTheory.Functor C D)
      [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span sq.f₁₂ sq.f₁₃) F], (sq.map F).IsPushout
-- Mathlib.LinearAlgebra.Projectivization.Independence
/-- A linearly dependent family of nonzero vectors gives a dependent family of points
in projective space.  -/
Projectivization.Dependent : {ι : Type u_1} →
  {K : Type u_2} →
    {V : Type u_3} →
      [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → (ι → Projectivization K V) → Prop
-- Mathlib.MeasureTheory.Function.UnifTight
MeasureTheory.UnifTight.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : NormedAddCommGroup β] {x : MeasurableSpace α} (f : ι → α → β)
  (p : ENNReal) (μ : MeasureTheory.Measure α),
  MeasureTheory.UnifTight f p μ =
    ∀ ⦃ε : NNReal⦄, 0 < ε → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), MeasureTheory.eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.one_hadamard_eq_zero_iff : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : MulZeroOneClass α] {A : Matrix n n α},
  Matrix.hadamard 1 A = 0 ↔ A.diag = 0
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.isOrtho_inl_inl_iff : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} (m₁ m₁' : M₁),
  (Q₁.prod Q₂).IsOrtho (m₁, 0) (m₁', 0) ↔ Q₁.IsOrtho m₁ m₁'
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G) [hA : A.IsTrivial]
  (f : ↥(groupCohomology.cocycles₁ A)) (a : Additive G),
  ((ModuleCat.Hom.hom (groupCohomology.cocycles₁IsoOfIsTrivial A).hom) f) a = f (Additive.toMul a)
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofUserWidgetInfo : Lean.Elab.UserWidgetInfo → Lean.Elab.Info
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.mk_eq_mk_iff_sub_mem : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided] (x y : R),
  (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y ↔ x - y ∈ I
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instContinuousConstVAdd : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : VAdd R M] [inst_3 : ContinuousConstVAdd R M], ContinuousConstVAdd R C(α, M)
-- Init.Data.BitVec.Lemmas
BitVec.getElem?_zero_ofNat_one : ∀ {w : ℕ}, (1#(w + 1))[0]? = some true
-- Lean.Parser.Do
Lean.Parser.Term.doFinally.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Aesop.Options.Public
/-- If this option is not `none`, the builtin `intros` rule unfolds the goal's
target with the given transparency to discover `∀` binders. For example, with
`def T := ∀ x y : Nat, x = y`, `introsTransparency? := some .default` and goal
`⊢ T`, the `intros` rule produces the goal `x, y : Nat ⊢ x = y`. With
`introsTransparency? := some .reducible`, it produces `⊢ T`. With
`introsTransparency? := none`, it only introduces arguments which are
syntactically bound by `∀` binders, so it also produces `⊢ T`.
 -/
Aesop.Options.introsTransparency? : Aesop.Options → Option Lean.Meta.TransparencyMode
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
min_le_add_of_nonneg_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddZeroClass α] [AddRightMono α] {a b : α}, 0 ≤ a → min a b ≤ a + b
-- Mathlib.Algebra.Order.Field.Pointwise
LinearOrderedField.smul_Ioc : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {a b r : K},
  0 < r → r • Set.Ioc a b = Set.Ioc (r * a) (r * b)
-- Mathlib.Data.Finsupp.Multiset
Multiset.toFinsupp_toMultiset : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), Finsupp.toMultiset (Multiset.toFinsupp s) = s
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.isTranscendenceBasis_of_lift_trdeg_le : ∀ {ι : Type u} {R : Type u_1} {A : Type w} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Nontrivial R] [NoZeroDivisors A],
  AlgebraicIndependent R x →
    Algebra.trdeg R A < Cardinal.aleph0 →
      Cardinal.lift.{u, w} (Algebra.trdeg R A) ≤ Cardinal.lift.{w, u} (Cardinal.mk ι) → IsTranscendenceBasis R x
-- Mathlib.Logic.Encodable.Basic
/-- The lift of an encodable type is encodable  -/
ULift.encodable : {α : Type u_1} → [Encodable α] → Encodable (ULift.{u_3, u_1} α)
-- Lean.Meta.ExprLens
/-- Given a valid `SubExpr`, return the raw current expression without performing any instantiation.
If the given `SubExpr` has a type subexpression coordinate, then throw an error.

This is a cheaper version of `Lean.Meta.viewSubexpr` and can be used to quickly view the
subexpression at a position. Note that because the resulting expression may contain
loose bound variables it can't be used in any `MetaM` methods.  -/
Lean.Core.viewSubexpr : {M : Type → Type} → [Monad M] → [Lean.MonadError M] → Lean.SubExpr.Pos → Lean.Expr → M Lean.Expr
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.deterministic_prod_apply' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : α → β} (mf : Measurable f) (κ : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsSFiniteKernel κ] (a : α) {s : Set (β × γ)},
  MeasurableSet s → (((ProbabilityTheory.Kernel.deterministic f mf).prod κ) a) s = (κ a) (Prod.mk (f a) ⁻¹' s)
-- Init.Data.Array.Extract
Array.popWhile_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Bool} {as : Array α},
  Array.popWhile p (Array.map f as) = Array.map f (Array.popWhile (p ∘ f) as)
-- Init.Data.String.Iterate
String.Slice.instInhabitedRevByteIterator : Inhabited String.Slice.RevByteIterator
-- Mathlib.LinearAlgebra.Orientation
/-- Given a basis, an orientation equals the negation of that given by that basis if and only
if it does not equal that given by that basis.  -/
Module.Basis.orientation_ne_iff_eq_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (e : Module.Basis ι R M) (x : Orientation R M ι), x ≠ e.orientation ↔ x = -e.orientation
-- Mathlib.Algebra.Group.Units.Defs
Units.instInhabited.eq_1 : ∀ {α : Type u} [inst : Monoid α], Units.instInhabited = { default := 1 }
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.isAbsoluteValue : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], IsAbsoluteValue fun a => ‖a‖
-- Mathlib.Algebra.Module.ZLattice.Basic
ZLattice.module_free : ∀ (K : Type u_1) [inst : NormedField K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K]
  {E : Type u_2} [inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace K E] [FiniteDimensional K E] [ProperSpace E]
  (L : Submodule ℤ E) [inst_9 : DiscreteTopology ↥L] [IsZLattice K L], Module.Free ℤ ↥L
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.IsometryEquiv.mk.injEq : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} (toLinearEquiv : M₁ ≃ₗ[R] M₂)
  (map_app' : ∀ (n m : M₁), (B₂ ((↑toLinearEquiv).toFun n)) ((↑toLinearEquiv).toFun m) = (B₁ n) m)
  (toLinearEquiv_1 : M₁ ≃ₗ[R] M₂)
  (map_app'_1 : ∀ (n m : M₁), (B₂ ((↑toLinearEquiv_1).toFun n)) ((↑toLinearEquiv_1).toFun m) = (B₁ n) m),
  ({ toLinearEquiv := toLinearEquiv, map_app' := map_app' } =
      { toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 }) =
    (toLinearEquiv = toLinearEquiv_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPair.eqOfHomEq_hom_app : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g f' g' : X ⟶ Y} (hf : f = f') (hg : g = g')
  (X_1 : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.parallelPair.eqOfHomEq hf hg).hom.app X_1 =
    (CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.Iso.refl X) (CategoryTheory.Iso.refl Y) X_1).hom
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_smul_const : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  [CompleteSpace E] {𝕜 : Type u_8} [inst_3 : RCLike 𝕜] [inst_4 : NormedSpace 𝕜 E] (f : ℝ → 𝕜) (c : E),
  ∫ (x : ℝ) in a..b, f x • c ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) • c
-- Mathlib.Topology.Algebra.LinearTopology
isLinearTopology_iff_hasBasis_open_twoSidedIdeal : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [ContinuousAdd R],
  IsLinearTopology R R ∧ IsLinearTopology Rᵐᵒᵖ R ↔ (nhds 0).HasBasis (fun I => IsOpen ↑I) fun I => ↑I
-- Init.Data.BitVec.Basic
/-- Returns the `i`th most significant bit or `none` if `i ≥ w`.  -/
BitVec.getMsb? : {w : ℕ} → BitVec w → ℕ → Option Bool
-- Mathlib.RingTheory.RootsOfUnity.Basic
/-- A variant of `mem_rootsOfUnity_prime_pow_mul_iff` in terms of `ζ ^ _`  -/
mem_rootsOfUnity_prime_pow_mul_iff' : ∀ (R : Type u_4) [inst : CommRing R] [IsReduced R] (p k m : ℕ) [ExpChar R p] {ζ : Rˣ},
  ζ ^ (p ^ k * m) = 1 ↔ ζ ∈ rootsOfUnity m R
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : CategoryTheory.GaloisCategory C}
  {F : CategoryTheory.Functor C FintypeCat} {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F}
  {val : A.obj ⟶ B.obj}
  {comp :
    autoParam ((CategoryTheory.ConcreteCategory.hom (F.map val)) A.pt = B.pt)
      CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.comp._autoParam}
  {val_1 : A.obj ⟶ B.obj}
  {comp_1 :
    autoParam ((CategoryTheory.ConcreteCategory.hom (F.map val_1)) A.pt = B.pt)
      CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.comp._autoParam},
  { val := val, comp := comp } = { val := val_1, comp := comp_1 } → val = val_1
-- Mathlib.Analysis.Calculus.Deriv.Linear
ContinuousLinearMap.hasDerivAtFilter : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {L : Filter (𝕜 × 𝕜)} (e : 𝕜 →L[𝕜] F), HasDerivAtFilter (⇑e) (e 1) L
-- Mathlib.Algebra.MvPolynomial.Basic
/-- Analog of `Polynomial.induction_on'`.
To prove something about `MVPolynomials`,
it suffices to show the condition is closed under taking sums,
and it holds for monomials.  -/
MvPolynomial.induction_on' : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {P : MvPolynomial σ R → Prop} (p : MvPolynomial σ R),
  (∀ (u : σ →₀ ℕ) (a : R), P ((MvPolynomial.monomial u) a)) → (∀ (p q : MvPolynomial σ R), P p → P q → P (p + q)) → P p