mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Multiset.Find
_private.Mathlib.Data.Multiset.Find.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.tosSupHom : {α : Type u_8} →
  {β : Type u_9} → [inst : CompleteLattice α] → [inst_1 : CompleteLattice β] → CompleteLatticeHom α β → sSupHom α β
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.instLE : {rel : ℤ → ℤ → Prop} → {n m : ℤ} → LE (Std.Time.Internal.Bounded rel n m)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instIsSMulApply : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F], IsSMulApply 𝕜 (SchwartzMap E F) E F
-- Mathlib.Algebra.Order.ToIntervalMod
QuotientAddGroup.equivIcoMod_coe : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), (QuotientAddGroup.equivIcoMod hp a) ↑b = ⟨toIcoMod hp a b, ⋯⟩
-- Init.Data.SInt.Lemmas
ISize.ofIntLE_mul : ∀ {a b : ℤ} {hab₁ : ISize.minValue.toInt ≤ a * b} {hab₂ : a * b ≤ ISize.maxValue.toInt},
  ISize.ofIntLE (a * b) hab₁ hab₂ = ISize.ofInt a * ISize.ofInt b
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_ne_one : ∀ {r : NNReal}, ↑r ≠ 1 ↔ r ≠ 1
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.binomial_real_zero : ∀ (n : ℕ) (p : ↑unitInterval), (ProbabilityTheory.binomial n p).real {0} = (1 - ↑p) ^ n
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.measurable_poissonPMFReal : ∀ (r : NNReal), Measurable (ProbabilityTheory.poissonPMFReal r)
-- Init.Data.List.Attach
List.attachWith_cons : ∀ {α : Type u_1} {x : α} {xs : List α} {p : α → Prop} (h : ∀ a ∈ x :: xs, p a),
  (x :: xs).attachWith p h = ⟨x, ⋯⟩ :: xs.attachWith p ⋯
-- Mathlib.LinearAlgebra.LinearPMap
/-- Compose a linear map with a `LinearPMap`  -/
LinearMap.compPMap : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : Ring R] →
        [inst_1 : Ring S] →
          [inst_2 : Ring T] →
            {σ : R →+* S} →
              {τ : S →+* T} →
                {E : Type u_4} →
                  [inst_3 : AddCommGroup E] →
                    [inst_4 : Module R E] →
                      {F : Type u_5} →
                        [inst_5 : AddCommGroup F] →
                          [inst_6 : Module S F] →
                            {G : Type u_6} →
                              [inst_7 : AddCommGroup G] →
                                [inst_8 : Module T G] →
                                  {ρ : R →+* T} → [RingHomCompTriple σ τ ρ] → (F →ₛₗ[τ] G) → (E →ₛₗ.[σ] F) → E →ₛₗ.[ρ] G
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2ComputableInTime.mk.injEq : ∀ {α β αΓ βΓ : Type} {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β}
  (toTM2ComputableAux : Turing.TM2ComputableAux αΓ βΓ) (time : ℕ → ℕ)
  (outputsFun :
    (a : α) →
      Turing.TM2OutputsInTime toTM2ComputableAux.tm (List.map toTM2ComputableAux.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux.outputAlphabet.invFun (eb (f a)))) (time (ea a).length))
  (toTM2ComputableAux_1 : Turing.TM2ComputableAux αΓ βΓ) (time_1 : ℕ → ℕ)
  (outputsFun_1 :
    (a : α) →
      Turing.TM2OutputsInTime toTM2ComputableAux_1.tm (List.map toTM2ComputableAux_1.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux_1.outputAlphabet.invFun (eb (f a)))) (time_1 (ea a).length)),
  ({ toTM2ComputableAux := toTM2ComputableAux, time := time, outputsFun := outputsFun } =
      { toTM2ComputableAux := toTM2ComputableAux_1, time := time_1, outputsFun := outputsFun_1 }) =
    (toTM2ComputableAux = toTM2ComputableAux_1 ∧ time = time_1 ∧ outputsFun ≍ outputsFun_1)
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.HasEval.zero : ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : TopologicalSpace S], PowerSeries.HasEval 0
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lmul'_comp_includeRight : ∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  (Algebra.TensorProduct.lmul' R).comp Algebra.TensorProduct.includeRight = AlgHom.id R S
-- Mathlib.Algebra.Order.ToIntervalMod
self_sub_toIcoDiv_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R), b - ↑(toIcoDiv hp a b) * p = toIcoMod hp a b
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_inf_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {f g : ι → α},
  min (⨅ x, f x) (⨅ x, g x) ≤ ⨅ x, min (f x) (g x)
-- Mathlib.Algebra.Category.ModuleCat.Products
/-- The categorical product of a family of objects in `ModuleCat`
agrees with the usual module-theoretical product.
 -/
ModuleCat.piIsoPi : {R : Type u} →
  [inst : Ring R] →
    {ι : Type v} →
      (Z : ι → ModuleCat R) → [inst_1 : CategoryTheory.Limits.HasProduct Z] → ∏ᶜ Z ≅ ModuleCat.of R ((i : ι) → ↑(Z i))
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.add_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f g : T₁ ⟶ T₂), (f + g).hom₂ = f.hom₂ + g.hom₂
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.case.inj : ∀ {tid : Lean.Name} {x : Lean.IR.VarId} {xType : Lean.IR.IRType} {cs : Array Lean.IR.Alt} {tid_1 : Lean.Name}
  {x_1 : Lean.IR.VarId} {xType_1 : Lean.IR.IRType} {cs_1 : Array Lean.IR.Alt},
  Lean.IR.FnBody.case tid x xType cs = Lean.IR.FnBody.case tid_1 x_1 xType_1 cs_1 →
    tid = tid_1 ∧ x = x_1 ∧ xType = xType_1 ∧ cs = cs_1
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.compl_symm : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α] {m : ℕ} {hm : m + n = Fintype.card α},
  (Set.powersetCard.compl hm).symm = Set.powersetCard.compl ⋯
-- Mathlib.Combinatorics.Matroid.Closure
/-- A set is `spanning` in `M` if its closure is equal to `M.E`, or equivalently if it contains
a base of `M`.  -/
Matroid.Spanning : {α : Type u_2} → Matroid α → Set α → Prop
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- Indexed version of `exists_linearIndependent`.  -/
exists_linearIndependent' : ∀ {ι : Type u'} (K : Type u_3) {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (v : ι → V),
  ∃ κ a,
    Function.Injective a ∧
      Submodule.span K (Set.range (v ∘ a)) = Submodule.span K (Set.range v) ∧ LinearIndependent K (v ∘ a)
-- Aesop.RuleTac.Cases
Aesop.CasesTarget'.patterns.inj : ∀ {ps ps_1 : Array (Lean.Expr × Lean.Meta.SavedState)},
  Aesop.CasesTarget'.patterns ps = Aesop.CasesTarget'.patterns ps_1 → ps = ps_1
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : (↑U).Opens),
  AlgebraicGeometry.Scheme.Hom.app (f ∣_ U) V =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.app f ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V))
      (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.range_lift_eq_closure : ∀ {α : Type u} {β : Type v} [inst : AddGroup β] {f : α → β},
  (FreeAddGroup.lift f).range = AddSubgroup.closure (Set.range f)
-- Lean.Syntax
Lean.Syntax.Range.mk : String.Pos.Raw → String.Pos.Raw → Lean.Syntax.Range
-- Init.Data.Vector.Lemmas
Vector.cast_cast : ∀ {α : Type u_1} {n m k : ℕ} {xs : Vector α n} {w : n = m} {w' : m = k},
  Vector.cast w' (Vector.cast w xs) = Vector.cast ⋯ xs
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- For `f : F` where `F` is a class of continuous additive monoid hom, this yields
an element `ContinuousAddMonoidHom A B`.  -/
ContinuousAddMonoidHom.ofClass : (A : Type u_2) →
  (B : Type u_3) →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : TopologicalSpace B] →
            (F : Type u_7) →
              [inst_4 : FunLike F A B] → [ContinuousMapClass F A B] → [AddMonoidHomClass F A B] → F → A →ₜ+ B
-- Lean.Elab.DeclModifiers
Lean.Elab.mkDeclName : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadError m] →
        [MonadFinally m] →
          [Lean.Elab.MonadInfoTree m] → Lean.Name → Lean.Elab.Modifiers → Lean.Name → m (Lean.Name × Lean.Name)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.comp_eq_zero_iff_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  (f : X ⟶ Y) {g : Y ⟶ Z} [CategoryTheory.Epi f], CategoryTheory.CategoryStruct.comp f g = 0 ↔ g = 0
-- Std.Http.Protocol.H1.Error
/-- Specific HTTP processing errors with detailed information.
 -/
Std.Http.Protocol.H1.Error : Type
-- Mathlib.Algebra.Notation.Pi.Defs
/-- **Alias** of `Function.prod`. -/
Pi.prod : {ι : Sort u_3} → {α : ι → Type u_1} → {β : ι → Type u_2} → ((i : ι) → α i) → ((i : ι) → β i) → (i : ι) → α i × β i
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.continuous_iff_continuous_comp : ∀ {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [inst : AddCommGroup E]
  [inst_1 : NormedField 𝕝] [inst_2 : Module 𝕝 E] [inst_3 : AddCommGroup F] [inst_4 : NormedField 𝕝₂]
  [inst_5 : Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [inst_6 : RingHomIsometric τ₁₂] {q : SeminormFamily 𝕝₂ F ι'}
  [inst_7 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_9 : TopologicalSpace F],
  WithSeminorms q → ∀ (f : E →ₛₗ[τ₁₂] F), Continuous ⇑f ↔ ∀ (i : ι'), Continuous ⇑((q i).comp f)
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a Haar measure under a continuous surjective proper group homomorphism is again
a Haar measure. See also `MulEquiv.isHaarMeasure_map` and `ContinuousMulEquiv.isHaarMeasure_map`.  -/
MeasureTheory.Measure.isHaarMeasure_map : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [BorelSpace G] [ContinuousMul G] {H : Type u_3} [inst_6 : Group H]
  [inst_7 : TopologicalSpace H] [inst_8 : MeasurableSpace H] [BorelSpace H] [IsTopologicalGroup H] (f : G →* H),
  Continuous ⇑f →
    Function.Surjective ⇑f →
      Filter.Tendsto (⇑f) (Filter.cocompact G) (Filter.cocompact H) → (MeasureTheory.Measure.map (⇑f) μ).IsHaarMeasure
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : β → β},
  (t.modify k f).getKey? k = if k ∈ t then some k else none
-- Mathlib.CategoryTheory.Core
/-- We can functorially associate to any functor from a groupoid to the core of a category `C`,
a functor from the groupoid to `C`, simply by composing with the embedding `Core C ⥤ C`.
 -/
CategoryTheory.Core.forgetFunctorToCore : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {G : Type u₂} →
      [inst_1 : CategoryTheory.Groupoid G] →
        CategoryTheory.Functor (CategoryTheory.Functor G (CategoryTheory.Core C)) (CategoryTheory.Functor G C)
-- Mathlib.Order.RelIso.Basic
RelEmbedding.stdRefl : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [Std.Refl s], Std.Refl r
-- Mathlib.CategoryTheory.Sites.Pretopology
/-- For all `X : C`, the coverings of `X` (sets of families of morphisms with target `X`)  -/
CategoryTheory.Pretopology.has_isos : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (self : CategoryTheory.Pretopology C) ⦃X Y : C⦄ (f : Y ⟶ X) [CategoryTheory.IsIso f],
  CategoryTheory.Presieve.singleton f ∈ self.coverings X
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_strictMono : ∀ {α : Type u} [Finite α], StrictMono (Cardinal.mk ∘ Set.Elem)
-- Mathlib.RingTheory.ZariskisMainTheorem
_private.Mathlib.RingTheory.ZariskisMainTheorem.0.Algebra.ZariskisMainProperty.of_algHom_polynomial : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
  [Algebra.WeaklyQuasiFiniteAt R p] (f : Polynomial R →ₐ[R] S), f.Finite → Algebra.ZariskisMainProperty R p
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms_assoc : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.Scheme} (f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y)
  (hf :
    ∀ (x y : 𝒰.I₀),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (f x) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) (f y))
  (x : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (𝒰.f x)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.glueMorphisms 𝒰 f hf) h) =
    CategoryTheory.CategoryStruct.comp (f x) h
-- Mathlib.Data.Int.Fib.Basic
Int.fib_of_odd : ∀ {n : ℤ}, Odd n → Int.fib n = ↑(Nat.fib n.natAbs)
-- Mathlib.Data.Seq.Computation
Computation.exists_results_of_mem : ∀ {α : Type u} {s : Computation α} {a : α}, a ∈ s → ∃ n, s.Results a n
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_mem_matrix_iff : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {S : Set α} {M : Matrix m n α}, M.transpose ∈ S.matrix ↔ M ∈ S.matrix
-- Mathlib.Analysis.Normed.Group.InfiniteSum
/-- Quantitative result associated to the direct comparison test for series:  If `∑' i, g i` is
summable, and for all `i`, `‖f i‖ ≤ g i`, then `‖∑' i, f i‖ ≤ ∑' i, g i`. Note that we do not
assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete space.  -/
tsum_of_norm_bounded : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E} {g : ι → ℝ} {a : ℝ},
  HasSum g a → (∀ (i : ι), ‖f i‖ ≤ g i) → ‖∑' (i : ι), f i‖ ≤ a
-- Mathlib.Algebra.GroupWithZero.Action.Prod
Prod.smulWithZero : {M : Type u_1} →
  {N : Type u_2} →
    {R : Type u_5} →
      [inst : Zero R] →
        [inst_1 : Zero M] → [inst_2 : Zero N] → [SMulWithZero R M] → [SMulWithZero R N] → SMulWithZero R (M × N)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.projKerOfRightInverse_apply_idem : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Ring R₁] [inst_1 : Ring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] {M₁ : Type u_4} {M₂ : Type u_5} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommGroup M₁] [inst_5 : Module R₁ M₁] [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommGroup M₂]
  [inst_8 : Module R₂ M₂] [inst_9 : IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁)
  (h : Function.RightInverse ⇑f₂ ⇑f₁) (x : ↥(↑f₁).ker), (f₁.projKerOfRightInverse f₂ h) ↑x = x
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
/-- The underlying topology of `Proj` is the projective spectrum of graded ring `A`.  -/
ProjectiveSpectrum.top : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] → [inst_2 : AddSubmonoidClass σ A] → (𝒜 : ℕ → σ) → [GradedRing 𝒜] → TopCat
-- Mathlib.Data.Nat.Init
Nat.two_mul_ne_two_mul_add_one : ∀ {m n : ℕ}, 2 * n ≠ 2 * m + 1
-- Mathlib.Combinatorics.Graph.Lattice
Graph.vertexSet_inf : ∀ {α : Type u_1} {β : Type u_2} (G H : Graph α β), (G ⊓ H).vertexSet = G.vertexSet ∩ H.vertexSet
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.WithGeneratedByTopology.isOpen_iff : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {U : Set (Topology.WithGeneratedByTopology X Y)},
  IsOpen U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen (⇑f ⁻¹' ⇑Topology.WithGeneratedByTopology.equiv.symm ⁻¹' U)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.disjoint_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f g : Equiv.Perm α},
  f.Disjoint g → Disjoint f.support g.support
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
/-- The sequence of maps which gives the null homotopic maps `Hσ` that shall be in
the inductive construction of the projections `P q : K[X] ⟶ K[X]`  -/
AlgebraicTopology.DoldKan.hσ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] →
      {X : CategoryTheory.SimplicialObject C} →
        ℕ → (n : ℕ) → X.obj (Opposite.op { len := n }) ⟶ X.obj (Opposite.op { len := n + 1 })
-- Mathlib.Analysis.Distribution.Support
/-- A distribution `f` vanishes on a set `s` if it vanishes for all test functions `u` with
`tsupport u ⊆ s`.

To make this definition work for all types of distributions, we define it for any function from
a `FunLike` type to a type with zero.  -/
Distribution.IsVanishingOn : {α : Type u_2} →
  {β : Type u_3} →
    {F : Type u_6} →
      {V : Type u_10} → [FunLike F α β] → [TopologicalSpace α] → [Zero β] → [Zero V] → (F → V) → Set α → Prop
-- Mathlib.Topology.Metrizable.Uniformity
PseudoMetricSpace.dist_ofPreNNDist_le : ∀ {X : Type u_1} (d : X → X → NNReal) (dist_self : ∀ (x : X), d x x = 0) (dist_comm : ∀ (x y : X), d x y = d y x)
  (x y : X), dist x y ≤ ↑(d x y)
-- Lean.Elab.Tactic.Try
/-- Returns `true` IF `tacs2` contains only tactics of the same kind, and one of the following
- contains `simp only ...` and `simp ...`
- contains `grind only ..` and `grind ...`

We say suggestions mixing `only` and non-`only` tactics are suboptimal and should not be displayed to
the user.
 -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.isOnlyAndNonOnly : Array (Lean.TSyntax `tactic) → Bool
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenEnd.hom_ext_iff : ∀ {J : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_3} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C] {X : C} {f g : X ⟶ CategoryTheory.Limits.chosenEnd F},
  f = g ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.chosenEnd.π F j) =
        CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.chosenEnd.π F j)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.liftCycles_comp_cyclesMap_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} {i : ι} [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j)
  (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (φ : K ⟶ L) {Z : C} (h : L.cycles i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj hk)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) h) =
    CategoryTheory.CategoryStruct.comp (L.liftCycles (CategoryTheory.CategoryStruct.comp k (φ.f i)) j hj ⋯) h
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.div_iUnion₂ : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Div α] (s : Set α) (t : (i : ι) → κ i → Set α),
  s / ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s / t i j
-- Mathlib.Data.Finset.Insert
Finset.exists_mem_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α) (p : α → Prop),
  (∃ x ∈ insert a s, p x) ↔ p a ∨ ∃ x ∈ s, p x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_eq_none_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → (t.min? = none ↔ t.isEmpty = true)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.isOpenMap_apply : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → TopologicalSpace (β i)] (i : ι),
  IsOpenMap fun f => f.ofLp i
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A normed commutative ring is a commutative ring endowed with a norm which satisfies
the inequality `‖x y‖ ≤ ‖x‖ ‖y‖`.  -/
NormedCommRing : Type u_5 → Type u_5
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mem_iSup_of_mem : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_4}
  {b : M} {p : ι → Submodule R M} (i : ι), b ∈ p i → b ∈ ⨆ i, p i
-- Lean.Compiler.NameMangling
/-- The mangled name of the name used to create the module initialization function.

This also used for the library name of a module plugin.
 -/
Lean.mkModuleInitializationStem : Lean.Name → optParam (Option Lean.PkgId) none → String
-- Std.Data.Internal.List.Associative
Std.Internal.List.List.getValue?_filter_containsKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getValue? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) =
      if Std.Internal.List.containsKey k l₂ = true then Std.Internal.List.getValue? k l₁ else none
-- Lean.LibrarySuggestions.Basic
/-- Wrapper for `Selector` that ensures
the `maxSuggestions` field in `Config` is respected, post-hoc.
 -/
Lean.LibrarySuggestions.Selector.maxSuggestions : Lean.LibrarySuggestions.Selector → Lean.LibrarySuggestions.Selector
-- Mathlib.Analysis.LocallyConvex.PointwiseConvergence
/-- The coercion `E →SLₚₜ[σ] F` to `E → F` as a linear map.

The topology on `E →SLₚₜ[σ] F` is induced by this map.  -/
PointwiseConvergenceCLM.inducingFn : {𝕜₁ : Type u_3} →
  {𝕜₂ : Type u_4} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          (E : Type u_7) →
            (F : Type u_8) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : NormedAddCommGroup F] → [inst_6 : NormedSpace 𝕜₂ F] → (E →SLₚₜ[σ] F) →ₗ[𝕜₂] E → F
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instHasDistribNeg : HasDistribNeg Complex.UnitClosedDisc
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.subtype_injective : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (L : BooleanSubalgebra α), Function.Injective ⇑L.subtype
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.erase_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {k : α}, ∅.erase k = ∅
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySumFactor.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.convexBodySumFactor K =
    2 ^ NumberField.InfinitePlace.nrRealPlaces K * (NNReal.pi / 2) ^ NumberField.InfinitePlace.nrComplexPlaces K /
      ↑(Module.finrank ℚ K).factorial
-- Mathlib.Logic.Equiv.Multiset
Denumerable.lower.eq_1 : ∀ (x : ℕ), Denumerable.lower [] x = []
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobjectMap_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'}
  [inst_3 : CategoryTheory.Limits.HasKernel f'] {X'' Y'' : C} {f'' : X'' ⟶ Y''}
  [inst_4 : CategoryTheory.Limits.HasKernel f''] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
  (sq' : CategoryTheory.Arrow.mk f' ⟶ CategoryTheory.Arrow.mk f''),
  CategoryTheory.Limits.kernelSubobjectMap (CategoryTheory.CategoryStruct.comp sq sq') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq)
      (CategoryTheory.Limits.kernelSubobjectMap sq')
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
/-- The compositum of two intermediate fields is equal to the compositum of them
as subalgebras, if one of them is algebraic over the base field.  -/
IntermediateField.sup_toSubalgebra_of_isAlgebraic : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (E1 E2 : IntermediateField K L),
  Algebra.IsAlgebraic K ↥E1 ∨ Algebra.IsAlgebraic K ↥E2 → (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra