mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_ite`. -/
Set.restrict_ite : ∀ {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [inst : (x : α) → Decidable (x ∈ s)],
  (s.domRestrict fun a => if a ∈ s then f a else g a) = s.domRestrict f
-- Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
cardinalMk_algHom_le_rank : ∀ (K : Type u_1) (M : Type u_2) (L : Type v) [inst : CommRing K] [inst_1 : Ring M] [inst_2 : Algebra K M]
  [Module.Free K M] [Module.Finite K M] [inst_5 : CommRing L] [IsDomain L] [inst_7 : Algebra K L],
  Cardinal.mk (M →ₐ[K] L) ≤ Cardinal.lift.{v, u_2} (Module.rank K M)
-- Init.Data.UInt.Lemmas
USize.ofNat_uInt64Size_sub_one : USize.ofNat (UInt64.size - 1) = USize.ofNatLT (USize.size - 1) ⋯
-- Mathlib.Topology.Algebra.Group.Units
ContinuousAddEquiv.piAddUnits.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → AddMonoid (M i)] [inst_1 : (i : ι) → TopologicalSpace (M i)],
  ContinuousAddEquiv.piAddUnits = { toAddEquiv := AddEquiv.piAddUnits, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Batteries.Data.Fin.Coding
Fin.decodePUnit_encodePUnit : ∀ (x : PUnit.{u_1}), Fin.decodePUnit (Fin.encodePUnit x) = x
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instPow : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → {α : Type u_3} → [Pow Y α] → Pow (LocallyConstant X Y) α
-- Mathlib.Util.Superscript
Mathlib.Tactic.Superscript.instHashableChar_mathlib : Hashable Char
-- Aesop.Stats.Basic
Aesop.ForwardClusterStateStats.mk.sizeOf_spec : ∀ (slots : ℕ) (instantiationStats : Array Aesop.ForwardInstantiationStats),
  sizeOf { slots := slots, instantiationStats := instantiationStats } = 1 + sizeOf slots + sizeOf instantiationStats
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.instInhabitedDirectLimit : {ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) →
      [inst_1 : (i : ι) → AddCommMonoid (G i)] →
        [inst_2 : DecidableEq ι] → (f : (i j : ι) → i ≤ j → G i →+ G j) → Inhabited (AddCommGroup.DirectLimit G f)
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
MvPowerSeries.gaussNorm.eq_1 : ∀ {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) (f : MvPowerSeries σ R) [inst : Semiring R],
  MvPowerSeries.gaussNorm v c f = ⨆ t, v ((MvPowerSeries.coeff t) f) * t.prod fun x1 x2 => c x1 ^ x2
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- The ordinal-indexed sequence approximating the least fixed point greater than
an initial value `x`. It is defined in such a way that we have `lfpApprox 0 x = x` and
`lfpApprox a x = ⨆ b < a, f (lfpApprox b x)`.  -/
OrdinalApprox.lfpApprox : {α : Type u} → [inst : CompleteLattice α] → (α →o α) → α → Ordinal.{u} → α
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionOptions.mk.inj : ∀ {toWorkDoneProgressOptions : Lean.Lsp.WorkDoneProgressOptions}
  {codeActionKinds? : Option (Array Lean.Lsp.CodeActionKind)} {resolveProvider? : Option Bool}
  {toWorkDoneProgressOptions_1 : Lean.Lsp.WorkDoneProgressOptions}
  {codeActionKinds?_1 : Option (Array Lean.Lsp.CodeActionKind)} {resolveProvider?_1 : Option Bool},
  { toWorkDoneProgressOptions := toWorkDoneProgressOptions, codeActionKinds? := codeActionKinds?,
        resolveProvider? := resolveProvider? } =
      { toWorkDoneProgressOptions := toWorkDoneProgressOptions_1, codeActionKinds? := codeActionKinds?_1,
        resolveProvider? := resolveProvider?_1 } →
    toWorkDoneProgressOptions = toWorkDoneProgressOptions_1 ∧
      codeActionKinds? = codeActionKinds?_1 ∧ resolveProvider? = resolveProvider?_1
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.conjAct_pointwise_smul_eq_self : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup G} {g : G}, g ∈ Subgroup.normalizer ↑H → ConjAct.toConjAct g • H = H
-- Mathlib.Analysis.Convex.EGauge
/-- **Alias** of the reverse direction of `egauge_zero_left_eq_top`. -/
egauge_zero_left : ∀ (𝕜 : Type u_1) [inst : NNNorm 𝕜] [Nonempty 𝕜] {E : Type u_2} [inst_2 : Zero E] [inst_3 : SMulZeroClass 𝕜 E] {x : E},
  x ≠ 0 → egauge 𝕜 0 x = ⊤
-- Mathlib.Algebra.Group.Defs
_private.Mathlib.Algebra.Group.Defs.0.npowRec.match_1.eq_1 : ∀ {M : Type u_2} (motive : ℕ → M → Sort u_1) (x : M) (h_1 : (x : M) → motive 0 x)
  (h_2 : (n : ℕ) → (a : M) → motive n.succ a),
  (match 0, x with
    | 0, x => h_1 x
    | n.succ, a => h_2 n a) =
    h_1 x
-- Mathlib.Topology.Compactness.LocallyCompact
Topology.IsOpenEmbedding.locallyCompactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyCompactSpace Y]
  {f : X → Y}, Topology.IsOpenEmbedding f → LocallyCompactSpace X
-- Mathlib.Computability.EpsilonNFA
εNFA.subset_εClosure : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ), S ⊆ M.εClosure S
-- Init.Data.Option.Basic
/-- Returns the first of its arguments that is `some`, or `none` if neither is `some`.

This is similar to the `<|>` operator, also known as `OrElse.orElse`, but both arguments are always
evaluated without short-circuiting.
 -/
Option.or : {α : Type u_1} → Option α → Option α → Option α
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.IsRootSystem.span_root_eq_top : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N}
  [self : P.IsRootSystem], Submodule.span R (Set.range ⇑P.root) = ⊤
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instToExprProof : Lean.ToExpr Mathlib.Tactic.ITauto.Proof
-- Mathlib.Data.TypeVec
TypeVec.ofSubtype.eq_2 : ∀ (n_2 : ℕ) (α_2 : TypeVec.{u} (n_2 + 1)) (p_2 : α_2.Arrow (TypeVec.repeat (n_2 + 1) Prop))
  (x_2 : TypeVec.Subtype_ p_2 Fin2.fz), TypeVec.ofSubtype p_2 Fin2.fz x_2 = x_2
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.prod_lt_prod' : ∀ {ι : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftStrictMono M] [MulLeftMono M]
  [MulRightStrictMono M] [MulRightMono M] {l : List ι} (f g : ι → M),
  (∀ i ∈ l, f i ≤ g i) → (∃ i ∈ l, f i < g i) → (List.map f l).prod < (List.map g l).prod
-- Mathlib.Analysis.Calculus.SmoothSeries
/-- Consider a series of functions `∑' n, f n x`. If the series converges at a
point, and all functions in the series are differentiable with a summable bound on the derivatives,
then the series converges everywhere.  -/
summable_of_summable_hasFDerivAt : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [CompleteSpace F]
  {u : α → ℝ} [inst_6 : NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {x₀ : E},
  Summable u →
    (∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x) →
      (∀ (n : α) (x : E), ‖f' n x‖ ≤ u n) → (Summable fun n => f n x₀) → ∀ (x : E), Summable fun n => f n x
-- Mathlib.Logic.Equiv.Defs
Equiv.refl_trans : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), (Equiv.refl α).trans e = e
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.apply_ne_zero_iff : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) [Nontrivial R] (a : ℤ),
  χ ↑a ≠ 0 ↔ IsCoprime a ↑n
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- Composition of functions on pseudoelements is composition of morphisms.  -/
CategoryTheory.Abelian.Pseudoelement.comp_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R),
  CategoryTheory.Abelian.Pseudoelement.pseudoApply g ∘ CategoryTheory.Abelian.Pseudoelement.pseudoApply f =
    CategoryTheory.Abelian.Pseudoelement.pseudoApply (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ι_add_mul_swap : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x y : M),
  (ExteriorAlgebra.ι R) x * (ExteriorAlgebra.ι R) y + (ExteriorAlgebra.ι R) y * (ExteriorAlgebra.ι R) x = 0
-- Mathlib.Data.List.Infix
List.insert_eq_ite : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α), insert a l = if a ∈ l then l else a :: l
-- Init.Data.SInt.Bitwise
Int16.toInt_not : ∀ (a : Int16), (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 16)
-- Init.Data.Nat.Fold
Nat.fold_eq_finRange_foldl : ∀ {α : Type u} (n : ℕ) (f : (i : ℕ) → i < n → α → α) (init : α),
  n.fold f init =
    List.foldl
      (fun acc x =>
        match x with
        | ⟨i, h⟩ => f i h acc)
      init (List.finRange n)
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coe_vadd : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (v : V) (b : AffineBasis ι k P), ⇑(v +ᵥ b) = v +ᵥ ⇑b
-- Mathlib.Geometry.Polygon.Basic
Affine.Triangle.toPolygon_vertices : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : AddTorsor V P] (t : Affine.Triangle R P), (Affine.Triangle.toPolygon t).vertices = t.points
-- Mathlib.NumberTheory.Cyclotomic.Basic
isCyclotomicExtension_iff_eq_adjoin : ∀ (S : Set ℕ) {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
  (C : Subalgebra A B),
  (∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n) →
    (IsCyclotomicExtension S A ↥C ↔ C = Algebra.adjoin A {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
-- Mathlib.Computability.StateTransition
StateTransition.Reaches₀.tail' : ∀ {σ : Type u_1} {f : σ → Option σ} {a b c : σ},
  StateTransition.Reaches₀ f a b → c ∈ f b → StateTransition.Reaches₁ f a c
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsTerminal.isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C}
  (hX : CategoryTheory.Limits.IsTerminal X), CategoryTheory.Limits.IsZero X
-- Mathlib.RingTheory.PowerSeries.Derivative
/-- **Alias** of `PowerSeries.derivative_C`. -/
PowerSeries.derivativeFun_C : ∀ {R : Type u_1} [inst : CommSemiring R] {r : R}, (PowerSeries.derivative R) (PowerSeries.C r) = 0
-- Mathlib.Order.Filter.CountablyGenerated
/-- A countable filter basis `B` on a type `α` is a nonempty countable collection of sets of `α`
such that the intersection of two elements of this collection contains some element
of the collection.  -/
Filter.CountableFilterBasis : Type u_6 → Type u_6
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
Std.Iterators.Types.TakeWhile.PlausibleStep.done : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} {it : Std.IterM m β},
  it.internalState.inner.IsPlausibleStep Std.IterStep.done →
    Std.Iterators.Types.TakeWhile.PlausibleStep it Std.IterStep.done
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.isGroundPattern : Lean.Expr → Bool
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeftIso_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (W X : C),
  CategoryTheory.MonoidalCategory.whiskerLeftIso W (CategoryTheory.Iso.refl X) =
    CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj W X)
-- Std.Time.Format.Modifier
Std.Time.DayPeriod.noConfusionType : Sort v✝ → Std.Time.DayPeriod → Std.Time.DayPeriod → Sort v✝
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.toLp_add : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f g : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.MemLp (⇑f) p μ)
  (hg : MeasureTheory.MemLp (⇑g) p μ), (f + g).toLp ⋯ = f.toLp hf + g.toLp hg
-- Mathlib.Analysis.Seminorm
/-- Seminorm-balls are convex.  -/
Seminorm.convex_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul ℝ 𝕜] [NormSMulClass ℝ 𝕜]
  [inst_4 : Module 𝕜 E] [inst_5 : Module ℝ E] [IsScalarTower ℝ 𝕜 E] (p : Seminorm 𝕜 E) (x : E) (r : ℝ),
  Convex ℝ (p.ball x r)
-- Mathlib.Analysis.Calculus.TangentCone.Real
/-- The real interval `[0, 1]` is a set of unique differentiability.  -/
uniqueDiffOn_Icc_zero_one : UniqueDiffOn ℝ (Set.Icc 0 1)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.Iterators.Types.DropWhile.instIterator.match_1.splitter : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} →
      (out : β) →
        (motive : Subtype (P out).Property → Sort u_3) →
          (__do_lift : Subtype (P out).Property) →
            ((h'' : (P out).Property { down := true }) → motive ⟨{ down := true }, h''⟩) →
              ((h'' : (P out).Property { down := false }) → motive ⟨{ down := false }, h''⟩) → motive __do_lift
-- Aesop.Script.Main
Aesop.checkAndTraceScript : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] →
      [Lean.MonadRef m] →
        [Lean.MonadError m] →
          [Lean.AddMessageContext m] →
            [Aesop.MonadStats m] →
              [MonadLiftT Lean.MetaM m] →
                Aesop.Script.UScript →
                  Option (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq × Aesop.ScriptGenerated) →
                    Lean.Meta.SavedState → Lean.MVarId → Aesop.Options' → Bool → String → m Unit
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.closure_sdiff_eq_closure : ∀ {M : Type u_1} [inst : MulOneClass M] {s t : Set M},
  t ⊆ ↑(Submonoid.closure (s \ t)) → Submonoid.closure (s \ t) = Submonoid.closure s
-- Lean.Meta.Match.MatcherApp.Transform
/-- Sets the user name of the FVars in the local context according to the given array of names.

If they differ in size the shorter size wins.
 -/
Lean.Meta.MatcherApp.withUserNames : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Array Lean.Expr → Array Lean.Name → n α → n α
-- Lean.Widget.InteractiveCode
/-- Pretty-printed syntax (usually but not necessarily an `Expr`) with embedded `Info`s.  -/
Lean.Widget.CodeWithInfos : Type
-- Mathlib.Topology.Bornology.Basic
instBornologyPUnit : Bornology PUnit.{u_4 + 1}
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instNonAssocRing : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : NonAssocRing A] →
          [inst_2 : Module R A] →
            [SMulCommClass R A A] →
              [IsScalarTower R A A] →
                [inst_5 : NonAssocSemiring B] →
                  [inst_6 : Module R B] →
                    [SMulCommClass R B B] → [IsScalarTower R B B] → NonAssocRing (TensorProduct R A B)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opProductIsoCoproduct'_comp_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  {f f' : CategoryTheory.Limits.Fan Z} {c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)}
  (hf : CategoryTheory.Limits.IsLimit f) (hf' : CategoryTheory.Limits.IsLimit f')
  (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).hom
      (CategoryTheory.Limits.opProductIsoCoproduct' hf' hc).inv =
    (hf.conePointUniqueUpToIso hf').op.inv
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.pure' : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {a : α} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond α ps}, (P ⊢ₛ Q.1 a) → ⦃P⦄ pure a ⦃Q⦄
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.lift_comp_ι : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (g : ExteriorAlgebra R M →ₐ[R] A),
  (ExteriorAlgebra.lift R) ⟨g.toLinearMap ∘ₗ ExteriorAlgebra.ι R, ⋯⟩ = g
-- Mathlib.GroupTheory.OreLocalization.OreSet
AddOreLocalization.addOreSetBot : {R : Type u_1} → [inst : AddMonoid R] → AddOreLocalization.AddOreSet ⊥
-- Init.Data.Nat.Gcd
Nat.eq_zero_of_gcd_eq_zero_right : ∀ {m n : ℕ}, m.gcd n = 0 → n = 0
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
CauchySeq.mul : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} [inst_3 : Preorder ι]
  {u v : ι → α}, CauchySeq u → CauchySeq v → CauchySeq (u * v)
-- Mathlib.Data.Multiset.Defs
Multiset.quot_mk_to_coe'' : ∀ {α : Type u_1} (l : List α), Quot.mk (⇑(List.isSetoid α)) l = ↑l
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.map₁_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C}
  {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G)
  (p : CategoryTheory.OverPresheafAux.YonedaCollection F X),
  (CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p).fst = p.fst
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A} (f : ℱ ⟶ ℱ'.obj)
  {𝒢' : CategoryTheory.Sheaf K A} (g : ℱ' ⟶ 𝒢'),
  CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom.symm (CategoryTheory.CategoryStruct.comp f g.hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom.symm f)
      (G.op.whiskerLeft g.hom)
-- Mathlib.Topology.Constructible
Topology.IsConstructible.sdiff : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X},
  Topology.IsConstructible s → Topology.IsConstructible t → Topology.IsConstructible (s \ t)
-- Mathlib.Algebra.Quandle
ShelfHom.mk.sizeOf_spec : ∀ {S₁ : Type u_1} {S₂ : Type u_2} [inst : Shelf S₁] [inst_1 : Shelf S₂] [inst_2 : SizeOf S₁] [inst_3 : SizeOf S₂]
  (toFun : S₁ → S₂) (map_act' : ∀ {x y : S₁}, toFun (Shelf.act x y) = Shelf.act (toFun x) (toFun y)),
  sizeOf { toFun := toFun, map_act' := map_act' } = 1
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_X : ∀ {R : Type u} [inst : Semiring R], Polynomial.X.toFinsupp = AddMonoidAlgebra.single 1 1
-- Mathlib.Topology.MetricSpace.HolderNorm
eHolderNorm_of_isEmpty : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  [hX : IsEmpty X], eHolderNorm r f = 0
-- Mathlib.Order.Bounds.Basic
isGLB_upperBounds : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsGLB (upperBounds s) a ↔ IsLUB s a
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
NormedAlgebra.toMulAlgebraNorm_apply : ∀ (K : Type u_1) (L : Type u_2) [inst : NormedField K] [inst_1 : NormedField L] [inst_2 : NormedAlgebra K L] (x : L),
  (NormedAlgebra.toMulAlgebraNorm K L) x = ‖x‖
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  -/
EuclideanSpace : Type u_7 → Type u_8 → Type (max u_7 u_8)
-- Init.Internal.Order.MonadTail
ReaderT.bind.eq_1 : ∀ {ρ : Type u} {m : Type u → Type v} [inst : Monad m] {α β : Type u} (x : ReaderT ρ m α) (f : α → ReaderT ρ m β)
  (r : ρ),
  x.bind f r = do
    let a ← x r
    f a r
-- Mathlib.CategoryTheory.Comma.Basic
/-- Morphism on left objects  -/
CategoryTheory.CommaMorphism.left : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {X Y : CategoryTheory.Comma L R} → CategoryTheory.CommaMorphism X Y → (X.left ⟶ Y.left)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.map_fst_toList_eq_keys : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], List.map Sigma.fst (↑m).toList = (↑m).keys
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.mk_eq_mk_iff_sub_mem : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (x y : ↥P.ker), Algebra.Extension.Cotangent.mk x = Algebra.Extension.Cotangent.mk y ↔ ↑x - ↑y ∈ P.ker ^ 2
-- Mathlib.Data.Finset.Pi
/-- **Alias** of `Set.piCongrLeft_comp_domRestrict`. -/
Set.piCongrLeft_comp_restrict : ∀ {ι : Type u_2} {π : ι → Type u_3} {s : Finset ι},
  ⇑(Equiv.piCongrLeft (fun i => π ↑i) s.equivToSet.symm) ∘ (↑s).domRestrict = s.restrict
-- Mathlib.Algebra.Category.Ring.Colimits
Quot.map₂.congr_simp : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  (f f_1 : α → β → γ) (e_f : f = f_1) (hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → t (f a b₁) (f a b₂))
  (hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → t (f a₁ b) (f a₂ b)) (q₁ q₁_1 : Quot r),
  q₁ = q₁_1 → ∀ (q₂ q₂_1 : Quot s), q₂ = q₂_1 → Quot.map₂ f hr hs q₁ q₂ = Quot.map₂ f_1 ⋯ ⋯ q₁_1 q₂_1
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mk_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (p : Submodule R E)
  (f : ↥p →ₛₗ[σ] F) (x : ↥p), ↑{ domain := p, toFun := f } x = f x
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.eq_zero_or_isProbabilityMeasure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsZeroOrProbabilityMeasure μ],
  μ = 0 ∨ MeasureTheory.IsProbabilityMeasure μ
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingSeminorm.mk.inj : ∀ {R : Type u_2} {inst : NonAssocRing R} {toAddGroupSeminorm : AddGroupSeminorm R}
  {map_one' : toAddGroupSeminorm.toFun 1 = 1}
  {map_mul' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y}
  {toAddGroupSeminorm_1 : AddGroupSeminorm R} {map_one'_1 : toAddGroupSeminorm_1.toFun 1 = 1}
  {map_mul'_1 :
    ∀ (x y : R), toAddGroupSeminorm_1.toFun (x * y) = toAddGroupSeminorm_1.toFun x * toAddGroupSeminorm_1.toFun y},
  { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' } =
      { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_1 } →
    toAddGroupSeminorm = toAddGroupSeminorm_1
-- Mathlib.Data.Finset.Image
Finset.mem_image_const : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Finset α} {b c : β},
  c ∈ Finset.image (Function.const α b) s ↔ s.Nonempty ∧ b = c
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_nonneg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : Quaternion R},
  0 ≤ Quaternion.normSq a
-- Mathlib.Order.Monotone.Basic
Nat.exists_strictMono_subsequence : ∀ {P : ℕ → Prop}, (∀ (N : ℕ), ∃ n > N, P n) → ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.hom_ext_iff : ∀ {R S : CommSemiRingCat} {f g : R ⟶ S}, f = g ↔ CommSemiRingCat.Hom.hom f = CommSemiRingCat.Hom.hom g
-- Mathlib.Order.BooleanSubalgebra
/-- The inclusion homomorphism from a Boolean subalgebra `L` to a bigger Boolean subalgebra `M`.  -/
BooleanSubalgebra.inclusion : {α : Type u_2} → [inst : BooleanAlgebra α] → {L M : BooleanSubalgebra α} → L ≤ M → BoundedLatticeHom ↥L ↥M