mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : LawfulBEq α] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.ExtDHashMap.ofList l).get? k = none
-- Mathlib.Algebra.Algebra.Subalgebra.Centralizer
Algebra.TensorProduct.includeLeftRingHom.eq_1 : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B],
  Algebra.TensorProduct.includeLeftRingHom =
    { toFun := (↑((TensorProduct.AlgebraTensorModule.mk R R A B).flip 1).toAddMonoidHom).toFun, map_one' := ⋯,
      map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Copy of a monoidal structure on a functor `F` with new `ε`, `μ`, `η` and `δ` fields equal to the
old ones.

This is useful to fix definitional equalities.  -/
CategoryTheory.Functor.Monoidal.copy : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (hF : F.Monoidal) →
                (ε' :
                    CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶
                      F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
                  (μ' :
                      (X Y : C) →
                        CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶
                          F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) →
                    (η' :
                        F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
                          CategoryTheory.MonoidalCategoryStruct.tensorUnit D) →
                      (δ' :
                          (X Y : C) →
                            F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶
                              CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) →
                        autoParam (ε' = CategoryTheory.Functor.LaxMonoidal.ε F)
                            CategoryTheory.Functor.Monoidal.copy._auto_1 →
                          autoParam (μ' = CategoryTheory.Functor.LaxMonoidal.μ F)
                              CategoryTheory.Functor.Monoidal.copy._auto_3 →
                            autoParam (η' = CategoryTheory.Functor.OplaxMonoidal.η F)
                                CategoryTheory.Functor.Monoidal.copy._auto_5 →
                              autoParam (δ' = CategoryTheory.Functor.OplaxMonoidal.δ F)
                                  CategoryTheory.Functor.Monoidal.copy._auto_7 →
                                F.Monoidal
-- Mathlib.Order.CompleteLattice.Basic
iSup_of_empty : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] [IsEmpty ι] (f : ι → α), iSup f = ⊥
-- Mathlib.Logic.ExistsUnique
existsUnique_of_exists_of_unique : ∀ {α : Sort u_1} {p : α → Prop}, (∃ x, p x) → (∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂) → ∃! x, p x
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.prod.rightUnitorEquivalence.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.prod.rightUnitorEquivalence C =
    { functor := CategoryTheory.prod.rightUnitor C, inverse := CategoryTheory.prod.rightInverseUnitor C,
      unitIso := CategoryTheory.Iso.refl (CategoryTheory.Functor.id (C × CategoryTheory.Discrete PUnit.{w + 1})),
      counitIso :=
        CategoryTheory.Iso.refl ((CategoryTheory.prod.rightInverseUnitor C).comp (CategoryTheory.prod.rightUnitor C)),
      functor_unitIso_comp := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.orderTop : {α : Type u_1} → [inst : LE α] → [OrderTop α] → OrderTop (Multiplicative α)
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.toSubsemiring_injective : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : StarRing R], Function.Injective StarSubsemiring.toSubsemiring
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Const.alterKey_cons_perm.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (v : β) → motive (some v)),
  (match none with
    | none => h_1 ()
    | some v => h_2 v) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Limits.Concrete.isColimit_exists_rep : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type t}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  [inst_3 : CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)] {D : CategoryTheory.Limits.Cocone F}
  (hD : CategoryTheory.Limits.IsColimit D) (x : CategoryTheory.ToType D.pt),
  ∃ j y, (CategoryTheory.ConcreteCategory.hom (D.ι.app j)) y = x
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The short complex that is part of an exact sequence `L₁.X₁ ⟶ P ⟶ L₀.X₃ ⟶ 0`.  -/
CategoryTheory.ShortComplex.SnakeInput.L₀' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.ShortComplex.SnakeInput C → CategoryTheory.ShortComplex C
-- Mathlib.Logic.Equiv.Defs
/-- Equivalence between equal types.  -/
Equiv.cast : {α β : Sort u_1} → α = β → α ≃ β
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_equivalence_functor_eq_map_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (Q : CategoryTheory.MorphismProperty C) [Q.RespectsIso] (E : C ≌ D), Q.inverseImage E.inverse = Q.map E.functor
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instReprOffset : Repr Std.Time.Minute.Offset
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapCocycles₁_one : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{max u u_1, u, u} k H}
  {B : Rep.{max u u_1, u, u} k G} (φ : Rep.res 1 A ⟶ B), groupCohomology.mapCocycles₁ 1 φ = 0
-- Mathlib.Topology.Filter
Filter.isOpen_Iic_principal : ∀ {α : Type u_2} {s : Set α}, IsOpen (Set.Iic (Filter.principal s))
-- Mathlib.Order.Notation
/-- The infimum/meet operation: `x ⊓ y`. It is notation for `min x y`
and should be used when the type is not a linear order.


Conventions for notations in identifiers:

 * The recommended spelling of `⊓` in identifiers is `inf`. -/
«term_⊓_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.support_smul : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : SMulZeroClass S R] (r : S) (p : Polynomial R),
  (r • p).support ⊆ p.support
-- Mathlib.Tactic.CongrExclamation
Congr!.Config.mk.injEq : ∀ (closePre closePost : Bool) (transparency preTransparency postTransparency : Lean.Meta.TransparencyMode)
  (preferLHS partialApp sameFun : Bool) (maxArgs : Option ℕ)
  (typeEqs etaExpand useCongrSimp beqEq closePre_1 closePost_1 : Bool)
  (transparency_1 preTransparency_1 postTransparency_1 : Lean.Meta.TransparencyMode)
  (preferLHS_1 partialApp_1 sameFun_1 : Bool) (maxArgs_1 : Option ℕ)
  (typeEqs_1 etaExpand_1 useCongrSimp_1 beqEq_1 : Bool),
  ({ closePre := closePre, closePost := closePost, transparency := transparency, preTransparency := preTransparency,
        postTransparency := postTransparency, preferLHS := preferLHS, partialApp := partialApp, sameFun := sameFun,
        maxArgs := maxArgs, typeEqs := typeEqs, etaExpand := etaExpand, useCongrSimp := useCongrSimp, beqEq := beqEq } =
      { closePre := closePre_1, closePost := closePost_1, transparency := transparency_1,
        preTransparency := preTransparency_1, postTransparency := postTransparency_1, preferLHS := preferLHS_1,
        partialApp := partialApp_1, sameFun := sameFun_1, maxArgs := maxArgs_1, typeEqs := typeEqs_1,
        etaExpand := etaExpand_1, useCongrSimp := useCongrSimp_1, beqEq := beqEq_1 }) =
    (closePre = closePre_1 ∧
      closePost = closePost_1 ∧
        transparency = transparency_1 ∧
          preTransparency = preTransparency_1 ∧
            postTransparency = postTransparency_1 ∧
              preferLHS = preferLHS_1 ∧
                partialApp = partialApp_1 ∧
                  sameFun = sameFun_1 ∧
                    maxArgs = maxArgs_1 ∧
                      typeEqs = typeEqs_1 ∧ etaExpand = etaExpand_1 ∧ useCongrSimp = useCongrSimp_1 ∧ beqEq = beqEq_1)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Equiv.union_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ m₄ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₃).WF → (↑m₄).WF → (↑m₁).Equiv ↑m₃ → (↑m₂).Equiv ↑m₄ → (↑(m₁.union m₂)).Equiv ↑(m₃.union m₄)
-- Mathlib.Data.Set.Defs
Set.instMembership : {α : Type u} → Membership α (Set α)
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.annihilator_eq_ker_aeval : ∀ {R : Type u_3} {A : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] [FaithfulSMul A M],
  Module.annihilator (Polynomial R) (Module.AEval R M a) = RingHom.ker (Polynomial.aeval a)
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.iSup_comap_le : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {ι : Sort u_7} (f : G →+ N)
  (s : ι → AddSubgroup N), ⨆ i, AddSubgroup.comap f (s i) ≤ AddSubgroup.comap f (iSup s)
-- Lean.Message
Lean.SerialMessage.toString : Lean.SerialMessage → optParam Bool false → String
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.LiftActionCoreResult.noConfusionType : Sort v✝ → Lean.Elab.Tactic.Grind.LiftActionCoreResult → Lean.Elab.Tactic.Grind.LiftActionCoreResult → Sort v✝
-- Mathlib.Analysis.SpecialFunctions.Pochhammer
/-- `deriv (descPochhammer ℝ n)` is monotone on `(n-1, ∞)`.  -/
monotoneOn_deriv_descPochhammer_eval : ∀ (n : ℕ), MonotoneOn (deriv fun x => Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteVerts_mono' : ∀ {V : Type u} {G G' : SimpleGraph V} (u : Set V), G ≤ G' → (⊤.deleteVerts u).coe ≤ (⊤.deleteVerts u).coe
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- A version of `contract_delete_contract` without the disjointness hypothesis,
and hence a less simple RHS.  -/
Matroid.contract_delete_contract' : ∀ {α : Type u_1} (M : Matroid α) (C D C' : Set α),
  ((M.contract C).delete D).contract C' = (M.contract (C ∪ C' \ D)).delete D
-- Mathlib.Topology.Order.IntermediateValue
IsPreconnected.intermediate_value_Iic : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] {s : Set X},
  IsPreconnected s →
    ∀ {a : X} {l : Filter X},
      a ∈ s →
        ∀ [l.NeBot],
          l ≤ Filter.principal s →
            ∀ {f : X → α}, ContinuousOn f s → Filter.Tendsto f l Filter.atBot → Set.Iic (f a) ⊆ f '' s
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.merge.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool),
  Batteries.PairingHeapImp.Heap.merge le Batteries.PairingHeapImp.Heap.nil Batteries.PairingHeapImp.Heap.nil =
    Batteries.PairingHeapImp.Heap.nil
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
_private.Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution.0.DiscreteConvolution.addFiber_swapEquiv.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] (x : M),
  DiscreteConvolution.addFiber_swapEquiv✝ x =
    {
      toFun := fun x_1 =>
        match x_1 with
        | ⟨p, h⟩ => ⟨p.swap, ⋯⟩,
      invFun := fun x_1 =>
        match x_1 with
        | ⟨p, h⟩ => ⟨p.swap, ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- Helper structure in order to show that a simplicial set is strict Segal.  -/
SSet.StrictSegalCore : SSet → ℕ → Type u
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k},
      List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
        ⟨k, v⟩ ∈ l → (t.insertMany l).get? k' = some (cast ⋯ v)
-- Std.Time.Time.Unit.Basic
/-- Converts a `Minute.Offset` to an `Hour.Offset`.
 -/
Std.Time.Hour.Offset.ofMinutes : Std.Time.Minute.Offset → Std.Time.Hour.Offset
-- Lean.Elab.Do.Basic
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.withTermInfoContext' : Lean.Name → Lean.Syntax → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.ObjectProperty.fullSubcategoryCongr_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P'),
  (CategoryTheory.ObjectProperty.fullSubcategoryCongr h).unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id P.FullSubcategory)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.tendsto_integral_Iic_zero : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a : ι → ℝ} {f : ℝ → E},
  Filter.Tendsto a l Filter.atBot → Filter.Tendsto (fun i => ∫ (x : ℝ) in Set.Iic (a i), f x ∂μ) l (nhds 0)
-- Mathlib.Tactic.CategoryTheory.ToApp
/-- Given an equation `t` of the form `η = θ` between 2-morphisms `f ⟶ g` with `f g : C ⟶ D` in the
bicategory `Cat` (possibly after a `∀` binder), `to_app_of% t` produces the equation
`∀ (X : C), η.app X = θ.app X` (where `X` is an object in the domain of `f` and `g`), and simplifies
it suitably using basic lemmas about `NatTrans.app`.
 -/
Mathlib.Tactic.CategoryTheory.ToApp.«termTo_app_of%_» : Lean.ParserDescr
-- Init.Data.Nat.Gcd
Nat.gcd_succ : ∀ (x y : ℕ), x.succ.gcd y = (y % x.succ).gcd x.succ
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.tail.aux.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (α × Stream'.WSeq α) → Sort u_2) (fst : α) (s : Stream'.WSeq α)
  (h_1 : Unit → motive none) (h_2 : (fst : α) → (s : Stream'.WSeq α) → motive (some (fst, s))),
  (match some (fst, s) with
    | none => h_1 ()
    | some (fst, s) => h_2 fst s) =
    h_2 fst s
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.revMatchesAt_iff_exists_isRevMatch : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt pat pos ↔
    ∃ startPos, ∃ (h : startPos ≤ pos), String.Slice.Pattern.Model.IsRevMatch pat (pos.sliceTo startPos h)
-- Init.Grind.Ring.Field
Lean.Grind.Field.mul_div : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {x y z : α}, x * (y / z) = x * y / z
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearEquiv.quotKerEquivRange.eq_1 : ∀ {R : Type u_1} {M : Type u_3} {Nₗ : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup Nₗ]
  [inst_3 : Module R M] [inst_4 : Module R Nₗ] {fₗ : M →ₗ[R] Nₗ} [inst_5 : TopologicalSpace M]
  [inst_6 : TopologicalSpace Nₗ] (hf : Topology.IsStrictMap ⇑fₗ),
  ContinuousLinearEquiv.quotKerEquivRange hf = ContinuousLinearEquiv.ofIsHomeomorph fₗ.quotKerEquivRange ⋯
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.apply_linearCombination_id : ∀ {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_8}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M') (l : M →₀ R),
  f ((Finsupp.linearCombination R id) l) = (Finsupp.linearCombination R ⇑f) l
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.brecOn.eq : ∀ {motive : Lean.Grind.Linarith.Expr → Sort u} (t : Lean.Grind.Linarith.Expr)
  (F_1 : (t : Lean.Grind.Linarith.Expr) → Lean.Grind.Linarith.Expr.below t → motive t),
  Lean.Grind.Linarith.Expr.brecOn t F_1 = F_1 t (Lean.Grind.Linarith.Expr.brecOn.go t F_1).2
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
ringKrullDim_le_ringKrullDim_quotient_add_card : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (s : Finset R),
  ↑s ⊆ ↑(Ring.jacobson R) → ringKrullDim R ≤ ringKrullDim (R ⧸ Ideal.span ↑s) + ↑s.card
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderUnitor.leftUnitor_hom_mem : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  (P : CategoryTheory.MorphismProperty C) [self : P.IsStableUnderUnitor] (c : C),
  P (CategoryTheory.MonoidalCategoryStruct.leftUnitor c).hom
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Measurable.iInf_Prop : ∀ {δ : Type u_4} {mδ : MeasurableSpace δ} {α : Type u_5} {mα : MeasurableSpace α}
  [inst : ConditionallyCompleteLattice α] (p : Prop) {f : δ → α}, Measurable f → Measurable fun b => ⨅ (_ : p), f b
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.uniformSpace_eq_inf_precomp_of_cover : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] (𝔖 : Set (Set α)) {δ₁ : Type u_5} {δ₂ : Type u_6} (φ₁ : δ₁ → α)
  (φ₂ : δ₂ → α) (𝔗₁ : Set (Set δ₁)) (𝔗₂ : Set (Set δ₂)),
  Set.MapsTo (fun x => φ₁ '' x) 𝔗₁ 𝔖 →
    Set.MapsTo (fun x => φ₂ '' x) 𝔗₂ 𝔖 →
      Set.MapsTo (fun x => φ₁ ⁻¹' x) 𝔖 𝔗₁ →
        Set.MapsTo (fun x => φ₂ ⁻¹' x) 𝔖 𝔗₂ →
          (∀ S ∈ 𝔖, S ⊆ Set.range φ₁ ∪ Set.range φ₂) →
            UniformOnFun.uniformSpace α β 𝔖 =
              UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔗₁) ∘ (fun x => x ∘ φ₁) ∘ ⇑(UniformOnFun.toFun 𝔖))
                  (UniformOnFun.uniformSpace δ₁ β 𝔗₁) ⊓
                UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(UniformOnFun.toFun 𝔖))
                  (UniformOnFun.uniformSpace δ₂ β 𝔗₂)
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeEquiv_apply : ∀ {α : Sort u_1} {β : Sort u_4} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (e a))
  (a : { a // p a }), (e.subtypeEquiv h) a = ⟨e ↑a, ⋯⟩
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.mem_span_image_iff_linearCombination : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M} {s : Set α} {x : M},
  x ∈ Submodule.span R (v '' s) ↔ ∃ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termL₁'_1 : Lean.ParserDescr
-- Std.Sync.Mutex
_private.Std.Sync.Mutex.0.Std.Mutex.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (ref : IO.Ref α) (mutex : Std.BaseMutex),
  sizeOf { ref := ref, mutex := mutex } = 1 + sizeOf ref + sizeOf mutex
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_eq_default : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Inhabited α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l = false → Std.Internal.List.getKey! a l = default
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.mk.injEq : ∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] (toFun : X → Y)
  (isLocallyConstant : IsLocallyConstant toFun) (toFun_1 : X → Y) (isLocallyConstant_1 : IsLocallyConstant toFun_1),
  ({ toFun := toFun, isLocallyConstant := isLocallyConstant } =
      { toFun := toFun_1, isLocallyConstant := isLocallyConstant_1 }) =
    (toFun = toFun_1)
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.homeomorph_comp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E],
  IsQuotientCoveringMap f G →
    ∀ {Y : Type u_4} [inst_4 : TopologicalSpace Y] (φ : X ≃ₜ Y), IsQuotientCoveringMap (⇑φ ∘ f) G
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.continuousAt_add_coe_coe : ∀ (a b : ℝ), ContinuousAt (fun p => p.1 + p.2) (↑a, ↑b)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- Notation for `Measurable` with respect to a non-standard σ-algebra in the domain.  -/
MeasureTheory.«termMeasurable[_]» : Lean.ParserDescr
-- Init.Data.Nat.Basic
Nat.ctor_eq_zero : Nat.zero = 0
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.HasExplicitFiniteCoproducts.mk : ∀ {P : TopCat → Prop},
  (∀ {α : Type w} [Finite α] (X : α → CompHausLike P), CompHausLike.HasExplicitFiniteCoproduct X) →
    CompHausLike.HasExplicitFiniteCoproducts P
-- Mathlib.Probability.Independence.Basic
/-- Two functions are independent if the two measurable space structures they generate are
independent. For a function `f` with codomain having measurable space structure `m`, the generated
measurable space structure is `MeasurableSpace.comap f m`.
We use the notation `f ⟂ᵢ[μ] g` for `IndepFun f g μ` (scoped in `ProbabilityTheory`).  -/
ProbabilityTheory.IndepFun : {Ω : Type u_1} →
  {β : Type u_6} →
    {γ : Type u_7} →
      {_mΩ : MeasurableSpace Ω} →
        [MeasurableSpace β] →
          [MeasurableSpace γ] →
            (Ω → β) → (Ω → γ) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IndepFun._auto_1 → Prop
-- Init.Core
/-- A dependent recursion principle for `Quot` that uses [heterogeneous
equality](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=HEq), analogous to a [recursor](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=recursors) for
a structure.

`Quot.recOn` is a version of this recursor that uses `Eq` instead of `HEq`.
 -/
Quot.hrecOn : {α : Sort u} →
  {r : α → α → Prop} →
    {motive : Quot r → Sort v} →
      (q : Quot r) → (f : (a : α) → motive (Quot.mk r a)) → (∀ (a b : α), r a b → f a ≍ f b) → motive q
-- Lean.Expr
Lean.MVarId.name : Lean.MVarId → Lean.Name
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- If `r ≠ 0` and `‖pₙ‖ rⁿ = O(aⁿ)` for some `-1 < a < 1`, then `r < p.radius`.  -/
FormalMultilinearSeries.lt_radius_of_isBigO : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal},
  r ≠ 0 → ∀ {a : ℝ}, a ∈ Set.Ioo (-1) 1 → ((fun n => ‖p n‖ * ↑r ^ n) =O[Filter.atTop] fun x => a ^ x) → ↑r < p.radius
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.isoMk_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom)
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f)))
      CategoryTheory.Oplax.OplaxTrans.isoMk._auto_1)
  (a : B), (CategoryTheory.Oplax.OplaxTrans.isoMk app naturality).hom.as.app a = (app a).hom
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.instIsNoetherianSpecOfOfIsNoetherianRing : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R],
  AlgebraicGeometry.IsNoetherian (AlgebraicGeometry.Spec (CommRingCat.of R))
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.subgroup_strong_bound_left : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G},
  ↑(A * A).card < 3 / 2 * ↑A.card → ∀ a ∈ A, A * A ⊆ a • MulOpposite.op a • (A⁻¹ * A)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aevalTower_id : ∀ {S : Type v} [inst : CommSemiring S], Polynomial.aevalTower (AlgHom.id S S) = Polynomial.aeval