mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- For a surjective `f : N →ₗ[R] P`,
the natural equivalence between `N ⊗[R] Q ⧸ (range (rTensor Q f))` and `P ⊗[R] Q`  -/
rTensor.equiv : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {P : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      {f : M →ₗ[R] N} →
                        {g : N →ₗ[R] P} →
                          (Q : Type u_5) →
                            [inst_7 : AddCommGroup Q] →
                              [inst_8 : Module R Q] →
                                Function.Exact ⇑f ⇑g →
                                  Function.Surjective ⇑g →
                                    (TensorProduct R N Q ⧸ (LinearMap.rTensor Q f).range) ≃ₗ[R] TensorProduct R P Q
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.rescale_eq : ∀ {R : Type u_2} [inst : CommRing R] (r : R) (f : PowerSeries R),
  (PowerSeries.rescale r) f = (MvPowerSeries.rescale fun x => r) f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g],
  (CategoryTheory.Limits.pushoutCoconeOfRightIso f g).ι.app CategoryTheory.Limits.WalkingSpan.left =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.span f g).obj CategoryTheory.Limits.WalkingSpan.left)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_obj_snd_obj : ∀ {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) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) (X_1 : X),
  ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).functor.obj J).snd.obj X_1 = (J.obj X_1).snd
-- Mathlib.Tactic.NormNum.DivMod
Mathlib.Meta.NormNum.isInt_emod_zero : ∀ {a b r : ℤ}, Mathlib.Meta.NormNum.IsInt a r → Mathlib.Meta.NormNum.IsNat b 0 → Mathlib.Meta.NormNum.IsInt (a % b) r
-- Mathlib.Data.Multiset.Defs
Multiset.instDecidableRListOfDecidableEq : {α : Type u_1} → [DecidableEq α] → (l₁ l₂ : List α) → Decidable ((List.isSetoid α) l₁ l₂)
-- Mathlib.RingTheory.NoetherNormalization
/-- For a finitely generated algebra `A` over a field `k`,
there exists a natural number `s` and an injective homomorphism
from `k[X_0, X_1, ..., X_(s-1)]` to `A` such that `A` is finite over `k[X_0, X_1, ..., X_(s-1)]`.  -/
exists_finite_inj_algHom_of_fg : ∀ (k : Type u_2) (R : Type u_3) [inst : Field k] [inst_1 : CommRing R] [Nontrivial R] [a : Algebra k R]
  [fin : Algebra.FiniteType k R], ∃ s g, Function.Injective ⇑g ∧ g.Finite
-- Mathlib.Topology.Constructible
/-- A variant that requires constructible in the ambient space.
This is as strong as the unprimed version only when the open cover consists of retrocompact sets.  -/
Topology.IsLocallyConstructible.of_isOpenCover' : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} {ι : Type u_4} {U : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover U →
    (∀ (i : ι), Topology.IsLocallyConstructible (s ∩ ↑(U i))) → Topology.IsLocallyConstructible s
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.liftIsometry_apply_apply : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {F : Type u_4}
  [inst_4 : SeminormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] (f : ContinuousMultilinearMap 𝕜 E F)
  (x : PiTensorProduct 𝕜 fun i => E i),
  ((PiTensorProduct.liftIsometry 𝕜 E F) f) x = (PiTensorProduct.lift f.toMultilinearMap) x
-- Init.Notation
/-- Whitespace handling for `#guard_msgs`:
- `whitespace := exact` requires an exact whitespace match.
- `whitespace := normalized` converts all newline characters to a space before matching
  (the default). This allows breaking long lines.
- `whitespace := lax` collapses whitespace to a single space before matching.
In all cases, leading and trailing whitespace is trimmed before matching.
 -/
Lean.guardMsgsWhitespace : Lean.ParserDescr
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Iso.inv_hom_id_triangle_hom₃_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (e : A ≅ B) {Z : C} (h : B.obj₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp e.inv.hom₃ (CategoryTheory.CategoryStruct.comp e.hom.hom₃ h) = h
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.addSubgroupOf_range_eq_of_le : ∀ {G₁ : Type u_7} {G₂ : Type u_8} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] {K : AddSubgroup G₂} (f : G₁ →+ G₂)
  (h : f.range ≤ K), f.range.addSubgroupOf K = (f.codRestrict K ⋯).range
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getEntryLT?_eq_findRev? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.getEntryLT? k t = List.findRev? (fun e => (compare e.fst k).isLT) t.toListModel
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isClosed_image_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsClosed (OnePoint.some '' s) ↔ IsClosed s ∧ IsCompact s
-- Lean.Elab.Tactic.RCases
/-- Interpret an rcases pattern as a tuple, where `p` becomes `⟨p⟩` if `p` is not already a tuple.
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.asTuple : Lean.Elab.Tactic.RCases.RCasesPatt → Bool × List Lean.Elab.Tactic.RCases.RCasesPatt
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.exists_mem_ne_one_of_prod_ne_one : ∀ {M : Type u_4} [inst : Monoid M] {l : List M}, l.prod ≠ 1 → ∃ x ∈ l, x ≠ 1
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- Any three points in a cospherical set are affinely independent.  -/
EuclideanGeometry.Cospherical.affineIndependent : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : Set P},
  EuclideanGeometry.Cospherical s → ∀ {p : Fin 3 → P}, Set.range p ⊆ s → Function.Injective p → AffineIndependent ℝ p
-- Mathlib.Data.Finset.Sups
Finset.coe_diffs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] (s t : Finset α),
  ↑(s.diffs t) = Set.image2 (fun x1 x2 => x1 \ x2) ↑s ↑t
-- Mathlib.Order.Filter.Map
Filter.comap_pure : ∀ {α : Type u_1} {β : Type u_2} {m : α → β} {b : β}, Filter.comap m (pure b) = Filter.principal (m ⁻¹' {b})
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_mono : ∀ {G : Type u_1} [inst : AddGroup G] {H₁ H₂ K₁ K₂ : AddSubgroup G}, H₁ ≤ K₁ → H₂ ≤ K₂ → ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardFactors_pow : ∀ {m k : ℕ}, ArithmeticFunction.cardFactors (m ^ k) = k * ArithmeticFunction.cardFactors m
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Coerce a pair by elementwise coercion.  -/
GenContFract.Pair.instCoe : {α : Type u_1} → {β : Type u_2} → [Coe α β] → Coe (GenContFract.Pair α) (GenContFract.Pair β)
-- Init.Data.List.Impl
/-- Removes the element at the specified index. If the index is out of bounds, the list is returned
unmodified.

`O(i)`.

This is a tail-recursive version of `List.eraseIdx`, used at runtime.

Examples:
* `[0, 1, 2, 3, 4].eraseIdxTR 0 = [1, 2, 3, 4]`
* `[0, 1, 2, 3, 4].eraseIdxTR 1 = [0, 2, 3, 4]`
* `[0, 1, 2, 3, 4].eraseIdxTR 5 = [0, 1, 2, 3, 4]`
 -/
List.eraseIdxTR : {α : Type u_1} → List α → ℕ → List α
-- Init.Data.List.Scan.Lemmas
List.getElem?_scanl : ∀ {α : Type u_1} {β : Type u_2} {a : α} {l : List β} {i : ℕ} {f : α → β → α},
  (List.scanl f a l)[i]? = if i ≤ l.length then some (List.foldl f a (List.take i l)) else none
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_map : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (S : AddSubmonoid M) (g : N →+ P) (f : M →+ N),
  AddSubmonoid.map g (AddSubmonoid.map f S) = AddSubmonoid.map (g.comp f) S
-- Init.Data.Vector.Find
Vector.find?_replicate_of_pos : ∀ {α : Type} {p : α → Bool} {n : ℕ} {a : α},
  p a = true → Vector.find? p (Vector.replicate n a) = if n = 0 then none else some a
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.IsFredholm.mk : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F},
  Topology.IsStrictMap ⇑u →
    IsClosed ↑(↑u).range → FiniteDimensional 𝕜 ↥(↑u).ker → (↑u).range.CoFG → (↑u).ker.ClosedComplemented → u.IsFredholm
-- Init.Core
Prod.map_fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α × γ),
  (Prod.map f g x).1 = f x.1
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.builderOptions : Aesop.Frontend.RuleConfig → Aesop.RuleBuilderOptions
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_le_range : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N : LieSubmodule R L M} {M' : Type u_1} [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M'), LieSubmodule.map f N ≤ f.range
-- Mathlib.Data.List.Lemmas
List.mapAccumr₂.eq_def : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ → γ × δ) (x : List α) (x_1 : List β)
  (x_2 : γ),
  List.mapAccumr₂ f x x_1 x_2 =
    match x, x_1, x_2 with
    | [], x, c => (c, [])
    | x, [], c => (c, [])
    | x :: xr, y :: yr, c =>
      have r := List.mapAccumr₂ f xr yr c;
      have q := f x y r.1;
      (q.1, q.2 :: r.2)
-- Init.Data.UInt.Lemmas
BitVec.ofNatLT_uSizeToNat : ∀ (n : USize), n.toNat#'⋯ = n.toBitVec
-- Init.Data.Iterators.Consumers.Access
Std.Iter.atIdxSlow?.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (n : ℕ) (it : Std.Iter β),
  Std.Iter.atIdxSlow? n it =
    WellFounded.extrinsicFix₂
      (InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel) fun p =>
        (p.snd, p.fst.finitelyManySkips!))
      (fun it n recur =>
        match it.step with
        | ⟨Std.IterStep.yield it' out, property⟩ =>
          match n, recur with
          | 0, recur => some out
          | k.succ, recur => recur it' k ⋯
        | ⟨Std.IterStep.skip it', property⟩ => recur it' n ⋯
        | ⟨Std.IterStep.done, property⟩ => none)
      it n
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.mk.inj : ∀ {α : Type u_2} {β : Type u_3} {inst : OmegaCompletePartialOrder α} {inst_1 : OmegaCompletePartialOrder β}
  {toOrderHom : α →o β}
  {map_ωSup' :
    ∀ (c : OmegaCompletePartialOrder.Chain α),
      toOrderHom.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map toOrderHom)}
  {toOrderHom_1 : α →o β}
  {map_ωSup'_1 :
    ∀ (c : OmegaCompletePartialOrder.Chain α),
      toOrderHom_1.toFun (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map toOrderHom_1)},
  { toOrderHom := toOrderHom, map_ωSup' := map_ωSup' } = { toOrderHom := toOrderHom_1, map_ωSup' := map_ωSup'_1 } →
    toOrderHom = toOrderHom_1
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryLT.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Ordered → (∃ a ∈ x, compare a k = Ordering.lt) → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.lt)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.lt) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β ky) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.lt) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.leaf, x, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_1 x he
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_unitIso_inv_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (X : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (X_1 : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.equivComma.unitIso.inv.app X).app X_1 =
    (match X_1 with
      | CategoryTheory.WithTerminal.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.incl.comp X)).app x
      | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithTerminal.star)).inv
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableWithinAt_snd : ∀ {𝕜 : 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'] {s : Set (M × M')} {x : M × M'},
  MDiffAt[s] Prod.snd x
-- Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Finset.zero_mul_subset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (s : Finset α), 0 * s ⊆ 0
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.shatters_univ : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} [inst_1 : Fintype α],
  𝒜.Shatters Finset.univ ↔ 𝒜 = Finset.univ
-- Mathlib.Order.Filter.Pointwise
Filter.sub_neBot_iff : ∀ {α : Type u_2} [inst : Sub α] {f g : Filter α}, (f - g).NeBot ↔ f.NeBot ∧ g.NeBot
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp], t.WF → ∀ {k : α}, k ∈ t.insert k
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_right_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  {X Y : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C} (η : X ⟶ Y) (X_1 : SimplexCategory),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.functor.map η).right.app X_1 =
    η.app (CategoryTheory.WithInitial.incl.obj X_1)
-- Mathlib.MeasureTheory.Function.L2Space
/-- The inner product in `L2` of the indicator of a set `indicatorConstLp 2 hs hμs c` and `f` is
equal to the integral of the inner product over `s`: `∫ x in s, ⟪c, f x⟫ ∂μ`.  -/
MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner : ∀ {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {s : Set α} (f : ↥(MeasureTheory.Lp E 2 μ))
  (hs : MeasurableSet s) (c : E) (hμs : μ s ≠ ⊤),
  inner 𝕜 (MeasureTheory.indicatorConstLp 2 hs hμs c) f = ∫ (x : α) in s, inner 𝕜 c (↑↑f x) ∂μ
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- The `R`-submodule of all elements of `S[M]` supported on a subset `s` of `M`.  -/
MonoidAlgebra.supported : (R : Type u_1) →
  (S : Type u_2) →
    {M : Type u_3} →
      [inst : Semiring R] → [inst_1 : Semiring S] → [inst_2 : Module R S] → Set M → Submodule R (MonoidAlgebra S M)
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.bijective : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y),
  Function.Bijective ⇑e
-- Mathlib.NumberTheory.Fermat
Nat.fermatNumber_injective : Function.Injective Nat.fermatNumber
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Applying a linear map to a vector is differentiable within a set. Version in vector spaces. For
a version in nontrivial vector bundles, see `MDifferentiableWithinAt.clm_apply_of_inCoordinates`.  -/
MDifferentiableWithinAt.clm_apply : ∀ {𝕜 : 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] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} {x : M},
  MDiffAt[s] g x → MDiffAt[s] f x → (MDiffAt[s] fun x => (g x) (f x)) x
-- Mathlib.Analysis.Real.Cardinality
/-- The cardinality of the reals, as a type.  -/
Cardinal.mk_real : Cardinal.mk ℝ = Cardinal.continuum
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.hasStrictDerivAt_const_rpow : ∀ {a : ℝ}, 0 < a → ∀ (x : ℝ), HasStrictDerivAt (fun x => a ^ x) (a ^ x * Real.log a) x
-- Mathlib.Data.Set.Pairwise.Basic
pairwise_disjoint_fiber : ∀ {α : Type u_1} {ι : Type u_4} (f : ι → α), Pairwise (Function.onFun Disjoint fun a => f ⁻¹' {a})
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle_div : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Group (G i)] [inst_3 : ∀ (i : ι), SubgroupClass (S i) (G i)] (i : ι)
  (r s : G i),
  RestrictedProduct.mulSingle A i (r / s) = RestrictedProduct.mulSingle A i r / RestrictedProduct.mulSingle A i s
-- Mathlib.CategoryTheory.Sums.Associator
/-- Characterizing the composition of the associator and the left inclusion.  -/
CategoryTheory.sum.inlCompAssociator : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (CategoryTheory.Sum.inl_ (C ⊕ D) E).comp (CategoryTheory.sum.associator C D E) ≅
              (CategoryTheory.Sum.inl_ C (D ⊕ E)).sum'
                ((CategoryTheory.Sum.inl_ D E).comp (CategoryTheory.Sum.inr_ C (D ⊕ E)))
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
tendsto_sub_comap_self : ∀ {α : Type u_1} {β : Type u_2} {hom : Type u_3} [inst : TopologicalSpace α] [inst_1 : AddGroup α]
  [IsTopologicalAddGroup α] [inst_3 : TopologicalSpace β] [inst_4 : AddGroup β] [inst_5 : FunLike hom β α]
  [AddMonoidHomClass hom β α] {e : hom},
  IsDenseInducing ⇑e →
    ∀ (x₀ : α), Filter.Tendsto (fun t => t.2 - t.1) (Filter.comap (fun p => (e p.1, e p.2)) (nhds (x₀, x₀))) (nhds 0)
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.End.smulLeft.congr_simp : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (α α_1 : R)
  (e_α : α = α_1) (hα : α ∈ Set.center R), Module.End.smulLeft α hα = Module.End.smulLeft α_1 ⋯
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.HomologySequence.snakeInput_L₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j),
  (HomologicalComplex.HomologySequence.snakeInput hS i j hij).L₃ =
    (HomologicalComplex.homologyFunctor C c j).mapShortComplex.obj S
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.ComputableSmall.choose : (α : Type v) → [small : Std.Internal.Small α] → Std.Internal.ComputableSmall α
-- Mathlib.Data.Fin.Tuple.Sort
/-- If the tuple `f` is not the same as `f ∘ sort f`, then `f` has a pair of strictly decreasing
entries.  -/
Tuple.antitone_pair_of_not_sorted : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α}, f ≠ f ∘ ⇑(Tuple.sort f) → ∃ i j, i < j ∧ f j < f i
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.commutative_iff : ∀ {n : ℕ}, IsMulCommutative (DihedralGroup n) ↔ n = 1 ∨ n = 2
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.mulLeftStrictMono : ∀ {α : Type u} [inst : LT α] [inst_1 : Mul α] [c : MulLeftStrictMono α], MulLeftStrictMono αᵒᵈ
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.extendScalars_restrictScalars : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  (h : F ≤ E), IntermediateField.restrictScalars K (IntermediateField.extendScalars h) = E
-- Init.Data.Nat.Lemmas
Nat.ne_zero_of_mul_ne_zero_left : ∀ {n m : ℕ}, n * m ≠ 0 → n ≠ 0
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.HasCoequalizerOfIsSplitPair.mk : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C},
  (∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], CategoryTheory.Limits.HasCoequalizer f g) →
    CategoryTheory.Monad.HasCoequalizerOfIsSplitPair G
-- Mathlib.Data.EReal.Inv
EReal.antitone_div_right_of_nonpos : ∀ {b : EReal}, b ≤ 0 → Antitone fun a => a / b
-- Mathlib.Topology.Constructions
TopologicalSpace.cofinite.eq_1 : ∀ {X : Type u_5},
  TopologicalSpace.cofinite =
    { IsOpen := fun s => s.Nonempty → sᶜ.Finite, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }
-- Mathlib.Analysis.Convex.Between
wbtw_sub_const_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Wbtw R (x - v) (y - v) (z - v) ↔ Wbtw R x y z
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalAlgebra.lift_toFun : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : CommSemiring R]
  [inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)] [inst_6 : (i : ι) → DistribMulAction R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] (P : Type u_7)
  [inst_9 : NonUnitalNonAssocSemiring P] [inst_10 : DistribMulAction R P] (g : (i : ι) → G i →ₙₐ[R] P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (z : DirectLimit G f),
  (DirectLimit.NonUnitalAlgebra.lift G f P g Hg) z = DirectLimit.lift f (fun x1 x2 => (g x1) x2) ⋯ z
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instMonoid : {M : Type u_2} →
  {N : Type u_3} →
    {X : Type u_4} →
      {Y : Type u_5} →
        {σ : M → N} →
          [inst : SMul M X] →
            [inst_1 : Monoid N] → [inst_2 : Monoid Y] → [inst_3 : MulDistribMulAction N Y] → Monoid (X →ₑ[σ] Y)
-- Mathlib.Data.Fin.Basic
Fin.ne_last_of_ne_last_of_le : ∀ {n : ℕ} {a b : Fin (n + 1)}, b ≠ Fin.last n → a ≤ b → a ≠ Fin.last n
-- Mathlib.Data.Set.Finite.Basic
Set.finite_union : ∀ {α : Type u} {s t : Set α}, (s ∪ t).Finite ↔ s.Finite ∧ t.Finite
-- Mathlib.Topology.Algebra.ConstMulAction
instContinuousConstSMulULift : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α],
  ContinuousConstSMul (ULift.{u_4, u_1} M) α