mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.MulAction
instContinuousVAddULift : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : VAdd M X]
  [ContinuousVAdd M X], ContinuousVAdd (ULift.{u_5, u_1} M) X
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α} [inst_2 : Inhabited (β k)],
  (Std.ExtDTreeMap.filter f t).get! k = (Option.filter (f k) (t.get? k)).get!
-- Mathlib.Algebra.Polynomial.Laurent
AddMonoidAlgebra.comapDomain.congr_simp : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f f_1 : M → N) (e_f : f = f_1)
  (hf : Function.Injective f) (x x_1 : AddMonoidAlgebra R N),
  x = x_1 → AddMonoidAlgebra.comapDomain f hf x = AddMonoidAlgebra.comapDomain f_1 ⋯ x_1
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.of_mul_add_left_left : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsRelPrime (y * z + x) y → IsRelPrime x y
-- Mathlib.Data.List.Perm.Basic
List.Perm.foldl_op_eq : ∀ {α : Type u_1} {op : α → α → α} [IA : Std.Associative op] [IC : Std.Commutative op] {l₁ l₂ : List α} {a : α},
  l₁.Perm l₂ → List.foldl op a l₁ = List.foldl op a l₂
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.single_hadamard_single_eq : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : MulZeroClass α]
  (i : m) (j : n) (a b : α), (Matrix.single i j a).hadamard (Matrix.single i j b) = Matrix.single i j (a * b)
-- Mathlib.Topology.Order.OrderClosed
continuousWithinAt_Ioc_iff_Iic : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α]
  [inst_3 : TopologicalSpace β] {a b : α} {f : α → β},
  a < b → (ContinuousWithinAt f (Set.Ioc a b) b ↔ ContinuousWithinAt f (Set.Iic b) b)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_id : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : FractionalIdeal S P), FractionalIdeal.map (AlgHom.id R P) I = I
-- Mathlib.Algebra.Order.Monoid.Basic
/-- The order embedding sending `b` to `b * a`, for some fixed `a`.
See also `OrderIso.mulRight` when working in an ordered group.  -/
OrderEmbedding.mulRight : {α : Type u_2} → [inst : Mul α] → [inst_1 : LinearOrder α] → [MulRightStrictMono α] → α → α ↪o α
-- Mathlib.Computability.RegularExpressions
RegularExpression.zero_rmatch : ∀ {α : Type u_1} [inst : DecidableEq α] (x : List α), RegularExpression.rmatch 0 x = false
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
HasStrictFDerivAt.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {x : E}
  {H : Type u_5} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {c' : E →L[𝕜] G →L[𝕜] H}
  {u : E → G} {u' : E →L[𝕜] G},
  HasStrictFDerivAt c c' x →
    HasStrictFDerivAt u u' x → HasStrictFDerivAt (fun y => (c y) (u y)) (c x ∘SL u' + c'.flip (u x)) x
-- Mathlib.Algebra.Order.Module.Rat
PosSMulMono.nnrat_of_rat : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : MulAction ℚ α] [inst_2 : MulAction ℚ≥0 α] [IsScalarTower ℚ≥0 ℚ α]
  [PosSMulMono ℚ α], PosSMulMono ℚ≥0 α
-- Mathlib.RingTheory.Ideal.Maps
RingEquiv.idealComapOrderIso_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (e : R ≃+* S) (I : Ideal R),
  e.idealComapOrderIso.symm I = Ideal.map e I
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.log_le_log : ∀ {G : Type u_3} [inst : Preorder G] [inst_1 : AddGroup G] {x y : WithZero (Multiplicative G)},
  x ≠ 0 → y ≠ 0 → (x.log ≤ y.log ↔ x ≤ y)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_div_Ioo : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => a / x) '' Set.Ioo b c = Set.Ioo (a / c) (a / b)
-- Mathlib.MeasureTheory.Measure.ContinuousPreimage
/-- Let `X` and `Y` be R₁ topological spaces
with Borel σ-algebras and measures `μ` and `ν`, respectively.
Suppose that `μ` is inner regular for finite measure sets with respect to compact sets
and `ν` is a locally finite measure.
Let `f : α → C(X, Y)` be a family of continuous maps
that converges to a continuous map `g : C(X, Y)` in the compact-open topology along a filter `l`.
Suppose that `g` is a measure-preserving map
and `f a` is a measure-preserving map eventually along `l`.
Then for any finite measure measurable set `s`,
the preimages `f a ⁻¹' s` tend to the preimage `g ⁻¹' s` in measure.
More precisely, the measure of the symmetric difference of these two sets tends to zero.  -/
MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero : ∀ {α : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X]
  [R1Space X] [inst_4 : TopologicalSpace Y] [inst_5 : MeasurableSpace Y] [BorelSpace Y] [R1Space Y]
  {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop]
  [MeasureTheory.IsLocallyFiniteMeasure ν] {l : Filter α} {f : α → C(X, Y)} {g : C(X, Y)} {s : Set Y},
  Filter.Tendsto f l (nhds g) →
    (∀ᶠ (a : α) in l, MeasureTheory.MeasurePreserving (⇑(f a)) μ ν) →
      MeasureTheory.MeasurePreserving (⇑g) μ ν →
        MeasureTheory.NullMeasurableSet s ν →
          ν s ≠ ⊤ → Filter.Tendsto (fun a => μ (symmDiff (⇑(f a) ⁻¹' s) (⇑g ⁻¹' s))) l (nhds 0)
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.prod_const_comp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {δ : Type u_6} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel β γ) [ProbabilityTheory.IsSFiniteKernel η]
  (μ : MeasureTheory.Measure δ) [MeasureTheory.SFinite μ],
  (η.prod (ProbabilityTheory.Kernel.const β μ)).comp κ = (η.comp κ).prod (ProbabilityTheory.Kernel.const α μ)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_nonneg_iff : ∀ {z : ℂ}, 0 ≤ z.arg ↔ 0 ≤ z.im
-- Mathlib.Combinatorics.Matroid.Rank.Finite
/-- An `IsRkFinite` set has a finset basis'  -/
Matroid.IsRkFinite.exists_finset_isBasis' : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.IsRkFinite X → ∃ I, M.IsBasis' (↑I) X
-- Mathlib.Analysis.Convex.Side
/-- If `x` and `y` are displaced from points of `s` by multiples of a common vector whose
coefficients have nonnegative product, they are weakly on the same side of `s`.  -/
AffineSubspace.wSameSide_of_vsub_eq_smul : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y p₁ p₂ : P} {m : V} {c₁ c₂ : R},
  p₁ ∈ s → p₂ ∈ s → x -ᵥ p₁ = c₁ • m → y -ᵥ p₂ = c₂ • m → 0 ≤ c₁ * c₂ → s.WSameSide x y
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.ofLE.congr_simp : ∀ {X : Type u_2} [inst : TopologicalSpace X] {A B : DiscreteQuotient X} (h : A ≤ B) (a a_1 : Quotient A.toSetoid),
  a = a_1 → DiscreteQuotient.ofLE h a = DiscreteQuotient.ofLE h a_1
-- Mathlib.Data.Set.Function
/-- If `f` maps `s` bijectively to `t` and a set `t'` is contained in the image of some `s₁ ⊇ s`,
then `s₁` has a subset containing `s` that `f` maps bijectively to `t'`.  -/
Set.BijOn.exists_extend_of_subset : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t : Set β} {f : α → β} {t' : Set β},
  Set.BijOn f s t → s ⊆ s₁ → t ⊆ t' → Set.SurjOn f s₁ t' → ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ Set.BijOn f s' t'
-- Init.Data.Sum.Lemmas
Sum.elim_lam_const_lam_const : ∀ {γ : Sort u_1} {α : Type u_2} {β : Type u_3} (c : γ), (Sum.elim (fun x => c) fun x => c) = fun x => c
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.MapsTo.add : ∀ {α : Type u_2} {β : Type u_3} [inst : Add β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β},
  Set.MapsTo f₁ A B₁ → Set.MapsTo f₂ A B₂ → Set.MapsTo (f₁ + f₂) A (B₁ + B₂)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
ClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} {inst : CommSemiring R} {inst_1 : StarRing R}
  {inst_2 : MetricSpace R} {inst_3 : IsTopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A}
  {inst_6 : StarRing A} {inst_7 : TopologicalSpace A} {inst_8 : Algebra R A}
  [self : ClosedEmbeddingContinuousFunctionalCalculus R A p] (a : A) (ha : p a), Topology.IsClosedEmbedding ⇑(cfcHom ha)
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.ι_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C) {Z : CategoryTheory.Functor C C} (h : Φ.quotient ⟶ Z),
  CategoryTheory.CategoryStruct.comp Φ.ι (CategoryTheory.CategoryStruct.comp Φ.π h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Lie.Solvable
_private.Mathlib.Algebra.Lie.Solvable.0.LieAlgebra.termD : Lean.ParserDescr
-- Mathlib.Algebra.Order.CauSeq.BigOperators
IsCauSeq.series_ratio_test : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] [Archimedean α] {f : ℕ → β} (n : ℕ) (r : α),
  0 ≤ r → r < 1 → (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) → IsCauSeq abv fun m => ∑ n ∈ Finset.range m, f n
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.isCusp_of_mem_strictPeriods : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} {h : ℝ}, 0 < h → h ∈ 𝒢.strictPeriods → IsCusp OnePoint.infty 𝒢
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerRight_inv : ∀ {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] {G H : CategoryTheory.Functor C D} (α : G ≅ H)
  (F : CategoryTheory.Functor D E),
  (CategoryTheory.Functor.isoWhiskerRight α F).inv = CategoryTheory.Functor.whiskerRight α.inv F
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_insert_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  t.isEmpty = true → (t.insert k v).minKey? = some k
-- Init.Data.Rat.Basic
/-- Multiplication of rational numbers. (This definition is `@[irreducible]` because you don't
want to unfold it. Use `Rat.mul_def` instead.)  -/
Rat.mul : ℚ → ℚ → ℚ
-- Mathlib.Data.Finset.NAry
/-- The image of a binary function `f : α → β → γ` as a function `Finset α → Finset β → Finset γ`.
Mathematically this should be thought of as the image of the corresponding function `α × β → γ`.  -/
Finset.image₂ : {α : Type u_1} → {β : Type u_3} → {γ : Type u_5} → [DecidableEq γ] → (α → β → γ) → Finset α → Finset β → Finset γ
-- Mathlib.GroupTheory.Subsemigroup.Center
/-- The center of an additive semigroup `M` is the set of elements that commute with
everything in `M`  -/
AddSubsemigroup.center : (M : Type u_1) → [inst : Add M] → AddSubsemigroup M
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_one : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁], ⇑1 = id
-- Init.Data.Range.Polymorphic.Basic
Std.Rxo.HasSize.mk : {α : Type u} → (α → α → ℕ) → Std.Rxo.HasSize α
-- Mathlib.LinearAlgebra.Coevaluation
coevaluation_apply_one : ∀ (K : Type u) [inst : Field K] (V : Type v) [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V],
  (coevaluation K V) 1 =
    have bV := Module.Basis.ofVectorSpace K V;
    ∑ i, bV i ⊗ₜ[K] bV.coord i
-- Mathlib.Tactic.Nontriviality.Core
/-- Tries to generate a `Nontrivial α` instance by performing case analysis on
`subsingleton_or_nontrivial α`,
attempting to discharge the subsingleton branch using lemmas with `@[nontriviality]` attribute,
including `Subsingleton.le` and `eq_iff_true_of_subsingleton`.
 -/
Mathlib.Tactic.Nontriviality.nontrivialityByElim : {u : Lean.Level} → Q(Type u) → Lean.MVarId → Array Lean.Syntax → Lean.MetaM Lean.MVarId
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.single_mapDomainOfBialgHom : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G]
  [inst_3 : Group H] (f : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H) (g : G) (r : R),
  MonoidAlgebra.single ((MonoidAlgebra.mapDomainOfBialgHom f) g) r = f (MonoidAlgebra.single g r)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instCommSemigroupOfContinuousMul : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : CommSemigroup β] → [ContinuousMul β] → CommSemigroup C(α, β)
-- Mathlib.MeasureTheory.Covering.LiminfLimsup
/-- An auxiliary result en route to `blimsup_thickening_mul_ae_eq`.  -/
blimsup_thickening_mul_ae_eq_aux : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α] [BorelSpace α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] (p : ℕ → Prop)
  (s : ℕ → Set α) {M : ℝ},
  0 < M →
    ∀ (r : ℕ → ℝ),
      Filter.Tendsto r Filter.atTop (nhds 0) →
        (∀ᶠ (i : ℕ) in Filter.atTop, p i → 0 < r i) →
          Filter.blimsup (fun i => Metric.thickening (M * r i) (s i)) Filter.atTop p =ᵐ[μ]
            Filter.blimsup (fun i => Metric.thickening (r i) (s i)) Filter.atTop p
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.restrict_apply_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : C(α, β)) (s : Set α)
  (x : α) (hx : x ∈ s), (ContinuousMap.restrict s f) ⟨x, hx⟩ = f x
-- Mathlib.RingTheory.Localization.FractionRing
FractionRing.algebraMap_liftAlgebra : ∀ (R : Type u_1) [inst : CommRing R] (K : Type u_5) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : FaithfulSMul R K],
  have this := ⋯;
  algebraMap (FractionRing R) K = IsFractionRing.lift ⋯
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanStaleDependencyParams : Lean.FromJson Lean.Lsp.LeanStaleDependencyParams
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_3_comp_cochainsIso₃ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  CategoryTheory.CategoryStruct.comp ((groupCohomology.cochainsMap f φ).f 3) (groupCohomology.cochainsIso₃ B).hom =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₃ A).hom (groupCohomology.cochainsMap₃ f φ)
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.zero : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal}
  [inst_2 : Zero Y], HolderWith C r 0
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_induction : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {p : α → Prop},
  (∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊓ a₂)) → (∀ b ∈ s, p (f b)) → p (s.inf' H f)
-- Mathlib.Topology.Specialization
Specialization.instPartialOrder : {α : Type u_1} → [inst : TopologicalSpace α] → [T0Space α] → PartialOrder (Specialization α)
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_succ : ∀ {R : Type u_1} [inst : Semiring R] (f : PowerSeries R) (n : ℕ),
  (PowerSeries.trunc n.succ) f = (PowerSeries.trunc n) f + (Polynomial.monomial n) ((PowerSeries.coeff n) f)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mrangeRestrict_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N),
  Function.Surjective ⇑f.mrangeRestrict
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.liminf_add_of_right_tendsto_zero : ∀ {ι : Type u_4} {u : Filter ι} {g : ι → ENNReal},
  Filter.Tendsto g u (nhds 0) → ∀ (f : ι → ENNReal), Filter.liminf (f + g) u = Filter.liminf f u
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.lTensorAlgEquiv_symm_single : ∀ {R : Type u_1} {M : Type u_2} {A : Type u_5} {B : Type u_6} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CommMonoid M] (m : M) (a : A)
  (b : B),
  (MonoidAlgebra.lTensorAlgEquiv R A B).symm (MonoidAlgebra.single m (a ⊗ₜ[R] b)) = MonoidAlgebra.single m a ⊗ₜ[R] b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_diff_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.diff m₂ ⋯).get? k = m₁.get? k
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.revSkip?_prop_eq_none_iff : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {pos : s.Pos},
  pos.revSkip? P = none ↔ ∀ (h : pos ≠ s.startPos), ¬P ((pos.prev h).get ⋯)
-- Mathlib.MeasureTheory.Group.Integral
/-- Translating a function by left-addition does not change its integral with respect to a
left-invariant measure.  -/
MeasureTheory.integral_add_left_eq_self : ∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure G} [inst_3 : AddGroup G] [MeasurableAdd G] [μ.IsAddLeftInvariant] (f : G → E) (g : G),
  ∫ (x : G), f (g + x) ∂μ = ∫ (x : G), f x ∂μ
-- Aesop.Builder.Cases
Aesop.RuleBuilder.mkCasesTarget : Lean.Name → Array Aesop.CasesPattern → Aesop.CasesTarget
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.Reason.optional : Std.Time.Reason✝
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.congr : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → (∀ y ∈ s, f₁ y = f y) → f₁ x = f x → ContDiffWithinAt 𝕜 n f₁ s x
-- Mathlib.Data.Num.Bitwise
/-- Bitwise `not` for `SNum`.  -/
SNum.«term~_» : Lean.ParserDescr
-- Mathlib.Algebra.GroupWithZero.Indicator
Set.indicator_mul_left : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroClass M₀] {i : ι} (s : Set ι) (f g : ι → M₀),
  s.indicator (fun j => f j * g j) i = s.indicator f i * g i
-- Batteries.Recycling.MonadSatisfying.Vector
Vector.mapIdxM_mk : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : MonadSatisfying m] (a : Array α) (h : a.size = n) (f : ℕ → α → m β),
  Vector.mapIdxM f (Vector.mk a h) =
    (fun x =>
        match x with
        | ⟨a_1, h'⟩ => Vector.mk a_1 ⋯) <$>
      satisfying ⋯
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.mapIso_hom_app : ∀ {X Y : TopCat} (f g : X ⟶ Y) (h : f = g) (U : TopologicalSpace.Opens ↑Y),
  (TopologicalSpace.Opens.mapIso f g h).hom.app U = CategoryTheory.eqToHom ⋯
-- Mathlib.Order.Monotone.MonovaryOrder
monovary_iff_exists_antitone : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β},
  Monovary f g ↔ ∃ x, Antitone f ∧ Antitone g
-- Mathlib.Topology.UniformSpace.Basic
preimage_entourageProd_prod : ∀ {α : Type ua} {β : Type ub} (u : SetRel α α) (v : SetRel β β) (s : Set α) (t : Set β),
  (entourageProd u v).preimage (s ×ˢ t) = u.preimage s ×ˢ v.preimage t
-- Mathlib.Data.Fin.Tuple.Curry
/-- Curry all the arguments of `Function.FromTypes p τ` to get a function from a tuple.  -/
Function.FromTypes.curry : {n : ℕ} → {p : Fin n → Type u} → {τ : Type u} → (((i : Fin n) → p i) → τ) → Function.FromTypes p τ
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b),
  CategoryTheory.CategoryStruct.comp (t.truncGEδLT a)
      (CategoryTheory.Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (CategoryTheory.shiftFunctor C 1)) =
    CategoryTheory.CategoryStruct.comp (t.natTransTruncGEOfLE a b h) (t.truncGEδLT b)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_eq_fallback : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {a fallback : α},
  a ∉ t → t.getD a fallback = fallback
-- Init.Data.Int.Linear
Int.not_le_eq : ∀ (a b : ℤ), (¬a ≤ b) = (b + 1 ≤ a)
-- Mathlib.Topology.Category.LightProfinite.Injective
LightProfinite.injective : ∀ (S : LightProfinite) [Nonempty ↑S.toTop], CategoryTheory.Injective S
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- The composition map `R →+* AdicCompletion I R →+* R ⧸ I ^ n` equals to the natural quotient map.
 -/
AdicCompletion.evalₐ_of : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (n : ℕ) (x : R),
  (AdicCompletion.evalₐ I n) ((AdicCompletion.of I R) x) = (Ideal.Quotient.mk (I ^ n)) x
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.isSelfAdjoint_toContinuousLinearMap_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E),
  have this := ⋯;
  IsSelfAdjoint (LinearMap.toContinuousLinearMap T) ↔ IsSelfAdjoint T
-- Mathlib.Topology.Category.Profinite.Product
/-- The isomorphism of cones induced by `isoindexConeLift`.  -/
Profinite.asLimitindexConeIso : {ι : Type u} →
  {X : ι → Type} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {C : Set ((i : ι) → X i)} →
        [inst_1 : ∀ (i : ι), T2Space (X i)] →
          [inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)] →
            (hC : IsCompact C) → Profinite.indexCone hC ≅ Profinite.limitCone (Profinite.indexFunctor hC)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.toNonUnitalSubring_top : ∀ {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A], ⊤.toNonUnitalSubring = ⊤
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_cast_Ioi : ∀ {m n : ℕ} (h : m = n) (i : Fin n), Fin.cast h ⁻¹' Set.Ioi i = Set.Ioi (Fin.cast ⋯ i)
-- Aesop.RuleSet.Filter
Aesop.RuleSetNameFilter.matches : Aesop.RuleSetNameFilter → Aesop.RuleSetName → Bool
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.ιFunctorObj_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY))
      C]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)]
  [inst_4 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πY)
      (CategoryTheory.SmallObject.functorObjLeft f πY)]
  {Z : C} (h : CategoryTheory.SmallObject.functorObj f πY ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πX)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMap f τ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left τ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πY) h)
-- Mathlib.Data.Set.Basic
Set.univ_unique : ∀ {α : Type u} [inst : Unique α], Set.univ = {default}