mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Pretopology
/-- The largest pretopology generating the given Grothendieck topology.

See [MM92] Chapter III, Section 2, Equations (3,4).
 -/
CategoryTheory.GrothendieckTopology.toPretopology : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      CategoryTheory.GrothendieckTopology C → CategoryTheory.Pretopology C
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyLT? : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → Option α
-- Mathlib.Data.Matrix.Mul
Matrix.row_vecMulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Mul α] (w : m → α) (v : n → α) (i : m),
  (Matrix.vecMulVec w v).row i = w i • v
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.extend_empty : ∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (P0 : P ∅),
  m ∅ P0 = 0 → MeasureTheory.extend m ∅ = 0
-- Mathlib.Data.Stream.Defs
/-- Proposition saying that at least one element of a stream satisfies a predicate.  -/
Stream'.Any : {α : Type u} → (α → Prop) → Stream' α → Prop
-- Lean.Meta.IntInstTesters
Lean.Meta.DefEq.isInstLEInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.LinearAlgebra.Dual.Defs
/-- If a linear map is surjective, then its dual is injective.  -/
LinearMap.dualMap_injective_of_surjective : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] {f : M₁ →ₗ[R] M₂},
  Function.Surjective ⇑f → Function.Injective ⇑f.dualMap
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.pi : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup F]
  [inst_2 : TopologicalSpace F] [inst_3 : Module 𝕜 F] {l : Filter α} {g : α → F} {ι : Type u_7} {E : ι → Type u_8}
  [inst_4 : (i : ι) → AddCommGroup (E i)] [inst_5 : (i : ι) → Module 𝕜 (E i)]
  [inst_6 : (i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {f : (i : ι) → α → E i},
  (∀ (i : ι), f i =O[𝕜; l] g) → (fun x i => f i x) =O[𝕜; l] g
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.pullbackHom_map_assoc : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : W ⟶ X)
  [inst_2 : ∀ (x : 𝒰.I₀), CategoryTheory.Limits.HasPullback f (𝒰.f x)] (i : 𝒰.toPreZeroHypercover.1)
  {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (𝒰.pullbackHom f i) (CategoryTheory.CategoryStruct.comp (𝒰.f i) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i)
      (CategoryTheory.CategoryStruct.comp f h)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k a : α} {v : β} {h₁ : a ∈ t.insertIfNew k v},
  (t.insertIfNew k v).getKey a h₁ = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKey a ⋯
-- Lean.Elab.DocString
/-- Built-in docstring roles, for bootstrapping.
 -/
Lean.Doc.builtinDocRoles : IO.Ref (Lean.NameMap (Array (Lean.Name × Lean.Doc.DocRoleExpander)))
-- Init.Data.List.Erase
List.erase_eq_self_iff : ∀ {α : Type u_1} [inst : BEq α] {a : α} [LawfulBEq α] {l : List α}, l.erase a = l ↔ a ∉ l
-- Init.Data.Order.Opposite
Min.oppositeMax_def : ∀ {α : Type u_1} {min : Min α}, min.oppositeMax = { max := Min.min }
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange_neg' : ∀ {ι : Type u_1} {F : Type u_2} {G : Type u_6} {H : Type u_7} [inst : AddGroup G] [inst_1 : SubtractionMonoid H]
  [inst_2 : FunLike F G H] [inst_3 : AddMonoidHomClass F G H] {f : F} (v : ι →₀ G),
  Finsupp.mapRange ⇑f ⋯ (-v) = -Finsupp.mapRange ⇑f ⋯ v
-- Init.Data.String.Defs
String.Internal.isEmptyImpl : String → Bool
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S : Solution`, we let `S.x` be any element such that
`S.a + S.b = λ ^ (3*S.multiplicity-2) * S.x`  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.x : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} →
      {hζ : IsPrimitiveRoot ζ 3} →
        FermatLastTheoremForThreeGen.Solution✝ hζ →
          [inst_1 : NumberField K] → [IsCyclotomicExtension {3} ℚ K] → NumberField.RingOfIntegers K
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restr_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set X), ↑(e.restr s) = ↑e
-- Mathlib.LinearAlgebra.Alternating.Basic
MultilinearMap.alternatization_coe : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (m : MultilinearMap R (fun x => M) N'),
  ↑(MultilinearMap.alternatization m) = ∑ σ, Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ m
-- Std.Data.TreeSet.Basic
/-- Returns the number of mappings present in the map.  -/
Std.TreeSet.size : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → ℕ
-- Mathlib.MeasureTheory.Measure.Prod
/-- Let `f : α → β` be a measure-preserving map.
For a.e. all `a`, let `g a : γ → δ` be a measure-preserving map.
Also suppose that `g` is measurable as a function of two arguments.
Then the map `fun (a, c) ↦ (f a, g a c)` is a measure-preserving map
for the product measures on `α × γ` and `β × δ`.

Some authors call a map of the form `fun (a, c) ↦ (f a, g a c)` a *skew product* over `f`,
thus the choice of a name.
 -/
MeasureTheory.MeasurePreserving.skew_product : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {δ : Type u_4} [inst_3 : MeasurableSpace δ] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ} {μd : MeasureTheory.Measure δ}
  [MeasureTheory.SFinite μa] [MeasureTheory.SFinite μc] {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb →
    ∀ {g : α → γ → δ},
      Measurable (Function.uncurry g) →
        (∀ᵐ (a : α) ∂μa, MeasureTheory.Measure.map (g a) μc = μd) →
          MeasureTheory.MeasurePreserving (fun p => (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd)
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
CategoryTheory.Bicategory.Comonad.comul_counit : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [inst_1 : CategoryTheory.Bicategory.Comonad t],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.Bicategory.whiskerLeft t CategoryTheory.Bicategory.Comonad.counit) =
    (CategoryTheory.Bicategory.rightUnitor t).inv
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.liftHomId : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a : B} → Mathlib.Tactic.BicategoryCoherence.LiftHom (CategoryTheory.CategoryStruct.id a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.forM_eq_forM_toArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : (a : α) × β a → m PUnit.{w + 1}},
  Std.DTreeMap.Internal.Impl.forM (fun k v => f ⟨k, v⟩) t = forM t.toArray f
-- Batteries.Tactic.Alias
Batteries.Tactic.Alias.AliasInfo.plain.injEq : ∀ (n n_1 : Lean.Name),
  (Batteries.Tactic.Alias.AliasInfo.plain n = Batteries.Tactic.Alias.AliasInfo.plain n_1) = (n = n_1)
-- Mathlib.Order.Filter.Map
Filter.comap_mono : ∀ {α : Type u_1} {β : Type u_2} {m : α → β}, Monotone (Filter.comap m)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) {c' c'' : C} (f : c' ⟶ c'') (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft c f) d =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d))
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c'' d).inv)
-- Std.Time.Duration
Std.Time.instInhabitedDuration : Inhabited Std.Time.Duration
-- Mathlib.Tactic.Sat.FromLRAT
Sat.instToExprLiteral : Lean.ToExpr Sat.Literal
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₃₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₃₄ = f.right.hom
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.ε_algSpec_left : ∀ {R : CommRingCat},
  CategoryTheory.Over.Hom.left (CategoryTheory.Functor.LaxMonoidal.ε (AlgebraicGeometry.algSpec R)) =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec R)
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.mk.inj : ∀ {carrier : Type u} {str : AddGroup carrier} {carrier_1 : Type u} {str_1 : AddGroup carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.Analysis.Analytic.OfScalars
/-- The ratio test stating that if `‖c n.succ‖ / ‖c n‖` tends to zero, the radius is unbounded.
This requires that the coefficients are eventually non-zero as
`‖c n.succ‖ / 0 = 0` by convention.  -/
FormalMultilinearSeries.ofScalars_radius_eq_top_of_tendsto : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing E] [inst_2 : NormedAlgebra 𝕜 E]
  (c : ℕ → 𝕜),
  (∀ᶠ (n : ℕ) in Filter.atTop, c n ≠ 0) →
    Filter.Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) Filter.atTop (nhds 0) →
      (FormalMultilinearSeries.ofScalars E c).radius = ⊤
-- Init.Sym.Lemmas
Lean.Sym.dite_cond_congr : ∀ {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬c → α) (c' : Prop) {inst' : Decidable c'} (h : c = c'),
  dite c a b = if h' : c' then a ⋯ else b ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The obvious functor `(ShortComplex C)ᵒᵖ ⥤ ShortComplex Cᵒᵖ`.  -/
CategoryTheory.ShortComplex.opFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      CategoryTheory.Functor (CategoryTheory.ShortComplex C)ᵒᵖ (CategoryTheory.ShortComplex Cᵒᵖ)
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
/-- A cocone for a functor `F : J ⥤ HomologicalComplex C c` which is given in degree `n` by
the colimit of `F ⋙ eval C c n`.  -/
HomologicalComplex.coconeOfHasColimitEval : {C : Type u_1} →
  {ι : Type u_2} →
    {J : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_3} J] →
          {c : ComplexShape ι} →
            [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (F : CategoryTheory.Functor J (HomologicalComplex C c)) →
                [∀ (n : ι), CategoryTheory.Limits.HasColimit (F.comp (HomologicalComplex.eval C c n))] →
                  CategoryTheory.Limits.Cocone F
-- Lean.Message
/-- A `Message` is a richly formatted piece of information emitted by Lean.
They are rendered by client editors in the infoview and in diagnostic windows.  -/
Lean.Message : Type
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.diag_toFun : ∀ (A : Type u_2) [inst : Monoid A] [inst_1 : TopologicalSpace A] (i : A), (ContinuousMonoidHom.diag A) i = (i, i)
-- Mathlib.Data.ZMod.Defs
ZMod.infinite : Infinite (ZMod 0)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedCases : {a : Lean.Compiler.LCNF.Purity} → Inhabited (Lean.Compiler.LCNF.Cases a)
-- Std.Tactic.Do.Syntax
/-- `mspecialize_pure` is like `mspecialize`, but it specializes a hypothesis from the
*pure* context with hypotheses from either the pure or stateful context or pure terms.
```lean
example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) (hΨ : ∀ x, ⊢ₛ P → Q → Ψ x) : ⊢ₛ Q → Ψ (y + 1) := by
  mintro HQ
  mspecialize_pure (hΨ (y + 1)) hP HQ => HΨ
  mexact HΨ
```
 -/
Lean.Parser.Tactic.mspecializePure : Lean.ParserDescr
-- Mathlib.Analysis.BoxIntegral.Integrability
/-- If `f` has integral `y` on a box `I` with respect to a locally finite measure `μ` and `g` is
a.e. equal to `f` on `I`, then `g` has the same integral on `I`.  -/
BoxIntegral.HasIntegral.congr_ae : ∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {y : E} {f g : (ι → ℝ) → E}
  {μ : MeasureTheory.Measure (ι → ℝ)} [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ],
  BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul y →
    f =ᵐ[μ.restrict ↑I] g → l.bRiemann = false → BoxIntegral.HasIntegral I l g μ.toBoxAdditive.toSMul y
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- Right homotopies are compatible with precomposition.  -/
HomotopicalAlgebra.PathObject.RightHomotopy.precomp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        {P : HomotopicalAlgebra.PathObject Y} →
          {f g : X ⟶ Y} →
            P.RightHomotopy f g →
              {Z : C} →
                (i : Z ⟶ X) →
                  P.RightHomotopy (CategoryTheory.CategoryStruct.comp i f) (CategoryTheory.CategoryStruct.comp i g)
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.Nonempty.mono : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C} [P.Nonempty],
  P ≤ Q → Q.Nonempty
-- Mathlib.Data.Set.NAry
/-- Symmetric statement to `Set.image_image2_right_comm`.  -/
Set.image_image2_distrib_right : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : Set α} {t : Set β}
  {g : γ → δ} {f' : α → β' → δ} {g' : β → β'},
  (∀ (a : α) (b : β), g (f a b) = f' a (g' b)) → g '' Set.image2 f s t = Set.image2 f' s (g' '' t)
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_one : ∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] {i : σ}, (MvPolynomial.pderiv i) 1 = 0
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_dite_irrel : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (p : Prop) [inst_1 : Decidable p] (s : Finset ι)
  (f : p → ι → M) (g : ¬p → ι → M),
  (∑ x ∈ s, if h : p then f h x else g h x) = if h : p then ∑ x ∈ s, f h x else ∑ x ∈ s, g h x
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isPosSemidef_zero : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I₁ : R →+* R}
  [inst_3 : Preorder R], LinearMap.IsPosSemidef 0
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct
SSet.prodStdSimplex.strongAnodyneExtensions_unionProd_ι : ∀ {m : ℕ} (k : Fin (m + 2)) (n : ℕ), SSet.strongAnodyneExtensions ((SSet.horn (m + 1) k).unionProd (SSet.boundary n)).ι
-- Mathlib.Analysis.Normed.Operator.Basic
_private.Mathlib.Analysis.Normed.Operator.Basic.0.ContinuousLinearMap.uniformity_eq_seminorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂],
  uniformity (E →SL[σ₁₂] F) = ⨅ r, ⨅ (_ : r > 0), Filter.principal {f | ‖-f.1 + f.2‖ < r}
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.idxOf.eq_1 : ∀ {α : Type u} [inst : BEq α] (a : α), Array.idxOf a = Array.findIdx fun x => x == a
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.ofList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α}, (Std.TreeSet.Raw.ofList l cmp).WF
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- The truth morphism is a monomorphism  -/
CategoryTheory.Subobject.Classifier.mono_truth : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Subobject.Classifier C),
  CategoryTheory.Mono self.truth
-- Mathlib.Geometry.Manifold.Instances.Icc
contMDiffWithinAt_comp_projIcc_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {x y : ℝ}
  [h : Fact (x < y)] {n : WithTop ℕ∞} {f : ↑(Set.Icc x y) → M} {w : ↑(Set.Icc x y)},
  ContMDiffWithinAt (modelWithCornersSelf ℝ ℝ) I n (f ∘ Set.projIcc x y ⋯) (Set.Icc x y) ↑w ↔
    ContMDiffAt (modelWithCornersEuclideanHalfSpace 1) I n f w
-- Mathlib.Topology.UniformSpace.Separation
eq_of_uniformity_basis : ∀ {α : Type u_1} [inst : UniformSpace α] [T0Space α] {ι : Sort u_2} {p : ι → Prop} {s : ι → Set (α × α)},
  (uniformity α).HasBasis p s → ∀ {x y : α}, (∀ {i : ι}, p i → (x, y) ∈ s i) → x = y
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.neg_mk : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x : ℕ × K),
  -PerfectClosure.mk K p x = PerfectClosure.mk K p (x.1, -x.2)
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.binaryProductLimitCone_cone_pt : ∀ {R : Type u} [inst : Ring R] (M N : ModuleCat R), (M.binaryProductLimitCone N).cone.pt = ModuleCat.of R (↑M × ↑N)
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_ofReal : ∀ (x : ℝ), (ENNReal.ofReal x).log = if x ≤ 0 then ⊥ else ↑(Real.log x)
-- Mathlib.Data.QPF.Univariate.Basic
/-- recursor of a type defined by a qpf  -/
QPF.Fix.rec : {F : Type u → Type u} → [q : QPF F] → {α : Type u} → (F α → α) → QPF.Fix F → α
-- Init.Data.Order.Lemmas
Std.ne_of_lt : ∀ {α : Type u} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2] {a b : α}, a < b → a ≠ b
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEq_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (u₀ : E.I₀ → F.I₀)
  (u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)) (k : E.I₁ i j),
  u₁ ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k) =
    (CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) (u₁ k)
-- Lean.Meta.Match.SolveOverlap
_private.Lean.Meta.Match.SolveOverlap.0.Lean.Meta.Match.InjectionAnyResult.subgoal.sizeOf_spec : ∀ (fvarId : Lean.FVarId) (mvarId : Lean.MVarId),
  sizeOf (Lean.Meta.Match.InjectionAnyResult.subgoal✝ fvarId mvarId) = 1 + sizeOf fvarId + sizeOf mvarId
-- Mathlib.Topology.Algebra.Group.Basic
/-- If multiplication is continuous in `α`, then it also is in `αᵐᵒᵖ`.  -/
instIsTopologicalGroupMulOpposite : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Group α] [IsTopologicalGroup α], IsTopologicalGroup αᵐᵒᵖ
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.whiskerRight_comp_unit_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G] {x x' : C} (y : C)
  (f : x ⟶ x') {Z : V}
  (h :
    (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).obj
        ((CategoryTheory.MonoidalCategory.tensor C).obj (x', y)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (G.obj y))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x', y)) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).map
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight f y))
        h)
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.mul_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  (x x' y : MonCat.Colimits.Prequotient F),
  MonCat.Colimits.Relation F x x' → MonCat.Colimits.Relation F (x.mul y) (x'.mul y)
-- Mathlib.MeasureTheory.Measure.AEDisjoint
/-- **Alias** of `MeasureTheory.AEDisjoint.sdiff_ae_eq_left`. -/
MeasureTheory.AEDisjoint.diff_ae_eq_left : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t → s \ t =ᵐ[μ] s
-- Mathlib.Analysis.Normed.Module.Basic
/-- The product of two normed spaces is a normed space, with the sup norm.  -/
Prod.normedSpace : {𝕜 : Type u_1} →
  {E : Type u_3} →
    {F : Type u_4} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup E] →
          [inst_2 : SeminormedAddCommGroup F] → [NormedSpace 𝕜 E] → [NormedSpace 𝕜 F] → NormedSpace 𝕜 (E × F)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub_nsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIcoMod hp a (b - m • p) = toIcoMod hp a b
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.mapAddEquiv`.

---

Additively isomorphic rings have additively isomorphic monoid algebras.

`MonoidAlgebra.map` as an `AddEquiv`.  -/
MonoidAlgebra.mapRangeAddEquiv : {R : Type u_3} →
  {S : Type u_4} →
    (M : Type u_6) →
      [inst : Semiring R] → [inst_1 : Semiring S] → [inst_2 : Mul M] → R ≃+ S → MonoidAlgebra R M ≃+ MonoidAlgebra S M
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.IsGood.fibration_p : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A : C}
  {inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C} {P : HomotopicalAlgebra.PathObject A}
  {inst_2 : CategoryTheory.Limits.HasBinaryProduct A A} {inst_3 : HomotopicalAlgebra.CategoryWithFibrations C}
  [self : P.IsGood], HomotopicalAlgebra.Fibration P.p
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.isEmpty = true → t.getKey? a = none
-- Mathlib.Order.Interval.Lex
NonemptyInterval.toLex_le_toLex : ∀ {α : Type u_1} [inst : LT α] [inst_1 : LE α] {x y : NonemptyInterval α},
  toLex x ≤ toLex y ↔ y.toProd.1 < x.toProd.1 ∨ x.toProd.1 = y.toProd.1 ∧ x.toProd.2 ≤ y.toProd.2
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
Std.Tactic.BVDecide.LRAT.Internal.CNF.convertLRAT_readyForRupAdd : ∀ (cnf : Std.Sat.CNF ℕ), (Std.Tactic.BVDecide.LRAT.Internal.CNF.convertLRAT cnf).ReadyForRupAdd
-- Mathlib.Control.Monad.Writer
WriterT.instMonadFunctor : {M : Type u → Type v} → {ω : Type u} → MonadFunctor M (WriterT ω M)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The inductively defined smallest additive congruence relation
containing a binary relation `r` equals the infimum of the set of additive congruence relations
containing `r`.  -/
AddCon.addConGen_eq : ∀ {M : Type u_1} [inst : Add M] (r : M → M → Prop), addConGen r = sInf {s | ∀ (x y : M), r x y → s x y}
-- Mathlib.Data.TypeVec
/-- turn an equality into an arrow, with reverse direction  -/
TypeVec.Arrow.mpr : {n : ℕ} → {α β : TypeVec.{u_1} n} → α = β → β.Arrow α