mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.extendWith_some : ∀ {ι : Type u} {α : Option ι → Type v} [inst : (i : Option ι) → Zero (α i)] (f : Π₀ (i : ι), α (some i)) (a : α none)
  (i : ι), (DFinsupp.extendWith a f) (some i) = f i
-- Mathlib.Algebra.Group.Commute.Units
isAddUnit_add_self_iff : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M}, IsAddUnit (a + a) ↔ IsAddUnit a
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint16.sizeOf_spec : ∀ (val : UInt16), sizeOf (Lean.Compiler.LCNF.LitValue.uint16 val) = 1 + sizeOf val
-- Init.Grind.Ring.Field
Lean.Grind.Field.zero_eq_inv_iff : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a : α}, 0 = a⁻¹ ↔ 0 = a
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.zeckendorf.induct : ∀ (motive : ℕ → Prop),
  motive 0 → (∀ (n : ℕ), motive (n + 1 - Nat.fib (n + 1).greatestFib) → motive n.succ) → ∀ (a : ℕ), motive a
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f g : PseudoEpimorphism α β},
  (∀ (a : α), f a = g a) → f = g
-- Mathlib.Data.Sum.Order
/-- `WithBot α` is order-isomorphic to `PUnit ⊕ₗ α`, by sending `⊥` to `Unit` and `↑a` to
`a`.  -/
WithBot.orderIsoPUnitSumLex : {α : Type u_1} → [inst : LE α] → WithBot α ≃o PUnit.{u_4 + 1} ⊕ₗ α
-- Mathlib.LinearAlgebra.Projectivization.Basic
/-- The projectivization of the `K`-vector space `V`.
The notation `ℙ K V` is preferred.  -/
Projectivization : (K : Type u_1) → (V : Type u_2) → [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [Module K V] → Type u_2
-- Init.Data.Array.Lemmas
Array.mem_append_left : ∀ {α : Type u_1} {a : α} {xs : Array α} (ys : Array α), a ∈ xs → a ∈ xs ++ ys
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.isFiniteMeasure_restrict : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.IsFiniteMeasure (μ.restrict s) ↔ μ s ≠ ⊤
-- Mathlib.Algebra.Ring.Pi
/-- **Alias** of `NonUnitalRingHom.pi_apply`. -/
Pi.nonUnitalRingHom_apply : ∀ {I : Type u} {f : I → Type u_1} {γ : Type u_2} [inst : (i : I) → NonUnitalNonAssocSemiring (f i)]
  [inst_1 : NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) (x : γ) (b : I),
  (NonUnitalRingHom.pi g) x b = (g b) x
-- Mathlib.Logic.Function.Coequalizer
/-- The coequalizer of two functions `f g : α → β` is the pair (`μ`, `p : β → μ`) that
satisfies the following universal property: Every function `u : β → γ`
with `u ∘ f = u ∘ g` factors uniquely via `p`.  -/
Function.Coequalizer : {α : Type u_1} → {β : Type v} → (α → β) → (α → β) → Type v
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.inhabitedCoconeMorphism : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (A : CategoryTheory.Limits.Cocone F) → Inhabited (CategoryTheory.Limits.CoconeMorphism A A)
-- Mathlib.Data.Set.Pairwise.Basic
exists_lt_mem_inter_of_not_pairwise_disjoint : ∀ {α : Type u_1} {ι : Type u_4} [inst : LinearOrder ι] {f : ι → Set α},
  ¬Pairwise (Function.onFun Disjoint f) → ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_alter!_eq_isEmpty_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).isEmpty =
        ((Std.DTreeMap.Internal.Impl.erase! k t).isEmpty && (f (t.get? k)).isNone)
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.comap_le_comap_of_le_range : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {K L : Subgroup N},
  K ≤ f.range → (Subgroup.comap f K ≤ Subgroup.comap f L ↔ K ≤ L)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimitsOfSize_opposite_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Limits.HasLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ ↔
    CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v₁, u₁} C
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.continuous_abs : ∀ {A : Type u_2} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [ContinuousStar A] [inst_3 : NormedSpace ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [CompleteSpace A], Continuous CFC.abs
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.TZifV2.toTZifV1 : Std.Time.TimeZone.TZif.TZifV2 → Std.Time.TimeZone.TZif.TZifV1
-- Mathlib.Tactic.Linter.Style
_private.Mathlib.Tactic.Linter.Style.0.Mathlib.Linter.Style.longLine.isImport : String → Bool
-- Lean.Data.KVMap
Lean.DataValue.ofName : Lean.Name → Lean.DataValue
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem : ∀ {K : Type u} [inst : Field K] {G : Type u_1} [inst_1 : Group G] [inst_2 : MulSemiringAction G K] {g : G}
  {S : ValuationSubring K} {x : K}, x ∈ g • S ↔ g⁻¹ • x ∈ S
-- Init.Data.Array.Range
Array.fst_eq_of_mem_zipIdx : ∀ {α : Type u_1} {x : α × ℕ} {xs : Array α} {k : ℕ} (h : x ∈ xs.zipIdx k), x.1 = xs[x.2 - k]
-- Mathlib.RingTheory.RingHom.LocallyStandardSmooth
/-- A ring homomorphism is étale if and only if it is standard smooth of relative dimension `0`.  -/
RingHom.etale_iff_isStandardSmoothOfRelativeDimension_zero : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.Etale ↔ RingHom.IsStandardSmoothOfRelativeDimension 0 f
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearEquiv.congrRight₂_trans : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N₁ : Type u_9}
  {N₂ : Type u_10} {N₃ : Type u_11} [inst_3 : AddCommMonoid N₁] [inst_4 : AddCommMonoid N₂] [inst_5 : AddCommMonoid N₃]
  [inst_6 : Module R N₁] [inst_7 : Module R N₂] [inst_8 : Module R N₃] (e₁₂ : N₁ ≃ₗ[R] N₂) (e₂₃ : N₂ ≃ₗ[R] N₃),
  (e₁₂ ≪≫ₗ e₂₃).congrRight₂ = e₁₂.congrRight₂ ≪≫ₗ e₂₃.congrRight₂
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
/-- Pull back a homogeneous ideal along a graded ring homomorphism.
The underlying ideal is (definitionally) equal to `Ideal.comap`, whose underlying set is
definitionally equal to the preimage.  -/
HomogeneousIdeal.comap : {A : Type u_1} →
  {B : Type u_2} →
    {σ : Type u_4} →
      {τ : Type u_5} →
        {ι : Type u_7} →
          [inst : Semiring A] →
            [inst_1 : Semiring B] →
              [inst_2 : SetLike σ A] →
                [inst_3 : SetLike τ B] →
                  [inst_4 : AddSubmonoidClass σ A] →
                    [inst_5 : AddSubmonoidClass τ B] →
                      [inst_6 : DecidableEq ι] →
                        [inst_7 : AddMonoid ι] →
                          {𝒜 : ι → σ} →
                            {ℬ : ι → τ} →
                              [inst_8 : GradedRing 𝒜] →
                                [inst_9 : GradedRing ℬ] → (𝒜 →+*ᵍ ℬ) → HomogeneousIdeal ℬ → HomogeneousIdeal 𝒜
-- Mathlib.Data.List.Rotate
List.isRotatedDecidable : {α : Type u} → [DecidableEq α] → (l l' : List α) → Decidable (l ~r l')
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.ClientInfo : Type
-- Mathlib.GroupTheory.Finiteness
Group.fg_iff_subgroup_fg : ∀ {G : Type u_3} [inst : Group G] (H : Subgroup G), Group.FG ↥H ↔ H.FG
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : LawfulBEq α] {a : α} [inst_1 : Inhabited (β a)],
  ∅.get! a = default
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.apply_val_ker : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (x : ↥(↑f).ker),
  f ↑x = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_le_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t.contains k = true → (cmp t.minKey! k).isLE = true
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
/-- Conditional expectation of the indicator of a measurable set with finite measure,
as a function in L1.  -/
MeasureTheory.condExpIndL1Fin : {α : Type u_1} →
  {G : Type u_4} →
    [inst : NormedAddCommGroup G] →
      {m m0 : MeasurableSpace α} →
        {μ : MeasureTheory.Measure α} →
          {s : Set α} →
            [NormedSpace ℝ G] →
              (hm : m ≤ m0) →
                [MeasureTheory.SigmaFinite (μ.trim hm)] → MeasurableSet s → μ s ≠ ⊤ → G → ↥(MeasureTheory.Lp G 1 μ)
-- Mathlib.Data.Option.Basic
Option.some_injective : ∀ (α : Type u_5), Function.Injective some
-- Mathlib.Topology.EMetricSpace.Defs
MulOpposite.edist_op : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x y : α), edist (MulOpposite.op x) (MulOpposite.op y) = edist x y
-- Init.Data.Fin.Lemmas
Fin.zero_ne_one : ∀ {n : ℕ}, 0 ≠ 1
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
mdifferentiable_of_mem_atlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {e : OpenPartialHomeomorph M H} [IsManifold I 1 M],
  e ∈ atlas H M → OpenPartialHomeomorph.MDifferentiable I I e
-- Mathlib.Data.Set.Lattice
Set.symmDiff_iUnion_subset : ∀ {α : Type u_1} {ι : Sort u_5} {s : Set α} [Nonempty ι] {f : ι → Set α}, symmDiff s (⋃ n, f n) ⊆ ⋃ n, symmDiff s (f n)
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Update the `ForwardRuleMatches` of a goal so that they are suitable for a
child goal. `newMatches` are new forward rule matches obtained by updating the
old goal's `ForwardState` with new hypotheses from the new goal. `erasedHyps`
are the hypotheses from the old goal that no longer appear in the new goal.
`consumedForwardRuleMatches` contains forward rule matches that were applied as
rules to transform the old goal into the new goal.  -/
Aesop.ForwardRuleMatches.update : Array Aesop.ForwardRuleMatch →
  Std.HashSet Lean.FVarId → Array Aesop.ForwardRuleMatch → Aesop.ForwardRuleMatches → Aesop.ForwardRuleMatches
-- Mathlib.Topology.Order.Bornology
BddAbove.isBounded : ∀ {α : Type u_1} {s : Set α} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α],
  BddAbove s → BddBelow s → Bornology.IsBounded s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α}
  (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ Std.DTreeMap.Const.insertMany t l},
  Std.DTreeMap.Const.get (Std.DTreeMap.Const.insertMany t l) k h' = Std.DTreeMap.Const.get t k ⋯
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftEq_hom_app_right : ∀ {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] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (l l' : L₁ ⟶ L₂) (h : l = l') (X : CategoryTheory.Comma L₂ R),
  ((CategoryTheory.Comma.mapLeftEq R l l' h).hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Analysis.Normed.Group.Basic
norm_add_sub_norm_sub_le_two_mul_min : ∀ {E : Type u_8} [inst : SeminormedAddCommGroup E] (u v : E), ‖u + v‖ - ‖u - v‖ ≤ 2 * min ‖u‖ ‖v‖
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_zero_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R], (MvPowerSeries.coeff 0) 1 = 1
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.ι_mapBifunctorShift₂Iso_hom_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ℤ) [inst_8 : K₁.HasMapBifunctor K₂ F] (n₁ n₂ n : ℤ) (h : n₁ + n₂ = n)
  (m₂ m : ℤ) (hm₂ : m₂ = n₂ + y) (hm : m = n + y),
  CategoryTheory.CategoryStruct.comp
      (K₁.ιMapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F n₁ n₂ n h)
      ((K₁.mapBifunctorShift₂Iso K₂ F y).hom.f n) =
    (n₁ * y).negOnePow •
      CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X n₁)).map (K₂.shiftFunctorObjXIso y n₂ m₂ hm₂).hom)
        (CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F n₁ m₂ m ⋯)
          ((K₁.mapBifunctor K₂ F).shiftFunctorObjXIso y n m hm).inv)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableUniformlyOn.summable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {x : β} {s : Set β}
  [inst_1 : UniformSpace α], SummableUniformlyOn f s → x ∈ s → Summable fun x_1 => f x_1 x
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a function has bounded variation, then the variation on
small closed intervals to the left of this point tends to the contribution of the point, i.e.,
the distance between the left limit and the value at the point  -/
BoundedVariationOn.tendsto_eVariationOn_Icc_left : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α} {l : E},
  BoundedVariationOn f s →
    ∀ {x : α},
      Filter.Tendsto f (nhdsWithin x (s ∩ Set.Iio x)) (nhds l) →
        x ∈ s →
          Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Icc y x)) (nhdsWithin x (s ∩ Set.Iio x))
            (nhds (edist (f x) l))
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.BohrMollerup.f_nat_eq : ∀ {f : ℝ → ℝ} {n : ℕ},
  (∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y) → n ≠ 0 → f ↑n = f 1 + Real.log ↑(n - 1).factorial
-- Mathlib.Data.Num.Lemmas
Num.of_nat_inj : ∀ {m n : ℕ}, ↑m = ↑n ↔ m = n
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.Measure.variation_toSignedMeasure : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} [inst : MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.VectorMeasure.variation μ.toSignedMeasure = μ
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.nsmul_self : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M) (n : ℕ), AddCommute (n • a) a
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.coe_coe : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), ⇑↑e = ⇑e
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
/-- Category of `V`-enriched categories for a monoidal category `V`.  -/
CategoryTheory.EnrichedCat : (V : Type v) →
  [inst : CategoryTheory.Category.{w, v} V] → [CategoryTheory.MonoidalCategory V] → Type (max (u + 1) (max u v) w)
-- Mathlib.Data.Sign.Defs
_private.Mathlib.Data.Sign.Defs.0.SignType.fin3Equiv.match_1.splitter : (motive : SignType → Sort u_1) →
  (a : SignType) →
    (Unit → motive SignType.zero) → (Unit → motive SignType.pos) → (Unit → motive SignType.neg) → motive a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : β → β} {h : k ∈ m.modify k f}, (m.modify k f)[k] = f m[k]
-- Mathlib.RingTheory.Multiplicity
multiplicity_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α] (a : α), multiplicity a 0 = 1
-- Mathlib.Topology.IsClosedRestrict
IsClosed.isClosed_image_eval : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} [inst : (i : ι) → TopologicalSpace (α i)] (i : ι),
  IsCompact s → IsClosed s → IsClosed ((fun x => x i) '' s)
-- Mathlib.Data.DFinsupp.Defs
/-- Equivalence between all dependent finitely supported functions `f : Π₀ i, β i` and type
of pairs `⟨s : Finset ι, f : ∀ i : s, {x : β i // x ≠ 0}⟩`.  -/
DFinsupp.sigmaFinsetFunEquiv : {ι : Type u} →
  {β : ι → Type v} →
    [DecidableEq ι] →
      [inst : (i : ι) → Zero (β i)] →
        [(i : ι) → (x : β i) → Decidable (x ≠ 0)] → (Π₀ (i : ι), β i) ≃ (s : Finset ι) × ((i : ↥s) → { x // x ≠ 0 })
-- Mathlib.Combinatorics.SetFamily.Compression.Down
/-- Elements of `𝒜` that do not contain `a`.  -/
Finset.nonMemberSubfamily : {α : Type u_1} → [DecidableEq α] → α → Finset (Finset α) → Finset (Finset α)
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_eq_toBitVec : ∀ (a : ISize) (h : System.Platform.numBits = 32), a.toBitVec32 h = BitVec.cast h a.toBitVec
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The canonical isomorphism between `W ×[X] Uᵢ` and `Uᵢ ×[X] Y`. That is, the preimage of `Uᵢ` in
`W` along `p1` is indeed `Uᵢ ×[X] Y`.  -/
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso : {X Y Z : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    (f : X ⟶ Z) →
      (g : Y ⟶ Z) →
        [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] →
          (i : 𝒰.I₀) →
            CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i) ≅
              CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
-- Mathlib.Topology.Algebra.ProperConstSMul
/-- `(c +ᵥ ·)` is a proper map.  -/
ProperConstVAdd.isProperMap_vadd : ∀ {M : Type u_1} {X : Type u_2} {inst : VAdd M X} {inst_1 : TopologicalSpace X} [self : ProperConstVAdd M X] (c : M),
  IsProperMap fun x => c +ᵥ x
-- Mathlib.Algebra.Polynomial.RuleOfSigns
/-- The number of sign changes does not change if we multiply by any nonzero scalar.  -/
Polynomial.signVariations_C_mul : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {η : R} (P : Polynomial R),
  η ≠ 0 → (Polynomial.C η * P).signVariations = P.signVariations
-- Mathlib.Data.Sym.Basic
Sym.append.eq_1 : ∀ {α : Type u_1} {n n' : ℕ} (s : Sym α n) (s' : Sym α n'), s.append s' = ⟨↑s + ↑s', ⋯⟩
-- Aesop.Tree.Stats
Aesop.Goal.stats : Aesop.Goal → Aesop.TreeM Aesop.GoalStats
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.instIsZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget @AlgebraicGeometry.IsPreimmersion
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Cardinal.mk_vadd_set : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (a : G) (s : Set α),
  Cardinal.mk ↑(a +ᵥ s) = Cardinal.mk ↑s
-- Lean.Setup
/-- Whether the module is participating in the module system.  -/
Lean.ModuleHeader.isModule : Lean.ModuleHeader → Bool
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.smulCommClass_left : ∀ {M' : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MulOneClass M'] [inst_1 : SMul M' β] [inst_2 : SMul α β]
  [SMulCommClass M' α β] (S : Submonoid M'), SMulCommClass (↥S) α β
-- Mathlib.Topology.EMetricSpace.Defs
/-- EMetric space instance on the additive opposite of an emetric space.  -/
instEMetricSpaceAddOpposite : {α : Type u_2} → [EMetricSpace α] → EMetricSpace αᵃᵒᵖ
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation_recursion : ∀ (n m k : ℕ), hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k)
-- Mathlib.CategoryTheory.Comma.CardinalArrow
CategoryTheory.hasCardinalLT_of_hasCardinalLT_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}},
  HasCardinalLT (CategoryTheory.Arrow C) κ → HasCardinalLT C κ
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instNonUnitalSeminormedRing : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : NonUnitalSeminormedRing β] → NonUnitalSeminormedRing (ZeroAtInftyContinuousMap α β)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.trans_toContinuousAffineMap : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂]
  [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃] [inst_11 : AddTorsor V₃ P₃]
  [inst_12 : TopologicalSpace P₃] (e : P₁ ≃ᴬ[k] P₂) (e' : P₂ ≃ᴬ[k] P₃),
  (e.trans e').toContinuousAffineMap = e'.toContinuousAffineMap.comp e.toContinuousAffineMap
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.instHashableOrigin : Hashable Lean.Meta.Grind.Origin
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.besselPotential_neg_two_laplacian_eq : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] (f : TemperedDistribution E F),
  (TemperedDistribution.besselPotential E F (-2)) (Laplacian.laplacian f) =
    -(2 * Real.pi) ^ 2 • (TemperedDistribution.fourierMultiplierCLM F fun x => ↑(‖x‖ ^ 2 * (1 + ‖x‖ ^ 2) ^ (-1))) f
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- **Alias** of `CategoryTheory.Functor.PreservesMonomorphisms.ofRetract`. -/
CategoryTheory.Functor.preservesMonomorphisms.ofRetract : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (r : CategoryTheory.Retract G F) [F.PreservesMonomorphisms],
  G.PreservesMonomorphisms
-- Mathlib.Combinatorics.SetFamily.FourFunctions
collapse_nonneg : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {𝒜 : Finset (Finset α)} {a : α} {f : Finset α → β}, 0 ≤ f → 0 ≤ collapse✝ 𝒜 a f
-- Lean.Meta.Tactic.NormCast
/-- A simp set which pushes coercions to the leaves.  -/
Lean.Meta.NormCast.NormCastExtension.down : Lean.Meta.NormCast.NormCastExtension → Lean.Meta.SimpExtension
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.getLast?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.RepresentationTheory.Coinvariants
Representation.toCoinvariantsKer.congr_simp : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (S : Subgroup G) [inst_4 : S.Normal],
  ρ.toCoinvariantsKer S = ρ.toCoinvariantsKer S
-- Mathlib.LinearAlgebra.Matrix.Cartan
/-- A Cartan matrix is simply laced if its off-diagonal entries are all `0` or `-1`.  -/
Matrix.IsSimplyLaced : {ι : Type u_1} → Matrix ι ι ℤ → Prop
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.isScalarTower_self : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} [inst : Semiring S] [inst_1 : DistribSMul R S] [inst_2 : Add M]
  [IsScalarTower R S S], IsScalarTower R (AddMonoidAlgebra S M) (AddMonoidAlgebra S M)