mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.postcompose₃_obj_obj_obj_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : 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} C₃] {E : Type u_7}
  [inst_3 : CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [inst_4 : CategoryTheory.Category.{v_8, u_8} E']
  (X : CategoryTheory.Functor E E')
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (X_1 : C₁) (X_2 : C₂)
  (X_3 : C₃),
  ((((CategoryTheory.Functor.postcompose₃.obj X).obj F).obj X_1).obj X_2).obj X_3 =
    X.obj (((F.obj X_1).obj X_2).obj X_3)
-- Mathlib.Analysis.Matrix.Normed
/-- Seminormed group instance (using sup norm of sup norm) for matrices over a seminormed group. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix.  -/
Matrix.seminormedAddCommGroup : {m : Type u_3} →
  {n : Type u_4} →
    {α : Type u_5} → [Fintype m] → [Fintype n] → [SeminormedAddCommGroup α] → SeminormedAddCommGroup (Matrix m n α)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_bind_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.max?.bind t.get? = t.max?
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.tr.match_1.eq_4 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (p : Turing.PartrecToTM2.Γ' → Bool) (k : Turing.PartrecToTM2.K')
  (q : Turing.PartrecToTM2.Λ')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k f q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 :
    (fs : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k)))
  (h_9 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k.cons₂))
  (h_10 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)))
  (h_11 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k)))
  (h_12 : Unit → motive (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt)),
  (match Turing.PartrecToTM2.Λ'.clear p k q with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k f q => h_2 k f q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k) => h_8 fs k
    | Turing.PartrecToTM2.Λ'.ret k.cons₂ => h_9 k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k) => h_10 f k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k) => h_11 f k
    | Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt => h_12 ()) =
    h_4 p k q
-- Mathlib.Tactic.IntervalCases
/-- Assuming `Bound` represents an upper bound, this returns the (inclusive)
greatest integer value which is allowed. So `e ≤ 3` means the lower bound is 3 and
`e < 3` means the upper bound is `2`. Note that in the case of `e < 0` on `Nat`
the upper bound is `-1`, which is not representable as a `Nat`;
this is why we have to treat the `.lt` and `.le` cases separately instead of normalizing
everything to `.le` bounds.
 -/
Mathlib.Tactic.IntervalCases.Bound.asUpper : Mathlib.Tactic.IntervalCases.Bound → ℤ
-- Lean.Meta.Tactic.Grind.Main
/-- Returns the `ExtensionState` for the default `grind` attribute.
 -/
Lean.Meta.Grind.getDefaultExtensionState : Lean.MetaM Lean.Meta.Grind.ExtensionState
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.cancel_counitInv_right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {W X X' Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (e.counitInv.app Y)) =
      CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (e.counitInv.app Y)) ↔
    CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
-- Mathlib.Order.Heyting.Basic
himp_le_himp_right : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b → b ⇨ c ≤ a ⇨ c
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.set_range_subset : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  Set.range ⇑(algebraMap K L) ⊆ ↑S
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_val : ∀ {M : Type u_3} [inst : CommMonoid M] (s : Finset M), s.val.prod = s.prod id
-- Mathlib.Algebra.Order.Monovary
monovary_inv_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Monovary f⁻¹ g ↔ Antivary f g
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.mk.injEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞} (toEquiv : M ≃ M')
  (contMDiff_toFun : ContMDiff I I' n ⇑toEquiv) (contMDiff_invFun : ContMDiff I' I n ⇑toEquiv.symm) (toEquiv_1 : M ≃ M')
  (contMDiff_toFun_1 : ContMDiff I I' n ⇑toEquiv_1) (contMDiff_invFun_1 : ContMDiff I' I n ⇑toEquiv_1.symm),
  ({ toEquiv := toEquiv, contMDiff_toFun := contMDiff_toFun, contMDiff_invFun := contMDiff_invFun } =
      { toEquiv := toEquiv_1, contMDiff_toFun := contMDiff_toFun_1, contMDiff_invFun := contMDiff_invFun_1 }) =
    (toEquiv = toEquiv_1)
-- Init.Data.String.Basic
String.replaceStart : (s : String) → s.Pos → String.Slice
-- Batteries.Data.BitVec.Lemmas
BitVec.getLsb_ofFnBE : ∀ {n : ℕ} (f : Fin n → Bool) (i : Fin n), (BitVec.ofFnBE f).getLsb i = f i.rev
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.smulLeftCLM_add : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F] {g₁ g₂ : E → ℂ},
  Function.HasTemperateGrowth g₁ →
    Function.HasTemperateGrowth g₂ →
      TemperedDistribution.smulLeftCLM F (g₁ + g₂) =
        TemperedDistribution.smulLeftCLM F g₁ + TemperedDistribution.smulLeftCLM F g₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_le_minKey_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, (cmp (t.minKey ⋯) ((t.erase k).minKey he)).isLE = true
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.of_le_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {κ : Cardinal.{w}}
  [inst_1 : Fact κ.IsRegular],
  P.IsCardinalFilteredGenerator κ →
    ∀ {P' : CategoryTheory.ObjectProperty C},
      P ≤ P'.isoClosure → P' ≤ CategoryTheory.isCardinalPresentable C κ → P'.IsCardinalFilteredGenerator κ
-- Mathlib.Topology.Basic
isClosed_const : ∀ {X : Type u} [inst : TopologicalSpace X] {p : Prop}, IsClosed {_x | p}
-- Init.Data.SInt.Basic
/-- Constructs an `ISize` from an `Int`, clamping if the value is too small or too large.  -/
ISize.ofIntClamp : ℤ → ISize
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mapCongr_hom_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f g : X ⟶ Y) (h : f = g)
  (X_1 : CategoryTheory.Under Y), (CategoryTheory.Under.mapCongr f g h).hom.app X_1 = CategoryTheory.eqToHom ⋯
-- Std.Internal.Do.Order.Basic
/-- Binary join (supremum)  -/
Lean.Order.join : {α : Type u} → [Lean.Order.CompleteLattice α] → α → α → α
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- Show that the extension of `f : S.functor ⟶ P` to all of `yoneda.obj X` is in fact an extension,
i.e. that the triangle below commutes, provided `P` is a sheaf for `S`
```
      f
   S  →  P
   ↓  ↗
   yX
```
 -/
CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
  {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (f : S.functor ⟶ P)
  {Z : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h_1 : P ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.functorInclusion (CategoryTheory.CategoryStruct.comp (h.extend f) h_1) =
    CategoryTheory.CategoryStruct.comp f h_1
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instLevel : List Lean.Name → List Lean.Level → Lean.Level → Lean.Level
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curry0_apply : ∀ {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (f : G [×0]→L[𝕜] G'),
  f.curry0 = f 0
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.bijective : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β),
  Function.Bijective ⇑e
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.endRingEquiv_symm_apply : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] (M : TopModuleCat R)
  (f : ↑M.toModuleCat →L[R] ↑M.toModuleCat), M.endRingEquiv.symm f = TopModuleCat.ofHom f
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.add_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} {n : ℕ} [inst_3 : HasDerivedCategory C]
  (α β : CategoryTheory.Abelian.Ext X Y n), (α + β).hom = α.hom + β.hom
-- Lean.Meta.Tactic.Grind.Internalize
/-- Internalizes the nested ground terms in the given pattern.  -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.internalizePattern : Lean.Expr → ℕ → Lean.Meta.Grind.Origin → Lean.Meta.Grind.GoalM Lean.Expr
-- Lean.Parser.Extra
/-- The parser `group(p)` parses the same thing as `p`, but it wraps the results in a `groupKind`
node.

This parser always has arity 1, even if `p` does not. Parsers like `p*` are automatically
rewritten to `group(p)*` if `p` does not have arity 1, so that the results from separate invocations
of `p` can be differentiated.  -/
Lean.Parser.group : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Action.Continuous
ContAction.instCoeAction : (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] → Coe (ContAction V G) (Action V G)
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.instFiniteResidueFieldOfQuasiFiniteAt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (P : Ideal S) [inst_4 : P.IsPrime] [inst_5 : P.LiesOver p] [Algebra.QuasiFiniteAt R P]
  [inst_7 : Algebra (Localization.AtPrime p) (Localization.AtPrime P)]
  [inst_8 : Localization.AtPrime.IsLiesOverAlgebra p P], Module.Finite p.ResidueField P.ResidueField
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.insertMany_list_eq_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)}, Std.ExtDTreeMap.Const.insertMany t l = List.foldl (fun acc p => acc.insert p.1 p.2) t l
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.hom_ext : ∀ {S : SSet.Truncated 2} {x y : SSet.OneTruncation₂ S} {f g : x ⟶ y}, f.edge = g.edge → f = g
-- Mathlib.Algebra.Module.Submodule.Map
AddMonoidHom.coe_toMultiplicative_map : ∀ {G : Type u_9} {G₂ : Type u_10} [inst : AddGroup G] [inst_1 : AddGroup G₂] (f : G →+ G₂) (s : AddSubgroup G),
  Subgroup.map (AddMonoidHom.toMultiplicative f) (AddSubgroup.toSubgroup s) =
    AddSubgroup.toSubgroup (AddSubgroup.map f s)
-- Mathlib.MeasureTheory.Measure.Restrict
/-- The restriction of the pushforward measure is the pushforward of the restriction. For a version
assuming only `AEMeasurable`, see `restrict_map_of_aemeasurable`.  -/
MeasureTheory.Measure.restrict_map : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {f : α → β},
  Measurable f →
    ∀ {s : Set β},
      MeasurableSet s → (MeasureTheory.Measure.map f μ).restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s))
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.reduce.churchRosser.eq_1 : ∀ {α : Type u_1} {L₁ L₂ L₃ : List (α × Bool)} [inst : DecidableEq α] (H12 : FreeGroup.Red L₁ L₂)
  (H13 : FreeGroup.Red L₁ L₃), FreeGroup.reduce.churchRosser H12 H13 = ⟨FreeGroup.reduce L₁, ⋯⟩
-- Mathlib.Analysis.Convex.Gauge
le_gauge_of_notMem : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} {a : ℝ},
  StarConvex ℝ 0 s → Absorbs ℝ s {x} → x ∉ a • s → a ≤ gauge s x
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.mapAddSubgroup_apply : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_6} [inst_1 : AddGroup H] (f : G ≃+ H) (H_1 : AddSubgroup G),
  f.mapAddSubgroup H_1 = AddSubgroup.map (↑f) H_1
-- Mathlib.Data.Finsupp.Basic
Finsupp.snd_sumFinsuppAddEquivProdFinsupp : ∀ {M : Type u_5} [inst : AddMonoid M] {α : Type u_12} {β : Type u_13} (f : α ⊕ β →₀ M) (y : β),
  (Finsupp.sumFinsuppAddEquivProdFinsupp f).2 y = f (Sum.inr y)
-- Init.Data.BitVec.Lemmas
/-- The absolute value of `x : BitVec w`, interpreted as an integer, is a case split:
- When `x = intMin w`, then `x.abs = intMin w`
- Otherwise, `x.abs.toInt` equals the absolute value (`x.toInt.natAbs`).

This is a simpler version of `BitVec.toInt_abs_eq_ite`, which hides a case split on `x.msb`.
 -/
BitVec.toInt_abs_eq_natAbs : ∀ {w : ℕ} {x : BitVec w}, x.abs.toInt = if x = BitVec.intMin w then (BitVec.intMin w).toInt else ↑x.toInt.natAbs
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.nextn_stop : ∀ {l m r : List Char} {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s →
    ∀ (n : ℕ), s.nextn n { byteIdx := String.utf8Len m } = { byteIdx := String.utf8Len m }
-- Mathlib.Order.CompleteBooleanAlgebra
/-- `⊤ \ a` is `￢a`  -/
Order.Coframe.top_sdiff : ∀ {α : Type u_1} [self : Order.Coframe α] (a : α), ⊤ \ a = ￢a
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.IsLocalizationMap.map_zero : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {F : Type u_4}
  [inst_2 : FunLike F M N] [AddHomClass F M N] {f : F}, S.IsLocalizationMap ⇑f → f 0 = 0
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- `s₁ == s₂`  -/
Lean.Grind.AC.SubsetResult.exact : Lean.Grind.AC.SubsetResult
-- Mathlib.Analysis.Calculus.Deriv.Prod
HasDerivWithinAt.prodMk : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f₁ : 𝕜 → F} {f₁' : F} {x : 𝕜} {s : Set 𝕜} {G : Type w} [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 G] {f₂ : 𝕜 → G} {f₂' : G},
  HasDerivWithinAt f₁ f₁' s x → HasDerivWithinAt f₂ f₂' s x → HasDerivWithinAt (fun x => (f₁ x, f₂ x)) (f₁', f₂') s x
-- Mathlib.Topology.Constructions
set_pi_mem_nhds_iff : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {I : Set ι},
  I.Finite → ∀ {s : (i : ι) → Set (A i)} (a : (i : ι) → A i), I.pi s ∈ nhds a ↔ ∀ i ∈ I, s i ∈ nhds (a i)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_mul_X_pow : ∀ {R : Type u} [inst : CommSemiring R] (n m : ℕ) (p : Polynomial R),
  (⇑Polynomial.derivative)^[n] (p * Polynomial.X ^ m) =
    ∑ k ∈ Finset.range (min m n).succ,
      (n.choose k * m.descFactorial k) • ((⇑Polynomial.derivative)^[n - k] p * Polynomial.X ^ (m - k))
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.toOplax_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Oplax.StrongTrans.Modification η θ) (a : B),
  Γ.toOplax.app a = Γ.app a
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.sSup_eq : ∀ {α : Type u_1} [inst : LE α] [inst_1 : SupSet α] {s : Set (WithBot α)},
  ¬s ⊆ {⊥} → BddAbove s → sSup s = ↑(sSup (WithBot.some ⁻¹' s))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol.mk.sizeOf_spec : ∀ (sym : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol), sizeOf (Lean.Lsp.DocumentSymbol.mk sym) = 1 + sizeOf sym
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.any_eq_false_iff_forall_mem_get : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {p : (a : α) → β a → Bool}, m.any p = false ↔ ∀ (a : α) (h : a ∈ m), p a (m.get a h) = false
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.π_homologyIsoSc'_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  CategoryTheory.CategoryStruct.comp (K.homologyπ j) (K.homologyIsoSc' i j k hi hk).hom =
    CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom (K.sc' i j k).homologyπ
-- Lean.Meta.Match.Match
/-- Remove constraints of the form `lhs ≋ rhs` where `lhs` and `rhs` are definitionally equal,
or `lhs` is a free variable.

Dropping unsolved constraints where `lhs` is a free variable seems unsound, but simply leads to later
errors about the type of the alternative not matching the goal type, which is arguably a bit more
user-friendly than showing possibly match-compilation-internal variable names.
 -/
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.filterTrivialCnstrs : Lean.Meta.Match.Alt → Lean.MetaM Lean.Meta.Match.Alt
-- Mathlib.Tactic.Convert
_private.Mathlib.Tactic.Convert.0.instEvalExprExpensiveConfig : Lean.Elab.ConfigEval.EvalExpr Convert.ExpensiveConfig
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
/-- An *increasing approximate unit* in a C⋆-algebra is an approximate unit contained in the
closed unit ball of nonnegative elements.  -/
Filter.IsIncreasingApproximateUnit : {A : Type u_1} → [NonUnitalCStarAlgebra A] → [PartialOrder A] → Filter A → Prop
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.addConst.eq_1 : ∀ (k k_1 : ℤ), (Int.Internal.Linear.Poly.num k_1).addConst k = Int.Internal.Linear.Poly.num (k + k_1)
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.vadd_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter β} {a : α}, f.NeBot → (a +ᵥ f).NeBot
-- Mathlib.Data.ENNReal.Basic
ENNReal.toNNReal_one : ENNReal.toNNReal 1 = 1
-- Mathlib.AlgebraicGeometry.Sites.Small
/-- The presieve defined by a `P`-cover of `S`-schemes with `Q`.  -/
AlgebraicGeometry.Scheme.Cover.toPresieveOverProp : {P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    [inst : P.IsStableUnderBaseChange] →
      {X : Q.Over ⊤ S} →
        (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X.left) →
          [inst_1 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] → (∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) → CategoryTheory.Presieve X
-- Mathlib.RingTheory.Trace.Basic
det_traceMatrix_ne_zero' : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (pb : PowerBasis K L)
  [Algebra.IsSeparable K L], (Algebra.traceMatrix K ⇑pb.basis).det ≠ 0
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- **Alias** of `iteratedFDeriv_fun_zero`. -/
iteratedFDeriv_zero_fun : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ},
  (iteratedFDeriv 𝕜 n fun x => 0) = 0
-- Mathlib.Analysis.Normed.Module.Convex
/-- The set of vectors in the same ray as `x` is connected.  -/
isConnected_setOfPred_sameRay : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : E), IsConnected {y | SameRay ℝ x y}
-- Init.Data.SInt.Lemmas
UInt8.toUInt8_toInt8 : ∀ (x : UInt8), x.toInt8.toUInt8 = x
-- Mathlib.Order.Filter.Basic
Filter.eventuallyEq_set : ∀ {α : Type u} {s t : Set α} {l : Filter α}, s =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If `p₃` bisects the angle `∡ p₁ p₂ p₄` externally, and `p₃` and `p₄` lie on the same side of
the line `p₁ p₂`, then the unoriented angle `∠ p₁ p₂ p₃` is half `∠ p₁ p₂ p₄` plus `π / 2`.  -/
EuclideanGeometry.angle_eq_angle_add_pi_div_two_of_oangle_eq_add_pi_of_sSameSide : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ : P},
  p₁ ≠ p₂ →
    EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₃ p₂ p₄ + ↑Real.pi →
      line[ℝ, p₁, p₂].SSameSide p₃ p₄ →
        EuclideanGeometry.angle p₁ p₂ p₃ = (EuclideanGeometry.angle p₁ p₂ p₄ + Real.pi) / 2
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.comm_trans_rTensor_trans_comm_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_8} {P : Type u_9} {Q : Type u_10} [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R N] [inst_5 : Module R P]
  [inst_6 : Module R Q] (g : N ≃ₗ[R] P),
  TensorProduct.comm R Q N ≪≫ₗ LinearEquiv.rTensor Q g ≪≫ₗ TensorProduct.comm R P Q = LinearEquiv.lTensor Q g
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.gcd_mk_mk : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b : α},
  gcd (Associates.mk a) (Associates.mk b) = Associates.mk (gcd a b)
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.zero_divMod : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {I J : FractionalIdeal (nonZeroDivisors R) K},
  FractionalIdeal.divMod 0 I J = 0
-- Batteries.Data.AssocList
Batteries.AssocList.contains.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α) (l : Batteries.AssocList α β),
  Batteries.AssocList.contains a l = Batteries.AssocList.any (fun k x => k == a) l
-- Mathlib.Data.Sym.Sym2
/-- The functor `Sym2` is functorial, and this function constructs the induced maps.
 -/
Sym2.map : {α : Type u_1} → {β : Type u_2} → (α → β) → Sym2 α → Sym2 β