mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
/-- The set of all maximal common tangent spaces to the spheres `s₁` and `s₂`.  -/
EuclideanGeometry.Sphere.commonTangents : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] →
            EuclideanGeometry.Sphere P → EuclideanGeometry.Sphere P → Set (AffineSubspace ℝ P)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ \ t₂).getKey? k = none
-- Mathlib.RingTheory.Flat.Basic
LinearMap.rTensor_injective_iff_subtype : ∀ {R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} {Q : Type u_3} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R P] [inst_7 : AddCommMonoid Q] [inst_8 : Module R Q] {f : N →ₗ[R] P},
  Function.Injective ⇑f →
    ∀ (e : P ≃ₗ[R] Q),
      Function.Injective ⇑(LinearMap.rTensor M f) ↔ Function.Injective ⇑(LinearMap.rTensor M (↑e ∘ₗ f).range.subtype)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_iInf_normal : ∀ {G : Type u_1} [inst : Group G] {ι : Sort u_6} {a : ι → Subgroup G}, (∀ (i : ι), (a i).Normal) → (iInf a).Normal
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.opowAux2.match_3.eq_4 : ∀ (motive : ONote × ℕ → Sort u_1) (a0 : ONote) (a : ℕ+) (a_1 : ONote) (m : ℕ) (h_1 : Unit → motive (ONote.zero, 0))
  (h_2 : Unit → motive (ONote.zero, 1)) (h_3 : (m : ℕ) → motive (ONote.zero, m.succ))
  (h_4 : (a a0 : ONote) → (a_2 : ℕ+) → (a_3 : ONote) → a = a0.oadd a_2 a_3 → (m : ℕ) → motive (a0.oadd a_2 a_3, m)),
  (match (a0.oadd a a_1, m) with
    | (ONote.zero, 0) => h_1 ()
    | (ONote.zero, 1) => h_2 ()
    | (ONote.zero, m.succ) => h_3 m
    | (a@h:(a0.oadd a_2 a_3), m) => h_4 a a0 a_2 a_3 h m) =
    h_4 (a0.oadd a a_1) a0 a a_1 ⋯ m
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Sheaf.isLocallySurjective_iff_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F G : CategoryTheory.Sheaf J (Type w)} (φ : F ⟶ G) [CategoryTheory.HasSheafify J (Type w)],
  CategoryTheory.Sheaf.IsLocallySurjective φ ↔ CategoryTheory.Epi φ
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- The variation can be expressed using strictly monotone functions. This formulation is
often less convenient than the one with monotone functions as it involves dependent types, but
it is sometimes handy.  -/
eVariationOn.eVariationOn_eq_strictMonoOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α),
  eVariationOn f s = ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constMaxEntryD_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {fallback : α × β},
          Std.DTreeMap.Internal.Impl.Const.maxEntryD t₁ fallback =
            Std.DTreeMap.Internal.Impl.Const.maxEntryD t₂ fallback
-- Mathlib.LinearAlgebra.Matrix.WithConv
instSemiringWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [Semiring α] → Semiring (WithConv (Matrix m n α))
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_union_closure_left_eq : ∀ {α : Type u_1} (M : Matroid α) (X Y : Set α), M.eRk (M.closure X ∪ Y) = M.eRk (X ∪ Y)
-- Mathlib.Topology.Inseparable
/-- **Alias** of the forward direction of `specializes_iff_mem_closure`. -/
Specializes.mem_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y → y ∈ closure {x}
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.mem_comap : ∀ {R : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] [inst_6 : AddCommMonoid F]
  [inst_7 : TopologicalSpace F] [inst_8 : Module R F] {x : E} {C : ProperCone R F} {f : E →L[R] F},
  x ∈ ProperCone.comap f C ↔ f x ∈ C
-- Mathlib.Probability.Density
ProbabilityTheory.IndepFun.pdf_mul_eq_mlconvolution_pdf' : ∀ {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [inst : Group G]
  {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant]
  {X Y : Ω → G} [MeasureTheory.SigmaFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ],
  MeasureTheory.SigmaFinite (MeasureTheory.Measure.map X ℙ) →
    MeasureTheory.SigmaFinite (MeasureTheory.Measure.map Y ℙ) →
      ProbabilityTheory.IndepFun X Y ℙ →
        MeasureTheory.pdf (X * Y) ℙ μ =ᵐ[μ]
          MeasureTheory.mlconvolution (MeasureTheory.pdf X ℙ μ) (MeasureTheory.pdf Y ℙ μ) μ
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.quoteArray.go.eq_def : ∀ {α : Type} [inst : Lean.Quote α] (xs : Array α) (i : ℕ) (args : Array Lean.Term),
  Lean.quoteArray.go✝ xs i args =
    if h : i < xs.size then Lean.quoteArray.go✝ xs (i + 1) (args.push (Lean.quote `term xs[i]))
    else Lean.Syntax.mkCApp (Lean.Name.mkStr2 "Array" (String.Internal.append "mkArray" (toString xs.size))) args
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.Aesop.rule_expr.quot : Lean.ParserDescr
-- Init.Data.String.Lemmas.Iterate
String.Slice.forIn_eq_forIn_toList : ∀ {β : Type u} {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {s : String.Slice} {b : β}
  {f : Char → β → m (ForInStep β)}, forIn s b f = forIn s.copy.toList b f
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.coe_incl : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L),
  ⇑L'.incl = Subtype.val
-- Mathlib.Algebra.Module.LinearMap.DivisionRing
LinearMap.range_smulRight_apply : ∀ {R : Type u_1} {M : Type u_2} {M₁ : Type u_3} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₁]
  [inst_2 : DivisionSemiring R] [inst_3 : Module R M] [inst_4 : Module R M₁] {f : M →ₗ[R] R},
  f ≠ 0 → ∀ (x : M₁), (f.smulRight x).range = R ∙ x
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, k ∉ m₂ → (m₁ \ m₂).get! k = m₁.get! k
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_counitIso_inv_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (X : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C)),
  (CategoryTheory.WithTerminal.equivComma.counitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_eq_some_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.minKey? = some (t.minKeyD fallback)
-- Lean.Meta.Sym.SymM
_private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.SymExtension.mk : {σ : Type} → ℕ → IO σ → Lean.Meta.Sym.SymExtension σ
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- Characterization of differentiable functions into a vector bundle in terms
of any trivialization. Version at a point.  -/
Bundle.Trivialization.mdifferentiableAt_totalSpace_iff : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB)
  {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
  [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  [inst_16 : (x : B) → AddCommMonoid (E x)] [inst_17 : (x : B) → Module 𝕜 (E x)] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle 1 F E IB] (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e]
  (f : M → Bundle.TotalSpace F E) {x₀ : M},
  f x₀ ∈ e.source → (MDiffAt f x₀ ↔ (MDiffAt fun x => (f x).proj) x₀ ∧ (MDiffAt fun x => (↑e (f x)).2) x₀)
-- Mathlib.RingTheory.WittVector.TeichmullerSeries
WittVector.teichmuller_mul_pow_coeff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [inst : CommRing R] [CharP R p] (n : ℕ) (x : R),
  ((WittVector.teichmuller p) x * ↑p ^ n).coeff n = x ^ p ^ n
-- Std.Data.DHashMap.Basic
Std.DHashMap.instBEqOfLawfulBEq : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → [LawfulBEq α] → [(k : α) → BEq (β k)] → BEq (Std.DHashMap α β)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.mk'_surjective : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal], Function.Surjective ⇑(QuotientGroup.mk' N)
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
IsScalarTower.toAlgHom.congr_simp : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A],
  IsScalarTower.toAlgHom R S A = IsScalarTower.toAlgHom R S A
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.edgeSet_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w),
  (p.append q).edgeSet = p.edgeSet ∪ q.edgeSet
-- Mathlib.Analysis.Normed.Algebra.Spectrum
QuasispectrumRestricts.compactSpace : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Algebra R S] [inst_4 : Module R A] [inst_5 : Module S A] [IsScalarTower S A A] [SMulCommClass S A A]
  [IsScalarTower R S A] [inst_9 : TopologicalSpace R] [inst_10 : TopologicalSpace S] {a : A} (f : C(S, R)),
  QuasispectrumRestricts a ⇑f → ∀ [h_cpct : CompactSpace ↑(quasispectrum S a)], CompactSpace ↑(quasispectrum R a)
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.brecOn_3.go : {motive_1 : Lean.Elab.InfoTree → Sort u} →
  {motive_2 : Lean.PersistentArray Lean.Elab.InfoTree → Sort u} →
    {motive_3 : Lean.PersistentArrayNode Lean.Elab.InfoTree → Sort u} →
      {motive_4 : Array Lean.Elab.InfoTree → Sort u} →
        {motive_5 : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u} →
          {motive_6 : List Lean.Elab.InfoTree → Sort u} →
            {motive_7 : List (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u} →
              (t : Array Lean.Elab.InfoTree) →
                ((t : Lean.Elab.InfoTree) → t.below → motive_1 t) →
                  ((t : Lean.PersistentArray Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_1 t → motive_2 t) →
                    ((t : Lean.PersistentArrayNode Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_2 t → motive_3 t) →
                      ((t : Array Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_3 t → motive_4 t) →
                        ((t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                            Lean.Elab.InfoTree.below_4 t → motive_5 t) →
                          ((t : List Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_5 t → motive_6 t) →
                            ((t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                                Lean.Elab.InfoTree.below_6 t → motive_7 t) →
                              motive_4 t ×' Lean.Elab.InfoTree.below_3 t
-- Lean.Server.CodeActions.Attr
Lean.CodeAction.CommandCodeActions.mk.sizeOf_spec : ∀ (onAnyCmd : Array Lean.CodeAction.CommandCodeAction) (onCmd : Lean.NameMap (Array Lean.CodeAction.CommandCodeAction)),
  sizeOf { onAnyCmd := onAnyCmd, onCmd := onCmd } = 1 + sizeOf onAnyCmd + sizeOf onCmd
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_piEquivPiSubtypeProd : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] {m : (i : ι) → MeasurableSpace (α i)}
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (p : ι → Prop)
  [inst_2 : DecidablePred p],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piEquivPiSubtypeProd α p)) (MeasureTheory.Measure.pi μ)
    ((MeasureTheory.Measure.pi fun i => μ ↑i).prod (MeasureTheory.Measure.pi fun i => μ ↑i))
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.lpMeasSubgroupToLpTrim_add : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f g : ↥(MeasureTheory.lpMeasSubgroup F m p μ)),
  MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm (f + g) =
    MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f + MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm g
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.comp_add : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] (ρ : Representation A G V) (σ : Representation A G W)
  (τ : Representation A G U) (f₁ f₂ : σ.IntertwiningMap τ) (g : ρ.IntertwiningMap σ),
  (f₁ + f₂).comp g = f₁.comp g + f₂.comp g
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformly.congr_inseparable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι} {G : ι → α → β},
  TendstoLocallyUniformly F f p →
    (∀ᶠ (n : ι) in p, ∀ (x : α), Inseparable (F n x) (G n x)) → TendstoLocallyUniformly G f p
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_join_right : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.meet (Lean.Order.join P Q) R = Lean.Order.join (Lean.Order.meet P R) (Lean.Order.meet Q R)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.map₀RingHom_apply : ∀ {ι : 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 : Nonempty ι]
  [inst_5 : (i : ι) → NonAssocSemiring (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)]
  (r : (i : ι) → G i), (DirectLimit.map₀RingHom f) r = DirectLimit.map₀ f r
-- Mathlib.Computability.Ackermann
ack_le_ack : ∀ {m₁ m₂ n₁ n₂ : ℕ}, m₁ ≤ m₂ → n₁ ≤ n₂ → ack m₁ n₁ ≤ ack m₂ n₂
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
dvd_mul_sub_mul_mul_right_of_dvd : ∀ {R : Type u_1} [inst : CommRing R] {p a b c d x y : R},
  p ∣ a * x + b * y → p ∣ c * x + d * y → p ∣ (a * d - b * c) * y
-- Init.Data.Float.Float
/-- Bit-for-bit conversion to `UInt64`. Interprets a `Float` as a `UInt64`, ignoring the numeric value
and treating the `Float`'s bit pattern as a `UInt64`.

`Float`s and `UInt64`s have the same endianness on all supported platforms. IEEE 754 very precisely
specifies the bit layout of floats.

This function is distinct from `Float.toUInt64`, which attempts to preserve the numeric value rather
than reinterpreting the bit pattern.
 -/
Float.toBits : Float → UInt64
-- Mathlib.Topology.Category.LightProfinite.Basic
instEssentiallySmallLightDiagram : CategoryTheory.EssentiallySmall.{u, u, u + 1} LightDiagram
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.curry_zero : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : (a : α) → (b : β a) → Zero (γ a b)],
  Sigma.curry 0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsZero.of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Epi f], CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsZero Y
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- The Coxeter matrix of type Bₙ.

The corresponding Coxeter-Dynkin diagram is:
```
       4
    o --- o --- o ⬝ ⬝ ⬝ ⬝ o --- o
```
 -/
CoxeterMatrix.B : (n : ℕ) → CoxeterMatrix (Fin n)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.ExactFunctor.forget_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : C ⥤ₑ D), (CategoryTheory.ExactFunctor.forget C D).obj F = F.obj
-- Batteries.Data.Nat.Basic
/-- Right leg for `Nat.recDiag`  -/
Nat.recDiag.right : {motive : ℕ → ℕ → Sort u_1} → motive 0 0 → ((m : ℕ) → motive m 0 → motive (m + 1) 0) → (m : ℕ) → motive m 0
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.isPositive_id : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  (ContinuousLinearMap.id 𝕜 E).IsPositive
-- Mathlib.Algebra.Homology.LocalCohomology
/-- Lifting `idealPowersDiagram J` from a diagram valued in `ideals R` to a diagram
valued in `SelfLERadical J`.  -/
localCohomology.idealPowersToSelfLERadical : {R : Type u} → [inst : CommRing R] → (J : Ideal R) → CategoryTheory.Functor ℕᵒᵖ (localCohomology.SelfLERadical J)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.sub_comp : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {R₃ : Type u_3} [inst_2 : Ring R₃] {M : Type u_4}
  [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup M] {M₂ : Type u_5} [inst_5 : TopologicalSpace M₂]
  [inst_6 : AddCommGroup M₂] {M₃ : Type u_6} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommGroup M₃]
  [inst_9 : Module R M] [inst_10 : Module R₂ M₂] [inst_11 : Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃}
  {σ₁₃ : R →+* R₃} [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_13 : IsTopologicalAddGroup M₃]
  (g₁ g₂ : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂), (g₁ - g₂) ∘SL f = g₁ ∘SL f - g₂ ∘SL f
-- Mathlib.Algebra.Order.Pi
Pi.single_le_single : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (α i)]
  [inst_2 : (i : ι) → Preorder (α i)] {i : ι} {a b : α i}, Pi.single i a ≤ Pi.single i b ↔ a ≤ b
-- Mathlib.Order.Filter.CountableSeparatingOn
/-- We say that a type `α` has a *countable separating family of sets* satisfying a predicate
`p : Set α → Prop` on a set `t` if there exists a countable family of sets `S : Set (Set α)` such
that all sets `s ∈ S` satisfy `p` and any two distinct points `x y ∈ t`, `x ≠ y`, can be separated
by `s ∈ S`: there exists `s ∈ S` such that exactly one of `x` and `y` belongs to `s`.

E.g., if `α` is a `T₀` topological space with second countable topology, then it has a countable
separating family of open sets and a countable separating family of closed sets.
 -/
HasCountableSeparatingOn : (α : Type u_1) → (Set α → Prop) → Set α → Prop
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
Lean.Elab.Structural.instReprRecArgInfo.repr : Lean.Elab.Structural.RecArgInfo → ℕ → Std.Format
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.single_zero : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → Zero (M i)] [inst_1 : DecidableEq ι] (i : ι), Pi.single i 0 = 0
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_add : ∀ (x y : ℂ), Complex.sin (x + y) = Complex.sin x * Complex.cos y + Complex.cos x * Complex.sin y
-- Init.Grind.AC
Lean.Grind.AC.Expr.toSeq'_k_eq_toSeq' : ∀ (e : Lean.Grind.AC.Expr) (s : Lean.Grind.AC.Seq), e.toSeq'_k s = e.toSeq' s
-- Lean.Meta.Tactic.LibrarySearch
Lean.Meta.LibrarySearch.DeclMod.mp.sizeOf_spec : sizeOf Lean.Meta.LibrarySearch.DeclMod.mp = 1
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.two_le_card_support_cycleOf_iff : ∀ {α : Type u_2} {f : Equiv.Perm α} {x : α} [inst : DecidableEq α] [inst_1 : Fintype α],
  2 ≤ (f.cycleOf x).support.card ↔ f x ≠ x
-- Mathlib.Combinatorics.SetFamily.FourFunctions
_private.Mathlib.Combinatorics.SetFamily.FourFunctions.0.collapse.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {inst : DecidableEq α} [inst_1 : DecidableEq α] [inst_2 : CommSemiring β]
  (𝒜 𝒜_1 : Finset (Finset α)),
  𝒜 = 𝒜_1 →
    ∀ (a a_1 : α),
      a = a_1 →
        ∀ (f f_1 : Finset α → β),
          f = f_1 → ∀ (s s_1 : Finset α), s = s_1 → collapse✝ 𝒜 a f s = collapse✝ 𝒜_1 a_1 f_1 s_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], (t₁ ∪ t₂)[k]! = t₂.getD k t₁[k]!
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).getKey k h' = t₁.getKey k ⋯
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.instInhabitedDiagramProps.default : ProofWidgets.Penrose.DiagramProps
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.image_exp_Ioc : ∀ (a b : ℝ), Real.exp '' Set.Ioc a b = Set.Ioc (Real.exp a) (Real.exp b)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.trans_toLinearEquiv : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_5 : RingHomInvPair σ₂₃ σ₃₂] [inst_6 : RingHomInvPair σ₃₂ σ₂₃]
  {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_7 : RingHomInvPair σ₁₃ σ₃₁] [inst_8 : RingHomInvPair σ₃₁ σ₁₃]
  [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {M₁ : Type u_4}
  [inst_11 : TopologicalSpace M₁] [inst_12 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_13 : TopologicalSpace M₂]
  [inst_14 : AddCommMonoid M₂] {M₃ : Type u_6} [inst_15 : TopologicalSpace M₃] [inst_16 : AddCommMonoid M₃]
  [inst_17 : Module R₁ M₁] [inst_18 : Module R₂ M₂] [inst_19 : Module R₃ M₃] (e₁ : M₁ ≃SL[σ₁₂] M₂)
  (e₂ : M₂ ≃SL[σ₂₃] M₃), ↑(e₁.trans e₂) = (↑e₁).trans ↑e₂
-- Mathlib.Data.Sym.Basic
Sym.exists : ∀ {α : Type u_1} {n : ℕ} {p : Sym α n → Prop}, (∃ s, p s) ↔ ∃ s, ∃ (hs : s.card = n), p (Sym.mk s hs)
-- Mathlib.Data.Fintype.Quotient
_private.Mathlib.Data.Fintype.Quotient.0.Quotient.listChoice.match_3.eq_2 : ∀ {ι : Type u_1} {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)}
  (motive : (l : List ι) → ((i : ι) → i ∈ l → Quotient (S i)) → Sort u_3) (i : ι) (tail : List ι)
  (q : (i_1 : ι) → i_1 ∈ i :: tail → Quotient (S i_1)) (h_1 : (q : (i : ι) → i ∈ [] → Quotient (S i)) → motive [] q)
  (h_2 : (i : ι) → (tail : List ι) → (q : (i_1 : ι) → i_1 ∈ i :: tail → Quotient (S i_1)) → motive (i :: tail) q),
  (match i :: tail, q with
    | [], q => h_1 q
    | i :: tail, q => h_2 i tail q) =
    h_2 i tail q
-- Mathlib.Topology.Algebra.Module.Compact
Module.Finite.compactSpace : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M] [CompactSpace R]
  [Module.Finite R M], CompactSpace M
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.mem_coe : ∀ {α : Type u_1} [inst : MeasurableSpace α] (a : α) (s : Subtype MeasurableSet), a ∈ ↑s ↔ a ∈ s
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_le : ∀ {a b : UInt8}, a.toUInt16 ≤ b.toUInt16 ↔ a ≤ b
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding_inv_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  (X₁ X₂ : CategoryTheory.Arrow C),
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding X₁ X₂).inv.right = (β_ X₁.right X₂.right).inv