mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- Taking the kernel density of intervals `Iic q` for `q : ℚ` gives a function with the property
`isRatCondKernelCDF`.  -/
ProbabilityTheory.Kernel.isRatCondKernelCDF_density_Iic : ∀ {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × ℝ))
  [ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsRatCondKernelCDF (fun p q => κ.density κ.fst p.1 p.2 (Set.Iic ↑q)) κ κ.fst
-- Mathlib.Probability.StrongLaw
/-- `Xᵢ` satisfies the strong law of large numbers along the sequence
`c^n`, for any `c > 1`. This follows from the version for the truncated `Xᵢ`, and the fact that
`Xᵢ` and its truncated version have the same asymptotic behavior.  -/
ProbabilityTheory.strong_law_aux6 : ∀ {Ω : Type u_1} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
  (X : ℕ → Ω → ℝ),
  MeasureTheory.Integrable (X 0) MeasureTheory.volume →
    Pairwise (Function.onFun (fun f g => ProbabilityTheory.IndepFun f g MeasureTheory.volume) X) →
      (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) →
        (∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω) →
          ∀ {c : ℝ},
            1 < c →
              ∀ᵐ (ω : Ω),
                Filter.Tendsto (fun n => (∑ i ∈ Finset.range ⌊c ^ n⌋₊, X i ω) / ↑⌊c ^ n⌋₊) Filter.atTop
                  (nhds (∫ (a : Ω), X 0 a))
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.piₗᵢ_symm_apply : ∀ (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_3 : Fintype ι]
  {ι' : Type v'} [inst_4 : Fintype ι'] {E' : ι' → Type wE'} [inst_5 : (i' : ι') → NormedAddCommGroup (E' i')]
  [inst_6 : (i' : ι') → NormedSpace 𝕜 (E' i')] (a : ContinuousMultilinearMap 𝕜 E ((i : ι') → E' i)) (i : ι'),
  (ContinuousMultilinearMap.piₗᵢ 𝕜 E).symm a i = (ContinuousLinearMap.proj i).compContinuousMultilinearMap a
-- Mathlib.Order.Comparable
not_symmGen_iff : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop}, ¬Relation.SymmGen r a b ↔ IncompRel r a b
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.measurePreserving_coe : MeasureTheory.MeasurePreserving Subtype.val MeasureTheory.volume (MeasureTheory.volume.restrict unitInterval)
-- Mathlib.Algebra.Field.Defs
Field.toSemifield : {K : Type u_1} → [Field K] → Semifield K
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instLTOrigin : LT Lean.Meta.Origin
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ ∩ t₂).getKey? k = if k ∈ t₂ then t₁.getKey? k else none
-- Mathlib.Algebra.Group.Subgroup.Actions
/-- The additive action by an `AddSubgroup` is the action by the underlying `AddGroup`.  -/
AddSubgroup.instAddAction : {G : Type u_1} → {α : Type u_2} → [inst : AddGroup G] → [AddAction G α] → {S : AddSubgroup G} → AddAction (↥S) α
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_one : ∀ {R : Type u} (M : Type v) [inst : One R] [inst_1 : Zero M], TrivSqZeroExt.inl 1 = 1
-- Mathlib.Analysis.Calculus.ContDiff.Basic
ftaylorSeriesWithin_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F], ftaylorSeriesWithin 𝕜 0 = 0
-- Std.Do.SPred.SVal
Std.Do.SVal.instGetTyCons : {σ : Type u_1} → {σs : List (Type u_1)} → Std.Do.SVal.GetTy σ (σ :: σs)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.insertMany_list_eq_foldl : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Internal.Raw₀ α β}
  {l : List ((a : α) × β a)}, ↑(m.insertMany l) = List.foldl (fun a b => a.insert b.fst b.snd) m l
-- Mathlib.Order.Basic
Prop.partialOrder : PartialOrder Prop
-- Lean.Data.Lsp.Extra
/-- `textDocument/waitForDiagnostics` client<-server reply.  -/
Lean.Lsp.WaitForDiagnostics : Type
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H0π_comp_map : ∀ {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),
  CategoryTheory.CategoryStruct.comp (groupHomology.H0π A) (groupHomology.map f φ 0) =
    CategoryTheory.CategoryStruct.comp (Rep.Hom.toModuleCatHom φ) (groupHomology.H0π B)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_left_unitality_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : CategoryTheory.Functor Y.Modules X.Modules}
  (h : AlgebraicGeometry.Scheme.Modules.pullback f ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Modules.pullbackComp f (CategoryTheory.CategoryStruct.id Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (AlgebraicGeometry.Scheme.Modules.pullbackId Y).hom
          (AlgebraicGeometry.Scheme.Modules.pullback f))
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.pullback f).leftUnitor.hom h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
-- Mathlib.Data.List.DropRight
List.rdropWhile.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.rdropWhile p l = (List.dropWhile p l.reverse).reverse
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.symm_symm_apply : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (equiv : S.Equiv S')
  (a : E), equiv.symm.symm a = equiv a
-- Mathlib.Computability.Language
/-- Language `l.reverse` is defined as the set of words from `l` backwards.  -/
Language.reverse : {α : Type u_1} → Language α → Language α
-- Init.Data.String.Basic
String.Pos.ofSliceTo_le : ∀ {s : String} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos}, String.Pos.ofSliceTo pos ≤ p₀
-- Mathlib.GroupTheory.Transfer
/-- The difference of two left transversals  -/
Subgroup.leftTransversals.diff : {G : Type u_1} →
  [inst : Group G] →
    {H : Subgroup G} →
      {A : Type u_2} → [inst_1 : CommGroup A] → (↥H →* A) → H.LeftTransversal → H.LeftTransversal → [H.FiniteIndex] → A
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_iInf : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ι → AddSubmonoid N),
  AddSubmonoid.comap f (iInf s) = ⨅ i, AddSubmonoid.comap f (s i)
-- Mathlib.Order.Partition.Basic
Partition.ext : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α] {P Q : Partition s}, (∀ (x : α), x ∈ P ↔ x ∈ Q) → P = Q
-- Lean.Elab.PreDefinition.TerminationMeasure
Lean.Elab.TerminationMeasure.fn : Lean.Elab.TerminationMeasure → Lean.Expr
-- Init.Data.List.Sublist
List.sublist_filterMap_iff : ∀ {β : Type u_1} {α : Type u_2} {l₂ : List α} {l₁ : List β} {f : α → Option β},
  l₁.Sublist (List.filterMap f l₂) ↔ ∃ l', l'.Sublist l₂ ∧ l₁ = List.filterMap f l'
-- Mathlib.RingTheory.TwoSidedIdeal.Kernel
/-- The kernel of a ring homomorphism, as a two-sided ideal.
 -/
TwoSidedIdeal.ker : {R : Type u_1} →
  {S : Type u_2} →
    [inst : NonUnitalNonAssocRing R] →
      [inst_1 : NonUnitalNonAssocSemiring S] →
        {F : Type u_3} → [inst_2 : FunLike F R S] → [NonUnitalRingHomClass F R S] → F → TwoSidedIdeal R
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.ext_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] {f g : OneHom M N}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiff_iff_forall_nat_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : ℕ∞}, ContDiff 𝕜 (↑n) f ↔ ∀ (m : ℕ), ↑m ≤ n → ContDiff 𝕜 (↑m) f
-- Mathlib.Topology.Inseparable
Inseparable.refl : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), Inseparable x x
-- Mathlib.RingTheory.Ideal.Maps
/-- The induced linear map from `I` to the span of `I` in an `R`-algebra `S`.  -/
Algebra.idealMap : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (I : Ideal R) → ↥I →ₗ[R] ↥(Ideal.map (algebraMap R S) I)
-- Mathlib.Data.Sign.Defs
/-- `SignType` is equivalent to `Fin 3`.  -/
SignType.fin3Equiv : SignType ≃* Fin 3
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_subgroupOf_eq_of_le : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H ≤ K → Subgroup.map K.subtype (H.subgroupOf K) = H
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.affineCombination_mem_closedInterior_face_iff_nonneg : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] [IsOrderedAddMonoid k] {n : ℕ} (s : Affine.Simplex k P n)
  {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) {w : Fin (n + 1) → k},
  ∑ i, w i = 1 →
    ((Finset.affineCombination k Finset.univ s.points) w ∈ (s.face h).closedInterior ↔
      (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.of_horiz_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} [CategoryTheory.IsIso f] [CategoryTheory.IsIso inr],
  CategoryTheory.CommSq f g inl inr → CategoryTheory.IsPushout f g inl inr
-- Std.Sync.Channel
Std.instNonemptySync : ∀ {α : Type}, Nonempty (Std.CloseableChannel.Sync α)
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Order.Defs.Unbundled
Std.Irrefl.decide : ∀ {α : Sort u_1} {r : α → α → Prop} [inst : DecidableRel r] [Std.Irrefl r], Std.Irrefl fun a b => decide (r a b) = true
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_add_aleph0 : Cardinal.continuum + Cardinal.aleph0 = Cardinal.continuum
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.tprod_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommGroup α] [inst_1 : UniformSpace α] [IsUniformGroup α]
  [CompleteSpace α] [T0Space α] {f : β × γ → α}, Multipliable f → ∏' (p : β × γ), f p = ∏' (b : β) (c : γ), f (b, c)
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_self_sub_right : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → AddGroup (N a)] (f g : Π₀ (a : α), N a), f.neLocus (f - g) = g.support
-- Init.Data.UInt.Bitwise
USize.toBitVec_xor : ∀ (a b : USize), (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
SSet.Subcomplex.Pairing.op_ancestralRel_iff : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (x y : ↑P.II),
  P.op.AncestralRel ⟨SSet.Subcomplex.N.opEquiv.symm ↑x, ⋯⟩ ⟨SSet.Subcomplex.N.opEquiv.symm ↑y, ⋯⟩ ↔ P.AncestralRel x y
-- Mathlib.Analysis.Convex.Between
AffineSubspace.mem_of_wbtw : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {s : AffineSubspace R P} {x y z : P},
  Wbtw R x y z → x ∈ s → z ∈ s → y ∈ s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Const
Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go_denote_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (c : BitVec w)
  (assign : α → Bool) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (hidx1 : idx < w),
  curr ≤ idx →
    ⟦assign,
        { aig := aig, ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go aig c curr s hcurr).get idx hidx1 }⟧ =
      c.getLsbD idx
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsCofilteredULift : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C],
  CategoryTheory.IsCofiltered (ULift.{u₂, u} C)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.toRationalMap_toPartialMap : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsReduced X] [inst_1 : Y.IsSeparated]
  (f : X.RationalMap Y), f.toPartialMap.toRationalMap = f
-- Mathlib.MeasureTheory.Integral.MeanInequalities
ENNReal.funMulInvSnorm_rpow : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ},
  0 < p → ∀ {f : α → ENNReal} {a : α}, ENNReal.funMulInvSnorm f p μ a ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
-- Init.Data.Option.Lemmas
Option.get!_or : ∀ {α : Type u_1} {o o' : Option α} [inst : Inhabited α], (o.or o').get! = o.getD o'.get!
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∈ m₂ → (m₁ ∩ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.Scheme.Hom.homeomorph.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f f_1 : X ⟶ Y) (e_f : f = f_1) [inst : CategoryTheory.IsIso f],
  AlgebraicGeometry.Scheme.Hom.homeomorph f = AlgebraicGeometry.Scheme.Hom.homeomorph f_1
-- Mathlib.RingTheory.HopfAlgebra.Basic
/-- Every commutative (semi)ring is a Hopf algebra over itself  -/
CommSemiring.toHopfAlgebra : (R : Type u) → [inst : CommSemiring R] → HopfAlgebra R R
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
Equiv.Perm.IsThreeCycle.alternating_normalClosure : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  5 ≤ Nat.card α → ∀ {f : Equiv.Perm α} (hf : f.IsThreeCycle), Subgroup.normalClosure {⟨f, ⋯⟩} = ⊤
-- Init.Data.String.Pattern.String
String.Slice.Pattern.BackwardSliceSearcher.skipSuffix? : String.Slice → (s : String.Slice) → Option s.Pos
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_relabel_sumInr : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {n : ℕ} (φ : L.Formula (Fin n)) {v : Empty → M}
  {x : Fin n → M}, (FirstOrder.Language.BoundedFormula.relabel Sum.inr φ).Realize v x ↔ φ.Realize x
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsMulIndecomposable.subset : ∀ {ι : Type u_1} {M : Type u_2} [inst : Monoid M] (v : ι → M) (s : Set ι), {i | IsMulIndecomposable v s i} ⊆ s
-- Init.BinderNameHint
/-- The expression `binderNameHint v binder e` defined to be `e`.

If it is used on the right-hand side of an equation that is used for rewriting by `rw` or `simp`,
and `v` is a local variable, and `binder` is an expression that (after beta-reduction) is a binder
(`fun w => …` or `∀ w, …`), then it will rename `v` to the name used in that binder, and remove
the `binderNameHint`.

A typical use of this gadget would be as follows; the gadget ensures that after rewriting, the local
variable is still `name`, and not `x`:
```
theorem all_eq_not_any_not (l : List α) (p : α → Bool) :
    l.all p = !l.any fun x => binderNameHint x p (!p x) := sorry

example (names : List String) : names.all (fun name => "Waldo".isPrefixOf name) = true := by
  rw [all_eq_not_any_not]
  -- ⊢ (!names.any fun name => !"Waldo".isPrefixOf name) = true
```

If `binder` is not a binder, then the name of `v` attains a macro scope. This only matters when the
resulting term is used in a non-hygienic way, e.g. in termination proofs for well-founded recursion.

This gadget is supported by
* `simp`, `dsimp` and `rw` in the right-hand-side of an equation
* `simp` in the assumptions of congruence rules

It is ineffective in other positions (hypotheses of rewrite rules) or when used by other tactics
(e.g. `apply`).
 -/
binderNameHint : {α : Sort u} → {β : Sort v} → {γ : Sort w} → α → β → γ → γ
-- Mathlib.Order.Sublattice
Sublattice.coe_map : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β) (L : Sublattice α),
  ↑(Sublattice.map f L) = ⇑f '' ↑L
-- Mathlib.CategoryTheory.Filtered.Final
/-- If `C` is filtered, then we can give an explicit condition for a functor `F : C ⥤ D` to
be final. The converse is also true, see `final_iff_of_isFiltered`.  -/
CategoryTheory.Functor.final_of_exists_of_isFiltered : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C],
  (∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) →
    (∀ {d : D} {c : C} (s s' : d ⟶ F.obj c),
        ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)) →
      F.Final
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.min?.eq_def : ∀ {α : Type u_1} (x : RBTree.RBNode α),
  x.min? =
    match x with
    | RBTree.RBNode.nil => none
    | RBTree.RBNode.node c RBTree.RBNode.nil v r => some v
    | RBTree.RBNode.node c l v r => l.min?
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instCommSemiring : {R : Type u_1} → [CommSemiring R] → CommSemiring (Lex R)
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_comap_iff_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {g : α → β}
  {f : β → γ}, Function.Surjective g → (Measurable f ↔ Measurable (f ∘ g))
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendScalars.map'.eq_1 : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {M1 M2 : ModuleCat R}
  (l : M1 ⟶ M2), ModuleCat.ExtendScalars.map' f l = ModuleCat.ofHom (LinearMap.baseChange S (ModuleCat.Hom.hom l))
-- Mathlib.RingTheory.Ideal.GoingDown
Ideal.exists_ideal_lt_liesOver_of_lt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.HasGoingDown R S] {p q : Ideal R} [p.IsPrime] [q.IsPrime] (Q : Ideal S) [Q.IsPrime] [Q.LiesOver q],
  p < q → ∃ P < Q, P.IsPrime ∧ P.LiesOver p
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Var : Type
-- Mathlib.RingTheory.WittVector.StructurePolynomial
bind₁_rename_expand_wittPolynomial : ∀ {p : ℕ} {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (n : ℕ),
  (∀ m < n + 1,
      (MvPolynomial.map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) =
        wittStructureRat p ((MvPolynomial.map (Int.castRingHom ℚ)) Φ) m) →
    (MvPolynomial.bind₁ fun b => (MvPolynomial.rename fun i => (b, i)) ((MvPolynomial.expand p) (wittPolynomial p ℤ n)))
        Φ =
      (MvPolynomial.bind₁ fun i => (MvPolynomial.expand p) (wittStructureInt p Φ i)) (wittPolynomial p ℤ n)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.basicOpen_res : ∀ (X : AlgebraicGeometry.Scheme) {V U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U)))
  (i : Opposite.op U ⟶ Opposite.op V),
  X.basicOpen ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map i)) f) = V ⊓ X.basicOpen f
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.single_strictMono : ∀ {I : Type u} {f : I → Type v} (i : I) [inst : DecidableEq I] [inst_1 : (i : I) → Preorder (f i)]
  [inst_2 : (i : I) → Zero (f i)], StrictMono (Pi.single i)
-- Mathlib.Probability.Kernel.Disintegration.Basic
/-- If the singleton `{x}` has non-zero mass for `ρ.fst`, then for all `s : Set Ω`,
`ρCond x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)` .  -/
MeasureTheory.Measure.IsCondKernel.apply_of_ne_zero : ∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω))
  (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] [MeasureTheory.IsFiniteMeasure ρ]
  [MeasurableSingletonClass α] {x : α}, ρ.fst {x} ≠ 0 → ∀ (s : Set Ω), (ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `upperHemicontinuous_iff_frequently`. -/
UpperHemicontinuous.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  (∀ (x : α) (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty) →
    UpperHemicontinuous f
-- Mathlib.Data.Set.Lattice
sInf_sUnion : ∀ {β : Type u_2} [inst : CompleteLattice β] (s : Set (Set β)), sInf (⋃₀ s) = ⨅ t ∈ s, sInf t
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instEssentiallySmallMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P]
  (F : CategoryTheory.Functor C D), CategoryTheory.ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
cast.eq_1 : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a = h ▸ a
-- Mathlib.MeasureTheory.Constructions.Projective
/-- A measure `μ` is the projective limit of a family of measures indexed by finite sets of `ι` if
for all `I : Finset ι`, the projection from `∀ i, α i` to `∀ i : I, α i` maps `μ` to `P I`.  -/
MeasureTheory.IsProjectiveLimit : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → MeasurableSpace (α i)] →
      MeasureTheory.Measure ((i : ι) → α i) → ((J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)) → Prop
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstr.compare : Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstr → Ordering
-- Lean.Meta.Basic
Lean.Meta.instHashableInfoCacheKey : Hashable Lean.Meta.InfoCacheKey
-- Mathlib.Data.Countable.Defs
not_injective_uncountable_countable : ∀ {α : Sort u} {β : Sort v} [Uncountable α] [Countable β] (f : α → β), ¬Function.Injective f
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- Copy a submonoid replacing `carrier` with a set that is equal to it.  -/
Submonoid.copy : {M : Type u_1} → [inst : MulOneClass M] → (S : Submonoid M) → (s : Set M) → s = ↑S → Submonoid M
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsMonoidalStable.toIsStableUnderAssociator : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P : CategoryTheory.MorphismProperty C}
  {inst_1 : CategoryTheory.MonoidalCategory C} [self : P.IsMonoidalStable], P.IsStableUnderAssociator
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt32.reduceGT : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.Hom.ext : ∀ {A B : AddMagmaCat} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Mathlib.Data.Fintype.Basic
Fintype.univ_bool : Finset.univ = {true, false}
-- Mathlib.Data.Nat.Log
Nat.log2_eq_log_two : ∀ {n : ℕ}, n.log2 = Nat.log 2 n
-- Mathlib.Data.Finset.Pi
Finset.restrict₂_def : ∀ {ι : Type u_2} {π : ι → Type u_3} {s t : Finset ι} (hst : s ⊆ t), Finset.restrict₂ hst = fun f x => f ⟨↑x, ⋯⟩
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.measure_mono_both : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s t : Set α}, μ ≤ ν → s ⊆ t → μ s ≤ ν t
-- Mathlib.Algebra.Group.Subgroup.Defs
Set.injOn_iff_map_eq_one : ∀ {F : Type u_3} {G : Type u_4} {H : Type u_5} {S : Type u_6} [inst : Group G] [inst_1 : Group H]
  [inst_2 : FunLike F G H] [MonoidHomClass F G H] (f : F) [inst_4 : SetLike S G] [OneMemClass S G] [MulMemClass S G]
  [InvMemClass S G] (s : S), Set.InjOn ⇑f ↑s ↔ ∀ a ∈ s, f a = 1 → a = 1
-- Mathlib.Topology.Spectral.Hom
SpectralMap.id_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] (a : α), (SpectralMap.id α) a = a
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.nle.inj : ∀ {lhs rhs : ℕ} {proof : Lean.Expr} {lhs_1 rhs_1 : ℕ} {proof_1 : Lean.Expr},
  Mathlib.Tactic.Order.AtomicFact.nle lhs rhs proof = Mathlib.Tactic.Order.AtomicFact.nle lhs_1 rhs_1 proof_1 →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ proof = proof_1