mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Vector.Lemmas
Vector.foldr_eq_apply_foldl : ∀ {α : Type u_1} {n : ℕ} {init x : α} {xs : Vector α n} {f : α → α → α} [Std.Associative f]
  [Std.LawfulLeftIdentity f init], Vector.foldr f x xs = f (Vector.foldl f init xs) x
-- Mathlib.Data.Set.Subset
Set.image_val_iUnion : ∀ {ι : Sort u_1} {α : Type u_2} {A : Set α} {t : ι → Set ↑A}, Subtype.val '' ⋃ i, t i = ⋃ i, Subtype.val '' t i
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (i : ℕ),
  (groupHomology.chainsMap f φ).f i =
    CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lmapDomain (↑A) k fun x => ⇑f ∘ x))
      (ModuleCat.ofHom (Finsupp.mapRange.linearMap (Rep.Hom.hom φ).toLinearMap))
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with
at most as many pigeons as the floor of the average number of pigeons across all pigeonholes.  ("The
minimum is at most the mean" specialized to integers.)

More formally, given a function `f`, a finite sets `s` in its domain, a finite set `t` in its
codomain, and a natural number `n` such that `#s < #t * n`, there exists `y ∈ t` such that
its preimage in `s` has less than `n` elements.  -/
Finset.exists_card_fiber_lt_of_card_lt_mul : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {n : ℕ},
  s.card < t.card * n → ∃ y ∈ t, {x ∈ s | f x = y}.card < n
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- Reflection through the trivial subspace `{0}` is just negation.  -/
Submodule.reflection_bot : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ⊥.reflection = LinearIsometryEquiv.neg 𝕜
-- Lean.Parser.Tactic
Lean.Parser.Tactic.matchRhs : Lean.Parser.Parser
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀_min : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] {a b : WithTop α},
  a ≠ ⊤ → b ≠ ⊤ → (min a b).untop₀ = min a.untop₀ b.untop₀
-- Aesop.Stats.Basic
Aesop.StatsRef : Type
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_eq_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : LawfulBEq α] {k fallback : α},
  k ∈ m → m.getD k fallback = k
-- Mathlib.CategoryTheory.Action.Continuous
ContAction.instHasForget₂HomSubtypeObjActionIsContinuousV : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
              (G : Type u_4) →
                [inst_4 : Monoid G] → [inst_5 : TopologicalSpace G] → CategoryTheory.HasForget₂ (ContAction V G) V
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_roc : ∀ {m n i : ℕ}, (m<...=n).toList[i]? = if i < n - m then some (m + 1 + i) else none
-- Mathlib.AlgebraicGeometry.Sites.Affine
AlgebraicGeometry.Scheme.affineOverMk_left : ∀ {S : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {R : CommRingCat}
  (f : AlgebraicGeometry.Spec R ⟶ S) (hf : P f), (AlgebraicGeometry.Scheme.affineOverMk f hf).left = Opposite.op R
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.X_pow_sub_C_ne_zero : ∀ {R : Type u} [inst : Ring R] [Nontrivial R] {n : ℕ}, 0 < n → ∀ (a : R), Polynomial.X ^ n - Polynomial.C a ≠ 0
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.isometry : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), Isometry ⇑e
-- Init.Data.Iterators.Combinators.Monadic.Append
_private.Init.Data.Iterators.Combinators.Monadic.Append.0.Std.Iterators.Types.Append.instProductivenessRelation : {α₁ α₂ : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Monad m] →
        [inst_1 : Std.Iterator α₁ m β] →
          [inst_2 : Std.Iterator α₂ m β] →
            [Std.Iterators.Productive α₁ m] →
              [Std.Iterators.Productive α₂ m] →
                Std.Iterators.ProductivenessRelation (Std.Iterators.Types.Append α₁ α₂ m β) m
-- Mathlib.Order.SuccPred.Tree
RootedTree.root_subtree : ∀ (t : RootedTree) (r : ↑t), (t.subtree r).root = r
-- Init.Data.Nat.Div.Basic
Nat.zero_mod : ∀ (b : ℕ), 0 % b = 0
-- Mathlib.Algebra.BigOperators.Group.Finset.Pi
/-- Taking a product over `univ.pi t` is the same as taking the product over `Fintype.piFinset t`.
`univ.pi t` and `Fintype.piFinset t` are essentially the same `Finset`, but differ
in the type of their element, `univ.pi t` is a `Finset (Π a ∈ univ, t a)` and
`Fintype.piFinset t` is a `Finset (Π a, t a)`.  -/
Finset.prod_univ_pi : ∀ {ι : Type u_1} {β : Type u_2} [inst : CommMonoid β] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {κ : ι → Type u_3}
  (t : (i : ι) → Finset (κ i)) (f : ((i : ι) → i ∈ Finset.univ → κ i) → β),
  ∏ x ∈ Finset.univ.pi t, f x = ∏ x ∈ Fintype.piFinset t, f fun a x_1 => x a
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.BinaryBicone.ofLimitCone_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)} (ht : CategoryTheory.Limits.IsLimit t),
  (CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).snd = t.π.app { as := CategoryTheory.Limits.WalkingPair.right }
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.prod_one_sub : ∀ {R : Type u_1} [inst : CommRing R] {I : Type u_3} {e : I → R},
  OrthogonalIdempotents e → ∀ (s : Finset I), ∏ i ∈ s, (1 - e i) = 1 - ∑ i ∈ s, e i
-- Mathlib.Data.DFinsupp.Defs
/-- `Filter p f` is the function which is `f i` if `p i` is true and 0 otherwise.  -/
DFinsupp.filter : {ι : Type u} →
  {β : ι → Type v} →
    [inst : (i : ι) → Zero (β i)] → (p : ι → Prop) → [DecidablePred p] → (Π₀ (i : ι), β i) → Π₀ (i : ι), β i
-- Mathlib.NumberTheory.MulChar.Basic
/-- Turn a `MulChar` into a homomorphism between the unit groups.  -/
MulChar.toUnitHom : {R : Type u_1} → [inst : CommMonoid R] → {R' : Type u_2} → [inst_1 : CommMonoidWithZero R'] → MulChar R R' → Rˣ →* R'ˣ
-- Mathlib.Order.Fin.Basic
Fin.strictMono_pred_comp : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : α → Fin (n + 1)} (hf : ∀ (a : α), f a ≠ 0),
  StrictMono f → StrictMono fun a => (f a).pred ⋯
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valued.toNormedField.one_lt_norm_iff : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne] {x : L}, 1 < ‖x‖ ↔ 1 < Valued.v x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.superpose : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (k₁ : ℤ)
  (m₁ : Lean.Grind.CommRing.Mon) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon)
  (p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.superpose_cert k₁ m₁ p₁ k₂ m₂ p₂ p = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ = 0 →
      Lean.Grind.CommRing.Poly.denote ctx p₂ = 0 → Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.instReflectsIsomorphismsCommaForgetOfRespectsIso : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (P : CategoryTheory.MorphismProperty T)
  (Q : CategoryTheory.MorphismProperty A) (W : CategoryTheory.MorphismProperty B) [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [Q.RespectsIso] [W.RespectsIso],
  (CategoryTheory.MorphismProperty.Comma.forget L R P Q W).ReflectsIsomorphisms
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.NatOffset.const.injEq : ∀ (n n_1 : ℕ), (Nat.NatOffset.const✝ n = Nat.NatOffset.const✝ n_1) = (n = n_1)
-- Mathlib.Data.Set.Subset
Set.image_val_inter_self_right_eq_coe : ∀ {α : Type u_2} {A : Set α} {D : Set ↑A}, A ∩ Subtype.val '' D = Subtype.val '' D
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.indent : Lean.PrettyPrinter.Formatter → optParam (Option ℤ) none → Lean.PrettyPrinter.Formatter
-- Mathlib.Tactic.FunProp.Theorems
/-- map: function name → function property → function theorem  -/
Mathlib.Meta.FunProp.FunctionTheorems.theorems : Mathlib.Meta.FunProp.FunctionTheorems →
  Std.TreeMap Lean.Name (Std.TreeMap Lean.Name (Array Mathlib.Meta.FunProp.FunctionTheorem) Lean.Name.quickCmp)
    Lean.Name.quickCmp
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Path.root.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf RBTree.RBNode.Path.root = 1
-- Mathlib.Tactic.Linter.OverlappingInstances
/-- Report a warning message if there are any overlapping instances in the local context.
For `Prop` instances, only report local instances that are redundant.  -/
_private.Mathlib.Tactic.Linter.OverlappingInstances.0.Mathlib.Linter.OverlappingInstances.runLinter : Lean.Elab.ContextInfo → Lean.LocalContext → Option Lean.Expr → IO (Option Lean.MessageData)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.CohomologyClass.toHom_bijective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n : ℤ), Function.Bijective ⇑CochainComplex.HomComplex.CohomologyClass.toHom
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version on a set.  -/
ContMDiffOn.mpullbackWithin_vectorField_inter : ∀ {𝕜 : 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] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} {t : Set M'} [CompleteSpace E] [inst_12 : IsManifold I 1 M]
  [inst_13 : IsManifold I' 1 M'],
  ContMDiffOn I' I'.tangent m (fun x => ⟨x, V x⟩) t →
    ContMDiffOn I I' n f s →
      (∀ x ∈ s ∩ f ⁻¹' t, (mfderiv[s] f x).IsInvertible) →
        UniqueMDiff[s] →
          m + 1 ≤ n → ContMDiffOn I I.tangent m (fun x => ⟨x, VectorField.mpullbackWithin I I' f V s x⟩) (s ∩ f ⁻¹' t)
-- Mathlib.Topology.Algebra.MulAction
/-- Eta-expanded form of `ContinuousAt.smul` -/
ContinuousAt.fun_smul : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : SMul M X] [ContinuousSMul M X] {f : Y → M} {g : Y → X} {b : Y},
  ContinuousAt f b → ContinuousAt g b → ContinuousAt (fun i => f i • g i) b
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.isSatisfiable_empty : ∀ (L : FirstOrder.Language), ∅.IsSatisfiable
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformly.tendsto_of_eventually_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {p' : Filter α} [p.NeBot] {L : ι → β} {ℓ : β},
  TendstoUniformly F f p →
    (∀ᶠ (i : ι) in p, Filter.Tendsto (F i) p' (nhds (L i))) → Filter.Tendsto L p (nhds ℓ) → Filter.Tendsto f p' (nhds ℓ)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cyclesMap_i_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g')
  (β : CategoryTheory.ComposableArrows.mk₁ g ⟶ CategoryTheory.ComposableArrows.mk₁ g') (n : ℤ),
  autoParam (β = CategoryTheory.ComposableArrows.homMk₁ (α.app 1) (α.app 2) ⋯)
      CategoryTheory.Abelian.SpectralObject.cyclesMap_i._auto_1 →
    ∀ {Z : C} (h : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g') ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.cyclesMap f g f' g' α n)
          (CategoryTheory.CategoryStruct.comp (X.iCycles f' g' n) h) =
        CategoryTheory.CategoryStruct.comp (X.iCycles f g n) (CategoryTheory.CategoryStruct.comp ((X.H n).map β) h)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.refl_symm : ∀ {R : Type u_1} {M : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  (LinearEquiv.refl R M).symm = LinearEquiv.refl R M
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.Const.alterKey.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (k : α) (f : Option β → Option β) (l : List ((_ : α) × β)),
  Std.Internal.List.Const.alterKey k f l =
    match f (Std.Internal.List.getValue? k l) with
    | none => Std.Internal.List.eraseKey k l
    | some v => Std.Internal.List.insertEntry k v l
-- Mathlib.Logic.Basic
forall₂_or_left : ∀ {α : Sort u_1} {r p q : α → Prop}, (∀ (x : α), p x ∨ q x → r x) ↔ (∀ (x : α), p x → r x) ∧ ∀ (x : α), q x → r x
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenEmbedding : (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] =>
    Topology.IsOpenEmbedding).RespectsIso
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
/-- The univariate polynomial `preΨ₄`, which is auxiliary to the 4-division polynomial
`ψ₄ = Ψ₄ = preΨ₄ψ₂`.  -/
WeierstrassCurve.preΨ₄ : {R : Type r} → [inst : CommRing R] → WeierstrassCurve R → Polynomial R
-- Mathlib.Combinatorics.SetFamily.Intersecting
/-- The empty family of finite sets is `L`-intersecting, vacuously, because it contains no pairs of
sets.
 -/
Set.IsIntersectingOf.empty : ∀ {L : Set ℕ} {α : Type u_1} [inst : DecidableEq α], L.IsIntersectingOf ∅
-- Std.Net.Addr
Std.Net.IPv6Addr.instToString : ToString Std.Net.IPv6Addr
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimit_rightOp_iff_hasColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  {F : CategoryTheory.Functor Jᵒᵖ C}, CategoryTheory.Limits.HasLimit F.rightOp ↔ CategoryTheory.Limits.HasColimit F
-- Init.Control.Lawful.MonadLift.Lemmas
liftM_bind : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] [inst_2 : MonadLiftT m n]
  [LawfulMonadLiftT m n] {α β : Type u} (ma : m α) (f : α → m β),
  liftM (ma >>= f) = do
    let a ← liftM ma
    liftM (f a)
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.SatelliteConfig.rpos : ∀ {α : Type u_1} [inst : MetricSpace α] {N : ℕ} {τ : ℝ} (self : Besicovitch.SatelliteConfig α N τ) (i : Fin N.succ),
  0 < self.r i
-- Mathlib.Tactic.Linter.MinImports
_private.Mathlib.Tactic.Linter.MinImports.0.Mathlib.Linter.ImportState.mk.sizeOf_spec : ∀ (transClosure : Option (Lean.NameMap Lean.NameSet)) (minImports : Lean.NameSet) (importSize : ℕ),
  sizeOf { transClosure := transClosure, minImports := minImports, importSize := importSize } =
    1 + sizeOf transClosure + sizeOf minImports + sizeOf importSize
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_restrict_of_ae_imp : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} {s : Set α}
  {φ : ι → Set α},
  MeasurableSet s →
    (∀ᵐ (x : α) ∂μ, x ∈ s → ∀ᶠ (n : ι) in l, x ∈ φ n) →
      (∀ (n : ι), MeasurableSet (φ n)) → MeasureTheory.AECover (μ.restrict s) l φ
-- Mathlib.Analysis.Convex.PathConnected
segment_image_Ioc : ∀ {x y : ℝ}, x < y → ⇑(Path.segment x y) '' Set.Ioc 0 1 = Set.Ioc x y
-- Mathlib.Logic.Equiv.Prod
/-- `γ`-valued functions on `α × β` are equivalent to functions `α → β → γ`.  -/
Equiv.curry : (α : Type u_9) → (β : Type u_10) → (γ : Sort u_11) → (α × β → γ) ≃ (α → β → γ)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
ChartedSpace.LiftPropWithinAt.continuousWithinAt : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : M → M'}
  {s : Set M} {x : M}, ChartedSpace.LiftPropWithinAt P f s x → ContinuousWithinAt f s x
-- Mathlib.Order.Basic
Eq.not_lt : ∀ {α : Type u_2} [inst : Preorder α] {a b : α}, a = b → ¬a < b
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Hom₂.mk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : CategoryTheory.Bicategory.Adj B} →
      {α β : a ⟶ b} →
        (τl : α.l ⟶ β.l) →
          (τr : β.r ⟶ α.r) →
            autoParam ((CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) τl = τr)
                CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_τl._autoParam →
              CategoryTheory.Bicategory.Adj.Hom₂ α β
-- Mathlib.Topology.Algebra.Order.Field
Filter.Tendsto.const_div_atTop : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {g : α → 𝕜},
  Filter.Tendsto g l Filter.atTop → ∀ (r : 𝕜), Filter.Tendsto (fun n => r / g n) l (nhds 0)
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.mk : {A : Type u_1} →
  [inst : CommSemiring A] →
    {I : Ideal A} →
      (dpow : ℕ → A → A) →
        (∀ {n : ℕ} {x : A}, x ∉ I → dpow n x = 0) →
          (∀ {x : A}, x ∈ I → dpow 0 x = 1) →
            (∀ {x : A}, x ∈ I → dpow 1 x = x) →
              (∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow n x ∈ I) →
                (∀ {n : ℕ} {x y : A},
                    x ∈ I →
                      y ∈ I → dpow n (x + y) = ∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, dpow k.1 x * dpow k.2 y) →
                  (∀ {n : ℕ} {a x : A}, x ∈ I → dpow n (a * x) = a ^ n * dpow n x) →
                    (∀ {m n : ℕ} {x : A}, x ∈ I → dpow m x * dpow n x = ↑((m + n).choose m) * dpow (m + n) x) →
                      (∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow m (dpow n x) = ↑(m.uniformBell n) * dpow (m * n) x) →
                        DividedPowers I
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- If `R` satisfies the strong rank condition, then for any linearly independent family `v : ι → M`
and spanning set `w : Set M`, the cardinality of `ι` is bounded by the cardinality of `w`.
 -/
linearIndependent_le_span'' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type v} {v : ι → M},
  LinearIndependent R v → ∀ (w : Set M), Submodule.span R w = ⊤ → Cardinal.mk ι ≤ Cardinal.mk ↑w
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.header.checkNonIndented : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.prodMk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} {g : M → M''}, MDiff f → MDiff g → MDiff fun x => (f x, g x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft_right : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G')
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (α : ψ ⟶ ψ'),
  (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft φ α).right = φ.right.whiskerLeft α.right
-- Mathlib.Topology.Order.Monotone
/-- **Alias** of `Antitone.countable_setOfPred_two_preimages`.

---

If a function is antitone in a second countable topological space, then there
are only countably many points that have several preimages.  -/
Antitone.countable_setOf_two_preimages : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {f : α → β} [SecondCountableTopology α],
  Antitone f → {c | ∃ x y, x < y ∧ f x = c ∧ f y = c}.Countable
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.stabilizerEquiv.eq_1 : ∀ {M : Type u_1} {R : Type u_3} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {N : Type u_4}
  [inst_3 : Group N] [inst_4 : MulSemiringAction N R] (I : Ideal R) (e : M ≃* N)
  (he : ∀ (m : M) (x : R), e m • x = m • x), I.stabilizerEquiv e he = { toEquiv := (↑e).subtypeEquiv ⋯, map_mul' := ⋯ }