mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Measure.ext_of_integral_prod_mul_prod_boundedContinuousFunction' : ∀ {ι : Type u_1} {κ : Type u_2} {X : ι → Type u_5} {Y : κ → Type u_6} {mX : (i : ι) → MeasurableSpace (X i)}
  [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)]
  {mY : (j : κ) → MeasurableSpace (Y j)} [inst_3 : (j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)]
  [∀ (j : κ), HasOuterApproxClosed (Y j)] [Finite ι] [Finite κ]
  {μ ν : MeasureTheory.Measure (((i : ι) → X i) × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (f : BoundedContinuousFunction ((i : ι) → X i) ℝ) (g : BoundedContinuousFunction ((j : κ) → Y j) ℝ),
      ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), f p.1 * g p.2 ∂μ =
        ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), f p.1 * g p.2 ∂ν) →
    μ = ν
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
Filter.EventuallyEq.mlieBracket_vectorField_eq : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {V W V₁ W₁ : (x : M) → TangentSpace I x},
  V₁ =ᶠ[nhds x] V → W₁ =ᶠ[nhds x] W → VectorField.mlieBracket I V₁ W₁ x = VectorField.mlieBracket I V W x
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- The minimal non-unital subalgebra that includes `s`.  -/
NonUnitalAlgebra.adjoin : (R : Type u) →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → Set A → NonUnitalSubalgebra R A
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_option : ∀ {α : Type u}, Cardinal.mk (Option α) = Cardinal.mk α + 1
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
MDifferentiableAt.differentiableWithinAt_writtenInExtChartAt : ∀ {𝕜 : 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' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M},
  MDiffAt f x → DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (Set.range ↑I) (↑(extChartAt I x) x)
-- Mathlib.Probability.Density
MeasureTheory.hasPDF_iff : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} {X : Ω → E}
  {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E},
  MeasureTheory.HasPDF X ℙ μ ↔
    AEMeasurable X ℙ ∧
      (MeasureTheory.Measure.map X ℙ).HaveLebesgueDecomposition μ ∧
        (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous μ
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.of_and_imp : ∀ {σs : List (Type u)} {P P' Q Q' : Std.Do.SPred σs}, (P ⊢ₛ P') → (Q ⊢ₛ P' → Q') → P ∧ Q ⊢ₛ P' ∧ Q'
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.hasForgetToMagmaCat.eq_1 : Semigrp.hasForgetToMagmaCat =
  {
    forget₂ :=
      { obj := fun R => MagmaCat.of ↑R, map := fun {X Y} f => MagmaCat.ofHom (Semigrp.Hom.hom f),
        map_id := Semigrp.hasForgetToMagmaCat._proof_1, map_comp := @Semigrp.hasForgetToMagmaCat._proof_2 },
    forget_comp := Semigrp.hasForgetToMagmaCat._proof_4 }
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_Icc_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (b : α i), Pi.mulSingle i '' Set.Icc 1 b = Set.Icc 1 (Pi.mulSingle i b)
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedCoreAux_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (s : Set E), balancedCoreAux 𝕜 s ⊆ s
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.OmissionReason.deep : Lean.PrettyPrinter.Delaborator.OmissionReason
-- Mathlib.RingTheory.GradedAlgebra.Radical
/-- The radical of a homogeneous ideal, as another homogeneous ideal.  -/
HomogeneousIdeal.radical : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : AddCommMonoid ι] →
          [inst_2 : LinearOrder ι] →
            [IsOrderedCancelAddMonoid ι] →
              [inst_4 : SetLike σ A] →
                [inst_5 : AddSubmonoidClass σ A] →
                  {𝒜 : ι → σ} → [inst_6 : GradedRing 𝒜] → HomogeneousIdeal 𝒜 → HomogeneousIdeal 𝒜
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.subset_pointwise_smul_iff : ∀ {M : Type u_1} {R : Type u_2} [inst : Group M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S T : Subring R}, S ≤ a • T ↔ a⁻¹ • S ≤ T
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.ofComplex_apply_of_im_pos : ∀ {z : ℂ} (hz : 0 < z.im), ↑UpperHalfPlane.ofComplex z = { coe := z, coe_im_pos := hz }
-- Init.Prelude
/-- `a <|> b` executes `a` and returns the result, unless it fails in which
case it executes and returns `b`. Because `b` is not always executed, it
is passed as a thunk so it can be forced only when needed.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `<|>` in identifiers is `orElse`. -/
HOrElse.hOrElse : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HOrElse α β γ] → α → (Unit → β) → γ
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd'_assoc_hom_app_assoc : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃)
  (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) {Z : C}
  (h :
    (CategoryTheory.shiftFunctor C a₃).obj
        ((CategoryTheory.shiftFunctor C a₂).obj ((CategoryTheory.shiftFunctor C a₁).obj X)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).hom.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X)) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).hom.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app ((CategoryTheory.shiftFunctor C a₁).obj X)) h)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph_adj_snd : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v), ¬w.Nil → w.toSubgraph.Adj u w.snd
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.max : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] [inst_1 : LinearOrder M] {f g : α → M},
  Function.HasFiniteMulSupport f →
    Function.HasFiniteMulSupport g → Function.HasFiniteMulSupport fun a => max (f a) (g a)
-- Init.Data.Vector.Lemmas
Vector.replicate_beq_replicate : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {n : ℕ}, (Vector.replicate n a == Vector.replicate n b) = (n == 0 || a == b)
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.continuous_fst : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M], Continuous TrivSqZeroExt.fst
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Methods.dpost : Lean.Meta.Simp.Methods → Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (S : J.Cover X) (f₁ f₂ : S.Arrow) {W : C} (p₁ : W ⟶ f₁.Y) (p₂ : W ⟶ f₂.Y),
  CategoryTheory.CategoryStruct.comp p₁ f₁.f = CategoryTheory.CategoryStruct.comp p₂ f₂.f →
    S.preOneHypercover.sieve₁ p₁ p₂ = ⊤
-- Mathlib.Algebra.Homology.CochainComplexOpposite
ComplexShape.instIsRelIffIntEmbeddingDownIntUpInt : ComplexShape.embeddingDownIntUpInt.IsRelIff
-- Mathlib.Order.UpperLower.Relative
IsLowerSet.isRelLowerSet_sep : ∀ {α : Type u_1} {s : Set α} (P : α → Prop) [inst : LE α], IsLowerSet s → IsRelLowerSet {x | x ∈ s ∧ P x} P
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.map_zero : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) [Nonempty ι], f 0 = 0
-- Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
IsAlgebraic.adjoin_singleton : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_3}
  [inst_3 : CommRing B] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B] {x : A} {y : B},
  Transcendental R x → Transcendental R y → IsAlgebraic (↥R[x]) y → IsAlgebraic (↥R[y]) ((algebraMap A B) x)
-- Mathlib.Order.Filter.Pi
Filter.hasBasis_pi_same_index : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {κ : Type u_3} {p : κ → Prop}
  {s : (i : ι) → κ → Set (α i)},
  (∀ (i : ι), (f i).HasBasis p (s i)) →
    (∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)) →
      (Filter.pi f).HasBasis (fun Ik => Ik.1.Finite ∧ p Ik.2) fun Ik => Ik.1.pi fun i => s i Ik.2
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
_private.Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete.0.CategoryTheory.Functor.toPseudofunctor.match_3.splitter : {C : Type u_2} →
  [inst : CategoryTheory.Category.{u_1, u_2} C] →
    {b b' : CategoryTheory.LocallyDiscrete C} →
      (motive : (b ⟶ b') → Sort u_3) → (x : b ⟶ b') → ((f : b.as ⟶ b'.as) → motive { as := f }) → motive x
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.Hom.mk.injEq : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y Z : ContinuousGeneratedByCat X}
  (hom hom_1 : Topology.ContinuousMapGeneratedBy X ↑Y ↑Z), ({ hom := hom } = { hom := hom_1 }) = (hom = hom_1)
-- Mathlib.Data.Set.Prod
/-- **Alias** of `Set.prod_sdiff_prod`. -/
Set.prod_diff_prod : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β}, s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [toPreadditive : CategoryTheory.Preadditive C] →
      [toIsNormalMonoCategory : CategoryTheory.IsNormalMonoCategory C] →
        [toIsNormalEpiCategory : CategoryTheory.IsNormalEpiCategory C] →
          [has_finite_products : CategoryTheory.Limits.HasFiniteProducts C] →
            [has_kernels : CategoryTheory.Limits.HasKernels C] →
              [has_cokernels : CategoryTheory.Limits.HasCokernels C] → CategoryTheory.Abelian C
-- Init.Data.UInt.Lemmas
UInt32.ofNat_mod_size : ∀ {x : ℕ}, UInt32.ofNat (x % 2 ^ 32) = UInt32.ofNat x
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.sub_mem_Icc_zero_iff_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b : α},
  b - a ∈ Set.Icc 0 b ↔ a ∈ Set.Icc 0 b
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Dual of `Monotone.covariant_of_const`  -/
Antitone.covariant_of_const : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {α : Type u_3} [inst : Preorder α] [inst_1 : Preorder N] {f : N → α}
  [CovariantClass M N μ fun x1 x2 => x1 ≤ x2], Antitone f → ∀ (m : M), Antitone fun x => f (μ m x)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
min_mul_min_le_min_mul_mul' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LinearOrder α] [MulLeftMono α] [MulRightMono α] {a b c d : α},
  min a c * min b d ≤ min (a * b) (c * d)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : β → β},
  Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.Const.modify m k f) k = Option.map f (Std.ExtDHashMap.Const.get? m k)
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndParamKind.dropped.sizeOf_spec : sizeOf Lean.Meta.FunIndParamKind.dropped = 1
-- Init.Data.Iterators.Consumers.Monadic.Collect
/-- Traverses the given iterator and stores the emitted values in an array.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.toArray` always terminates after finitely many steps.
 -/
Std.IterM.toArray : {α β : Type w} → {m : Type w → Type w'} → [Monad m] → [Std.Iterator α m β] → Std.IterM m β → m (Array β)
-- Init.Data.Option.Basic
/-- Checks whether an optional value is not `none` and satisfies a Boolean predicate.

Examples:
* `(some 33).any (· % 2 == 0) = false
* `(some 22).any (· % 2 == 0) = true
* `none.any (fun x : Nat => true) = false
 -/
Option.any : {α : Type u_1} → (α → Bool) → Option α → Bool
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.ι_D₃ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : ⋯ = j)
  [inst_23 : ⋯], ⋯
-- Mathlib.Algebra.Star.Basic
star_ne_zero : ∀ {R : Type u} [inst : AddMonoid R] [inst_1 : StarAddMonoid R] {x : R}, star x ≠ 0 ↔ x ≠ 0
-- Mathlib.Analysis.Calculus.TangentCone.Real
uniqueDiffOn_Iio : ∀ (a : ℝ), UniqueDiffOn ℝ (Set.Iio a)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConeMapCone_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₅, u₅} E] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D}
  {H' : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Functor.mapConeMapCone c).inv.hom = CategoryTheory.CategoryStruct.id (H'.obj (H.obj c.pt))
-- Std.Http.Protocol.H1.Reader
/-- State waiting for HTTP headers, tracking number of headers parsed.
 -/
Std.Http.Protocol.H1.Reader.State.needHeader : {dir : Std.Http.Protocol.H1.Direction} → ℕ → Std.Http.Protocol.H1.Reader.State dir
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_eq_zero : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] {f : Π₀ (i : ι), β i}
  {h : (i : ι) → β i → γ}, (∀ (i : ι), h i (f i) = 0) → f.sum h = 0
-- Init.Data.Array.Find
Array.findIdx_getElem : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} {w : Array.findIdx p xs < xs.size}, p xs[Array.findIdx p xs] = true
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.dropSuffix?_prop_eq_dropSuffix?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.dropSuffix? p = s.dropSuffix? fun x => decide (p x)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {n w : ℕ} (aig : Std.Sat.AIG α) (distance : aig.RefVec n)
  (curr : ℕ) (acc : aig.RefVec w) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go aig distance curr acc).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go aig distance curr acc).aig.decls[idx] = aig.decls[idx]
-- Mathlib.Data.Fin.Basic
Fin.instNeZeroHAddNatOfNat_mathlib : ∀ {n m : ℕ} [NeZero n] [inst : NeZero (OfNat.ofNat m)], NeZero (OfNat.ofNat m)
-- Mathlib.RepresentationTheory.Rep.Res
Rep.resMap_hom_apply : ∀ {k : Type u} [inst : Semiring k] {G : Type v1} {H : Type v2} [inst_1 : Monoid G] [inst_2 : Monoid H] (f : H →* G)
  {M N : Rep.{u_1, u, v1} k G} (p : M ⟶ N) (x : ↑M), (Rep.Hom.hom (Rep.resMap f p)) x = (Rep.Hom.hom p) x
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The essential image of a fully faithful functor between cartesian-monoidal categories is the
same on monoid objects as on objects.  -/
CategoryTheory.Functor.essImage_mapMon : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [F.Full] [F.Faithful] {M : CategoryTheory.Mon D},
  F.mapMon.essImage M ↔ F.essImage M.X
-- Mathlib.Order.Hom.BoundedLattice
/-- A `SupBotHomClass` morphism preserves the bottom element.  -/
SupBotHomClass.map_bot : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : Max α} {inst_1 : Max β} {inst_2 : Bot α} {inst_3 : Bot β}
  {inst_4 : FunLike F α β} [self : SupBotHomClass F α β] (f : F), f ⊥ = ⊥
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.mk.sizeOf_spec : ∀ {d : ℤ} (re im : ℤ), sizeOf { re := re, im := im } = 1 + sizeOf re + sizeOf im
-- Mathlib.Algebra.Group.TypeTags.Basic
Pi.mulSingle_multiplicativeOfAdd_eq : ∀ {ι : Type u_1} [inst : DecidableEq ι] {M : ι → Type u_2} [inst_1 : (i : ι) → AddMonoid (M i)] (i : ι) (a : M i)
  (j : ι), Pi.mulSingle i (Multiplicative.ofAdd a) j = Multiplicative.ofAdd (Pi.single i a j)
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.pointwise_smul_toAddSubgroup : ∀ {M : Type u_1} [inst : Monoid M] {R : Type u_4} [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] (a : M)
  (S : Ideal R), (Function.Surjective fun r => a • r) → Submodule.toAddSubgroup (a • S) = a • Submodule.toAddSubgroup S
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.Hom.toImageAux.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Scheme.Hom.toImageAux f =
    AlgebraicGeometry.Scheme.Cover.glueMorphisms
      (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i => ↑i) ⋯))
      (fun U =>
        CategoryTheory.CategoryStruct.comp
          (AlgebraicGeometry.Scheme.Hom.liftQuotient
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (↑U).ι) (↑U).toSpecΓ)
            ((AlgebraicGeometry.Scheme.Hom.ker f).ideal U) ⋯)
          ((AlgebraicGeometry.Scheme.Hom.ker f).subschemeCover.f U))
      ⋯
-- Lean.Environment
_private.Lean.Environment.0.Lean.registerEnvExtension.unsafe_impl_2 : {σ : Type} → Lean.EnvExtension σ → Lean.EnvExtension Lean.EnvExtensionState
-- Mathlib.LinearAlgebra.BilinearForm.Hom
/-- When `N₁` and `N₂` are equivalent, bilinear maps on `M` into `N₁` are equivalent to bilinear
maps into `N₂`.  -/
LinearEquiv.congrRight₂ : {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} →
              [inst_3 : AddCommMonoid N₁] →
                [inst_4 : AddCommMonoid N₂] →
                  [inst_5 : Module R N₁] →
                    [inst_6 : Module R N₂] → (N₁ ≃ₗ[R] N₂) → LinearMap.BilinMap R M N₁ ≃ₗ[R] LinearMap.BilinMap R M N₂
-- Mathlib.Analysis.Matrix.Normed
/-- Normed algebra instance (using sup norm of L1 norm) for matrices over a normed algebra. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix.  -/
Matrix.linftyOpNormedAlgebra : {R : Type u_1} →
  {n : Type u_4} →
    {α : Type u_5} →
      [inst : Fintype n] →
        [inst_1 : NormedField R] →
          [inst_2 : SeminormedRing α] → [NormedAlgebra R α] → [inst_4 : DecidableEq n] → NormedAlgebra R (Matrix n n α)
-- Mathlib.Geometry.RingedSpace.SheafedSpace
/-- Constructor for isomorphisms in the category `SheafedSpace C`.  -/
AlgebraicGeometry.SheafedSpace.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : AlgebraicGeometry.SheafedSpace C} → (X.toPresheafedSpace ≅ Y.toPresheafedSpace) → (X ≅ Y)
-- Init.GrindInstances.ToInt
Lean.Grind.instLENatCiOfNatInt : Lean.Grind.ToInt.LE ℕ (Lean.Grind.IntInterval.ci 0)
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- A strict affine subspace has measure zero.  -/
MeasureTheory.Measure.addHaar_affineSubspace : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : AffineSubspace ℝ E), s ≠ ⊤ → μ ↑s = 0
-- Mathlib.Data.List.Lattice
List.inter_subset_right : ∀ {α : Type u_1} [inst : DecidableEq α] {l₁ l₂ : List α}, l₁ ∩ l₂ ⊆ l₂
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.List.length_filter_strict_mono : ∀ {α : Type u} {l : List α} {P Q : α → Bool} {a : α},
  (∀ (a : α), P a = true → Q a = true) →
    a ∈ l → ¬P a = true → Q a = true → (List.filter P l).length < (List.filter Q l).length
-- Init.Data.Vector.OfFn
Vector.ofFnM_zero : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] {f : Fin 0 → m α}, Vector.ofFnM f = pure #v[]
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_inter_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₁.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Hover.mk.sizeOf_spec : ∀ (contents : Lean.Lsp.MarkupContent) (range? : Option Lean.Lsp.Range),
  sizeOf { contents := contents, range? := range? } = 1 + sizeOf contents + sizeOf range?
-- Mathlib.Data.Multiset.Interval
Multiset.card_Icc : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α),
  (Finset.Icc s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, (Multiset.count i t + 1 - Multiset.count i s)
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.instExistsAddOfLE : ∀ {α : Type u_1}, ExistsAddOfLE (Multiset α)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.IsTriangulated.toContainsZero : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.HasShift C ℤ} {inst_3 : CategoryTheory.Preadditive C}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_5 : CategoryTheory.Pretriangulated C}
  {P : CategoryTheory.ObjectProperty C} [self : P.IsTriangulated], P.ContainsZero