mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.subtypeEquivToFinset_symm_apply_coe : ∀ {α : Type u} {s : Set α} (hs : s.Finite) (b : ↥hs.toFinset), ↑(hs.subtypeEquivToFinset.symm b) = ↑b
-- Init.Data.Iterators.Basic
/-- The relation of plausible successors while skipping on `IterM.TerminationMeasures.Productive`.
It is well-founded if there is a `Productive` instance.
 -/
Std.IterM.TerminationMeasures.Productive.Rel : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        Std.IterM.TerminationMeasures.Productive α m → Std.IterM.TerminationMeasures.Productive α m → Prop
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsKolmogorovProcess.stronglyMeasurable_edist : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E},
  ProbabilityTheory.IsKolmogorovProcess X P p q M →
    ∀ {s t : T}, MeasureTheory.StronglyMeasurable fun ω => edist (X s ω) (X t ω)
-- Mathlib.Algebra.Algebra.Tower
AlgHom.extendScalarsOfSurjective_symm_apply : ∀ {R : Type u} {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (h : Function.Surjective ⇑(algebraMap R S)) (f : A →ₐ[S] B),
  (AlgHom.extendScalarsOfSurjective h).symm f = AlgHom.restrictScalars R f
-- Mathlib.Order.Filter.CountableInter
Filter.EventuallyEq.countable_bUnion : ∀ {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι},
  S.Countable →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi) → ⋃ i, ⋃ (h : i ∈ S), s i h =ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h
-- Std.Data.HashMap.Basic
/-- Computes the intersection of the given hash maps. The result will only contain entries from the first map.

This function always iterates through the smaller map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.HashMap.inter : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashMap α β → Std.HashMap α β → Std.HashMap α β
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.Faithful.of_comp_iso : ∀ {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 : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} [H.Faithful] (h : F.comp G ≅ H), F.Faithful
-- Mathlib.Order.Filter.Pointwise
Filter.mapAddMonoidHom.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddZeroClass α] [inst_1 : AddZeroClass β]
  [inst_2 : FunLike F α β] [inst_3 : AddMonoidHomClass F α β] (φ : F),
  Filter.mapAddMonoidHom φ = { toFun := Filter.map ⇑φ, map_zero' := ⋯, map_add' := ⋯ }
-- Init.Data.Fin.Lemmas
Fin.last_le_iff : ∀ {n : ℕ} {k : Fin (n + 1)}, Fin.last n ≤ k ↔ k = Fin.last n
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual.congr_simp : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsFractionRing A K]
  [inst_12 : IsIntegrallyClosed A] [inst_13 : FiniteDimensional K L] [inst_14 : IsIntegralClosure B A L]
  [inst_15 : Algebra.IsSeparable K L] [inst_16 : IsDomain A] [inst_17 : IsFractionRing B L] [inst_18 : Nontrivial B]
  [inst_19 : NoZeroDivisors B] (I I_1 : FractionalIdeal (nonZeroDivisors B) L),
  I = I_1 → FractionalIdeal.dual A K I = FractionalIdeal.dual A K I_1
-- Mathlib.Topology.Piecewise
ContinuousOn.piecewise' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s t : Set α}
  [inst_2 : (a : α) → Decidable (a ∈ t)],
  (∀ a ∈ s ∩ frontier t, Filter.Tendsto f (nhdsWithin a (s ∩ t)) (nhds (t.piecewise f g a))) →
    (∀ a ∈ s ∩ frontier t, Filter.Tendsto g (nhdsWithin a (s ∩ tᶜ)) (nhds (t.piecewise f g a))) →
      ContinuousOn f (s ∩ t) → ContinuousOn g (s ∩ tᶜ) → ContinuousOn (t.piecewise f g) s
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.AddConstAsyncResult.constName : Lean.Environment.AddConstAsyncResult → Lean.Name
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β] (f : sInfHom α β), f.toFun = ⇑f
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_fiber : ∀ {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] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).obj X).fiber =
    CategoryTheory.CostructuredArrow.mk X.hom
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- `Cone.toStructuredArrow` can be expressed in terms of `Functor.toStructuredArrow`.  -/
CategoryTheory.Limits.Cone.toStructuredArrowIsoToStructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cone F) →
            c.toStructuredArrow ≅ (CategoryTheory.Functor.id J).toStructuredArrow c.pt F c.π.app ⋯
-- Mathlib.Algebra.Polynomial.RingDivision
/-- `_ %ₘ q` as an `R`-linear map.  -/
Polynomial.modByMonicHom : {R : Type u} → [inst : CommRing R] → Polynomial R → Polynomial R →ₗ[R] Polynomial R
-- Mathlib.NumberTheory.Padics.WithVal
Padic.norm_rat_le_one_iff_padicValuation_le_one : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {x : ℚ}, ‖↑x‖ ≤ 1 ↔ (Rat.padicValuation p) x ≤ 1
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.forget₂_obj_moduleCat_of : ∀ (R : Type u) [inst : Ring R] (X : Type v) [inst_1 : AddCommGroup X] [inst_2 : Module R X],
  (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj (ModuleCat.of R X) = AddCommGrpCat.of X
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldr_cons : ∀ {α : Type u_1} (t : RBTree.RBNode α) (l : List α), RBTree.RBNode.foldr (fun x1 x2 => x1 :: x2) t l = t.toList ++ l
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformly.prodMap : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [inst_1 : UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'}
  {p' : Filter ι'},
  TendstoUniformly F f p →
    TendstoUniformly F' f' p' → TendstoUniformly (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Reachable.one_lt_dist_of_ne_of_not_adj : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.Reachable u v → u ≠ v → ¬G.Adj u v → 1 < G.dist u v
-- Init.Data.Bool
Bool.eq_not : ∀ {a b : Bool}, a = !b ↔ a ≠ b
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible : ∀ {R : Type u_1} [inst : CommRing R] [UniqueFactorizationMonoid R],
  (∃ p, Irreducible p) →
    (∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q) →
      IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization R
-- Mathlib.Order.Defs.Unbundled
/-- The carrier of an `UpperSet`.  -/
UpperSet.carrier : {α : Type u_1} → [inst : LE α] → UpperSet α → Set α
-- Mathlib.Topology.Category.CompHausLike.Cartesian
/-- When the predicate `P` is preserved under taking type-theoretic sums, that sum is a
category-theoretic coproduct in `CompHausLike P`.
 -/
CompHausLike.coproductIsColimit : {P : TopCat → Prop} →
  (X Y : CompHausLike P) →
    [inst : CompHausLike.HasProp P (↑X.toTop ⊕ ↑Y.toTop)] → CategoryTheory.Limits.IsColimit (X.coproductCocone Y)
-- Init.Data.String.Basic
String.Slice.startInclusive_sliceFrom : ∀ {s : String.Slice} {pos : s.Pos}, (s.sliceFrom pos).startInclusive = pos.str
-- Mathlib.Data.DFinsupp.Order
DFinsupp.support_sup_union_support_inf : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Lattice (α i)]
  (f g : Π₀ (i : ι), α i) [inst_2 : DecidableEq ι] [inst_3 : (i : ι) → (x : α i) → Decidable (x ≠ 0)],
  (f ⊔ g).support ∪ (f ⊓ g).support = f.support ∪ g.support
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃'_obj_obj_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : C)
  {X Y : C} (φ : X ⟶ Y),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃' C).obj X₁).obj X₂).map φ =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂ φ)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertIfNew_ne_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, ¬t.insertIfNew k v = ∅
-- Mathlib.Combinatorics.Colex
Finset.Colex.lt_iff_exists_filter_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Finset α},
  toColex s < toColex t ↔ ∃ w ∈ t \ s, {a ∈ s | w < a} = {a ∈ t | w < a}
-- Mathlib.Algebra.Algebra.Equiv
RingEquiv.toNatAlgEquiv_injective : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S], Function.Injective RingEquiv.toNatAlgEquiv
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.State.mk.injEq : ∀ (toDerive : Lean.NameMap Lean.ExprSet) (toOmit : Array (Lean.Ident × Lean.Name))
  (toDerive_1 : Lean.NameMap Lean.ExprSet) (toOmit_1 : Array (Lean.Ident × Lean.Name)),
  ({ toDerive := toDerive, toOmit := toOmit } = { toDerive := toDerive_1, toOmit := toOmit_1 }) =
    (toDerive = toDerive_1 ∧ toOmit = toOmit_1)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- When both maps `S.f` and `S.g` of a short complex `S` are zero, this is the left homology map
data (for the identity of `S`) which relates the left homology data `ofZeros` and
`ofIsColimitCokernelCofork`.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        (hf : S.f = 0) →
          (hg : S.g = 0) →
            (c : CategoryTheory.Limits.CokernelCofork S.f) →
              (hc : CategoryTheory.Limits.IsColimit c) →
                CategoryTheory.ShortComplex.LeftHomologyMapData (CategoryTheory.CategoryStruct.id S)
                  (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg)
                  (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc)
-- Init.Data.Array.BasicAux
_private.Init.Data.Array.BasicAux.0.mapMonoMImp : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → Array α → (α → m α) → m (Array α)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.comp_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {G : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (g : F.Hom G)
  (a : E.I₀), (f.comp g).s₀ a = g.s₀ (f.s₀ a)
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- **Alias** of `ModularForm.qExpansion_smul`. -/
ModularFormClass.qExpansion_smul : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ},
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (a : ℂ) (f : F) [ModularFormClass F Γ k],
        UpperHalfPlane.qExpansion h (a • ⇑f) = a • UpperHalfPlane.qExpansion h ⇑f
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_mul_of_le_mul_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulRightMono α] {a b c d : α}, a ≤ b * c → b ≤ d → a ≤ d * c
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_fintype : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α]
  [inst_2 : Fintype α] (f : α → ENNReal), ∫⁻ (x : α), f x ∂μ = ∑ x, f x * μ {x}
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.fpqcPrecoverage.eq_1 : AlgebraicGeometry.Scheme.fpqcPrecoverage = AlgebraicGeometry.Scheme.propQCPrecoverage @AlgebraicGeometry.Flat
-- Init.Data.UInt.Lemmas
UInt16.ofNat_size : UInt16.ofNat UInt16.size = 0
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffWithinAt_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {G : Type u_9} [inst_8 : TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {s : Set (M × N)} {p : M × N},
  ContMDiffWithinAt (I.prod J) J n Prod.snd s p
-- Mathlib.Data.Rat.Sqrt
/-- `IsSquare` can be decided on `ℚ` by checking against the square root.  -/
Rat.instDecidablePredIsSquare : DecidablePred IsSquare
-- Lean.Data.Lsp.Extra
/-- Procedure to invoke. Must be fully qualified.  -/
Lean.Lsp.RpcCallParams.method : Lean.Lsp.RpcCallParams → Lean.Name
-- Init.Data.Range.Polymorphic.Map
/-- Compatibility class for `Map` and `<`.  -/
Std.PRange.UpwardEnumerable.Map.PreservesLT : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : Std.PRange.UpwardEnumerable β] → [LT α] → [LT β] → Std.PRange.UpwardEnumerable.Map α β → Prop
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.d_EIsoH_hom : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.d_EIsoH_hom._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.d_EIsoH_hom._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.d_EIsoH_hom._auto_5),
  CategoryTheory.CategoryStruct.comp
      (X.d (CategoryTheory.CategoryStruct.id i₀) f₁ (CategoryTheory.CategoryStruct.id i₁) f₂
        (CategoryTheory.CategoryStruct.id i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)
      (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    CategoryTheory.CategoryStruct.comp (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom (X.δ f₁ f₂ n₁ n₂ hn₂)
-- Mathlib.Algebra.Order.Archimedean.Defs
exists_pow_lt : ∀ {R : Type u_1} [inst : CommGroup R] [inst_1 : LinearOrder R] [IsOrderedMonoid R] [MulArchimedean R] {a : R},
  a < 1 → ∀ (b : R), ∃ n, a ^ n < b
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionResult.solved : Lean.Meta.InjectionResult
-- Mathlib.Data.Fintype.Card
Finset.card_compl_lt_iff_nonempty : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), sᶜ.card < Fintype.card α ↔ s.Nonempty
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.divRight_apply : ∀ {G : Type u_5} [inst : Group G] (a b : G), (Equiv.divRight a) b = b / a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insertMany_empty_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α] {l : List (α × β)}
  {k : α} [inst_2 : Inhabited β],
  (List.map Prod.fst l).contains k = false →
    Std.DTreeMap.Internal.Impl.Const.get!
        (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)) k =
      default
-- Mathlib.Algebra.Order.Monoid.Units
Units.instPartialOrderUnits : {α : Type u_1} → [inst : Monoid α] → [PartialOrder α] → PartialOrder αˣ
-- Lean.Meta.Match.MatcherApp.Transform
/-- The `altParams` that were used for `instantiateLambda alt altParams` inside `transform`.  -/
Lean.Meta.MatcherApp.TransformAltFVars.altParams : Lean.Meta.MatcherApp.TransformAltFVars → Array Lean.Expr
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
exists_eq_ciSup_of_finite : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [Nonempty ι] [Finite ι] {f : ι → α},
  ∃ i, f i = ⨆ i, f i
-- Std.Data.DTreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is
less than the given key.
 -/
Std.DTreeMap.Const.getEntryLT : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      [Std.TransCmp cmp] → (t : Std.DTreeMap α (fun x => β) cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.lt) → α × β
-- Mathlib.Data.Fintype.Order
Finite.ciInf_le : ∀ {α : Type u_1} {ι : Type u_2} [Finite ι] [inst : ConditionallyCompleteLattice α] (f : ι → α) (i : ι), ⨅ j, f j ≤ f i
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.ι_app_self : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  AlgebraicGeometry.Scheme.Hom.app U.ι U = X.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.OplaxTrans.id_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {x x_1 : B} (f : x ⟶ x_1),
  (CategoryTheory.CategoryStruct.id F).naturality f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom
      (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv
-- Lean.Server.Requests
Lean.Language.SnapshotTree.foldSnaps.Control.done : Lean.Language.SnapshotTree.foldSnaps.Control
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic, then their
separable degrees satisfy the tower law: $[E:F]_s [K:E]_s = [K:F]_s$.  -/
Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E],
  Cardinal.lift.{w, v} (Field.sepDegree F E) * Cardinal.lift.{v, w} (Field.sepDegree E K) =
    Cardinal.lift.{v, w} (Field.sepDegree F K)
-- Mathlib.Data.List.AList
AList.erase_erase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a a' : α) (s : AList β),
  AList.erase a' (AList.erase a s) = AList.erase a (AList.erase a' s)
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
isCompactOperator_zero : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Zero M₁] [inst_1 : TopologicalSpace M₁] [inst_2 : TopologicalSpace M₂]
  [inst_3 : Zero M₂], IsCompactOperator 0
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.filterMap_replicate.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.le_degree_of_mem_supp : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, ∀ a ∈ p.support, ↑a ≤ p.degree
-- Mathlib.Data.ENat.Lattice
ENat.mul_iInf : ∀ {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞} [Nonempty ι], a * ⨅ i, f i = ⨅ i, a * f i
-- Mathlib.Data.Seq.Computation
Computation.Mem.left_unique : ∀ {α : Type u}, Relator.LeftUnique fun x1 x2 => x1 ∈ x2
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
Std.Tactic.BVDecide.LRAT.Internal.CNF.Clause.convertLRAT_sat_of_sat : ∀ {n : ℕ} {lratClause : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n}
  {assign : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool}
  (clause : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  Std.Tactic.BVDecide.LRAT.Internal.CNF.Clause.convertLRAT' clause = some lratClause →
    Std.Sat.CNF.Clause.eval assign clause = true → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval assign lratClause
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_bot_left : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), ⊥.relIndex H = Nat.card ↥H
-- Mathlib.Algebra.Category.ModuleCat.Injective
ModuleCat.ulift_injective_of_injective : ∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Small.{v, u} R]
  [CategoryTheory.Injective (ModuleCat.of R M)], CategoryTheory.Injective (ModuleCat.of R (ULift.{v', v} M))
-- Mathlib.Data.Set.Lattice
Set.biInter_empty : ∀ {α : Type u_1} {β : Type u_2} (u : α → Set β), ⋂ x ∈ ∅, u x = Set.univ
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.intercalateTR.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List (List α) → Array α → Sort u_2) (x : List α) (acc : Array α)
  (h_1 : (x : List α) → (acc : Array α) → motive x [] acc)
  (h_2 : (x y : List α) → (xs : List (List α)) → (acc : Array α) → motive x (y :: xs) acc),
  (match x, [], acc with
    | x, [], acc => h_1 x acc
    | x, y :: xs, acc => h_2 x y xs acc) =
    h_1 x acc
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
/-- The `MonoidWithZero` version of `mul_inv_eq_mul_inv_iff_mul_eq_mul`.  -/
Commute.mul_inv_eq_mul_inv_iff : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c d : G₀},
  Commute b d → b ≠ 0 → d ≠ 0 → (a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.isExtTheorem : Lean.Name → Lean.Meta.Grind.GrindM Bool
-- Init.Data.String.Search
String.foldlAux : {α : Type u} → (α → Char → α) → String → String.Pos.Raw → String.Pos.Raw → α → α
-- Mathlib.Order.Filter.Map
Filter.lawfulMonad : LawfulMonad Filter
-- Mathlib.Topology.Algebra.Order.Field
tendsto_const_mul_zpow_atTop_zero : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {n : ℤ} {c : 𝕜}, n < 0 → Filter.Tendsto (fun x => c * x ^ n) Filter.atTop (nhds 0)
-- Mathlib.Order.Lex
toColex_symm_eq : ∀ {α : Type u_1}, toColex.symm = ofColex
-- Lean.Parser.Basic
Lean.Parser.instReprLeadingIdentBehavior.repr : Lean.Parser.LeadingIdentBehavior → ℕ → Std.Format
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.Trivialization.mdifferentiableWithinAt_snd_comp_iff₂ : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB)
  {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
  [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  [inst_16 : (x : B) → AddCommMonoid (E x)] [inst_17 : (x : B) → Module 𝕜 (E x)] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle 1 F E IB] {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e]
  [MemTrivializationAtlas e'] {f : M → Bundle.TotalSpace F E} {s : Set M} {x₀ : M},
  f x₀ ∈ e.source →
    f x₀ ∈ e'.source →
      MDiffAt[s] (Bundle.TotalSpace.proj ∘ f) x₀ →
        ((MDiffAt[s] fun x => (↑e (f x)).2) x₀ ↔ (MDiffAt[s] fun x => (↑e' (f x)).2) x₀)