mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Restrict the domain and codomain of a `MonoidHom`.  -/
MonoidHom.restrict : {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        {M' : Submonoid M} → {N' : Submonoid N} → {f : M →* N} → Set.MapsTo ⇑f ↑M' ↑N' → ↥M' →* ↥N'
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- Given a family of measures `μ : (n : ℕ) → Measure (Π i : Iic n, X i)`, the induced family
equals `μ` over the intervals `Iic n`.  -/
MeasureTheory.inducedFamily_Iic : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (μ : (n : ℕ) → MeasureTheory.Measure ((i : ↥(Finset.Iic n)) → X ↑i)) (n : ℕ),
  MeasureTheory.inducedFamily μ (Finset.Iic n) = μ n
-- Mathlib.RingTheory.Smooth.Basic
/-- Smooth is stable under base change.  -/
Algebra.Smooth.baseChange : ∀ (R : Type u_4) [inst : CommRing R] (A : Type u_5) (B : Type u_6) [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.Smooth R A], Algebra.Smooth B (TensorProduct R B A)
-- Mathlib.Condensed.Discrete.Colimit
Condensed.lanPresheafNatIso_hom_app : ∀ {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))}
  (hF : (S : Profinite) → CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) (S : Profiniteᵒᵖ),
  (Condensed.lanPresheafNatIso hF).hom.app S =
    CategoryTheory.Limits.colimit.desc
      ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op (Opposite.op (Opposite.unop S))).comp
        (FintypeCat.toProfinite.op.comp F))
      (Profinite.Extend.cocone F (Opposite.unop S))
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.zero_apply : ∀ {p : ENNReal} {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → SeminormedAddCommGroup (β i)] (i : ι),
  WithLp.ofLp 0 i = 0
-- Mathlib.CategoryTheory.Yoneda
/-- We have a type-level equivalence between natural transformations from the yoneda embedding
and elements of `F.obj X`, without any universe switching.
 -/
CategoryTheory.yonedaEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} → (CategoryTheory.yoneda.obj X ⟶ F) ≃ F.obj (Opposite.op X)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.inv_whiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G H : CategoryTheory.Functor D E} (α : G ⟶ H) [inst_3 : CategoryTheory.IsIso α],
  CategoryTheory.inv (F.whiskerLeft α) = F.whiskerLeft (CategoryTheory.inv α)
-- Mathlib.Data.Set.Enumerate
Set.enumerate_mem : ∀ {α : Type u_1} (sel : Set α → Option α),
  (∀ (s : Set α) (a : α), sel s = some a → a ∈ s) →
    ∀ {s : Set α} {n : ℕ} {a : α}, Set.enumerate sel s n = some a → a ∈ s
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMk₂_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 2}
  (app₀ : f.obj' 0 _proof_245✝ ≅ g.obj' 0 _proof_245✝) (app₁ : f.obj' 1 _proof_246✝ ≅ g.obj' 1 _proof_246✝)
  (app₂ : f.obj' 2 _proof_247✝ ≅ g.obj' 2 _proof_247✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝)
          app₁.hom =
        CategoryTheory.CategoryStruct.comp app₀.hom
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝))
      CategoryTheory.ComposableArrows.isoMk₂._auto_1)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_247✝) app₂.hom =
        CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_246✝ _proof_247✝))
      CategoryTheory.ComposableArrows.isoMk₂._auto_3),
  (CategoryTheory.ComposableArrows.isoMk₂ app₀ app₁ app₂ w₀ w₁).hom =
    CategoryTheory.ComposableArrows.homMk₂ app₀.hom app₁.hom app₂.hom w₀ w₁
-- Mathlib.Data.Ineq
Mathlib.Ineq.instToFormat : Std.ToFormat Mathlib.Ineq
-- Mathlib.Algebra.Group.UniqueProds.Basic
Prod.instTwoUniqueProds : ∀ {G : Type u} {H : Type v} [inst : Mul G] [inst_1 : Mul H] [TwoUniqueProds G] [TwoUniqueProds H],
  TwoUniqueProds (G × H)
-- Mathlib.Computability.RecursiveIn
/-- If every function in `O` is partial recursive,
then a function which is `RecursiveIn O` is also partial recursive.  -/
RecursiveIn.partrec_of_oracle : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α →. σ} {O : Set (ℕ →. ℕ)},
  (∀ g ∈ O, Partrec g) → RecursiveIn O f → Partrec f
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- The universal property of a strongly co-Cartesian morphism.

This lemma is more flexible with respect to non-definitional equalities than the field
`universal_property'` of `IsStronglyCocartesian`.  -/
CategoryTheory.Functor.IsStronglyCocartesian.universal_property : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCocartesian f φ] {S' : 𝒮}
  {b' : 𝒳} (g : S ⟶ S') (f' : R ⟶ S'),
  f' = CategoryTheory.CategoryStruct.comp f g →
    ∀ (φ' : a ⟶ b') [p.IsHomLift f' φ'], ∃! χ, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp φ χ = φ'
-- Mathlib.Data.Set.Lattice
/-- **Alias** of `Set.sUnion_subset_sUnion`. -/
Set.sUnion_mono : ∀ {α : Type u_1} {S T : Set (Set α)}, S ⊆ T → ⋃₀ S ⊆ ⋃₀ T
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integral_comp_mul_left_Ioi' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : ℝ → E) (a : ℝ) {b : ℝ},
  0 < b → b • ∫ (x : ℝ) in Set.Ioi a, g (b * x) = ∫ (x : ℝ) in Set.Ioi (b * a), g x
-- Lean.Message
Lean.instToMessageDataOfToFormat : {α : Type} → [Std.ToFormat α] → Lean.ToMessageData α
-- Mathlib.Algebra.MonoidAlgebra.Lift
AddMonoidAlgebra.liftNC_one : ∀ {k : Type u₁} {G : Type u₂} {R : Type u_2} [inst : Semiring k] [inst_1 : Zero G] [inst_2 : NonAssocSemiring R]
  {g_hom : Type u_6} [inst_3 : FunLike g_hom (Multiplicative G) R] [OneHomClass g_hom (Multiplicative G) R]
  (f : k →+* R) (g : g_hom), (AddMonoidAlgebra.liftNC ↑f ⇑g) 1 = 1
-- Mathlib.Tactic.Ring.Basic
/-- `ring1` solves the goal when it is an equality in *commutative* (semi)rings,
allowing variables in the exponent.

This version of `ring` fails if the target is not an equality.

* `ring1!` uses a more aggressive reducibility setting to determine equality of atoms.


Extensions:

 * * `ring1_nf` additionally uses `ring_nf` to simplify in atoms.
   * `ring1_nf!` will use a more aggressive reducibility setting
     to determine equality of atoms. -/
Mathlib.Tactic.Ring.tacticRing1! : Lean.ParserDescr
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} [inst_1 : Inhabited (β k)], (m₁ \ m₂).get! k = if k ∈ m₂ then default else m₁.get! k
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.get_eq_of_singleton : ∀ {s : String} {p : s.Pos} {h : p ≠ s.endPos} {t₁ t₂ : String} {c : Char},
  (p.next h).Splits (t₁ ++ String.singleton c) t₂ → p.get h = c
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
AEMeasurable.congr : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {f g : α → β}
  {μ : MeasureTheory.Measure α}, AEMeasurable f μ → f =ᵐ[μ] g → AEMeasurable g μ
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x y : M` and Localization maps `F : M →* N, G : M →* P` away from `x` and `x * y`
respectively, the homomorphism induced from `N` to `P`.  -/
Submonoid.LocalizationMap.awayToAwayRight : {M : Type u_1} →
  [inst : CommMonoid M] →
    {N : Type u_2} →
      [inst_1 : CommMonoid N] →
        {P : Type u_3} →
          [inst_2 : CommMonoid P] →
            (x : M) →
              Submonoid.LocalizationMap.AwayMap x N → (y : M) → Submonoid.LocalizationMap.AwayMap (x * y) P → N →* P
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.MemBaseSet.mk : ∀ {ι : Type u_1} [inst : Fintype ι] {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {c : NNReal}
  {r : (ι → ℝ) → ↑(Set.Ioi 0)} {π : BoxIntegral.TaggedPrepartition I},
  π.IsSubordinate r →
    (l.bHenstock = true → π.IsHenstock) →
      (l.bDistortion = true → π.distortion ≤ c) →
        (l.bDistortion = true → ∃ π', π'.iUnion = ↑I \ π.iUnion ∧ π'.distortion ≤ c) → l.MemBaseSet I c r π
-- Init.Data.List.Range
List.range'_subset_right : ∀ {step s m n : ℕ}, 0 < step → (List.range' s m step ⊆ List.range' s n step ↔ m ≤ n)
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.pairingIn_two_two_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  (i j : ι) [Finite ι] [CharZero R] [IsDomain R] [Module.IsTorsionFree R M] [inst_9 : CommRing S]
  [inst_10 : Algebra S R] [FaithfulSMul S R] [inst_12 : P.IsValuedIn S],
  P.pairingIn S i j = 2 ∧ P.pairingIn S j i = 2 ↔ i = j
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.smul_of_top_right : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_8} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 β] [IsBoundedSMul 𝕜 β] {f : α → β} {φ : α → 𝕜},
  MeasureTheory.Integrable f μ → MeasureTheory.MemLp φ ⊤ μ → MeasureTheory.Integrable (φ • f) μ
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.toOption.eq_1 : ∀ {s : String.Slice} (pos : s.Pos),
  String.Slice.Pattern.ForwardSliceSearcher.toOption✝ (String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos) =
    some (pos.remainingBytes, 1)
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
/-- `ofFunction` of a set `s` is the infimum of `∑ᵢ, m (tᵢ)` for all collections of sets
`tᵢ` that cover `s`, with all `tᵢ` satisfying a predicate `P` such that `m` is infinite for sets
that don't satisfy `P`.
This is similar to `ofFunction_apply`, except that the sets `tᵢ` satisfy `P`.
The hypothesis `m_top` applies in particular to a function of the form `extend m'`.  -/
MeasureTheory.OuterMeasure.ofFunction_eq_iInf_mem : ∀ {α : Type u_1} (m : Set α → ENNReal) (m_empty : m ∅ = 0) {P : Set α → Prop},
  (∀ (s : Set α), ¬P s → m s = ⊤) →
    ∀ (s : Set α),
      (MeasureTheory.OuterMeasure.ofFunction m m_empty) s =
        ⨅ t, ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i)
-- Init.Data.Array.Basic
Array.getElem_mem : ∀ {α : Type u} {xs : Array α} {i : ℕ} (h : i < xs.size), xs[i] ∈ xs
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.le_bound : ∀ (ε : ℝ) (l : ℕ), l ≤ SzemerediRegularity.bound ε l
-- Init.Data.List.MinMaxOn
List.maxOn?_append : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] (xs ys : List α)
  (f : α → β), List.maxOn? f (xs ++ ys) = Option.merge (maxOn f) (List.maxOn? f xs) (List.maxOn? f ys)
-- Mathlib.Data.Int.Bitwise
Int.bitwise_diff : (Int.bitwise fun a b => a && !b) = Int.ldiff
-- Mathlib.Order.Sublattice
Sublattice.infClosed : ∀ {α : Type u_2} [inst : Lattice α] (L : Sublattice α), InfClosed ↑L
-- Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
/-- The `AlgEquiv` between `R[X][Y]` and `R[a][Y]` for some transcendental `a`.  -/
Polynomial.Bivariate.Transcendental.algEquivAdjoin : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R A] → {x : A} → Transcendental R x → Polynomial (Polynomial R) ≃ₐ[R] Polynomial ↥R[x]
-- Mathlib.Data.Tree.Basic
BinaryTree.height.eq_def : ∀ {α : Type u} (x : BinaryTree α),
  x.height =
    match x with
    | BinaryTree.nil => 0
    | BinaryTree.node value a b => max a.height b.height + 1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited γ] {f : α → β → Option γ} {k : α} (h : t.WF),
  (Std.TreeMap.Raw.filterMap f t)[k]! = (t[k]?.pbind fun x h' => f (t.getKey k ⋯) x).get!
-- Mathlib.Analysis.Seminorm
/-- The closed ball of radius `r` at `x` with respect to seminorm `p` is the set of elements `y`
with `p (y - x) ≤ r`.  -/
Seminorm.closedBall : {𝕜 : Type u_3} →
  {E : Type u_7} →
    [inst : SeminormedRing 𝕜] → [inst_1 : AddCommGroup E] → [inst_2 : SMul 𝕜 E] → Seminorm 𝕜 E → E → ℝ → Set E
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_φ₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₂.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.L₀X₂ToP (CategoryTheory.CategoryStruct.comp S.φ₁ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- **Alias** of `AddHom.domRestrict_apply`. -/
AddHom.restrict_apply : ∀ {M : Type u_1} {σ : Type u_4} [inst : Add M] {N : Type u_5} [inst_1 : Add N] [inst_2 : SetLike σ M]
  [inst_3 : AddMemClass σ M] (f : M →ₙ+ N) {S : σ} (x : ↥S), (f.domRestrict S) x = f ↑x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.latticeBasis_repr_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : K)
  (i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)),
  ((NumberField.mixedEmbedding.latticeBasis K).repr ((NumberField.mixedEmbedding K) x)) i =
    ↑(((NumberField.integralBasis K).repr x) i)
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
RingSubgroupsBasis.of_comm : ∀ {A : Type u_3} {ι : Type u_4} [inst : CommRing A] (B : ι → AddSubgroup A),
  (∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j) →
    (∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)) →
      (∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)) → RingSubgroupsBasis B
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.mk.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (leftFun leftFun_1 : E → F) (e_leftFun : leftFun = leftFun_1)
  (leftDeriv leftDeriv_1 : E →L[𝕜] F) (e_leftDeriv : leftDeriv = leftDeriv_1) (rightFun rightFun_1 : E → G)
  (e_rightFun : rightFun = rightFun_1) (rightDeriv rightDeriv_1 : E →L[𝕜] G) (e_rightDeriv : rightDeriv = rightDeriv_1)
  (pt pt_1 : E) (e_pt : pt = pt_1) (hasStrictFDerivAt_leftFun : HasStrictFDerivAt leftFun leftDeriv pt)
  (hasStrictFDerivAt_rightFun : HasStrictFDerivAt rightFun rightDeriv pt) (range_leftDeriv : (↑leftDeriv).range = ⊤)
  (range_rightDeriv : (↑rightDeriv).range = ⊤) (isCompl_ker : IsCompl (↑leftDeriv).ker (↑rightDeriv).ker),
  { leftFun := leftFun, leftDeriv := leftDeriv, rightFun := rightFun, rightDeriv := rightDeriv, pt := pt,
      hasStrictFDerivAt_leftFun := hasStrictFDerivAt_leftFun, hasStrictFDerivAt_rightFun := hasStrictFDerivAt_rightFun,
      range_leftDeriv := range_leftDeriv, range_rightDeriv := range_rightDeriv, isCompl_ker := isCompl_ker } =
    { leftFun := leftFun_1, leftDeriv := leftDeriv_1, rightFun := rightFun_1, rightDeriv := rightDeriv_1, pt := pt_1,
      hasStrictFDerivAt_leftFun := ⋯, hasStrictFDerivAt_rightFun := ⋯, range_leftDeriv := ⋯, range_rightDeriv := ⋯,
      isCompl_ker := ⋯ }
-- Mathlib.Analysis.Analytic.Linear
/-- `snd` is analytic  -/
analyticAt_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F},
  AnalyticAt 𝕜 (fun p => p.2) p
-- Mathlib.Data.Prod.Basic
Prod.mk.eta : ∀ {α : Type u_1} {β : Type u_2} {p : α × β}, (p.1, p.2) = p
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_fst_eq_iff_leftCosetEquivalence : ∀ {G : Type u_1} [inst : Group G] {K : Subgroup G} {S : Set G} (hSK : Subgroup.IsComplement S ↑K) {g₁ g₂ : G},
  (hSK.equiv g₁).1 = (hSK.equiv g₂).1 ↔ LeftCosetEquivalence (↑K) g₁ g₂
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.State : Type
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_inter_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α] (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.inter m₂ ⋯).getKey! k = m₁.getKey! k
-- Mathlib.Algebra.Category.Ring.Topology
CommRingCat.HomTopology.mvPolynomialHomeomorph_symm_apply_hom : ∀ (σ : Type v) (R A : CommRingCat) [inst : TopologicalSpace ↑R] [inst_1 : IsTopologicalRing ↑R]
  (fx : (A ⟶ R) × (σ → ↑R)),
  CommRingCat.Hom.hom ((CommRingCat.HomTopology.mvPolynomialHomeomorph σ R A).symm fx) =
    MvPolynomial.eval₂Hom (CommRingCat.Hom.hom fx.1) fx.2
-- Mathlib.Data.Set.Basic
Set.inter_congr_left : ∀ {α : Type u} {s t u : Set α}, s ∩ u ⊆ t → s ∩ t ⊆ u → s ∩ t = s ∩ u
-- Mathlib.Algebra.Homology.Linear
HomologicalComplex.smul_f_apply : ∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {ι : Type u_4} {c : ComplexShape ι}
  {X Y : HomologicalComplex C c} (r : R) (f : X ⟶ Y) (n : ι), (r • f).f n = r • f.f n
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.IsProbabilityMeasure.ae_neBot : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ],
  (MeasureTheory.ae μ).NeBot
-- Mathlib.Algebra.BigOperators.Fin
finFunctionFinEquiv_apply : ∀ {m n : ℕ} (f : Fin n → Fin m), ↑(finFunctionFinEquiv f) = ∑ i, ↑(f i) * m ^ ↑i
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.instDecidableEqLiteral : DecidableEq BitVec.Literal✝
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_as_app_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (a_1 : f ⟶ g) (x : Bᵒᵖ)
  (x_1 : Opposite.unop x ⟶ a),
  ((CategoryTheory.Bicategory.yoneda.map₂ a_1).as.app x).toNatTrans.app x_1 =
    CategoryTheory.Bicategory.whiskerLeft x_1 a_1
-- Init.Data.String.Bootstrap
String.Internal.front : String → Char
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.inter_ofPred_eq_sep`. -/
Set.inter_setOf_eq_sep : ∀ {α : Type u} (s : Set α) (p : α → Prop), s ∩ {a | p a} = {a | a ∈ s ∧ p a}
-- Mathlib.Analysis.MellinTransform
mellin_comp_inv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E) (s : ℂ),
  mellin (fun t => f t⁻¹) s = mellin f (-s)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- The canonical image of the `TensorAlgebra` in the `CliffordAlgebra`, which maps
`TensorAlgebra.ι R x` to `CliffordAlgebra.ι Q x`.  -/
TensorAlgebra.toClifford : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {Q : QuadraticForm R M} → TensorAlgebra R M →ₐ[R] CliffordAlgebra Q
-- Init.Data.List.Attach
List.attachWith_congr : ∀ {α : Type u_1} {l₁ l₂ : List α} (w : l₁ = l₂) {P : α → Prop} {H : ∀ x ∈ l₁, P x},
  l₁.attachWith P H = l₂.attachWith P ⋯
-- Lean.Elab.Tactic.Rewrite
Lean.Elab.Tactic.elabRewriteConfig : Lean.Syntax →
  optParam Lean.Meta.Rewrite.Config { } → optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Meta.Rewrite.Config
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flipping_functor_obj_obj_obj : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (k : D) (j : C),
  ((CategoryTheory.Functor.flipping.functor.obj F).obj k).obj j = (F.obj j).obj k
-- Mathlib.GroupTheory.Finiteness
AddGroup.instFGInt : AddGroup.FG ℤ
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
TopCat.Sheaf.interUnionPullbackCone_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Sheaf C X)
  (U V : TopologicalSpace.Opens ↑X), (F.interUnionPullbackCone U V).fst = F.obj.map (CategoryTheory.homOfLE ⋯).op
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Const.maxEntry?.eq_def : ∀ {α : Type u} {β : Type v} (x : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.maxEntry? x =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf => none
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => some (k, v)
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
      Std.DTreeMap.Internal.Impl.Const.maxEntry? r
-- Lean.Elab.Term.TermElabM
/-- The body as a fully elaborated term. `none` if the body failed to elaborate.  -/
Lean.Elab.Term.BodyInfo.value? : Lean.Elab.Term.BodyInfo → Option Lean.Expr
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `lowerSemiContinuous_neg_iff`. -/
UpperSemicontinuous.neg : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β], UpperSemicontinuous f → LowerSemicontinuous (-f)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_v_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (i j k : ℤ)
  (hij : i + -1 = j) (hik : k + -1 = i),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v i j hij)
      ((CochainComplex.mappingCone φ).d j i) =
    CategoryTheory.CategoryStruct.comp (φ.f i) ((CochainComplex.mappingCone.inr φ).f i) -
      CategoryTheory.CategoryStruct.comp (F.d i k) ((CochainComplex.mappingCone.inl φ).v k i hik)
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolAlg_symm_eq : ∀ {α : Type u_1}, ofBoolAlg.symm = toBoolAlg
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isIso_leftRightHomologyComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : S.HasHomology], CategoryTheory.IsIso S.leftRightHomologyComparison
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
ContinuousMap.coe_toLp : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : CompactSpace α] [inst_5 : MeasureTheory.IsFiniteMeasure μ]
  {𝕜 : Type u_3} [inst_6 : Fact (1 ≤ p)] [inst_7 : NormedRing 𝕜] [inst_8 : Module 𝕜 E] [inst_9 : IsBoundedSMul 𝕜 E]
  (f : C(α, E)), ↑((ContinuousMap.toLp p μ 𝕜) f) = ContinuousMap.toAEEqFun μ f
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.logSizeBallStruct.mk.sizeOf_spec : ∀ {T : Type u_2} [inst : SizeOf T] (finset : Finset T) (point : T) (radius : ℕ),
  sizeOf { finset := finset, point := point, radius := radius } = 1 + sizeOf finset + sizeOf point + sizeOf radius
-- Mathlib.ModelTheory.Basic
/-- The homomorphism commutes with the interpretations of the function symbols  -/
FirstOrder.Language.HomClass.map_fun : ∀ {L : outParam FirstOrder.Language} {F : Type u_3} {M : outParam (Type u_4)} {N : outParam (Type u_5)}
  {inst : FunLike F M N} {inst_1 : L.Structure M} {inst_2 : L.Structure N} [self : L.HomClass F M N] (φ : F) {n : ℕ}
  (f : L.Functions n) (x : Fin n → M),
  φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)