mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.quotientRangeInlEquivRight.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  (S : AddGroupExtension N E G), S.quotientRangeInlEquivRight = QuotientAddGroup.liftEquiv S.inl.range ⋯ ⋯
-- Init.Data.UInt.Bitwise
UInt64.toFin_shiftLeft : ∀ (a b : UInt64), b < 64 → (a <<< b).toFin = a.toFin <<< b.toFin
-- Mathlib.Topology.Order.LiminfLimsup
eventually_le_limsup : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [FirstCountableTopology α] {f : Filter β} [CountableInterFilter f] {u : β → α},
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) eventually_le_limsup._auto_1 →
    ∀ᶠ (b : β) in f, u b ≤ Filter.limsup u f
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
/-- Given a diagram of `PresheafedSpace C`s, its colimit is computed by pushing the sheaves onto
the colimit of the underlying spaces, and taking componentwise limit.
This is the componentwise diagram for an open set `U` of the colimit of the underlying spaces.
 -/
AlgebraicGeometry.PresheafedSpace.componentwiseDiagram : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F) → CategoryTheory.Functor Jᵒᵖ C
-- Mathlib.Topology.Constructions
nhds_ne_subtype_eq_bot_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {S : Set X} {x : ↑S},
  nhdsWithin x {x}ᶜ = ⊥ ↔ nhdsWithin ↑x {↑x}ᶜ ⊓ Filter.principal S = ⊥
-- Mathlib.Topology.Category.Stonean.Basic
Profinite.lift_lifts_assoc : ∀ {X Y : Profinite} {Z : Stonean} (e : Stonean.toProfinite.obj Z ⟶ Y) (f : X ⟶ Y) [inst : CategoryTheory.Epi f]
  {Z_1 : Profinite} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (Profinite.lift e f) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp e h
-- Mathlib.Probability.Distributions.Poisson.Basic
/-- The integral of a function taking values in a finite-dimensional space
against `poissonMeasure r` is given by its sum weighted by `exp (-r) * r ^ n / n!`. This version
does not require integrability, as the integral exists if and only if the sum exists, and otherwise
they are both defined to be zero.

See `integral_poissonMeasure'` with a general codomain which assumes integrability.  -/
ProbabilityTheory.integral_poissonMeasure : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (r : NNReal)
  (f : ℕ → E),
  ∫ (n : ℕ), f n ∂ProbabilityTheory.poissonMeasure r = ∑' (n : ℕ), (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) • f n
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- The pair `f,g` is a `G`-split pair if there is an `h : G Y ⟶ Z` so that `G f, G g, h` forms a split
coequalizer in `D`.
 -/
CategoryTheory.Functor.IsSplitPair : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → {X Y : C} → (X ⟶ Y) → (X ⟶ Y) → Prop
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.homEquiv_apply_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} {f : I ⟶ J}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f]
  {X : CategoryTheory.Over I} {A : CategoryTheory.Over J}
  (u : (CategoryTheory.ChosenPullbacksAlong.pullback f).obj A ⟶ X),
  ((CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj f).homEquiv A X) u =
    CategoryTheory.ExponentiableMorphism.pushforwardCurry u
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShift.comp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F₁ F₂ F₃ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) (τ' : F₂ ⟶ F₃)
  (A : Type u_5) [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] [inst_7 : F₃.CommShift A] [CategoryTheory.NatTrans.CommShift τ A]
  [CategoryTheory.NatTrans.CommShift τ' A],
  CategoryTheory.NatTrans.CommShift (CategoryTheory.CategoryStruct.comp τ τ') A
-- Init.Data.Iterators.Combinators.Monadic.Attach
Std.Iterators.Types.Attach.invariant : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {P : β → Prop}
  (self : Std.Iterators.Types.Attach α m P) (out : β), self.inner.IsPlausibleIndirectOutput out → P out
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
/-- This follows the proof from `Borceux, Handbook of categorical algebra 1, Theorem 2.13.4`
although with different names.
 -/
CategoryTheory.Limits.colimitLimitToLimitColimit_surjective : ∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [inst_2 : Small.{v, u₂} K] [inst_3 : CategoryTheory.FinCategory J] (F : CategoryTheory.Functor (J × K) (Type v))
  [CategoryTheory.IsFiltered K],
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitLimitToLimitColimit F))
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {s : CategoryTheory.Limits.Cone F} {G : CategoryTheory.Functor K C} {t : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (e : J ≌ K) (w : e.functor.comp G ≅ F),
  (P.conePointsIsoOfEquivalence Q e w).inv =
    P.lift ((CategoryTheory.Limits.Cone.equivalenceOfReindexing e w).functor.obj t)
-- Mathlib.Algebra.Field.Basic
/-- See `inv_add_inv` for the more convenient version when `K` is commutative.  -/
inv_add_inv' : ∀ {K : Type u_1} [inst : DivisionSemiring K] {a b : K}, a ≠ 0 → b ≠ 0 → a⁻¹ + b⁻¹ = a⁻¹ * (a + b) * b⁻¹
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
instAddCommMonoidWeakSpace : (𝕜 : Type u_2) →
  (E : Type u_1) →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] →
              [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → AddCommMonoid (WeakSpace 𝕜 E)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mkPostcomp_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {Y Y' : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) (g : Y ⟶ Y'),
  (CategoryTheory.StructuredArrow.mkPostcomp f g).right = g
-- Mathlib.Order.Category.Frm
Frm.forget_map : ∀ {X Y : Frm} (f : X ⟶ Y),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget Frm).map f)) = ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β} {hc : k ∈ t.alter k f}, (t.alter k f)[k] = (f t[k]?).get ⋯
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.indexAt : {ι : Type u_5} →
  {B : Type u_6} →
    [inst : TopologicalSpace B] → {F : Type u_7} → [inst_1 : TopologicalSpace F] → FiberBundleCore ι B F → B → ι
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingCoeff_eq_coeff_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.coeff 0 ≠ 0 → p.trailingCoeff = p.coeff 0
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.pOpcycles_π_isoOpcyclesOfIsColimit_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] {cc : CategoryTheory.Limits.CokernelCofork S.f}
  (hcc : CategoryTheory.Limits.IsColimit cc) {Z : C} (h : cc.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.pOpcycles
      (CategoryTheory.CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc) h
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.ofHom₂_hom₂ : ∀ {R : Type u_1} [inst : CommSemiring R] {M N P : SemimoduleCat R} (f : M ⟶ SemimoduleCat.of R (N ⟶ P)),
  SemimoduleCat.ofHom₂ (SemimoduleCat.Hom.hom₂ f) = f
-- Mathlib.Algebra.Star.Subsemiring
/-- The actual `StarSubsemiring` obtained from an element of a `StarSubsemiringClass`.  -/
StarSubsemiring.ofClass : {S : Type u_1} →
  {R : Type u_2} →
    [inst : NonAssocSemiring R] →
      [inst_1 : SetLike S R] →
        [inst_2 : StarRing R] → [SubsemiringClass S R] → [StarMemClass S R] → S → StarSubsemiring R
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.instPartialOrderDiagramWithUniqueTerminal : (J : Type w) →
  [inst : CategoryTheory.SmallCategory J] →
    (κ : Cardinal.{w}) →
      PartialOrder (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ)
-- Init.Data.List.Impl
/-- Folds a function over a list from the right, accumulating a value starting with `init`. The
accumulated value is combined with the each element of the list in reverse order, using `f`.

`O(|l|)`. This is the tail-recursive replacement for `List.foldr` in runtime code.

Examples:
 * `[a, b, c].foldrTR f init  = f a (f b (f c init))`
 * `[1, 2, 3].foldrTR (toString · ++ ·) "" = "123"`
 * `[1, 2, 3].foldrTR (s!"({·} {·})") "!" = "(1 (2 (3 !)))"`
 -/
List.foldrTR : {α : Type u_1} → {β : Type u_2} → (α → β → β) → β → List α → β
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → ENNReal} {g : α → E},
  AEMeasurable f μ →
    (∀ᵐ (x : α) ∂μ, f x < ⊤) →
      MeasureTheory.Integrable (fun x => (f x).toReal • g x) μ →
        (μ.withDensityᵥ fun x => (f x).toReal • g x) = (μ.withDensity f).withDensityᵥ g
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.toQ_ofNat : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (n : ℕ), ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of left-invariant measures**:
Given two left-invariant measures which are finite on compacts, they coincide in the following
sense: they give the same value to sets with compact closure, up to the multiplicative
constant `addHaarScalarFactor μ' μ`.  -/
MeasureTheory.Measure.measure_isAddInvariant_eq_smul_of_isCompact_closure : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsAddLeftInvariant]
  {s : Set G}, IsCompact (closure s) → μ' s = μ'.addHaarScalarFactor μ • μ s
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
DirectedOn.notMem_of_csSup_lt : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {x : α} {s : Set α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → sSup s < x → BddAbove s → x ∉ s
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.flip_totalFlipIso : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J] [inst_7 : TotalComplexShapeSymmetry c₂ c₁ c] [TotalComplexShapeSymmetrySymmetry c₁ c₂ c],
  K.flip.totalFlipIso c = (K.totalFlipIso c).symm
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.fixLevelParams : Array Lean.Elab.PreDefinition → List Lean.Name → List Lean.Name → Lean.Elab.TermElabM (Array Lean.Elab.PreDefinition)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_natCast_add : ∀ (r : ENNReal) (n : ℕ), ⌊↑n + r⌋ₑ = ↑n + ⌊r⌋ₑ
-- Mathlib.MeasureTheory.PiSystem
/-- **Dynkin's π-λ theorem**:
Given a collection of sets closed under binary intersections, then the Dynkin system it
generates is equal to the σ-algebra it generates.
This result is known as the π-λ theorem.
A collection of sets closed under binary intersection is called a π-system (often requiring
additionally that it is non-empty, but we drop this condition in the formalization).
 -/
MeasurableSpace.DynkinSystem.generateFrom_eq : ∀ {α : Type u_3} {s : Set (Set α)} (hs : IsPiSystem s),
  MeasurableSpace.generateFrom s = (MeasurableSpace.DynkinSystem.generate s).toMeasurableSpace ⋯
-- Mathlib.Topology.Order.LiminfLimsup
Filter.Tendsto.isBoundedUnder_ge : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedGENhdsClass α] {f : Filter ι}
  {u : ι → α} {a : α}, Filter.Tendsto u f (nhds a) → Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.getElem_toArray_eq : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {i : ℕ} {h : i < r.toArray.size},
  r.toArray[i] = (Std.PRange.succMany? i r.lower).get ⋯
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- The ideal `I` equals the finprod `∏_v v^(val_v(I))`, when both sides are regarded as fractional
ideals of `R`.  -/
Ideal.finprod_heightOneSpectrum_factorization_coe : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {I : Ideal R},
  I ≠ 0 →
    ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R),
        ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) =
      ↑I
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negAddY_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P Q : Fin 3 → R) (u v : R),
  W'.negAddY (u • P) (v • Q) = ((u * v) ^ 2) ^ 3 * W'.negAddY P Q
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
/-- If `e : c.Embedding c'` is an embedding of complex shapes,
`f` and `g` are morphism between cochain complexes of shape `c`,
and `h` is an homotopy between the extensions `extendMap f e` and `extendMap g e`,
then this is the corresponding homotopy between `f` and `g`.  -/
Homotopy.ofExtend : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
              [inst_2 : CategoryTheory.Preadditive C] →
                {K L : HomologicalComplex C c} →
                  {f g : K ⟶ L} →
                    {e : c.Embedding c'} →
                      [e.IsRelIff] →
                        Homotopy (HomologicalComplex.extendMap f e) (HomologicalComplex.extendMap g e) → Homotopy f g
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.cancelBaseChange_tmul : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_8)
  (B : Type u_9) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (M : Type u_10) [inst_12 : AddCommGroup M] [inst_13 : Module R M]
  [inst_14 : Module A M] [inst_15 : IsScalarTower R A M] (m : M),
  (Algebra.IsPushout.cancelBaseChange R S A B M) (1 ⊗ₜ[A] m) = 1 ⊗ₜ[R] m
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.isLUB_sSup : ∀ {s : Set ℝ}, s.Nonempty → BddAbove s → IsLUB s (sSup s)
-- Mathlib.Algebra.Polynomial.Monomial
Polynomial.infinite : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], Infinite (Polynomial R)
-- Mathlib.RingTheory.Bialgebra.Convolution
BialgHom.toLinearMap_convPow : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R C] [inst_5 : Coalgebra.IsCocomm R C] (f : WithConv (C →ₐc[R] A))
  (n : ℕ), WithConv.toConv (f ^ n).ofConv.toLinearMap = WithConv.toConv f.ofConv.toLinearMap ^ n
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.toSubmonoid'_closure : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Set (Additive M)),
  AddSubmonoid.toSubmonoid' (AddSubmonoid.closure S) = Submonoid.closure (⇑Additive.ofMul ⁻¹' S)
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Meta.Grind.Params.eraseCasesTypes : Lean.Meta.Grind.Params → Lean.Name → Lean.CoreM Lean.Meta.Grind.Params
-- Lean.Meta.IndPredBelow
/-- This function adds an additional `below` discriminant to a matcher application and transforms each
alternative with the provided `transformAlt` function. The provided recursion context is used for
finding below proofs that correspond to discriminants and is extended with new proofs when calling
`transformAlt`. `belowParams` should contain parameters and motives for `below` applications where
the first `nrealParams` are parameters and the remaining are motives.
 -/
Lean.Meta.IndPredBelow.mkBelowMatcher : Lean.Meta.MatcherApp →
  Array Lean.Expr →
    ℕ →
      Lean.Meta.IndPredBelow.RecursionContext →
        (Lean.Meta.IndPredBelow.RecursionContext → Lean.Expr → Lean.MetaM Lean.Expr) →
          Lean.MetaM (Option (Lean.Expr × Lean.MetaM Unit))
-- Init.Data.SInt.Lemmas
Int8.le_toInt : ∀ (x : Int8), -2 ^ 7 ≤ x.toInt
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedAddCommGroup.toSeminormedAddGroup.eq_1 : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E],
  SeminormedAddCommGroup.toSeminormedAddGroup =
    { toNorm := inst.toNorm, toAddGroup := inst.toAddGroup, toPseudoMetricSpace := inst.toPseudoMetricSpace,
      dist_eq := ⋯ }
-- Mathlib.Probability.Kernel.CondDistrib
/-- The conditional expectation of a function `f` of the product `(X, Y)` is almost everywhere equal
to the integral of `y ↦ f(X, y)` against the `condDistrib` kernel.  -/
ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib' : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F}
  [inst_5 : NormedSpace ℝ F] [CompleteSpace F],
  Measurable X →
    AEMeasurable Y μ →
      MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
        μ[fun a => f (X a, Y a) | MeasurableSpace.comap X mβ] =ᵐ[μ] fun a =>
          ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
-- Std.Data.DHashMap.IteratorLemmas
_private.Std.Data.DHashMap.IteratorLemmas.0.Std.DHashMap.keysIter.eq_1 : ∀ {α : Type u} {β : α → Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap α β),
  m.keysIter = m.inner.keysIter
-- Mathlib.Algebra.Ring.CentroidHom
/-- Composition of `CentroidHom`s as a `CentroidHom`.  -/
CentroidHom.comp : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → CentroidHom α → CentroidHom α → CentroidHom α
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.instNontrivial : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R], Nontrivial (SkewPolynomial R)
-- Mathlib.MeasureTheory.Measure.Regular
/-- A measure `μ` is outer regular if `μ(A) = inf {μ(U) | A ⊆ U open}` for a measurable set `A`.

This definition implies the same equality for any (not necessarily measurable) set, see
`Set.measure_eq_iInf_isOpen`.  -/
MeasureTheory.Measure.OuterRegular : {α : Type u_1} → [inst : MeasurableSpace α] → [TopologicalSpace α] → MeasureTheory.Measure α → Prop
-- Mathlib.Order.Heyting.Basic
CoheytingAlgebra.toHNot : {α : Type u_4} → [self : CoheytingAlgebra α] → HNot α
-- Mathlib.Topology.Category.Sequential
Sequential.sequentialToTop_map : ∀ {X Y : CategoryTheory.InducedCategory TopCat Sequential.toTop} (f : X ⟶ Y), Sequential.sequentialToTop.map f = f.hom
-- Mathlib.Algebra.Group.Defs
CommGroup.toCommMonoid : {G : Type u} → [self : CommGroup G] → CommMonoid G
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Ring homomorphisms preserve subtraction.  -/
RingHom.map_sub : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocRing α] [inst_1 : NonAssocRing β] (f : α →+* β) (x y : α),
  f (x - y) = f x - f y
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.dvd_comp_C_mul_X_add_C_iff : ∀ {R : Type u} [inst : CommRing R] (p q : Polynomial R) (a b : R) [inst_1 : Invertible a],
  p ∣ q.comp (Polynomial.C a * Polynomial.X + Polynomial.C b) ↔
    p.comp (Polynomial.C ⅟a * (Polynomial.X - Polynomial.C b)) ∣ q
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {ι : Type u_2} {c : ComplexShape ι} {x y : TopPair.HomologyPretheory C c},
  x = y ↔ x.Hₚ = y.Hₚ ∧ x.H = y.H ∧ x.iso ≍ y.iso ∧ x.δ ≍ y.δ
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.instToMessageDataIndGroupInst : Lean.ToMessageData Lean.Elab.Structural.IndGroupInst
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.subset_closure : ∀ {α : Type u_2} (M : Matroid α) (X : Set α), autoParam (X ⊆ M.E) Matroid.subset_closure._auto_1 → X ⊆ M.closure X
-- Mathlib.CategoryTheory.Filtered.Basic
/-- Being cofiltered or empty is preserved by equivalence of categories.  -/
CategoryTheory.IsCofilteredOrEmpty.of_equivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (h : C ≌ D), CategoryTheory.IsCofilteredOrEmpty D
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.image_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} [inst_1 : CategoryTheory.Limits.HasImages C]
  (f : CategoryTheory.Over X), CategoryTheory.MonoOver.image.obj f = CategoryTheory.MonoOver.imageMonoOver f.hom
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.not_mem_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α}, k ∉ ∅
-- Mathlib.Order.Lattice
/-- The binary infimum, used to derive `Min α`  -/
Lattice.inf : {α : Type u} → [self : Lattice α] → α → α → α
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_mul_comm_of_le : ∀ {R : Type u_1} [inst : CommRing R] {m : Type u_3} {n : Type u_4} [inst_1 : DecidableEq m] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m] [inst_4 : Fintype n] (A : Matrix m n R) (B : Matrix n m R),
  Fintype.card n ≤ Fintype.card m →
    (A * B).charpoly = Polynomial.X ^ (Fintype.card m - Fintype.card n) * (B * A).charpoly
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Two morphisms are equal if there is a cofork whose projection is mono.  -/
CategoryTheory.Limits.eq_of_mono_cofork_π : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Cofork f g)
  [CategoryTheory.Mono t.π], f = g
-- Mathlib.Topology.MetricSpace.Isometry
Fin.appendIsometryOfEq_apply : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {n m l : ℕ} (hmln : m + l = n) (a : (Fin m → α) × (Fin l → α))
  (a_1 : Fin n), (Fin.appendIsometryOfEq hmln) a a_1 = Fin.append a.1 a.2 (Fin.cast ⋯ a_1)
-- Mathlib.Data.Set.Lattice
Set.iInter₂_eq_empty_iff : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α},
  ⋂ i, ⋂ j, s i j = ∅ ↔ ∀ (a : α), ∃ i j, a ∉ s i j