mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Transform
/-- Recursively transforms `input` using `pre` and `post` callbacks.

For each subexpression:
1. `pre` is invoked first; recursion continues according to the `TransformStep` result.
2. After recursion (if any), `post` is invoked on the resulting expression.

The expressions passed to `pre` and `post` may contain loose bound variables.
Use `Meta.transform` instead if you need operations like `whnf` or `inferType`
that require expressions without loose bound variables.

Results are cached using pointer equality (`ExprStructEq`), so structurally
identical subexpressions are transformed only once.
 -/
Lean.Core.transform : {m : Type → Type} →
  [inst : Monad m] →
    [MonadLiftT Lean.CoreM m] →
      [MonadControlT Lean.CoreM m] →
        Lean.Expr →
          (optParam (Lean.Expr → m Lean.TransformStep) fun x => pure Lean.TransformStep.continue) →
            (optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) → m Lean.Expr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → Bool},
  (Std.TreeMap.filter f t).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ t), f (t.getKey k h) t[k] = true
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.productiveRel_fstDone : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α₁ m β]
  [inst_2 : Std.Iterator α₂ m β] [inst_3 : Std.Iterators.Productive α₁ m] [inst_4 : Std.Iterators.Productive α₂ m]
  {it₁ : Std.IterM m β} {it₂ : Std.IterM m β},
  Std.Iterators.Types.Append.ProductiveRel α₁ α₂ m β (Std.IterM.Intermediate.appendSnd α₁ it₂) (it₁.append it₂)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.iUnion_isBasis_iUnion : ∀ {α : Type u_1} {M : Matroid α} {ι : Type u_2} (X I : ι → Set α),
  (∀ (i : ι), M.IsBasis (I i) (X i)) → M.Indep (⋃ i, I i) → M.IsBasis (⋃ i, I i) (⋃ i, X i)
-- Init.Data.List.TakeDrop
List.dropWhile_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {p : β → Bool} {l : List α},
  List.dropWhile p (List.filterMap f l) = List.filterMap f (List.dropWhile (fun a => Option.all p (f a)) l)
-- Mathlib.Algebra.Group.Action.Sum
Sum.smul_inr : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst_1 : SMul M β] (a : M) (c : β),
  a • Sum.inr c = Sum.inr (a • c)
-- Mathlib.LinearAlgebra.TensorProduct.Finiteness
/-- For any element `x` of `M ⊗[R] N`, there exists a finite subset `{ (m_i, n_i) }`
of `M × N` such that each `m_i` is distinct (we represent it as an element of `M →₀ N`),
such that `x` is equal to the sum of `m_i ⊗ₜ[R] n_i`.  -/
TensorProduct.exists_finsupp_left : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x : TensorProduct R M N),
  ∃ S, x = S.sum fun m n => m ⊗ₜ[R] n
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.darts_getElem_eq_getVert : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (n : ℕ) (h : n < p.darts.length),
  p.darts[n] = { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }
-- Mathlib.Logic.Equiv.Defs
EquivLike.coe_coe : ∀ {α : Sort u} {β : Sort v} {F : Sort u_1} [inst : EquivLike F α β] (e : F), ⇑↑e = ⇑e
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_prod_X_sub_C : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (s : Finset R),
  (∏ a ∈ s, (Polynomial.X - Polynomial.C a)).roots = s.val
-- Init.Data.FloatArray.Basic
FloatArray.push : FloatArray → Float → FloatArray
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_eq_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k fallback : α}, k ∈ t → t.getKeyD k fallback = k
-- Mathlib.Data.Sym.Sym2
/-- Partial map. If `f : ∀ a, p a → β` is a partial function defined on `a : α` satisfying `p`,
then `pmap f s h` is essentially the same as `map f s` but is defined only when all members of `s`
satisfy `p`, using the proof to apply `f`.
 -/
Sym2.pmap : {α : Type u_1} → {β : Type u_2} → {P : α → Prop} → ((a : α) → P a → β) → (s : Sym2 α) → (∀ a ∈ s, P a) → Sym2 β
-- Mathlib.Order.Filter.Partial
Filter.tendsto_iff_ptendsto : ∀ {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (s : Set α) (f : α → β),
  Filter.Tendsto f (l₁ ⊓ Filter.principal s) l₂ ↔ Filter.PTendsto (PFun.res f s) l₁ l₂
-- Mathlib.Probability.Kernel.Basic
/-- The Markov kernel to the `PUnit` type.  -/
ProbabilityTheory.Kernel.discard : (α : Type u_4) → [inst : MeasurableSpace α] → ProbabilityTheory.Kernel α PUnit.{u_5 + 1}
-- Mathlib.Algebra.Module.Presentation.Free
/-- The presentation of the `A`-module `G →₀ A` with generators indexed by `G`,
and no relation. (Note that there is an auxiliary universe parameter `w₁` for the
empty type `R`.)  -/
Module.presentationFinsupp : (A : Type u) → [inst : Ring A] → (G : Type w₀) → Module.Presentation A (G →₀ A)
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.instGeometricallyIntegralFiberToSpecResidueField : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (s : ↥S) [AlgebraicGeometry.GeometricallyIntegral f],
  AlgebraicGeometry.GeometricallyIntegral (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f s)
-- Mathlib.Analysis.Calculus.Deriv.Linear
LinearMap.hasDerivAtFilter : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {L : Filter (𝕜 × 𝕜)} (e : 𝕜 →ₗ[𝕜] F), HasDerivAtFilter (⇑e) (e 1) L
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.lratChecker.match_3.eq_4 : ∀ {α : Type u_1} {β : Type u_2} (motive : List (Std.Tactic.BVDecide.LRAT.Action β α) → Sort u_3) (id : ℕ) (c : β)
  (pivot : Std.Sat.Literal α) (rupHints : Array ℕ) (ratHints : Array (ℕ × Array ℕ))
  (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) (h_1 : Unit → motive [])
  (h_2 :
    (id : ℕ) →
      (rupHints : Array ℕ) →
        (tail : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
          motive (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail))
  (h_3 :
    (id : ℕ) →
      (c : β) →
        (rupHints : Array ℕ) →
          (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
            motive (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf))
  (h_4 :
    (id : ℕ) →
      (c : β) →
        (pivot : Std.Sat.Literal α) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf))
  (h_5 :
    (ids : Array ℕ) →
      (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
        motive (Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf)),
  (match Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf with
    | [] => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail => h_2 id rupHints tail
    | Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf => h_3 id c rupHints restPrf
    | Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf =>
      h_4 id c pivot rupHints ratHints restPrf
    | Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf => h_5 ids restPrf) =
    h_4 id c pivot rupHints ratHints restPrf
-- Lean.Util.Recognizers
_private.Lean.Util.Recognizers.0.Lean.Expr.listLit?.loop : Lean.Expr → List Lean.Expr → Option (Lean.Expr × List Lean.Expr)
-- Mathlib.Topology.GDelta.Basic
IsGδ.inter : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, IsGδ s → IsGδ t → IsGδ (s ∩ t)
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_range_succ_div_top : ∀ {M : Type u_4} (f : ℕ → M) {n : ℕ} [inst : CommGroup M],
  (∏ i ∈ Finset.range (n + 1), f i) / f n = ∏ i ∈ Finset.range n, f i
-- Mathlib.GroupTheory.Perm.ClosureSwap
/-- A permutation is a product of transpositions if and only if it has finite support.  -/
mem_closure_isSwap' : ∀ {α : Type u_2} [inst : DecidableEq α] {f : Equiv.Perm α},
  f ∈ Subgroup.closure {σ | σ.IsSwap} ↔ (MulAction.fixedBy α f)ᶜ.Finite
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J],
  W.transfiniteCompositionsOfShape J ≤ W → W.IsStableUnderTransfiniteCompositionOfShape J
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- A regular pairing for `Subcomplex.unionProd.{u} Λ[m + 1, k.castSucc] ∂Δ[n]`
when `k : Fin (m + 1)` and `n : ℕ`.  -/
SSet.prodStdSimplex.pairing : {m : ℕ} → (k : Fin (m + 2)) → (n : ℕ) → ((SSet.horn (m + 1) k).unionProd (SSet.boundary n)).Pairing
-- Init.Data.Array.Lemmas
Array.getElem_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {xs : Array α} {i : ℕ} (hi : i < (Array.map f xs).size),
  (Array.map f xs)[i] = f xs[i]
-- Mathlib.Data.FunLike.Basic
/-- The coercion from `F` to a function.  -/
DFunLike.coe : {F : Sort u_1} → {α : outParam (Sort u_2)} → {β : outParam (α → Sort u_3)} → [self : DFunLike F α β] → F → (a : α) → β a
-- Init.Data.Ord.Basic
Ordering.then.eq_1 : ∀ (b : Ordering), Ordering.eq.then b = b
-- Init.Data.UInt.Lemmas
UInt32.toNat_lt_usizeSize : ∀ (n : UInt32), n.toNat < USize.size
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If the interior of the interval `integrableExpSet X μ` is nonempty,
then `X` is a.e. measurable.  -/
ProbabilityTheory.aemeasurable_of_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ},
  v ∈ interior (ProbabilityTheory.integrableExpSet X μ) → AEMeasurable X μ
-- Mathlib.Analysis.InnerProductSpace.Basic
_private.Mathlib.Analysis.InnerProductSpace.Basic.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_lt_map_iff_of_injective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N},
  Function.Injective ⇑f → ∀ {H K : AddSubgroup G}, AddSubgroup.map f H < AddSubgroup.map f K ↔ H < K
-- Mathlib.Data.Countable.Basic
WithTop.instUncountable : ∀ {α : Type u} [Uncountable α], Uncountable (WithTop α)
-- Mathlib.Algebra.Category.FGModuleCat.Colimits
FGModuleCat.instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG : ∀ {k : Type u} [inst : Ring k],
  CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.coe_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (v : NumberField.FinitePlace K) (x : K), v x = ↑v x
-- Init.Data.List.Perm
List.isSetoid : (α : Type u_1) → Setoid (List α)
-- Mathlib.Topology.Inseparable
SeparationQuotient.image_mk_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  SeparationQuotient.mk '' closure s = closure (SeparationQuotient.mk '' s)
-- Init.Data.Array.Int
Array.sum_le_max_mul_length_int : ∀ {xs : Array ℤ} (h : xs ≠ #[]), xs.sum ≤ xs.max h * ↑xs.size
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.InducedCategory.homAddEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  {F : D → C} {X Y : CategoryTheory.InducedCategory C F} (f : X ⟶ Y),
  CategoryTheory.InducedCategory.homAddEquiv f = f.hom
-- Mathlib.Tactic.Linarith.Datatypes
/-- `l.zfind n` returns the value associated with key `n` if there is one, and 0 otherwise.
 -/
Mathlib.Tactic.Linarith.Linexp.zfind : ℕ → Mathlib.Tactic.Linarith.Linexp → ℤ
-- Mathlib.Data.Multiset.Basic
Multiset.strongInductionOn_eq : ∀ {α : Type u_1} {p : Multiset α → Sort u_3} (s : Multiset α)
  (H : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s),
  s.strongInductionOn H = H s fun t _h => t.strongInductionOn H
-- Mathlib.Algebra.Group.Units.Defs
Units.commute_coe_inv : ∀ {α : Type u} [inst : Monoid α] (a : αˣ), Commute ↑a ↑a⁻¹
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.FineSubfamilyOn.index_subset : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v : VitaliFamily μ} {f : X → Set (Set X)} {s : Set X} (h : v.FineSubfamilyOn f s), ∀ p ∈ h.index, p.1 ∈ s
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.completion_id : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G],
  (NormedAddGroupHom.id G).completion = NormedAddGroupHom.id (UniformSpace.Completion G)
-- Lean.Elab.RecAppSyntax
/-- Retrieve (if available) the syntax object attached to a recursive application.
 -/
Lean.getRecAppSyntax? : Lean.Expr → Option Lean.Syntax
-- Aesop.Rule.Name
Aesop.RuleName.compare : Aesop.RuleName → Aesop.RuleName → Ordering
-- Mathlib.MeasureTheory.PiSystem
generatePiSystem_eq : ∀ {α : Type u_1} {S : Set (Set α)}, IsPiSystem S → generatePiSystem S = S
-- Mathlib.Topology.Sets.Closeds
/-- See Note [custom simps projection].  -/
TopologicalSpace.Closeds.Simps.coe : {α : Type u_2} → [inst : TopologicalSpace α] → TopologicalSpace.Closeds α → Set α
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.PreservesKernel.iso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f] [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G],
  CategoryTheory.Limits.PreservesKernel.iso G f =
    (CategoryTheory.Limits.isLimitOfHasKernelOfPreservesLimit G f).conePointUniqueUpToIso
      (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.parallelPair (G.map f) 0))
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.karoubi.F'_obj_p : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] (X : A),
  ((CategoryTheory.Abelian.LeftResolution.karoubi.F' Λ).obj X).p =
    CategoryTheory.CategoryStruct.id (Λ.F.obj X) - Λ.F.map 0
-- Mathlib.Computability.NFA
NFA.eval_singleton : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (a : α), M.eval [a] = M.stepSet M.start a
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.symm_toCoalgEquiv : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B), ↑e.symm = (↑e).symm
-- Mathlib.Geometry.RingedSpace.Basic
AlgebraicGeometry.RingedSpace.zeroLocus.eq_1 : ∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
  (s : Set ↑(X.presheaf.obj (Opposite.op U))), X.zeroLocus s = ⋂ f ∈ s, (↑(X.basicOpen f))ᶜ
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.coe_C : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
  ↑(MvPolynomial.C a) = (algebraMap R (DividedPowerAlgebra R M)) a
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Ioi_of_strictAntiOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Ici a) →
    StrictAntiOn f (Set.Ici a) → Filter.Tendsto f Filter.atTop Filter.atBot → f '' Set.Ioi a = Set.Iio (f a)
-- Mathlib.SetTheory.Cardinal.Free
nonempty_semiring_iff : ∀ (α : Type u), Nonempty (Semiring α) ↔ Nonempty α
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.evalFacProp : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] {l : Profinite.NobelingProof.Products I} (J : I → Prop),
  (∀ a ∈ ↑l, J a) →
    ∀ [inst_1 : (j : I) → Decidable (J j)],
      ⇑(Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C J) l) ∘
          Profinite.NobelingProof.ProjRestrict C J =
        ⇑(Profinite.NobelingProof.Products.eval C l)
-- Mathlib.Data.Finset.Card
/-- Suppose that, given objects defined on all nonempty strict subsets of any nontrivial finset `s`,
one knows how to define an object on `s`. Then one can inductively define an object on all finsets,
starting from singletons and iterating.

TODO: Currently this can only be used to prove properties.
Replace `Finset.Nonempty.exists_eq_singleton_or_nontrivial` with computational content
in order to let `p` be `Sort`-valued.  -/
Finset.Nonempty.strong_induction : ∀ {α : Type u_1} {p : (s : Finset α) → s.Nonempty → Prop},
  (∀ (a : α), p {a} ⋯) →
    (∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯) →
      ∀ ⦃s : Finset α⦄ (hs : s.Nonempty), p s hs
-- Mathlib.Data.Num.ZNum
PosNum.to_int_eq_succ_pred : ∀ (n : PosNum), ↑n = ↑↑n.pred' + 1
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_single_same : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] (a : Γ) (r : R),
  ((HahnSeries.single a) r).coeff a = r
-- Mathlib.Topology.Separation.Regular
instT4SpaceOfT1SpaceOfNormalSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] [NormalSpace X], T4Space X
-- Mathlib.Tactic.Sat.FromLRAT
/-- The representation of a global clause.  -/
Mathlib.Tactic.Sat.Clause : Type
-- Init.Data.List.Lemmas
List.any_replicate : ∀ {α : Type u_1} {f : α → Bool} {n : ℕ} {a : α}, (List.replicate n a).any f = if n = 0 then false else f a
-- Mathlib.Data.Sym.Basic
Sym.map_zero : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Sym.map f 0 = 0
-- Mathlib.Data.Prod.Basic
Prod.instAntisymmLexOfIsStrictOrder : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsStrictOrder α r] [Std.Antisymm s],
  Std.Antisymm (Prod.Lex r s)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.Equiv.mapWithPostcondition : ∀ {α₁ α₂ β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : Monad n] [inst_3 : LawfulMonad n] [inst_4 : Std.Iterator α₁ m β] [inst_5 : Std.Iterator α₂ m β]
  [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Std.Iterators.PostconditionT n γ} {ita : Std.IterM m β}
  {itb : Std.IterM m β},
  ita.Equiv itb → (Std.IterM.mapWithPostcondition f ita).Equiv (Std.IterM.mapWithPostcondition f itb)
-- Mathlib.RingTheory.Polynomial.GaussNorm
PowerSeries.gaussNorm_C : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) {c : ℝ} (r : R)
  [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ], 0 ≤ c → PowerSeries.gaussNorm (⇑v) c (PowerSeries.C r) = v r
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.δ_comp_σ_succ'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.succ →
    ∀ {Z : C} (h : X.obj { len := n } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.δ j) (CategoryTheory.CategoryStruct.comp (X.σ i) h) = h
-- Mathlib.Util.AtomM
/-- If an atomic expression has already been encountered, return `true`, the index and the stored
form of the atom (which will be defeq at the specified transparency, but not necessarily
syntactically equal). If the atomic expression has *not* already been encountered, store it in the
list of atoms, and return the new index (and the stored form of the atom, which will be itself).

In a normalizing tactic, the expression returned by `AtomM.containsThenAddQ` should be considered
the normal form.

This is a strongly-typed version of `AtomM.containsThenAdd` for code using `Qq`.
 -/
Mathlib.Tactic.AtomM.containsThenAddQ : {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → Mathlib.Tactic.AtomM (Bool × ℕ × { e' // «$e» =Q «$e'» })
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_eq_ite : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} {f : ι → M} (a : ι),
  (∀ b ∈ s, b ≠ a → f b = 1) → ∏ x ∈ s, f x = if a ∈ s then f a else 1
-- Mathlib.CategoryTheory.FinCategory.AsType
/-- The constructed category (`AsType α`) is indeed equivalent to `α`.  -/
CategoryTheory.FinCategory.equivAsType : (α : Type u_1) →
  [inst : Fintype α] →
    [inst_1 : CategoryTheory.SmallCategory α] →
      [inst_2 : CategoryTheory.FinCategory α] → CategoryTheory.FinCategory.AsType α ≌ α
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_eta : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R),
  MvPolynomial.eval₂ MvPolynomial.C MvPolynomial.X p = p
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.PollSources.timeout : {α β : Type} → Std.Http.Server.Connection.PollSources✝ α β → Std.Time.Millisecond.Offset
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.funLike : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → FunLike (A →ₐc[R] B) A B
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_7.eq : ∀ {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_2 :
    Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Sort u}
  {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} (t : Task Lean.Elab.Tactic.TacticParsedSnapshot)
  (F_1 : (t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t)
  (F_2 :
    (t :
        Lean.Language.TransformedSnap
          (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t)
  (F_5 :
    (t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t)
  (F_6 :
    (t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t)
  (F_7 :
    (t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t)
  (F_8 :
    (t : Task Lean.Elab.Tactic.TacticParsedSnapshot) → Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t),
  Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_7 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 =
    F_8 t (Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_7.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8).2