mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.phase.injEq : ∀ (p p_1 : Aesop.PhaseName), (Aesop.Frontend.Feature.phase p = Aesop.Frontend.Feature.phase p_1) = (p = p_1)
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.associatesNonZeroDivisorsEquivIsPrincipal_mul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (x y : Associates ↥(nonZeroDivisors R)),
  ↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) (x * y)) =
    ↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) x) *
      ↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) y)
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.ComonadicLeftAdjoint.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          (R : CategoryTheory.Functor D C) →
            (adj : L ⊣ R) →
              (CategoryTheory.Comonad.comparison adj).IsEquivalence → CategoryTheory.ComonadicLeftAdjoint L
-- Mathlib.Analysis.Normed.Module.FiniteDimension
summable_of_isEquivalent_nat : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {f g : ℕ → E},
  Summable g → Asymptotics.IsEquivalent Filter.atTop f g → Summable f
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
nhds_comap_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (a : α), Filter.comap (fun x => dist x a) (nhds 0) = nhds a
-- Mathlib.Algebra.GroupWithZero.Regular
/-- In a non-trivial integral domain, an element is regular iff it is non-zero.  -/
isRegular_iff_ne_zero : ∀ {R : Type u_1} [inst : MulZeroClass R] [IsCancelMulZero R] {a : R} [Nontrivial R], IsRegular a ↔ a ≠ 0
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {V W : (x : M) → TangentSpace I x},
  VectorField.mlieBracketWithin I V W Set.univ = VectorField.mlieBracket I V W
-- Lean.Elab.DocString
/-- A canonical way to convert a documentation extension's argument into a Lean value of type `α`.
 -/
Lean.Doc.FromDocArg : Type → Type
-- Mathlib.Order.Filter.Map
Filter.map_surjOn_Iic_iff_surjOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β},
  Set.SurjOn (Filter.map m) (Set.Iic (Filter.principal s)) (Set.Iic (Filter.principal t)) ↔ Set.SurjOn m s t
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.fiberHomeomorph.eq_1 : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] {x : X} (h : IsEvenlyCovered f x I),
  h.fiberHomeomorph =
    (fun U x_1 =>
        (fun H hH =>
            { toFun := fun i => ⟨↑(H.symm (⟨x, ⋯⟩, i)), ⋯⟩, invFun := fun e => (H ⟨↑e, ⋯⟩).2, left_inv := ⋯,
              right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ })
          (Classical.choose ⋯) ⋯)
      (Classical.choose ⋯) ⋯
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.starMemClass : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : StarRing R], StarMemClass (StarSubsemiring R) R
-- Mathlib.Data.Set.Image
Subtype.range_val_subtype : ∀ {α : Type u_1} {p : α → Prop}, Set.range Subtype.val = {x | p x}
-- Mathlib.Order.Lattice.Nat
Nat.nonempty_of_sInf_eq_succ : ∀ {s : Set ℕ} {k : ℕ}, sInf s = k + 1 → s.Nonempty
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_preimage : ∀ {α : Type u_2} [inst : Inv α] {s : Set α}, Inv.inv ⁻¹' s = s⁻¹
-- Init.Data.Vector.Perm
Vector.Perm.trans : ∀ {α : Type u_1} {n : ℕ} {xs ys zs : Vector α n}, xs.Perm ys → ys.Perm zs → xs.Perm zs
-- Init.Data.Sum.Lemmas
Sum.getRight?_eq_some_iff : ∀ {β : Type u_1} {b : β} {α : Type u_2} {x : α ⊕ β}, x.getRight? = some b ↔ x = Sum.inr b
-- Batteries.Data.List.Lemmas
List.rel_of_isChain_cons_cons : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α}, List.IsChain R (a :: b :: l) → R a b
-- Mathlib.GroupTheory.OrderOfElement
coe_powCardSubgroup : ∀ {G : Type u_6} [inst : Group G] [inst_1 : Fintype G] (S : Set G) (hS : S.Nonempty),
  ↑(powCardSubgroup S hS) = S ^ Fintype.card G
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.contains_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.contains k = t₂.contains k
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.toLinearMap_apply_CoPolarization : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι]
  (x : N), P.toLinearMap (P.CoPolarization x) = P.CorootForm x
-- Mathlib.NumberTheory.Real.Irrational
Irrational.ne_ofNat : ∀ {x : ℝ}, Irrational x → ∀ (n : ℕ) [inst : n.AtLeastTwo], x ≠ OfNat.ofNat n
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_union : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} (s t : Set M), PointedCone.dual p (s ∪ t) = PointedCone.dual p s ⊓ PointedCone.dual p t
-- Mathlib.Analysis.Calculus.Deriv.AffineMap
AffineMap.differentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {s : Set 𝕜} {x : 𝕜}, DifferentiableWithinAt 𝕜 (⇑f) s x
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableOn.coordChangeL : ∀ {𝕜 : 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)]
  {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [inst_18 : MemTrivializationAtlas e]
  [inst_19 : MemTrivializationAtlas e'] [inst_20 : VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {s : Set M}
  {f : M → B},
  MDiff[s] f →
    Set.MapsTo f s e.baseSet →
      Set.MapsTo f s e'.baseSet → MDiff[s] fun y => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' (f y))
-- Mathlib.GroupTheory.FiniteAbelian.Duality
CommGroup.subgroupOrderIsoSubgroupMonoidHom.congr_simp : ∀ (G : Type u_1) (M : Type u_2) [inst : CommGroup G] [inst_1 : Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)],
  CommGroup.subgroupOrderIsoSubgroupMonoidHom G M = CommGroup.subgroupOrderIsoSubgroupMonoidHom G M
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_append_extract : ∀ {a : ByteArray} {i j k : ℕ}, a.extract i j ++ a.extract j k = a.extract (min i j) (max j k)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- Given a continuous bilinear map `G → E → F`, construct the associated continuous bilinear map
`G → Lp E p μ → Lp F p μ`.  -/
ContinuousLinearMap.compLpL₂ : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      (p : ENNReal) →
        (μ : MeasureTheory.Measure α) →
          [inst : NormedAddCommGroup E] →
            {𝕜 : Type u_6} →
              [inst_1 : NontriviallyNormedField 𝕜] →
                [inst_2 : NormedSpace 𝕜 E] →
                  {F : Type u_8} →
                    {G : Type u_9} →
                      [inst_3 : NormedAddCommGroup F] →
                        [inst_4 : NormedSpace 𝕜 F] →
                          [inst_5 : NormedAddCommGroup G] →
                            [inst_6 : NormedSpace 𝕜 G] →
                              [inst_7 : Fact (1 ≤ p)] →
                                (G →L[𝕜] E →L[𝕜] F) → G →L[𝕜] ↥(MeasureTheory.Lp E p μ) →L[𝕜] ↥(MeasureTheory.Lp F p μ)
-- Lean.Meta.SynthInstance
Lean.Meta.trace.Meta.synthInstance : Lean.Option Bool
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.boundedFormula_realize_eq_realize : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} (φ : L.Formula α) (x : α → M)
  (y : Fin 0 → M), FirstOrder.Language.BoundedFormula.Realize φ x y ↔ φ.Realize x
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- A submodule `I` is a fractional ideal with respect to a submonoid `S`
if `a I ⊆ R` for some `a ∈ S`.  -/
IsFractional : {R : Type u_1} →
  [inst : CommRing R] →
    Submonoid R → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → Submodule R P → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.ι_coproductUniqueIso_hom : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C) (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b)
      (CategoryTheory.Limits.coproductUniqueIso f).hom =
    CategoryTheory.eqToHom ⋯
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.p_nonunit : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], ↑p ∈ nonunits ℤ_[p]
-- Std.Internal.Do.Order.PreservesSup
/-- `f` preserves joins.  -/
Lean.Order.PreservesSup.map_sup : ∀ {α : Type u} {inst : Lean.Order.CompleteLattice α} {f : α → α} [self : Lean.Order.PreservesSup f] (s : α → Prop),
  f (Lean.Order.CompleteLattice.sup s) = Lean.Order.CompleteLattice.sup fun y => ∃ x, s x ∧ y = f x
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.UnfoldLift.read : ∀ {m : Type u → Type v} {n : Type u → Type u_1} {ρ : Type u} [inst : MonadLift m n] [inst_1 : MonadReaderOf ρ m],
  MonadReaderOf.read = monadLift MonadReaderOf.read
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.op_π : ∀ {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.Cocone F), c.op.π = CategoryTheory.NatTrans.op c.ι
-- Mathlib.Data.EReal.Basic
EReal.toENNReal_top : ⊤.toENNReal = ⊤
-- Mathlib.Algebra.Homology.BifunctorShift
CategoryTheory.Functor.instCommShift₂IntCochainComplexIntMap₂CochainComplex : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            [inst_3 : CategoryTheory.Preadditive C₁] →
              [inst_4 : CategoryTheory.Preadditive C₂] →
                [inst_5 : CategoryTheory.Preadditive D] →
                  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                    [inst_6 : F.Additive] →
                      [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] →
                        [inst_8 : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F] →
                          F.map₂CochainComplex.CommShift₂Int
-- Mathlib.LinearAlgebra.Isomorphisms
LinearMap.quotKerEquivOfSurjective_apply_mk : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂) (hf : Function.Surjective ⇑f) (x : M),
  (f.quotKerEquivOfSurjective hf) (Submodule.Quotient.mk x) = f x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertMany_empty_list_singleton : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {k : α} {v : β},
  ↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty [(k, v)] ⋯) =
    (Std.DTreeMap.Internal.Impl.insert k v Std.DTreeMap.Internal.Impl.empty ⋯).impl
-- Mathlib.Order.Fin.InsertNth
Fin.insertNth_last_monotone : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α},
  Monotone f → ∀ (x : α), f (Fin.last n) ≤ x → Monotone ((Fin.last (n + 1)).insertNth x f)
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.singleTriangleIso.hom.hom₂ = ((DerivedCategory.singleFunctorsPostcompQIso C).hom.hom 0).app S.X₂
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryGTD : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → (a : α) × β a → (a : α) × β a
-- Mathlib.Algebra.Star.StarRingHom
/-- By definition, a non-unital ⋆-ring homomorphism preserves the `star` operation.  -/
NonUnitalStarRingHom.map_star' : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] (self : A →⋆ₙ+* B) (a : A),
  self.toFun (star a) = star (self.toFun a)
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height does not change under re-indexing.  -/
Height.mulHeight_comp_equiv : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} (e : ι ≃ ι')
  (x : ι' → K), Height.mulHeight (x ∘ ⇑e) = Height.mulHeight x
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.toMeasure_comp_toFiniteMeasure_eq_toMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω), ↑ν.toFiniteMeasure = ↑ν
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The duality equivalence `(WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J`  -/
CategoryTheory.Limits.widePullbackShapeOpEquiv : (J : Type w) → (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ ≌ CategoryTheory.Limits.WidePushoutShape J
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_dotProduct : ∀ {α : Type u_1} {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α] (v : V) (vec : V → α),
  SimpleGraph.adjMatrix α G v ⬝ᵥ vec = ∑ u ∈ G.neighborFinset v, vec u
-- Mathlib.Geometry.Manifold.Bordism
/-- The underlying map `M → X` of a singular `n`-manifold `(M, f)` on `X`  -/
SingularManifold.f : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {k : WithTop ℕ∞} →
      {E : Type u_2} →
        {H : Type u_3} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace ℝ E] →
              [inst_3 : FiniteDimensional ℝ E] →
                [inst_4 : TopologicalSpace H] →
                  {I : ModelWithCorners ℝ E H} → (self : SingularManifold X k I) → self.M → X
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.equivSubtype'_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] (a : TopologicalSpace.IrreducibleCloseds α),
  TopologicalSpace.IrreducibleCloseds.equivSubtype' a = ⟨a.carrier, ⋯⟩
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Theory.model_insert_iff : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {T : L.Theory} {φ : L.Sentence},
  M ⊨ insert φ T ↔ M ⊨ φ ∧ M ⊨ T
-- Mathlib.Order.Hom.WithTopBot
SupHom.withBot'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] [inst_2 : OrderBot β]
  (f : SupHom α β), f.withBot' = { toFun := fun a => Option.elim a ⊥ ⇑f, map_sup' := ⋯, map_bot' := ⋯ }
-- Lean.Data.Options
_private.Lean.Data.Options.0.Lean.Options.mk.sizeOf_spec : ∀ (map : Lean.NameMap Lean.DataValue) (hasTrace : Bool),
  sizeOf { map := map, hasTrace := hasTrace } = 1 + sizeOf map + sizeOf hasTrace
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_preserving_pi_empty : ∀ {ι : Type u} (α : ι → Type v) [inst : Fintype ι] [inst_1 : IsEmpty ι]
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (α i)],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit)) MeasureTheory.volume
    MeasureTheory.volume
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The center of a ring `R` is the set of elements that commute with everything in `R`  -/
NonUnitalSubring.center : (R : Type u) → [inst : NonUnitalNonAssocRing R] → NonUnitalSubring R
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.struct.effectiveEpi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preregular C]
  [inst_2 : CategoryTheory.FinitaryExtensive C]
  {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))}
  (self : CategoryTheory.coherentTopology.struct✝ F) (n : ℕ),
  CategoryTheory.EffectiveEpi (CategoryTheory.coherentTopology.struct.map✝ self n)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_insertMany_list : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {l : List ((a : α) × β a)} {k : α}, k ∈ m.insertMany l ↔ k ∈ m ∨ (List.map Sigma.fst l).contains k = true
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insert.match_1.splitter : {n : ℕ} →
  (motive : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → Sort u_1) →
    (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) →
      ((clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) →
          (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) →
            (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
              motive { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }) →
        motive f
-- Mathlib.Logic.Encodable.Basic
/-- The encoding function has decidable range.  -/
Encodable.decidableRangeEncode : (α : Type u_3) → [inst : Encodable α] → DecidablePred fun x => x ∈ Set.range Encodable.encode
-- Lean.Server.InfoUtils
_private.Lean.Server.InfoUtils.0.Lean.Elab.InfoTree.foldInfo.go : {α : Type u_1} →
  (Lean.Elab.ContextInfo → Lean.Elab.Info → α → α) → Option Lean.Elab.ContextInfo → α → Lean.Elab.InfoTree → α
-- Mathlib.Topology.Algebra.InfiniteSum.Order
sum_le_hasSum : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} [L.NeBot] [L.LeAtTop]
  (s : Finset ι), (∀ i ∉ s, 0 ≤ f i) → HasSum f a L → ∑ i ∈ s, f i ≤ a
-- Mathlib.SetTheory.Cardinal.Finite
ENat.one_lt_card : ∀ {α : Type u_1} [Nontrivial α], 1 < ENat.card α
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.exists_ne_zero : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : LieModule.Weight R L M), ∃ x ∈ LieModule.genWeightSpace M ⇑χ, x ≠ 0
-- Mathlib.Topology.Maps.Proper.Basic
/-- Characterization of proper maps by ultrafilters.  -/
isProperMap_iff_ultrafilter : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsProperMap f ↔
    Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Filter.Tendsto f (↑𝒰) (nhds y) → ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x
-- Init.Data.Array.MapIdx
Array.size_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {xs : Array α}, (Array.mapIdx f xs).size = xs.size
-- Init.Data.List.Sublist
List.append_sublist_append_right : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), (l₁ ++ l).Sublist (l₂ ++ l) ↔ l₁.Sublist l₂
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_eq_getD : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α}
  {h' : a ∈ m}, m.get a h' = m.getD a fallback
-- Mathlib.Tactic.Ring.Common
_private.Mathlib.Tactic.Ring.Common.0.Mathlib.Tactic.Ring.Common.instMonadLiftTOptionT_mathlib : {m : Type u_2 → Type u_3} → {m' : Type u_2 → Type u_4} → [MonadLiftT m m'] → MonadLiftT (OptionT m) (OptionT m')
-- Mathlib.Data.Rat.BigOperators
Rat.cast_prod : ∀ {ι : Type u_1} {α : Type u_2} [inst : Field α] [CharZero α] (s : Finset ι) (f : ι → ℚ),
  ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.RingTheory.Binomial
Ring.map_multichoose : ∀ {R : Type u_3} {S : Type u_4} {F : Type u_5} [inst : Ring R] [inst_1 : Ring S] [inst_2 : BinomialRing R]
  [inst_3 : BinomialRing S] [inst_4 : FunLike F R S] [RingHomClass F R S] (f : F) (a : R) (n : ℕ),
  f (Ring.multichoose a n) = Ring.multichoose (f a) n
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isIso_homologyι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), S.g = 0 → ∀ [inst_2 : S.HasHomology], CategoryTheory.IsIso S.homologyι
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.mk.inj : ∀ {α : Type u_1} {inst : DecidableEq α} {inst_1 : Fintype α} {g : Equiv.Perm α} {toFun : ↥g.cycleFactorsFinset → α}
  {mem_support_self' : ∀ (c : ↥g.cycleFactorsFinset), toFun c ∈ (↑c).support} {toFun_1 : ↥g.cycleFactorsFinset → α}
  {mem_support_self'_1 : ∀ (c : ↥g.cycleFactorsFinset), toFun_1 c ∈ (↑c).support},
  { toFun := toFun, mem_support_self' := mem_support_self' } =
      { toFun := toFun_1, mem_support_self' := mem_support_self'_1 } →
    toFun = toFun_1
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_set_sdiff : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s t : Set β} {a : α},
  a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_alter : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : Std.LawfulEqOrd α]
  {t : Std.DTreeMap.Internal.Impl α β} {a : α} {f : Option (β a) → Option (β a)} (htb : t.Balanced),
  t.Ordered → (Std.DTreeMap.Internal.Impl.alter a f t htb).impl.Ordered
-- Mathlib.Algebra.DirectSum.Algebra
DirectSum.algHom_ext'_iff : ∀ {ι : Type uι} {R : Type uR} {A : ι → Type uA} {B : Type uB} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (A i)] [inst_2 : (i : ι) → Module R (A i)] [inst_3 : AddMonoid ι]
  [inst_4 : DirectSum.GSemiring A] [inst_5 : Semiring B] [inst_6 : DirectSum.GAlgebra R A] [inst_7 : Algebra R B]
  [inst_8 : DecidableEq ι] {f g : (DirectSum ι fun i => A i) →ₐ[R] B},
  f = g ↔ ∀ (i : ι), f.toLinearMap ∘ₗ DirectSum.lof R ι A i = g.toLinearMap ∘ₗ DirectSum.lof R ι A i
-- Aesop.Script.SScript
Aesop.Script.SScript.onGoal.sizeOf_spec : ∀ (goalPos : ℕ) (step : Aesop.Script.Step) (tail : Aesop.Script.SScript),
  sizeOf (Aesop.Script.SScript.onGoal goalPos step tail) = 1 + sizeOf goalPos + sizeOf step + sizeOf tail
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_le_size_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : Option β → Option β}, t.size - 1 ≤ (t.alter k f).size