mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Count
Array.count_push_of_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {b a : α} {xs : Array α},
  b ≠ a → Array.count a (xs.push b) = Array.count a xs
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.dropUntil.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {v w : V} (p p_1 : G.Walk v w) (e_p : p = p_1) (u : V)
  (a : u ∈ p.support), p.dropUntil u a = p_1.dropUntil u ⋯
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfOrdArgs.mk : {α : Type u} →
  (toLinearPreorderOfOrdArgs : Std.Packages.LinearPreorderOfOrdArgs α) →
    autoParam
        (let this := toLinearPreorderOfOrdArgs.ord;
        let this_1 := toLinearPreorderOfOrdArgs.le;
        ∀ (a b : α), compare a b = Ordering.eq → a = b)
        Std.Packages.LinearOrderOfOrdArgs.eq_of_compare._autoParam →
      (min :
          autoParam
            (let this := toLinearPreorderOfOrdArgs.ord;
            Min α)
            Std.Packages.LinearOrderOfOrdArgs.min._autoParam) →
        (max :
            autoParam
              (let this := toLinearPreorderOfOrdArgs.ord;
              Max α)
              Std.Packages.LinearOrderOfOrdArgs.max._autoParam) →
          autoParam
              (let this := toLinearPreorderOfOrdArgs.ord;
              let this_1 := toLinearPreorderOfOrdArgs.le;
              let this_2 := min;
              have this_3 := ⋯;
              ∀ (a b : α), a ⊓ b = if (compare a b).isLE = true then a else b)
              Std.Packages.LinearOrderOfOrdArgs.min_eq._autoParam →
            autoParam
                (let this := toLinearPreorderOfOrdArgs.ord;
                let this_1 := toLinearPreorderOfOrdArgs.le;
                let this_2 := max;
                have this_3 := ⋯;
                ∀ (a b : α), a ⊔ b = if (compare a b).isGE = true then a else b)
                Std.Packages.LinearOrderOfOrdArgs.max_eq._autoParam →
              Std.Packages.LinearOrderOfOrdArgs α
-- Mathlib.Data.Finmap
_private.Mathlib.Data.Finmap.0.«term⟦_⟧» : Lean.ParserDescr
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.mul_right' : ∀ {n a b : ℕ} (c : ℕ), a ≡ b [MOD n] → a * c ≡ b * c [MOD n * c]
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.LRATStep.del.inj : ∀ {ids ids_1 : Array ℕ}, Mathlib.Tactic.Sat.LRATStep.del ids = Mathlib.Tactic.Sat.LRATStep.del ids_1 → ids = ids_1
-- Init.Data.UInt.Lemmas
UInt8.mul_one : ∀ (a : UInt8), a * 1 = a
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.TermElabM : Type → Type
-- Std.Http.Internal.IndexMultiMap
_private.Std.Http.Internal.IndexMultiMap.0.Std.Internal.IndexMultiMap.insert.match_1.splitter : (motive : Option (Array ℕ) → Sort u_1) →
  (x : Option (Array ℕ)) → ((idxs : Array ℕ) → motive (some idxs)) → (Unit → motive none) → motive x
-- Mathlib.CategoryTheory.LiftingProperties.Adjunction
/-- When we have an adjunction `G ⊣ F`, any commutative square where the left
map is of the form `i` and the right map is `F.map p` has an "adjoint" commutative
square whose left map is `G.map i` and whose right map is `p`.  -/
CategoryTheory.CommSq.left_adjoint : ∀ {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] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C}
  {A B : C} {X Y : D} {i : B ⟶ A} {p : Y ⟶ X} {u : X ⟶ G.obj A} {v : Y ⟶ G.obj B},
  CategoryTheory.CommSq v p (G.map i) u →
    ∀ (adj : F ⊣ G), CategoryTheory.CommSq ((adj.homEquiv' B Y) v) (F.map p) i ((adj.homEquiv' A X) u)
-- Mathlib.Analysis.Normed.Algebra.Unitization
/-- The uniformity on `Unitization 𝕜 A` is inherited from `𝕜 × A`.  -/
Unitization.instUniformSpace : {𝕜 : Type u_1} → {A : Type u_2} → [NontriviallyNormedField 𝕜] → [NonUnitalNormedRing A] → UniformSpace (Unitization 𝕜 A)
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instCompScheme : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z) [AlgebraicGeometry.IsFinite f]
  [AlgebraicGeometry.IsFinite g], AlgebraicGeometry.IsFinite (CategoryTheory.CategoryStruct.comp f g)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.toNormPoly : Nat.Internal.Linear.Expr → Nat.Internal.Linear.Poly
-- Mathlib.Combinatorics.Configuration
/-- A configuration is nondegenerate if:
1) there does not exist a line that passes through all of the points,
2) there does not exist a point that is on all of the lines,
3) there is at most one line through any two points,
4) any two lines have at most one intersection point.

Conditions 3 and 4 are equivalent.  -/
Configuration.Nondegenerate : (P : Type u_1) → (L : Type u_2) → [Membership P L] → Prop
-- Init.Data.SInt.Lemmas
Int32.toBitVec_mul : ∀ {a b : Int32}, (a * b).toBitVec = a.toBitVec * b.toBitVec
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.IsLeftDescent.eq_1 : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B),
  cs.IsLeftDescent w i = (cs.length (cs.simple i * w) < cs.length w)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α}, Std.DHashMap.Raw.Const.get! (m₁ ∩ m₂) k = if k ∈ m₂ then Std.DHashMap.Raw.Const.get! m₁ k else default
-- Mathlib.Combinatorics.Matroid.Circuit
/-- **Alias** of `Matroid.IsCircuit.isBasis_iff_eq_sdiff_singleton`. -/
Matroid.IsCircuit.isBasis_iff_eq_diff_singleton : ∀ {α : Type u_1} {M : Matroid α} {C I : Set α}, M.IsCircuit C → (M.IsBasis I C ↔ ∃ e ∈ C, I = C \ {e})
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.coeff_prod_sum_degree : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {ι : Type u_3} (P : ι → MvPolynomial σ R)
  (s : Finset ι), MvPolynomial.coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndep_iff_forall_condIndepSet : ∀ {Ω : Type u_1} {m' m₁ m₂ mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ ↔
    ∀ (s t : Set Ω), MeasurableSet s → MeasurableSet t → ProbabilityTheory.CondIndepSet m' hm' s t μ
-- Mathlib.Analysis.Normed.Operator.Mul
RegularNormedAlgebra.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_3} [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R],
  Isometry ⇑(ContinuousLinearMap.mul 𝕜 R) → RegularNormedAlgebra 𝕜 R
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.NatTrans.mapHomologicalComplex_naturality : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] {c : ComplexShape ι} {F G : CategoryTheory.Functor W₁ W₂}
  [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms] (α : F ⟶ G) {C D : HomologicalComplex W₁ c}
  (f : C ⟶ D),
  CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplex c).map f)
      ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app D) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C)
      ((G.mapHomologicalComplex c).map f)
-- Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Finset.finsuppAntidiagEquivSubtype_apply_coe : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ] (s : Finset ι) (n : μ) (f : ↥(s.finsuppAntidiag n)),
  ↑((s.finsuppAntidiagEquivSubtype n) f) = Finsupp.subtypeDomain (fun x => x ∈ s) ↑f
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- Standard equivalence relations on types are internal equivalence relations in the category of
types.  -/
TypeCat.EquivalenceRelation.ofEquivalence : {X : Type w} →
  {φ : X → X → Prop} → Equivalence φ → CategoryTheory.EquivalenceRelation (TypeCat.p₁OfRel φ) (TypeCat.p₂OfRel φ)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_iff_infinite_and_pos : ∀ {x : ℝ*}, x.InfinitePos ↔ x.Infinite ∧ 0 < x
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.mk.inj : ∀ {α : Type u} {inst : BEq α} {inst_1 : Hashable α} {set set_1 : Lean.PersistentHashMap α Unit},
  { set := set } = { set := set_1 } → set = set_1
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι_midπ_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q : ℕ) (i : ℤ),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι✝ f n₀).f i)
      ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q).f i) =
    ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj (Opposite.op q)).obj.ι.f i
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.instAddGroupOreLocalization : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} → [inst_2 : AddGroup X] → [inst_3 : DistribMulAction R X] → AddGroup (OreLocalization S X)
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
SeparatingDual.t1Space : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : TopologicalSpace R] [inst_4 : Module R V] [SeparatingDual R V] [T1Space R], T1Space V
-- Init.Data.Array.Lemmas
Array.forIn_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {xs : Array α} {b : β}
  {f : α → β → m (ForInStep β)}, forIn xs.toList b f = forIn xs b f
-- Mathlib.Topology.MetricSpace.PiNat
PiCountable.edist_lt_top : ∀ {ι : Type u_2} [inst : Encodable ι] {F : ι → Type u_3} [inst_1 : (i : ι) → EDist (F i)] {x y : (i : ι) → F i},
  edist x y < ⊤
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicField.algebra : (n : ℕ) → (K : Type w) → [inst : Field K] → Algebra K (CyclotomicField n K)
-- Mathlib.Topology.Order
induced_iff_nhds_eq : ∀ {α : Type u} {β : Type v} [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (f : β → α),
  tβ = TopologicalSpace.induced f tα ↔ ∀ (b : β), nhds b = Filter.comap f (nhds (f b))
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.tmul_smul : ∀ {R : Type u_1} {R' : Type u_4} [inst : CommSemiring R] [inst_1 : Monoid R'] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : DistribMulAction R' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : SMulCommClass R R' M] [inst_8 : DistribMulAction R' N]
  [TensorProduct.CompatibleSMul R R' M N] (r : R') (x : M) (y : N), x ⊗ₜ[R] (r • y) = r • x ⊗ₜ[R] y
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasSum_weierstrassPExcept : ∀ (L : PeriodPair) (l₀ z : ℂ),
  HasSum (fun l => if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) (L.weierstrassPExcept l₀ z)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Polynomial.Chebyshev.integral_eval_T_real_measureT_zero : ∫ (x : ℝ), Polynomial.eval x (Polynomial.Chebyshev.T ℝ 0) ∂Polynomial.Chebyshev.measureT = Real.pi
-- Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
ProperlyDiscontinuousVAdd.ofFiniteRelIndex : ∀ {Γ : Type u_1} {α : Type u_2} [inst : AddGroup Γ] [inst_1 : TopologicalSpace α] [inst_2 : AddAction Γ α]
  [ContinuousConstVAdd Γ α] (G H : AddSubgroup Γ) [hH : ProperlyDiscontinuousVAdd (↥H) α] [H.IsFiniteRelIndex G],
  ProperlyDiscontinuousVAdd (↥G) α
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
/-- The integral of `ω` along `[a -[ℝ] b]`, as a function of `b`, has derivative `ω a` at `b = a`.
This is a `HasFDerivAt` version assuming that `ω` is continuous in a neighborhood of `a`.  -/
HasFDerivAt.curveIntegral_segment_source' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F]
  [CompleteSpace F] {a : E} {ω : E → E →L[𝕜] F},
  (∀ᶠ (z : E) in nhds a, ContinuousAt ω z) → HasFDerivAt (fun x => ∫ᶜ (x : E) in Path.segment a x, ω x) (ω a) a
-- Mathlib.Data.List.ToFinsupp
List.toFinsupp_nil : ∀ {M : Type u_1} [inst : Zero M] [inst_1 : DecidablePred fun i => [].getD i 0 ≠ 0], [].toFinsupp = 0
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} (e : S' ≅ S)
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w :
    ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) e.hom)
  {β : ι → ι'} {q' : (i : ι) → X i ⟶ X' (β i)}
  (w' :
    ∀ (i : ι), CategoryTheory.CategoryStruct.comp (q' i) (f' (β i)) = CategoryTheory.CategoryStruct.comp (f i) e.inv),
  (CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence F e w w').unitIso =
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso F S).symm ≪≫
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorIso F ⋯ ⋯ ≪≫
        (CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso F w w' (CategoryTheory.CategoryStruct.id S) ⋯
            ⋯).symm
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.sieve_apply : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {X : C} (data : F.OneHypercoverDenseData J₀ J X) {X₀ : C₀}
  (f : F.obj X₀ ⟶ X) (Y₀ : C₀) (g : Y₀ ⟶ X₀), (data.sieve f).arrows g = Nonempty (data.SieveStruct f g)
-- Mathlib.RingTheory.PowerSeries.NoZeroDivisors
/-- The ideal spanned by the variable in the power series ring
over an integral domain is a prime ideal.  -/
PowerSeries.span_X_isPrime : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R], (Ideal.span {PowerSeries.X}).IsPrime
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.instMonoidalCategoryStructFullSubcategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (P : CategoryTheory.ObjectProperty C) → [P.IsMonoidal] → CategoryTheory.MonoidalCategoryStruct P.FullSubcategory
-- Std.Http.Data.Body.Full
_private.Std.Http.Data.Body.Full.0.Std.Http.Body.Full.takeChunk : Std.AtomicT (Option ByteArray) Std.Async.Async (Option Std.Http.Chunk)
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.instHasFunctorialSurjectiveInjectiveFactorization : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] [(CategoryTheory.forget C).PreservesMonomorphisms]
  [(CategoryTheory.forget C).PreservesEpimorphisms],
  CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization C
-- Init.Core
Char.mk.inj : ∀ {val : UInt32} {valid : val.isValidChar} {val_1 : UInt32} {valid_1 : val_1.isValidChar},
  { val := val, valid := valid } = { val := val_1, valid := valid_1 } → val = val_1
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.pres_val_comp_inr : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b),
  (Algebra.Generators.PresentationOfFreeCotangent.Aux.pres✝ D).val ∘ Sum.inr = P.val
-- Init.Grind.AC
Lean.Grind.AC.Seq.union.eq_1 : ∀ (s₁ s₂ : Lean.Grind.AC.Seq), s₁.union s₂ = Lean.Grind.AC.Seq.unionFuel Lean.Grind.AC.hugeFuel s₁ s₂
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.coeFn_ofInjective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : L.IsAlgebraic] {f : L.Hom M N} (hf : Function.Injective ⇑f),
  ⇑(FirstOrder.Language.Embedding.ofInjective hf) = ⇑f
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- If `f` is integrable, then `∫ x in s, f x ∂μ` is absolutely continuous in `s`: it tends
to zero as `μ s` tends to zero.  -/
MeasureTheory.Integrable.tendsto_setIntegral_nhds_zero : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_6} {f : α → G},
  MeasureTheory.Integrable f μ →
    ∀ {l : Filter ι} {s : ι → Set α},
      Filter.Tendsto (⇑μ ∘ s) l (nhds 0) → Filter.Tendsto (fun i => ∫ (x : α) in s i, f x ∂μ) l (nhds 0)
-- Init.Data.Array.Basic
Array.size_eraseIdx : ∀ {α : Type u} {xs : Array α} (i : ℕ) (h : i < xs.size), (xs.eraseIdx i h).size = xs.size - 1
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m)
  (q :
    ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
            (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace)
  (a : A),
  a ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q ↔
    ∀ (i : ℕ),
      HomogeneousLocalization.mk
          { deg := m * i, num := ⟨(GradedRing.proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈
        q.asIdeal
-- Mathlib.Data.TypeVec
/-- Support for extending a `TypeVec` by one element.  -/
TypeVec.append1 : {n : ℕ} → TypeVec.{u_1} n → Type u_1 → TypeVec.{u_1} (n + 1)
-- Mathlib.Condensed.Discrete.Module
/-- `functorToPresheaves` in the case of `LightProfinite`.  -/
LightCondMod.LocallyConstant.functorToPresheaves : (R : Type u) →
  [inst : Ring R] → CategoryTheory.Functor (ModuleCat R) (CategoryTheory.Functor LightProfiniteᵒᵖ (ModuleCat R))
-- Mathlib.CategoryTheory.Limits.Unit
CategoryTheory.Limits.instHasColimitsOfSizeDiscretePUnit : CategoryTheory.Limits.HasColimitsOfSize.{v', v, u_1, u_1} (CategoryTheory.Discrete PUnit.{u_1 + 1})
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.lift_comp_inv_right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj B] (f : A ⟶ B) {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp f CategoryTheory.GrpObj.inv))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
/-- If the equalizer comparison map for `G` at `(f,g)` is an isomorphism, then `G` preserves the
equalizer of `(f,g)`.
 -/
CategoryTheory.Limits.PreservesEqualizer.of_iso_comparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasEqualizer f g]
  [inst_3 : CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)]
  [i : CategoryTheory.IsIso (CategoryTheory.Limits.equalizerComparison f g G)],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G
-- Mathlib.Topology.Separation.NotNormal
IsClosed.two_pow_mk_lt_continuum : ∀ {X : Type u} [inst : TopologicalSpace X] [TopologicalSpace.SeparableSpace X] [NormalSpace X] {s : Set X},
  IsClosed s → ∀ [DiscreteTopology ↑s], 2 ^ Cardinal.mk ↑s ≤ Cardinal.continuum
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- The `n`-th Fréchet derivative applied to a vector `(m 0, ..., m (n-1))` is the derivative
multiplied by the product of the `m i`s.  -/
iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} {m : Fin n → 𝕜},
  (iteratedFDerivWithin 𝕜 n f s x) m = (∏ i, m i) • iteratedDerivWithin n f s x
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.cube_of_castHom_ne_zero : ∀ {n : ZMod 9}, (ZMod.castHom ⋯ (ZMod 3)) n ≠ 0 → n ^ 3 = 1 ∨ n ^ 3 = 8
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sum_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X)
  (F : CategoryTheory.PreZeroHypercover X), (E.sum F).I₀ = (E.I₀ ⊕ F.I₀)
-- Init.Data.Nat.Lemmas
Nat.add_self_ne_one : ∀ (n : ℕ), n + n ≠ 1
-- Lean.Environment
Lean.AsyncConstantInfo.mk.inj : ∀ {name : Lean.Name} {kind : Lean.ConstantKind} {sig : Task Lean.ConstantVal} {constInfo : Task Lean.ConstantInfo}
  {name_1 : Lean.Name} {kind_1 : Lean.ConstantKind} {sig_1 : Task Lean.ConstantVal}
  {constInfo_1 : Task Lean.ConstantInfo},
  { name := name, kind := kind, sig := sig, constInfo := constInfo } =
      { name := name_1, kind := kind_1, sig := sig_1, constInfo := constInfo_1 } →
    name = name_1 ∧ kind = kind_1 ∧ sig = sig_1 ∧ constInfo = constInfo_1
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.ofSlice_prev : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {h' : p ≠ (s.slice p₀ p₁ h).startPos},
  String.Slice.Pos.ofSlice (p.prev h') = (String.Slice.Pos.ofSlice p).prev ⋯
-- Mathlib.Algebra.Free
FreeAddSemigroup.recOnAdd.eq_1 : ∀ {α : Type u} {C : FreeAddSemigroup α → Sort l} (x : FreeAddSemigroup α) (ih1 : (x : α) → C (FreeAddSemigroup.of x))
  (ih2 : (x : α) → (y : FreeAddSemigroup α) → C (FreeAddSemigroup.of x) → C y → C (FreeAddSemigroup.of x + y)),
  x.recOnAdd ih1 ih2 =
    FreeAddSemigroup.recOn x fun f s =>
      List.recOn (motive := fun x => (x_1 : α) → C { head := x_1, tail := x }) s ih1
        (fun hd tl ih f => ih2 f { head := hd, tail := tl } (ih1 f) (ih hd)) f
-- Mathlib.Analysis.Normed.Group.Basic
norm_multiset_prod_le : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (m : Multiset E), ‖m.prod‖ ≤ (Multiset.map (fun x => ‖x‖) m).sum
-- Mathlib.Topology.Algebra.Monoid.Defs
/-- Basic hypothesis to talk about a topological additive monoid or a topological additive
semigroup. A topological additive monoid over `M`, for example, is obtained by requiring both the
instances `AddMonoid M` and `ContinuousAdd M`.

Continuity in each argument separately can be stated using `SeparatelyContinuousAdd α`. If one wants
only continuity in either the left or right argument, but not both one can use
`ContinuousConstVAdd α α`/`ContinuousConstVAdd αᵐᵒᵖ α`.  -/
ContinuousAdd : (M : Type u_1) → [TopologicalSpace M] → [Add M] → Prop
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSets.union_iff : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s₁ s₂ s' : Set (Set Ω)},
  ProbabilityTheory.IndepSets (s₁ ∪ s₂) s' μ ↔ ProbabilityTheory.IndepSets s₁ s' μ ∧ ProbabilityTheory.IndepSets s₂ s' μ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_sq_add_sin_sq : ∀ (θ : Real.Angle), θ.cos ^ 2 + θ.sin ^ 2 = 1
-- Init.Data.Format.Basic
Std.Format.FlattenBehavior.noConfusionType : Sort v✝ → Std.Format.FlattenBehavior → Std.Format.FlattenBehavior → Sort v✝