mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Neighborhoods
/-- **Alias** of `interior_setOfPred_eq`. -/
interior_setOf_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop}, interior {x | p x} = {x | ∀ᶠ (y : X) in nhds x, p y}
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.eval.eq_1 : Std.Tactic.BVDecide.Gate.and.eval = fun x1 x2 => x1 && x2
-- Mathlib.Tactic.Rify
/-- The `Simp.Context` generated by `rify` (with no optional arguments or local context).  -/
Mathlib.Tactic.Rify.mkRifyContext : Lean.MetaM Lean.Meta.Simp.Context
-- Mathlib.Topology.Subpath
/-- **Alias** of `Set.Icc.convexComb_zero`. -/
Path.subpathAux_zero : ∀ {a b : ℝ} (x y : ↑(Set.Icc a b)), Set.Icc.convexComb x y 0 = x
-- Mathlib.Data.Semiquot
Semiquot.get_mem : ∀ {α : Type u_1} {q : Semiquot α} (p : q.IsPure), q.get p ∈ q
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.restrict_prod_eq_prod_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (s : Set α),
  (μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ Set.univ)
-- Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Meta.NormNum.jacobiSymNat.even_odd₅ : ∀ (a b c : ℕ) (r : ℤ),
  a % 2 = 0 →
    b % 8 = 5 → a / 2 = c → Mathlib.Meta.NormNum.jacobiSymNat c b = r → Mathlib.Meta.NormNum.jacobiSymNat a b = -r
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.disjoint_ker_aeval_of_isCoprime : ∀ {R : Type u} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : M →ₗ[R] M)
  {p q : Polynomial R}, IsCoprime p q → Disjoint ((Polynomial.aeval f) p).ker ((Polynomial.aeval f) q).ker
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- The multiplicative closure of `W` is the smallest multiplicative property greater than or equal
to `W`.  -/
CategoryTheory.MorphismProperty.multiplicativeClosure_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W W' : CategoryTheory.MorphismProperty C)
  [W'.IsMultiplicative], W.multiplicativeClosure ≤ W' ↔ W ≤ W'
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_mul_self : ∀ (a b : ℤ), a.tdiv b * b = a - a.tmod b
-- Mathlib.Analysis.Quaternion
Quaternion.coeComplex_mul : ∀ (z w : ℂ), ↑(z * w) = ↑z * ↑w
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.op_top : ∀ {G : Type u_2} [inst : Group G], ⊤.op = ⊤
-- Mathlib.Tactic.GRewrite.Elab
/-- `nth_grewrite n₁ ... nₖ [e₁, ..., eₙ]` is a variant of `grewrite` that for each expression
`eᵢ : R aᵢ bᵢ` only replaces the `n₁, ..., nₖ`th occurrence of `aᵢ` with `bᵢ`.
Use `nth_grewrite n₁ ... nₖ [← eᵢ]` to rewrite in the other direction, replacing occurrences of `bᵢ`
with `aᵢ`.

If an expression `e` is a defined constant, then the equational theorems associated with `e` are
used. This provides a convenient way to unfold `e`. If `e` has parameters, the tactic will try to
fill these in by unification with the matching part of the target. Parameters are only filled in
once per rule, restricting which later rewrites can be found. Parameters that are not filled in
after unification will create side goals.

To be able to use `nth_grewrite`, the relevant lemmas need to be tagged with `@[gcongr]`.
To rewrite inside a transitive relation, you can also give it an `IsTrans` instance.
Rewriting with a strict inequality `a < b` may change the strictness of the goal,
replacing a goal `_ < _` by `_ ≤ _`. If this is not possible, then `a < b` is treated as `a ≤ b`.

* `nth_grewrite n₁ ... nₖ [← e]` applies the rewrite rule `e : R a b` in the reverse direction,
  replacing the `n₁, ..., nₖ`th occurrences of `b` with `a`.
* `nth_grewrite (config := cfg) n₁ ... nₖ [e₁, ..., eₙ]` uses `cfg` as configuration. See
  `GRewrite.Config` for details.
  * To let `nth_grewrite` unfold more aggressively, as in `erw`, use
    `nth_grewrite (transparency := default) n₁ ... nₖ [e₁, ..., eₙ]`.
  * `nth_grewrite +implicationHyp n₁ ... nₖ [e₁, ..., eₙ]` interprets `· → ·` as a relation.
* `nth_grewrite n₁ ... nₖ [e₁, ..., eₙ] at l` rewrites at the location(s) `l`.
 -/
Mathlib.Tactic.GRewrite.tacticNth_grewrite_____ : Lean.ParserDescr
-- Init.Data.Array.Lemmas
Array.back_mem : ∀ {α : Type u_1} {xs : Array α} (h : 0 < xs.size), xs.back h ∈ xs
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.subNegMonoid : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [SubNegMonoid G] → SubNegMonoid (l.Germ G)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Replacing a point in an affine independent triple with a collinear point preserves affine
independence.  -/
affineIndependent_of_affineIndependent_collinear_ne : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ p : P},
  AffineIndependent k ![p₁, p₂, p₃] → Collinear k {p₂, p₃, p} → p₂ ≠ p → AffineIndependent k ![p₁, p₂, p]
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.assoc_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y}
  {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (Q : CategoryTheory.Limits.IsLimit sYZ)
  (s : CategoryTheory.Limits.BinaryFan sXY.pt Z),
  (CategoryTheory.Limits.BinaryFan.assoc Q s).snd =
    Q.lift (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp s.fst sXY.snd) s.snd)
-- Lean.Elab.Tactic.Simp
/-- If `stx` is the syntax of a `simp`, `simp_all` or `dsimp` tactic invocation, and
`usedSimps` is the set of simp lemmas used by this invocation, then `mkSimpOnly`
creates the syntax of an equivalent `simp only`, `simp_all only` or `dsimp only`
invocation.
 -/
Lean.Elab.Tactic.mkSimpOnly : Lean.Syntax → Lean.Meta.Simp.UsedSimps → Lean.MetaM Lean.Syntax
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- Extend `T : Set α → E →L[ℝ] F` to `(α → E) → F` (for integrable functions `α → E`). We set it to
0 if the function is not integrable or if the target space is not complete.  -/
MeasureTheory.setToFun : {α : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              {m : MeasurableSpace α} →
                (μ : MeasureTheory.Measure α) →
                  (T : Set α → E →L[ℝ] F) → {C : ℝ} → MeasureTheory.DominatedFinMeasAdditive μ T C → (α → E) → F
-- Mathlib.Analysis.Normed.Unbundled.FiniteExtension
/-- For any `K`-basis of `L`, `B.norm` is bounded with respect to multiplication. That is,
`∃ (c : ℝ), c > 0` such that ` ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y`.  -/
Module.Basis.norm_mul_le_const_mul_norm : ∀ {K : Type u_1} {L : Type u_2} [inst : NormedField K] [inst_1 : Ring L] [inst_2 : Algebra K L] {ι : Type u_3}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] {B : Module.Basis ι K L} {i : ι},
  B i = 1 → IsNonarchimedean norm → ∃ c, ∃ (_ : 0 < c), ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.natDegree_eq_reverse_natDegree_add_natTrailingDegree : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), f.natDegree = f.reverse.natDegree + f.natTrailingDegree
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.resolveDottedIdentFn.throwNoExpectedType : Lean.Name → {α : Type} → Lean.Elab.TermElabM α
-- Mathlib.Algebra.Star.LinearMap
Pi.intrinsicStar_comul : ∀ {R : Type u_5} [inst : CommSemiring R] [inst_1 : StarRing R] {n : Type u_8} [inst_2 : DecidableEq n]
  {B : n → Type u_9} [inst_3 : (i : n) → AddCommMonoid (B i)] [inst_4 : (i : n) → Module R (B i)]
  [inst_5 : (i : n) → StarAddMonoid (B i)] [inst_6 : ∀ (i : n), StarModule R (B i)] [inst_7 : Fintype n]
  [inst_8 : (i : n) → CoalgebraStruct R (B i)],
  (∀ (i : n),
      star (WithConv.toConv CoalgebraStruct.comul) =
        WithConv.toConv (↑(TensorProduct.comm R (B i) (B i)) ∘ₗ CoalgebraStruct.comul)) →
    star (WithConv.toConv CoalgebraStruct.comul) =
      WithConv.toConv (↑(TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) ∘ₗ CoalgebraStruct.comul)
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.instMulActionSpecialLinearGroupFixedDetMatrix : (n : Type u_1) →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      (R : Type u_2) →
        [inst_2 : CommRing R] → (m : R) → MulAction (Matrix.SpecialLinearGroup n R) (FixedDetMatrix n R m)
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_nat : Order.cof ℕ = Cardinal.aleph0
-- Mathlib.Data.Nat.Log
Nat.clog_zero_left : ∀ (n : ℕ), Nat.clog 0 n = 0
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.algebraMap_germ : ∀ {R : Type u} [inst : CommRing R] (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hxU : x ∈ U),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom (algebraMap R ((AlgebraicGeometry.structureSheafInType R R).obj.obj (Opposite.op U))))
      ((AlgebraicGeometry.structurePresheafInCommRingCat R).germ U x hxU) =
    AlgebraicGeometry.StructureSheaf.toStalk R x
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.isRoot_of_mem_roots : ∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R}, a ∈ p.roots → p.IsRoot a
-- Lean.Meta.CollectMVars
/-- Collect the metavariables which `mvarId` depends on. These are the metavariables
which appear in the type and local context of `mvarId`, as well as the
metavariables which *those* metavariables depend on, etc.
 -/
Lean.MVarId.getMVarDependencies : Lean.MVarId → optParam Bool false → Lean.MetaM (Std.HashSet Lean.MVarId)
-- Mathlib.Analysis.Convex.Function
ConcaveOn.convex_hypograph : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulMono 𝕜 β] {s : Set E} {f : E → β}, ConcaveOn 𝕜 s f → Convex 𝕜 {p | p.1 ∈ s ∧ p.2 ≤ f p.1}
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.coconeOfCoconeCurry_pt : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C)
  {D : CategoryTheory.Limits.DiagramOfCocones (CategoryTheory.Functor.curry.obj G)}
  (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) (c : CategoryTheory.Limits.Cocone G),
  (CategoryTheory.Limits.coconeOfCoconeCurry G Q c).pt = c.pt
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
/-- **Alias** of `FractionalIdeal.one_mem_inv_coe_ideal`. -/
one_mem_inv_coe_ideal : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] [inst_4 : IsDomain A] {I : Ideal A}, I ≠ ⊥ → 1 ∈ (↑I)⁻¹
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- **Alias** of `CategoryTheory.Functor.PreservesEpimorphisms.ofRetract`. -/
CategoryTheory.Functor.preservesEpimorphisms.ofRetract : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (r : CategoryTheory.Retract G F) [F.PreservesEpimorphisms], G.PreservesEpimorphisms
-- Mathlib.Topology.Algebra.Group.Pointwise
IsDiscrete.exists_nhds_eq_one_of_image_mulRight_inter_nonempty : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (S : Subgroup G),
  IsDiscrete ↑S → ∃ U ∈ nhds 1, U⁻¹ = U ∧ ∀ g ∈ S, ((fun x => x * g) '' U ∩ U).Nonempty → g = 1
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.le_sum_of_subadditive : ∀ {α : Type u_5} {β : Type u_6} [inst : AddMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedAddMonoid β] (f : α → β),
  f 0 ≤ 0 → (∀ (a b : α), f (a + b) ≤ f a + f b) → ∀ (l : List α), f l.sum ≤ (List.map f l).sum
-- Mathlib.Data.Finset.Lattice.Union
Finset.sup'_biUnion : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] (f : β → α) [inst_1 : DecidableEq β]
  {s : Finset γ} (Hs : s.Nonempty) {t : γ → Finset β} (Ht : ∀ (b : γ), (t b).Nonempty),
  (s.biUnion t).sup' ⋯ f = s.sup' Hs fun b => (t b).sup' ⋯ f
-- Init.Data.List.Lex
List.not_lex_lt : ∀ {α : Type u_1} [inst : LT α] {l₁ l₂ : List α}, ¬List.Lex (fun x1 x2 => x1 < x2) l₁ l₂ ↔ l₂ ≤ l₁
-- Std.Http.Data.Method
Std.Http.Method.checkout.sizeOf_spec : sizeOf Std.Http.Method.checkout = 1
-- Mathlib.Order.Filter.Basic
Filter.eventuallyEq_top : ∀ {α : Type u} {β : Type v} {f g : α → β}, f =ᶠ[⊤] g ↔ f = g
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  [inst_5 : CategoryTheory.BraidedCategory C] (X Y : C),
  ((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).hom.app
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app
      ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) X Y)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map (β_ X Y).hom)
        (CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) Y X))
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.closure_pow_le : ∀ {G : Type u_2} [inst : Group G] {s : Set G} {n : ℕ}, Subgroup.closure (s ^ n) ≤ Subgroup.closure s
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.strictMono_semilength : StrictMono DyckWord.semilength
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (α : Type w)
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] {X Y : CategoryTheory.Functor (CategoryTheory.Discrete α) C}
  (β : X ⟶ Y) (x : Finset (CategoryTheory.Discrete α)),
  ((CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α).map β).app x =
    CategoryTheory.Limits.Sigma.map fun x_1 => β.app ↑x_1
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.realize_boundedFormula_top : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u_3} {n : ℕ} {φ : L.BoundedFormula α n}
  {v : α → ↥⊤} {xs : Fin n → ↥⊤}, φ.Realize v xs ↔ φ.Realize (Subtype.val ∘ v) (Subtype.val ∘ xs)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit.inj : ∀ {α : Type u} {l l_1 : Std.Sat.Literal α},
  Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l =
      Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l_1 →
    l = l_1
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (Polynomial.X ^ n).toFinsupp = AddMonoidAlgebra.single n 1
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
/-- `abs a`, denoted `|a|`, is the absolute value of `a`  -/
abs : {α : Type u_1} → [Lattice α] → [AddGroup α] → α → α
-- Mathlib.Combinatorics.Matroid.Map
/-- `M.restrictSubtype M.E` is isomorphic to `M`.  -/
Matroid.map_val_restrictSubtype_ground_eq : ∀ {α : Type u_1} (M : Matroid α), (M.restrictSubtype M.E).map Subtype.val ⋯ = M
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.pow_mem : ∀ {R : Type u_1} [inst : Ring R] (s : Subring R) {x : R}, x ∈ s → ∀ (n : ℕ), x ^ n ∈ s
-- Mathlib.Data.Int.Bitwise
Int.bitwise.eq_4 : ∀ (f : Bool → Bool → Bool) (m n : ℕ),
  Int.bitwise f (Int.negSucc m) (Int.negSucc n) = Int.natBitwise (fun x y => f (!x) !y) m n
-- Mathlib.Geometry.Convex.Cone.DualFinite
/-- The double dual of a dually finitely generated cone is the cone itself.  -/
PointedCone.DualFG.dual_flip_dual : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} {C : PointedCone R M},
  PointedCone.DualFG p.flip C → PointedCone.dual p.flip ↑(PointedCone.dual p ↑C) = C
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.maxEntryD.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (x_1 : α × β) →
          ((fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback) →
            ((size : ℕ) →
                (k : α) →
                  (v : β) →
                    (l : Std.DTreeMap.Internal.Impl α fun x => β) →
                      (x : α × β) →
                        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β) →
                      (l : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (size_1 : ℕ) →
                          (k_1 : α) →
                            (v_1 : β) →
                              (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                                (fallback : α × β) →
                                  motive
                                    (Std.DTreeMap.Internal.Impl.inner size k v l
                                      (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
                                    fallback) →
                motive x x_1
-- Lean.PrettyPrinter.Delaborator.FieldNotation
/-- If `f` is a function that can be used for field notation,
returns the field name to use and the argument index for the object of the field notation.
 -/
Lean.PrettyPrinter.Delaborator.fieldNotationCandidate? : Lean.Expr → Array Lean.Expr → Bool → Lean.MetaM (Option (Lean.Name × ℕ))
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.foldM_filterMapWithPostcondition.match_1.splitter : {γ : Type u_1} →
  (motive : Option γ → Sort u_2) →
    (__x : Option γ) →
      ((c : γ) → motive (some c)) → ((x : Option γ) → (∀ (c : γ), x = some c → False) → motive x) → motive __x
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.mem_stabilizer_set_iff_vadd_set_subset : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} {s : Set α},
  s.Finite → (a ∈ AddAction.stabilizer G s ↔ a +ᵥ s ⊆ s)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.comp_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ sq₃ : CategoryTheory.Square C} (f : sq₁.Hom sq₂)
  (g : sq₂.Hom sq₃), (f.comp g).τ₃ = CategoryTheory.CategoryStruct.comp f.τ₃ g.τ₃
-- Mathlib.RingTheory.MvPowerSeries.Rename
_private.Mathlib.RingTheory.MvPowerSeries.Rename.0.MvPowerSeries.coeff_renameFun : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [inst : Filter.TendstoCofinite f] [inst_1 : Semiring R]
  {p : MvPowerSeries σ R} {x : τ →₀ ℕ},
  (MvPowerSeries.coeff x) (MvPowerSeries.renameFun f p) = ∑ x ∈ ⋯.toFinset, (MvPowerSeries.coeff x) p
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.subset_lieSpan : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {s : Set L},
  s ⊆ ↑(LieSubalgebra.lieSpan R L s)
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.inv_add_inv_ennreal : ∀ {p q : ℝ}, p.HolderConjugate q → (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1
-- Mathlib.Analysis.Normed.Group.Defs
ENormedAddCommMonoid.toENormedAddMonoid : {E : Type u_8} → [inst : TopologicalSpace E] → [self : ENormedAddCommMonoid E] → ENormedAddMonoid E
-- Lean.Declaration
Lean.RecursorVal.isUnsafeEx : Lean.RecursorVal → Bool
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
SeparationQuotient.liftNormedAddGroupHom_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
  (f : NormedAddGroupHom M N) (hf : ∀ (x : M), ‖x‖ = 0 → f x = 0) (a : SeparationQuotient M),
  (SeparationQuotient.liftNormedAddGroupHom f hf) a = (SeparationQuotient.liftContinuousAddMonoidHom ↑f ⋯) a
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.UsedSimps.mk.inj : ∀ {map : Lean.PHashMap Lean.Meta.Origin ℕ} {size : ℕ} {map_1 : Lean.PHashMap Lean.Meta.Origin ℕ} {size_1 : ℕ},
  { map := map, size := size } = { map := map_1, size := size_1 } → map = map_1 ∧ size = size_1
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.coe_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : SemilatticeInf β]
  [inst_3 : ContinuousInf β] (f g : C(α, β)), ⇑(f ⊓ g) = ⇑f ⊓ ⇑g
-- Mathlib.GroupTheory.Index
AddSubgroup.index_inf_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.index ≠ 0 → K.index ≠ 0 → (H ⊓ K).index ≠ 0
-- Std.Http.Data.Method
/-- A method is a verb that describes the action to be performed.

Covers all methods in the IANA HTTP Method Registry.

* Reference: https://www.iana.org/assignments/http-methods/http-methods.xhtml
 -/
Std.Http.Method : Type
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_eq_getD_back?_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {fallback : α},
  t.maxKeyD fallback = t.keysArray.back?.getD fallback
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.ι_descMapObj : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) [inst_1 : X.HasMap p] {A : C} {j : J}
  (φ : (i : I) → p i = j → (X i ⟶ A)) (i : I) (hi : p i = j),
  CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) (X.descMapObj p φ) = φ i hi
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_intCast_mul_add : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIocMod hp a (↑m * p + b) = toIocMod hp a b
-- Lean.Elab.Tactic.Rewrite
Lean.Elab.Tactic.rewriteTarget : Lean.Syntax → Bool → optParam Lean.Meta.Rewrite.Config { } → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.integral_norm_condExp_rpow_le : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {p : ℝ},
  1 ≤ p →
    ∀ {f : α → E},
      MeasureTheory.Integrable (fun x => ‖f x‖ ^ p) μ → ∫ (x : α), ‖μ[f | m] x‖ ^ p ∂μ ≤ ∫ (x : α), ‖f x‖ ^ p ∂μ
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  (f : W ⟶ X) [inst_2 : W.Over S] [inst_3 : X.Over S] [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰]
  [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  [inst_6 : Q.HasOfPostcompProperty Q] [inst_7 : Q.IsStableUnderBaseChange] [inst_8 : Q.IsStableUnderComposition]
  (hX : Q (X ↘ S)) (hW : Q (W ↘ S)) (hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) (x : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).X x =
    (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Hom.asOverProp f S)
        (AlgebraicGeometry.Scheme.Hom.asOverProp (𝒰.f x) S)).left