mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_eq_get_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {h : a ∈ t}, t.getKey a h = (t.getKey? a).get ⋯
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda₀_mapId_hom_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) (a : Bᵒᵖ) (X : Opposite.unop a ⟶ x),
  ((CategoryTheory.Bicategory.yoneda₀ x).mapId a).hom.toNatTrans.app X = (CategoryTheory.Bicategory.leftUnitor X).hom
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `AddCommMonoid.addTorsion.isAddTorsion`.

---

Torsion additive submonoids are torsion.  -/
AddCommMonoid.addTorsion.isTorsion : ∀ {G : Type u_1} [inst : AddCommMonoid G], IsAddTorsion ↥(AddCommMonoid.addTorsion G)
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.CallHierarchy.item : Lean.Lsp.Ipc.CallHierarchy → Lean.Lsp.CallHierarchyItem
-- Mathlib.Data.Num.Basic
Num.pos : PosNum → Num
-- Init.Core
/-- **Function extensionality.** If two functions return equal results for all possible arguments, then
they are equal.

It is called “extensionality” because it provides a way to prove two objects equal based on the
properties of the underlying mathematical functions, rather than based on the syntax used to denote
them. Function extensionality is a theorem that can be [proved using quotient
types](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=quotient-funext).
 -/
funext : ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_update_ne_zero : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ) {a : R},
  a ≠ 0 → (p.update n a).support = insert n p.support
-- Lean.Data.RArray
_private.Lean.Data.RArray.0.Lean.RArray.ofFn.go.congr_simp : ∀ {α : Type u_1} {n : ℕ} (f f_1 : Fin n → α),
  f = f_1 →
    ∀ (lb lb_1 : ℕ) (e_lb : lb = lb_1) (ub ub_1 : ℕ) (e_ub : ub = ub_1) (h1 : lb < ub) (h2 : ub ≤ n),
      Lean.RArray.ofFn.go✝ f lb ub h1 h2 = Lean.RArray.ofFn.go✝ f_1 lb_1 ub_1 ⋯ ⋯
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.one_le_iff_ne_zero : ∀ {o : Ordinal.{u_1}}, 1 ≤ o ↔ o ≠ 0
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.apply_mem_neighborSet : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {v w : V},
  w ∈ G.neighborSet v → f w ∈ G'.neighborSet (f v)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.subst.sizeOf_spec : ∀ (x : Int.Internal.Linear.Var) (c₁ : Lean.Meta.Grind.Arith.Cutsat.EqCnstr)
  (c₂ : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.subst x c₁ c₂) = 1 + sizeOf x + sizeOf c₁ + sizeOf c₂
-- Mathlib.Analysis.Convolution
/-- The convolution `f * g` is continuous if `f` is locally integrable and `g` is continuous and
compactly supported. Version where `g` depends on an additional parameter in an open subset `s` of
a parameter space `P` (and the compact support `k` is independent of the parameter in `s`),
given in terms of compositions with an additional continuous map.  -/
MeasureTheory.continuousOn_convolution_right_with_param_comp : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} [inst_3 : NontriviallyNormedField 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F)
  [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F] [inst_9 : AddGroup G]
  [inst_10 : TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [inst_13 : TopologicalSpace P] {s : Set P}
  {v : P → G},
  ContinuousOn v s →
    ∀ {g : P → G → E'} {k : Set G},
      IsCompact k →
        (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
          MeasureTheory.LocallyIntegrable f μ →
            ContinuousOn (↿g) (s ×ˢ Set.univ) → ContinuousOn (fun x => MeasureTheory.convolution f (g x) L μ (v x)) s
-- Mathlib.RingTheory.Nilpotent.Defs
instIsReducedForall : ∀ (ι : Type u_4) (R : ι → Type u_3) [inst : (i : ι) → Zero (R i)] [inst_1 : (i : ι) → Pow (R i) ℕ]
  [∀ (i : ι), IsReduced (R i)], IsReduced ((i : ι) → R i)
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.instUnique : {R : Type u_1} →
  {A : Type u_6} →
    {B : Type u_7} →
      {ι : Type u_10} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : DecidableEq ι] →
                    [inst_6 : AddMonoid ι] →
                      {𝒜 : ι → Submodule R A} →
                        {ℬ : ι → Submodule R B} →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] → [Subsingleton B] → Unique (𝒜 →ₐᵍ[R] ℬ)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.mkIso_hom_hom_toLinearMap : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (e : ρ.Equiv σ), (Rep.Hom.hom (Rep.mkIso e).hom).toLinearMap = (↑e).toLinearMap
-- Mathlib.Topology.Order.MonotoneConvergence
iInf_eq_of_tendsto : ∀ {β : Type u_2} {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompleteLinearOrder α] [OrderTopology α]
  [Nonempty β] [inst_4 : SemilatticeSup β] {f : β → α} {a : α},
  Antitone f → Filter.Tendsto f Filter.atTop (nhds a) → iInf f = a
-- Mathlib.Algebra.Order.Module.Defs
/-- A constructor for `PosSMulMono` requiring you to prove `b₁ ≤ b₂ → a • b₁ ≤ a • b₂` only when
`0 < a`  -/
PosSMulMono.of_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] [inst_3 : PartialOrder α]
  [inst_4 : Preorder β], (∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂) → PosSMulMono α β
-- Init.Data.Int.Order
Int.sub_le_of_sub_le : ∀ {a b c : ℤ}, a - b ≤ c → a - c ≤ b
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.coe_prodEqualWeights : ∀ {ι : Type} {s : Finset ι} {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne]
  (f : ι → SlashInvariantForm Γ k), ⇑(SlashInvariantForm.prodEqualWeights f) = ∏ i ∈ s, ⇑(f i)
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.mk.sizeOf_spec : ∀ (toAddGrp : AddGrpCat) [isFinite : Finite ↑toAddGrp],
  sizeOf { toAddGrp := toAddGrp, isFinite := isFinite } = 1 + sizeOf toAddGrp + sizeOf isFinite
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- `LinearMap.BilinMap.toQuadraticMap` as an additive homomorphism  -/
LinearMap.BilinMap.toQuadraticMapAddMonoidHom : (R : Type u_3) →
  (M : Type u_4) →
    {N : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → LinearMap.BilinMap R M N →+ QuadraticMap R M N
-- Mathlib.Topology.Sequences
/-- Every Fréchet-Urysohn space is a sequential space.  -/
FrechetUrysohnSpace.to_sequentialSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [FrechetUrysohnSpace X], SequentialSpace X
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map.eq_1 : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (H : Subgroup G),
  Subgroup.map f H = { carrier := ⇑f '' ↑H, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- `WithLp.equiv` as a continuous linear equivalence.  -/
WithLp.prodContinuousLinearEquiv : (p : ENNReal) →
  (𝕜 : Type u_1) →
    (α : Type u_2) →
      (β : Type u_3) →
        [inst : TopologicalSpace α] →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : Semiring 𝕜] →
              [inst_3 : AddCommGroup α] →
                [inst_4 : AddCommGroup β] → [inst_5 : Module 𝕜 α] → [inst_6 : Module 𝕜 β] → WithLp p (α × β) ≃L[𝕜] α × β
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.instFunLike : {L : FirstOrder.Language} →
  {M : Type w} → {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → FunLike (L.Hom M N) M N
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
/-- The tensor product of `ι →₀ M` and `κ →₀ N` is linearly equivalent to `(ι × κ) →₀ (M ⊗ N)`.  -/
finsuppTensorFinsupp : (R : Type u_1) →
  (S : Type u_2) →
    (M : Type u_3) →
      (N : Type u_4) →
        (ι : Type u_5) →
          (κ : Type u_6) →
            [inst : CommSemiring R] →
              [inst_1 : AddCommMonoid M] →
                [inst_2 : Module R M] →
                  [inst_3 : AddCommMonoid N] →
                    [inst_4 : Module R N] →
                      [inst_5 : Semiring S] →
                        [inst_6 : Algebra R S] →
                          [inst_7 : Module S M] →
                            [inst_8 : IsScalarTower R S M] →
                              TensorProduct R (ι →₀ M) (κ →₀ N) ≃ₗ[S] ι × κ →₀ TensorProduct R M N
-- Init.Data.Option.Attach
Option.toArray_pfilter : ∀ {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool},
  (o.pfilter p).toArray = (Array.filter (fun x => p ↑x ⋯) o.toArray.attach).unattach
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.of_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughProjectives C] (Z : C),
  CategoryTheory.ProjectiveResolution.of Z =
    { complex := CategoryTheory.ProjectiveResolution.ofComplex Z, projective := ⋯, hasHomology := ⋯,
      π := ((CategoryTheory.ProjectiveResolution.ofComplex Z).toSingle₀Equiv Z).symm ⟨CategoryTheory.Projective.π Z, ⋯⟩,
      quasiIso := ⋯ }
-- Mathlib.Topology.Algebra.InfiniteSum.Order
/-- Positivity extension for infinite sums.

This extension only proves non-negativity, strict positivity is more delicate for infinite sums and
requires more assumptions.  -/
Mathlib.Meta.Positivity.evalTsum : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.Precomp.obj.match_1.eq_1 : ∀ {n : ℕ} (motive : Fin (n + 1 + 1) → Sort u_1) (isLt : 0 < n + 1 + 1) (h_1 : (isLt : 0 < n + 1 + 1) → motive ⟨0, isLt⟩)
  (h_2 : (i : ℕ) → (hi : i + 1 < n + 1 + 1) → motive ⟨i.succ, hi⟩),
  (match ⟨0, isLt⟩ with
    | ⟨0, isLt⟩ => h_1 isLt
    | ⟨i.succ, hi⟩ => h_2 i hi) =
    h_1 isLt
-- Mathlib.Analysis.Convex.BetweenList
List.Sbtw.pairwise_ne : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {l : List P}, List.Sbtw R l → List.Pairwise (fun x1 x2 => x1 ≠ x2) l
-- Mathlib.Data.List.Defs
List.Forall.eq_3 : ∀ {α : Type u_1} (p : α → Prop) (x_1 : α) (l : List α),
  (l = [] → False) → List.Forall p (x_1 :: l) = (p x_1 ∧ List.Forall p l)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.incidenceSet_subset_incidenceSet : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V), G'.incidenceSet v ⊆ G.incidenceSet v
-- Mathlib.RingTheory.KrullDimension.NonZeroDivisors
ringKrullDim_quotient : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), ringKrullDim (R ⧸ I) = Order.krullDim ↑(PrimeSpectrum.zeroLocus ↑I)
-- Mathlib.Data.List.Perm.Basic
List.perm_comp_forall₂ : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {l u : List α} {v : List β},
  l.Perm u → List.Forall₂ r u v → Relation.Comp (List.Forall₂ r) List.Perm l v
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {Z : AlgebraicGeometry.Scheme}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp U.toSpecΓ (CategoryTheory.CategoryStruct.comp hU.fromSpec h) =
    CategoryTheory.CategoryStruct.comp U.ι h
-- Mathlib.Algebra.Ring.Action.Subobjects
/-- A stronger version of `Submonoid.distribMulAction`.  -/
Submonoid.mulSemiringAction : {M : Type u_1} →
  {R : Type u_3} →
    [inst : Monoid M] → [inst_1 : Semiring R] → [MulSemiringAction M R] → (H : Submonoid M) → MulSemiringAction (↥H) R
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffOn.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieAddGroup I n G] {f : M → G} {s : Set M}, ContMDiffOn I' I n f s → ContMDiffOn I' I n (fun x => -f x) s
-- Mathlib.Order.Sublocale
Sublocale.coe_sInf : ∀ {X : Type u_1} [inst : Order.Frame X] {S : Sublocale X} (s : Set ↥S), ↑(sInf s) = sInf (Subtype.val '' s)
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.submonoidPresheafOfStalk_obj : ∀ {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (S : (x : ↑X) → Submonoid ↑(F.stalk x))
  (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (F.submonoidPresheafOfStalk S).obj U =
    ⨅ x, Submonoid.comap (CommRingCat.Hom.hom (F.germ (Opposite.unop U) ↑x ⋯)) (S ↑x)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.toPartOrd_obj : ∀ (n : SimplexCategory),
  SimplexCategory.toPartOrd.obj n = { carrier := ULift.{u, 0} (Fin (n.len + 1)), str := ULift.instPartialOrder }
-- Mathlib.Analysis.MeanInequalities
/-- **Hölder inequality**: the scalar product of two functions is bounded by the product of their
`L^p` and `L^q` norms when `p` and `q` are conjugate exponents. Version for sums over finite sets,
with real-valued nonnegative functions.  -/
Real.inner_le_Lp_mul_Lq_of_nonneg : ∀ {ι : Type u} (s : Finset ι) {f g : ι → ℝ} {p q : ℝ},
  p.HolderConjugate q →
    (∀ i ∈ s, 0 ≤ f i) →
      (∀ i ∈ s, 0 ≤ g i) → ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.map_π_app : ∀ {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] {J : CategoryTheory.Limits.MulticospanShape}
  {d : CategoryTheory.Limits.MulticospanIndex J C} (c : CategoryTheory.Limits.Multifork d)
  (F : CategoryTheory.Functor C D) (x : CategoryTheory.Limits.WalkingMulticospan J),
  (c.map F).π.app x =
    match x with
    | CategoryTheory.Limits.WalkingMulticospan.left a => F.map (c.ι a)
    | CategoryTheory.Limits.WalkingMulticospan.right b =>
      CategoryTheory.CategoryStruct.comp (F.map (c.ι (J.fst b))) (F.map (d.fst b))
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `edist (f n) (f (n+1))` is bounded by `C * r^n`, then the distance from
`f 0` to the limit of `f` is bounded above by `C / (1 - r)`.  -/
edist_le_of_edist_le_geometric_of_tendsto₀ : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (r C : ENNReal) {f : ℕ → α},
  (∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n) →
    ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → edist (f 0) a ≤ C / (1 - r)
-- Init.PropLemmas
Decidable.not_iff_not : ∀ {a b : Prop} [Decidable a] [Decidable b], (¬a ↔ ¬b) ↔ (a ↔ b)
-- Batteries.Data.AssocList
/-- `O(n)`. Convert an `AssocList α β` into the equivalent `List (α × β)`.
This is used to give specifications for all the `AssocList` functions
in terms of corresponding list functions.
 -/
Batteries.AssocList.toList : {α : Type u_1} → {β : Type u_2} → Batteries.AssocList α β → List (α × β)
-- Lean.Meta.MethodSpecs
/-- Generate method specification theorems for the methods of the given type class instance.

This expects all (non-proof) methods of the instance to be defined via separate helper functions,
which must take the same arguments as the instance itself, in the same order.

If it is applied to an instance
```
instance instClsT : Cls T where op := opImpl
```
it produces a theorem `instClsT.op_spec` based on `opImpl.eq_def`, but phrased in terms of the
overloaded `Cls.op` operation, and similarly `instClsT.op_spec_<n>` based on the equational theorems
`opImpl.eq_<n>`.
 -/
_private.Lean.Meta.MethodSpecs.0.Lean.methodSpecsAttr : Lean.ParametricAttribute Lean.MethodSpecsAttrData
-- Mathlib.RingTheory.Polynomial.Basic
MvPolynomial.map_mvPolynomial_eq_eval₂ : ∀ {R : Type u} {σ : Type v} [inst : CommRing R] {S : Type u_2} [inst_1 : CommSemiring S] [Finite σ]
  (ϕ : MvPolynomial σ R →+* S) (p : MvPolynomial σ R),
  ϕ p = MvPolynomial.eval₂ (ϕ.comp MvPolynomial.C) (fun s => ϕ (MvPolynomial.X s)) p
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiff_finsetSum'`. -/
contMDiff_finset_sum' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiff I' I n (f i)) → ContMDiff I' I n (∑ i ∈ t, f i)
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (S.toBiprod F n) (S.fromBiprod F n) = 0
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getInt64Value? : Lean.Expr → OptionT Id Int64
-- Mathlib.Geometry.Euclidean.MongePoint
Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter.eq_2 : ∀ {n : ℕ} (i₁ i₂ : Fin (n + 3)),
  Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂
      Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex =
    -2 / ↑(n + 1)
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Balanced.ins : ∀ {α : Type u_1} {c₀ : RBTree.RBColor} {n₀ : ℕ} {c : RBTree.RBColor} {n : ℕ} {t : RBTree.RBNode α}
  {path : RBTree.RBNode.Path α},
  RBTree.RBNode.Path.Balanced c₀ n₀ path c n →
    RBTree.RBNode.RedRed (c = RBTree.RBColor.red) t n → ∃ n, (path.ins t).Balanced RBTree.RBColor.black n
-- Std.Time.DateTime.PlainDateTime
/-- Converts a `PlainTime` to a `WallTime`.
 -/
Std.Time.PlainTime.toWallTime : Std.Time.PlainTime → Std.Time.WallTime
-- Lean.Meta.CoeAttr
Lean.Meta.CoeFnInfo.mk.inj : ∀ {numArgs coercee : ℕ} {type : Lean.Meta.CoeFnType} {numArgs_1 coercee_1 : ℕ} {type_1 : Lean.Meta.CoeFnType},
  { numArgs := numArgs, coercee := coercee, type := type } =
      { numArgs := numArgs_1, coercee := coercee_1, type := type_1 } →
    numArgs = numArgs_1 ∧ coercee = coercee_1 ∧ type = type_1
-- Mathlib.Algebra.Star.SelfAdjoint
/-- The self-adjoint elements of a star additive group, as an additive subgroup.  -/
selfAdjoint : (R : Type u_1) → [inst : AddGroup R] → [StarAddMonoid R] → AddSubgroup R
-- Lean.Compiler.IR.Format
Lean.IR.formatFnBodyHead : Lean.IR.FnBody → Std.Format
-- Mathlib.Order.LatticeIntervals
Set.Ici.coe_sup : ∀ {α : Type u_1} [inst : SemilatticeSup α] {a : α} {x y : ↑(Set.Ici a)}, ↑(x ⊔ y) = ↑x ⊔ ↑y
-- Mathlib.Combinatorics.Graph.Basic
Graph.mk.inj : ∀ {α : Type u_3} {β : Type u_4} {vertexSet : Set α} {IsLink : β → α → α → Prop} {edgeSet : Set β}
  {isLink_symm : ∀ ⦃e : β⦄, e ∈ edgeSet → Std.Symm (IsLink e)}
  {eq_or_eq_of_isLink_of_isLink : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w}
  {edge_mem_iff_exists_isLink :
    autoParam (∀ (e : β), e ∈ edgeSet ↔ ∃ x y, IsLink e x y) Graph.edge_mem_iff_exists_isLink._autoParam}
  {left_mem_of_isLink :
    autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink e x y → x ∈ vertexSet) Graph.left_mem_of_isLink._autoParam}
  {vertexSet_1 : Set α} {IsLink_1 : β → α → α → Prop} {edgeSet_1 : Set β}
  {isLink_symm_1 : ∀ ⦃e : β⦄, e ∈ edgeSet_1 → Std.Symm (IsLink_1 e)}
  {eq_or_eq_of_isLink_of_isLink_1 : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink_1 e x y → IsLink_1 e v w → x = v ∨ x = w}
  {edge_mem_iff_exists_isLink_1 :
    autoParam (∀ (e : β), e ∈ edgeSet_1 ↔ ∃ x y, IsLink_1 e x y) Graph.edge_mem_iff_exists_isLink._autoParam}
  {left_mem_of_isLink_1 :
    autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink_1 e x y → x ∈ vertexSet_1) Graph.left_mem_of_isLink._autoParam},
  { vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
        eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink,
        edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink, left_mem_of_isLink := left_mem_of_isLink } =
      { vertexSet := vertexSet_1, IsLink := IsLink_1, edgeSet := edgeSet_1, isLink_symm := isLink_symm_1,
        eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink_1,
        edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink_1, left_mem_of_isLink := left_mem_of_isLink_1 } →
    vertexSet = vertexSet_1 ∧ IsLink = IsLink_1 ∧ edgeSet = edgeSet_1
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] {x : M} (hx : x ∉ (↑f).domain)
  (c : FiniteArchimedeanClass M),
  toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (f.eval x))) ∈ (f.extendFun hx).toFun.range
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Traversal.0.SimpleGraph.Walk.getVert.match_1.splitter : {V : Type u_1} →
  {G : SimpleGraph V} →
    {u : V} →
      (motive : (v : V) → G.Walk u v → ℕ → Sort u_2) →
        (v : V) →
          (x : G.Walk u v) →
            (x_1 : ℕ) →
              ((x : ℕ) → motive u SimpleGraph.Walk.nil x) →
                ((v v_1 : V) → (h : G.Adj u v_1) → (p : G.Walk v_1 v) → motive v (SimpleGraph.Walk.cons h p) 0) →
                  ((v v_1 : V) →
                      (h : G.Adj u v_1) → (q : G.Walk v_1 v) → (n : ℕ) → motive v (SimpleGraph.Walk.cons h q) n.succ) →
                    motive v x x_1
-- Lean.Expr
/-- Returns `Classical.em p`  -/
Lean.mkEM : Lean.Expr → Lean.Expr
-- Mathlib.RingTheory.Complex
Algebra.norm_complex_apply : ∀ (z : ℂ), (Algebra.norm ℝ) z = Complex.normSq z
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_snd : ∀ {A : Type u_2} {E : Type u_3} {F : Type u_4} (x : WithCStarModule A (E × F)),
  ((WithCStarModule.equiv A (E × F)) x).2 = x.2
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.id_asNatTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {e : C ≌ D},
  CategoryTheory.Equivalence.asNatTrans (CategoryTheory.CategoryStruct.id e) =
    CategoryTheory.CategoryStruct.id e.functor
-- Mathlib.Order.Hom.CompleteLattice
OrderIsoClass.tosSupHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [OrderIsoClass F α β], sSupHomClass F α β
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.absolutelyContinuous_toFinite : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SFinite μ],
  μ.AbsolutelyContinuous μ.toFinite