mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMapGE.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (lowerBound : α)
  (it : Std.DTreeMap.Internal.Zipper α β),
  Std.DTreeMap.Internal.Zipper.prependMapGE t lowerBound it =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => it
    | Std.DTreeMap.Internal.Impl.inner size k v l r =>
      match compare lowerBound k with
      | Ordering.lt =>
        Std.DTreeMap.Internal.Zipper.prependMapGE l lowerBound (Std.DTreeMap.Internal.Zipper.cons k v r it)
      | Ordering.eq => Std.DTreeMap.Internal.Zipper.cons k v r it
      | Ordering.gt => Std.DTreeMap.Internal.Zipper.prependMapGE r lowerBound it
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.coe_univ_sum_single : ∀ {α : Type u_1} {M : Type u_8} [inst : Fintype α] [inst_1 : AddCommMonoid M] (f : α → M), ⇑(∑ a, fun₀ | a => f a) = f
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X),
  (TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U).π.app CategoryTheory.Limits.WalkingParallelPair.zero =
    TopCat.Presheaf.SheafConditionEqualizerProducts.res F U
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.inl_i_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct A A] {Z : C} (h : P.I ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp P.i h) =
    CategoryTheory.CategoryStruct.comp P.i₀ h
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval'.of_symm_X_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (φ : M →ₗ[R] M)
  (m : Module.AEval' φ), (Module.AEval'.of φ).symm (Polynomial.X • m) = φ ((Module.AEval'.of φ).symm m)
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.iSup : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] [inst_1 : ConditionallyCompleteLattice M] {ι : Sort u_3} [Nonempty ι]
  [Finite ι] {f : ι → α → M},
  (∀ (i : ι), Function.HasFiniteMulSupport (f i)) → Function.HasFiniteMulSupport fun a => ⨆ i, f i a
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- A product of countably many standard Borel spaces is standard Borel.  -/
StandardBorelSpace.pi_countable : ∀ {ι : Type u_3} [Countable ι] {α : ι → Type u_4} [inst : (n : ι) → MeasurableSpace (α n)]
  [∀ (n : ι), StandardBorelSpace (α n)], StandardBorelSpace ((n : ι) → α n)
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
instLieGroupOfNatWithTopENat : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] [LieGroup I 2 G], LieGroup I 1 G
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.generator_eq_coeff : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥),
  RatFunc.Luroth.generator E = ↑((RatFunc.Luroth.φ✝ E).coeff (RatFunc.Luroth.generatorIndex✝ h))
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.SupportsStmt.match_1.eq_5 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4) (l : Γ → σ → Λ)
  (h_1 : (a : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.move a q))
  (h_2 : (a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.write a q))
  (h_3 : (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.load a q))
  (h_4 : (a : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.branch a q₁ q₂))
  (h_5 : (l : Γ → σ → Λ) → motive (Turing.TM1.Stmt.goto l)) (h_6 : Unit → motive Turing.TM1.Stmt.halt),
  (match Turing.TM1.Stmt.goto l with
    | Turing.TM1.Stmt.move a q => h_1 a q
    | Turing.TM1.Stmt.write a q => h_2 a q
    | Turing.TM1.Stmt.load a q => h_3 a q
    | Turing.TM1.Stmt.branch a q₁ q₂ => h_4 a q₁ q₂
    | Turing.TM1.Stmt.goto l => h_5 l
    | Turing.TM1.Stmt.halt => h_6 ()) =
    h_5 l
-- Mathlib.Analysis.Convex.EGauge
egauge_smul_right : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {c : 𝕜}
  {s : Set E}, (c = 0 → s.Nonempty) → ∀ (x : E), egauge 𝕜 s (c • x) = ‖c‖ₑ * egauge 𝕜 s x
-- Mathlib.Algebra.Field.Basic
div_add_same : ∀ {K : Type u_1} [inst : DivisionSemiring K] {a b : K}, b ≠ 0 → (a + b) / b = a / b + 1
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- If all the elements of a set `s` commute, then `closure s` is a non-unital commutative
semiring.  -/
NonUnitalSubsemiring.closureNonUnitalCommSemiringOfComm : {R : Type u_1} →
  [inst : NonUnitalSemiring R] →
    {s : Set R} → (∀ x ∈ s, ∀ y ∈ s, x * y = y * x) → NonUnitalCommSemiring ↥(NonUnitalSubsemiring.closure s)
-- Std.Async.Basic
Std.Async.EAsync.instMonadLiftBaseIO : {ε : Type} → MonadLift BaseIO (Std.Async.EAsync ε)
-- Mathlib.CategoryTheory.Sites.SheafHom
CategoryTheory.Presheaf.IsSheaf.hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] (F G : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf J G → CategoryTheory.Presheaf.IsSheaf J (CategoryTheory.presheafHom F G)
-- Init.Data.UInt.Lemmas
UInt8.lt_or_le : ∀ (a b : UInt8), a < b ∨ b ≤ a
-- Mathlib.Combinatorics.Additive.Energy
Finset.le_mulEnergy : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α}, s.card * t.card ≤ s.mulEnergy t
-- Mathlib.CategoryTheory.Limits.Types.End
/-- A `ChosenEnds` instance on `Type` given by the explicit subtype construction above.  -/
CategoryTheory.Limits.instChosenEndsType : CategoryTheory.Limits.ChosenEnds.{v, u, max u w, max (u + 1) (w + 1)} (Type (max w u))
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Step.visit.inj : ∀ {e e_1 : Lean.Meta.Simp.Result}, Lean.Meta.Simp.Step.visit e = Lean.Meta.Simp.Step.visit e_1 → e = e_1
-- Mathlib.Algebra.GroupWithZero.Submonoid.CancelMulZero
/-- A submagma with zero of a left cancellative magma with zero inherits left cancellation.  -/
MulZeroMemClass.isLeftCancelMulZero : ∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] {S : Type u_2} [inst_2 : SetLike S M₀] [inst_3 : MulMemClass S M₀]
  [inst_4 : ZeroMemClass S M₀] (s : S) [IsLeftCancelMulZero M₀], IsLeftCancelMulZero ↥s
-- Mathlib.Data.Setoid.Basic
/-- The infimum of a set of equivalence relations.  -/
Setoid.instInfSet : {α : Type u_1} → InfSet (Setoid α)
-- Mathlib.Data.List.Dedup
List.dedup_idem : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α}, l.dedup.dedup = l.dedup
-- Mathlib.Control.Combinators
/-- Collapses two layers of monadic structure into one,
passing the effects of the inner monad through the outer.  -/
joinM : {m : Type u → Type u} → [Monad m] → {α : Type u} → m (m α) → m α
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenEnd.lift.congr_simp : ∀ {J : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_3} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C] {X : C} (f f_1 : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j)
  (e_f : f = f_1)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) =
        CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)),
  CategoryTheory.Limits.chosenEnd.lift f hf = CategoryTheory.Limits.chosenEnd.lift f_1 ⋯
-- Mathlib.Data.Num.Prime
PosNum.minFacAux.eq_2 : ∀ (n x : PosNum) (fuel : ℕ),
  n.minFacAux fuel.succ x = if n < x.bit1 * x.bit1 then n else if x.bit1 ∣ n then x.bit1 else n.minFacAux fuel x.succ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : β → β}, (t.modify k f)[k']? = if cmp k k' = Ordering.eq then Option.map f t[k]? else t[k']?
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldl_eq_foldl_keys : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {f : δ → α → δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldl (fun d a x => f d a) init t = List.foldl f init t.keys
-- Mathlib.Combinatorics.Enumerative.Composition
/-- If one joins a list of lists and then splits the flattening along the right composition,
one gets back the original list of lists.  -/
List.splitWrtComposition_flatten : ∀ {α : Type u_1} (L : List (List α)) (c : Composition L.flatten.length),
  List.map List.length L = c.blocks → L.flatten.splitWrtComposition c = L
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addXYZ_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2 →
            W.addXYZ P Q =
              WeierstrassCurve.Jacobian.addZ P Q •
                ![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2)
                    (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)),
                  W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3)
                    (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)),
                  1]
-- Mathlib.Analysis.SumIntegralComparisons
/-- **Integral test**: a nonnegative antitone function is summable if it is integrable.  -/
AntitoneOn.summable_of_integrableOn_Ioi_zero : ∀ {f : ℝ → ℝ},
  AntitoneOn f (Set.Ici 0) →
    MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume → (∀ t ∈ Set.Ioi 0, 0 ≤ f t) → Summable fun n => f ↑n
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coe_sub : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommGroup R]
  (s t : HahnSeries.SummableFamily Γ R α), ⇑(s - t) = ⇑s - ⇑t
-- Mathlib.RingTheory.SurjectiveOnStalks
RingHom.surjectiveOnStalks_of_exists_div : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S},
  (∀ (x : S), ∃ r s, IsUnit (f s) ∧ f s * x = f r) → f.SurjectiveOnStalks
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.mk : {C : Type u} → C → CategoryTheory.LocallyDiscrete C
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The affine span of a single point, coerced to a set, contains just that point.  -/
AffineSubspace.coe_affineSpan_singleton : ∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (p : P), ↑(affineSpan k {p}) = {p}
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- The canonical isomorphism relating `(parallelPair f g).op` and `parallelPair f.op g.op`  -/
CategoryTheory.Limits.opParallelPairIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      (f g : X ⟶ Y) →
        (CategoryTheory.Limits.parallelPair f g).op ≅
          CategoryTheory.Limits.walkingParallelPairOpEquiv.inverse.comp (CategoryTheory.Limits.parallelPair f.op g.op)
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_of_mul_apply_of_not_le : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddCommMonoid ι] [inst_5 : PartialOrder ι]
  [CanonicallyOrderedAdd ι] [inst_7 : SetLike.GradedMonoid A] {i : ι} (r : ↥(A i)) (r' : DirectSum ι fun i => ↥(A i))
  (n : ι), ¬i ≤ n → ↑(((DirectSum.of (fun i => ↥(A i)) i) r * r') n) = 0
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Functor.mapDerivedCategory.congr_simp : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.Abelian C₁]
  [inst_2 : HasDerivedCategory C₁] {C₂ : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂]
  [inst_4 : CategoryTheory.Abelian C₂] [inst_5 : HasDerivedCategory C₂] (F F_1 : CategoryTheory.Functor C₁ C₂)
  (e_F : F = F_1) [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F], F.mapDerivedCategory = F_1.mapDerivedCategory
-- Mathlib.Order.RelClasses
/-- A class for a well-founded relation `>`.  -/
WellFoundedGT : (α : Type u_1) → [LT α] → Prop
-- Mathlib.Combinatorics.Enumerative.Partition.GenFun
/-- Generating function associated with character $f(i, c)$ for partition functions, where $i$ is a
part of the partition, and $c$ is the count of that part in the partition. The character function is
multiplied within one `n.Partition`, and summed among all `n.Partition` for a fixed `n`. This way,
each `n` is assigned a value, which we use as the coefficients of the power series.

See the module docstring of `Combinatorics.Enumerative.Partition.GenFun` for more details.  -/
Nat.Partition.genFun : {R : Type u_1} → [CommSemiring R] → (ℕ → ℕ → R) → PowerSeries R
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instZero : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Zero (CuspForm Γ k)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral_nonneg : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder F] [IsOrderedAddMonoid F] [IsOrderedModule ℝ F]
  {f : MeasureTheory.SimpleFunc α F}, 0 ≤ᵐ[μ] ⇑f → 0 ≤ MeasureTheory.SimpleFunc.integral μ f
-- Mathlib.Topology.UniformSpace.Basic
instUniformSpaceAdditive : {α : Type ua} → [UniformSpace α] → UniformSpace (Additive α)
-- Mathlib.Order.Monotone.Defs
/-- **Alias** of the reverse direction of `monotone_iff_apply₂`. -/
Monotone.of_apply₂ : ∀ {ι : Type u_1} {α : Type u} {β : ι → Type u_4} [inst : (i : ι) → Preorder (β i)] [inst_1 : Preorder α]
  {f : α → (i : ι) → β i}, (∀ (i : ι), Monotone fun x => f x i) → Monotone f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_le_size_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {l : List ((a : α) × β a)}, t.size ≤ (t.insertMany l).size
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_map_pi : ∀ {ι : Type u_2} {C : ι → Type u_3} [inst : (i : ι) → PartialOrder (C i)] [inst_1 : (i : ι) → NonUnitalRing (C i)]
  [inst_2 : (i : ι) → TopologicalSpace (C i)] [inst_3 : (i : ι) → StarRing (C i)]
  [inst_4 : ∀ (i : ι), StarOrderedRing (C i)] [inst_5 : StarOrderedRing ((i : ι) → C i)]
  [inst_6 : (i : ι) → Module ℝ (C i)] [inst_7 : ∀ (i : ι), SMulCommClass ℝ (C i) (C i)]
  [inst_8 : ∀ (i : ι), IsScalarTower ℝ (C i) (C i)]
  [inst_9 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint]
  [inst_10 : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint]
  [∀ (i : ι), IsSemitopologicalRing (C i)] [∀ (i : ι), T2Space (C i)] [inst_13 : NonnegSpectrumClass ℝ ((i : ι) → C i)]
  [inst_14 : ∀ (i : ι), NonnegSpectrumClass ℝ (C i)] {c : (i : ι) → C i} {x : NNReal},
  autoParam (∀ (i : ι), 0 ≤ c i) CFC.nnrpow_map_pi._auto_1 → CFC.nnrpow c x = fun i => c i ^ x
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.imageSieve.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {FA : A → A → Type u_1} {CA : A → Type w'} [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_3 : CategoryTheory.ConcreteCategory A FA] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : C}
  (s : CategoryTheory.ToType (G.obj (Opposite.op U))),
  CategoryTheory.Presheaf.imageSieve f s =
    {
      arrows := fun V i =>
        ∃ t,
          (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op V))) t =
            (CategoryTheory.ConcreteCategory.hom (G.map i.op)) s,
      downward_closed := ⋯ }
-- Mathlib.Topology.MetricSpace.Defs
Metric.subsingleton_closedBall : ∀ {γ : Type w} [inst : MetricSpace γ] (x : γ) {r : ℝ}, r ≤ 0 → (Metric.closedBall x r).Subsingleton
-- Mathlib.LinearAlgebra.Alternating.Basic
LinearMap.zero_compAlternatingMap : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {N₂ : Type u_11} [inst_5 : AddCommMonoid N₂]
  [inst_6 : Module R N₂] (f : M [⋀^ι]→ₗ[R] N), LinearMap.compAlternatingMap 0 f = 0
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : CompleteSpace E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [inst_7 : FiniteDimensional 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤),
  (f a, 0) ∈ (HasStrictFDerivAt.implicitToOpenPartialHomeomorph f f' hf hf').target
-- Mathlib.Data.PNat.Basic
instAddCommSemigroupPNat : AddCommSemigroup ℕ+
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineMap.vadd_lineMap : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (v : V₁) (p₁ p₂ : P₁) (c : k),
  v +ᵥ (AffineMap.lineMap p₁ p₂) c = (AffineMap.lineMap (v +ᵥ p₁) (v +ᵥ p₂)) c
-- Mathlib.Data.Bool.Basic
Bool.ofNat_add_one : ∀ {n : ℕ}, Bool.ofNat (n + 1) = true
-- Mathlib.Topology.MetricSpace.PartitionOfUnity
/-- Let `X` be an extended metric space. Let `K : ι → Set X` be a locally finite family of closed
sets, let `U : ι → Set X` be a family of open sets such that `K i ⊆ U i` for all `i`. Then there
exists a positive continuous function `δ : C(X, ℝ≥0∞)` such that for any `i` and `x ∈ K i`,
we have `Metric.closedEBall x (δ x) ⊆ U i`.  -/
Metric.exists_continuous_ennreal_forall_closedEBall_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K → ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedEBall x (δ x) ⊆ U i
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.CliqueFree.fiveWheelLikeFree_of_le : ∀ {α : Type u_1} {G : SimpleGraph α} {r k : ℕ} [inst : DecidableEq α],
  G.CliqueFree (r + 2) → r ≤ k → G.FiveWheelLikeFree r k
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- If `G` acts on a domain `C` with `IsGaloisGroup G A C`, and a subgroup `H` acts on `C` with
`IsGaloisGroup H B C`, then the fixing subgroup of `algebraMap B C` equals `H`.  -/
IsGaloisGroup.fixingSubgroup_range_algebraMap : ∀ (G : Type u_1) [inst : Group G] [Finite G] (A : Type u_5) (B : Type u_6) (C : Type u_7) (H : Subgroup G)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : CommRing C] [IsDomain C] [inst_6 : Algebra A C]
  [FaithfulSMul A C] [inst_8 : MulSemiringAction G C] [hGAC : IsGaloisGroup G A C] [inst_9 : Algebra B C]
  [FaithfulSMul B C] [hH : IsGaloisGroup (↥H) B C], fixingSubgroup G (Set.range ⇑(algebraMap B C)) = H
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.density.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (a : α) (x : γ) (s : Set β),
  κ.density ν a x s = Filter.limsup (fun n => κ.densityProcess ν n a x s) Filter.atTop
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.functoriality_faithful : ∀ {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] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) [G.Faithful], (CategoryTheory.Limits.Cone.functoriality F G).Faithful
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMapClass.instZeroAtInftyContinuousMapClass : ∀ {F : Type u_1} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ]
  [inst_2 : Zero γ] [inst_3 : FunLike F β γ] [CompactlySupportedContinuousMapClass F β γ],
  ZeroAtInftyContinuousMapClass F β γ
-- Mathlib.Data.Sigma.Basic
Sigma.eq : ∀ {α : Type u_7} {β : α → Type u_8} {p₁ p₂ : (a : α) × β a} (h₁ : p₁.fst = p₂.fst),
  Eq.recOn h₁ p₁.snd = p₂.snd → p₁ = p₂
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.compRight_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v w : CategoryTheory.Arrow V} {e f : u ⟶ v} (h : CategoryTheory.Arrow.LeftHomotopy e f) (g : v ⟶ w),
  (h.compRight g).hom = CategoryTheory.CategoryStruct.comp h.hom (CategoryTheory.Arrow.Hom.left g)
-- Init.SimpLemmas
Lean.true_arrow_congr : ∀ (p q q' : Prop), p = True → q = q' → Lean.Arrow p q = q'
-- Mathlib.Probability.Kernel.MeasurableLIntegral
/-- This is an auxiliary lemma for `measurable_kernel_prodMk_left`.  -/
ProbabilityTheory.Kernel.measurable_kernel_prodMk_left_of_finite : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {t : Set (α × β)},
  MeasurableSet t → (∀ (a : α), MeasureTheory.IsFiniteMeasure (κ a)) → Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.kerFunctor_obj : ∀ (Y : AlgebraicGeometry.Scheme) (f : (CategoryTheory.Over Y)ᵒᵖ),
  Y.kerFunctor.obj f = AlgebraicGeometry.Scheme.Hom.ker (Opposite.unop f).hom
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.selfLeftAction_actionObj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y : C),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x y =
    CategoryTheory.MonoidalCategoryStruct.tensorObj x y
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfcₙAux_mem_range_inr : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : StarModule 𝕜 A]
  {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop} (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x) (a : A) (ha : p a)
  [inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁] [CompleteSpace A]
  (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜),
  (cfcₙAux ⋯ a ha) f ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)
-- Mathlib.NumberTheory.AlmostPrime
Nat.Prime.sq_isAlmostPrime_two : ∀ {p : ℕ}, Nat.Prime p → Nat.IsAlmostPrime 2 (p ^ 2)
-- Mathlib.NumberTheory.AbelSummation
tendsto_sum_mul_atTop_nhds_one_sub_integral₀ : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜},
  c 0 = 0 →
    (∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t) →
      MeasureTheory.LocallyIntegrableOn (deriv f) (Set.Ici 1) MeasureTheory.volume →
        ∀ {l : 𝕜},
          Filter.Tendsto (fun n => f ↑n * ∑ k ∈ Finset.Icc 0 n, c k) Filter.atTop (nhds l) →
            ∀ {g : ℝ → ℝ},
              (fun t => deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k) =O[Filter.atTop] g →
                MeasureTheory.IntegrableAtFilter g Filter.atTop MeasureTheory.volume →
                  Filter.Tendsto (fun n => ∑ k ∈ Finset.Icc 0 n, f ↑k * c k) Filter.atTop
                    (nhds (l - ∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k))