mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.map_obj_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] {X Y : T} [inst_2 : P.IsStableUnderComposition]
  {f : X ⟶ Y} (hPf : P f)
  (X_1 :
    CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.id T) (CategoryTheory.Functor.fromPUnit X) P Q ⊤),
  ((CategoryTheory.MorphismProperty.Over.map Q hPf).obj X_1).left = X_1.left
-- Aesop.Stats.Basic
Aesop.ForwardInstantiationStats.mk.inj : ∀ {«matches» hyps matches_1 hyps_1 : ℕ},
  { «matches» := «matches», hyps := hyps } = { «matches» := matches_1, hyps := hyps_1 } →
    «matches» = matches_1 ∧ hyps = hyps_1
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.integral_integral_add'_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} [inst_1 : NormedSpace ℝ E] ⦃f g : γ → E⦄,
  MeasureTheory.Integrable f ((η.comp κ) a) →
    MeasureTheory.Integrable g ((η.comp κ) a) →
      ∫ (x : β), ∫ (y : γ), (f + g) y ∂η x ∂κ a =
        ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a + ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- The constant sheaf functor is by definition left-adjoint to the global sections functor.  -/
CategoryTheory.constantSheafΓAdj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₂) →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          [inst_2 : CategoryTheory.HasWeakSheafify J A] →
            [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] →
              CategoryTheory.constantSheaf J A ⊣ CategoryTheory.Sheaf.Γ J A
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_iff_fmod_eq_zero : ∀ {a b : ℤ}, a ∣ b ↔ b.fmod a = 0
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.as_sum_range_C_mul_X_pow' : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) {n : ℕ},
  p.natDegree < n → p = ∑ i ∈ Finset.range n, Polynomial.C (p.coeff i) * Polynomial.X ^ i
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- For `A B` two nonempty finite sets, there always exist `a0 ∈ A, b0 ∈ B` such that
`UniqueMul A B a0 b0`  -/
UniqueProds.uniqueMul_of_nonempty : ∀ {G : Type u_1} {inst : Mul G} [self : UniqueProds G] {A B : Finset G},
  A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.mk.injEq : ∀
  (transformed :
    Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot))
  (next : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot))
  (transformed_1 :
    Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot))
  (next_1 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)),
  ({ transformed := transformed, next := next } = { transformed := transformed_1, next := next_1 }) =
    (transformed = transformed_1 ∧ next = next_1)
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.TZSpec.zoneId.inj : ∀ {id id_1 : String}, Std.Time.Database.TZdb.TZSpec.zoneId id = Std.Time.Database.TZdb.TZSpec.zoneId id_1 → id = id_1
-- Init.Data.Iterators.Basic
/-- Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
given iterator `it` while no value is emitted (see `IterStep.skip`).
 -/
Std.Iter.IsPlausibleSkipSuccessorOf : {α β : Type w} → [Std.Iterator α Id β] → Std.Iter β → Std.Iter β → Prop
-- Mathlib.Data.Part
Part.toOption_isSome : ∀ {α : Type u_1} (o : Part α) [inst : Decidable o.Dom], o.toOption.isSome = true ↔ o.Dom
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.State.mk.sizeOf_spec : ∀ (congrThms : Lean.PHashMap Lean.Meta.Grind.CongrTheoremCacheKey Lean.Meta.CongrTheorem) (simp : Lean.Meta.Simp.State)
  (lastTag : Lean.Name) (counters : Lean.Meta.Grind.Counters) (splitDiags : Lean.PArray Lean.Meta.Grind.SplitDiagInfo)
  (ematchDiags : Lean.PArray Lean.Meta.Grind.EMatchDiagInfo)
  (lawfulEqCmpMap reflCmpMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr))
  (anchors : Lean.PHashMap Lean.Meta.Sym.ExprPtr UInt64)
  (instanceMap : Std.HashMap Lean.Name Lean.Meta.Grind.EMatchTheorem),
  sizeOf
      { congrThms := congrThms, simp := simp, lastTag := lastTag, counters := counters, splitDiags := splitDiags,
        ematchDiags := ematchDiags, lawfulEqCmpMap := lawfulEqCmpMap, reflCmpMap := reflCmpMap, anchors := anchors,
        instanceMap := instanceMap } =
    1 + sizeOf congrThms + sizeOf simp + sizeOf lastTag + sizeOf counters + sizeOf splitDiags + sizeOf ematchDiags +
            sizeOf lawfulEqCmpMap +
          sizeOf reflCmpMap +
        sizeOf anchors +
      sizeOf instanceMap
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.map_fst_toList_eq_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  List.map Prod.fst t.toList = t.keys
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizer.isoTargetOfSelf.eq_1 : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y),
  CategoryTheory.Limits.coequalizer.isoTargetOfSelf f =
    (CategoryTheory.asIso (CategoryTheory.Limits.coequalizer.π f f)).symm
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeftIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
  (f : Y ≅ Z),
  (CategoryTheory.MonoidalCategory.whiskerLeftIso X f).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f.hom
-- Mathlib.Logic.Denumerable
Nat.Subtype.ofNat.congr_simp : ∀ (s : Set ℕ) [inst : DecidablePred fun x => x ∈ s] [inst_1 : Infinite ↑s] (a a_1 : ℕ),
  a = a_1 → Nat.Subtype.ofNat s a = Nat.Subtype.ofNat s a_1
-- Mathlib.Condensed.Light.Functors
/-- The functor from `LightProfinite` to `LightCondSet` factors through `TopCat`.
 -/
lightProfiniteToLightCondSetIsoTopCatToLightCondSet : lightProfiniteToLightCondSet ≅ LightProfinite.toTopCat.comp topCatToLightCondSet
-- Mathlib.Algebra.Ring.GeomSum
geom_sum₂_self : ∀ {R : Type u_1} [inst : Semiring R] (x : R) (n : ℕ), ∑ i ∈ Finset.range n, x ^ i * x ^ (n - 1 - i) = ↑n * x ^ (n - 1)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_lt_iff : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α},
  s.inf' H f < a ↔ ∃ b ∈ s, f b < a
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_iff_norm_div_tendsto_zero : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedCommGroup E] {f : α → E} {a : Filter α} {b : E},
  Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun e => ‖f e / b‖) a (nhds 0)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.map_one_of_isLeftRegular : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S), IsLeftRegular (abv 1) → abv 1 = 1
-- Mathlib.Algebra.Lie.OfAssociative
/-- The adjoint action of a Lie algebra on itself.  -/
LieAlgebra.ad : (R : Type u) →
  (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → L →ₗ⁅R⁆ Module.End R L
-- Lean.Data.Format
Lean.Std.Format.pretty' : Std.Format → optParam Lean.Options ∅ → String
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.lengthParity_eq_ofAdd_length : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W),
  cs.lengthParity w = Multiplicative.ofAdd ↑(cs.length w)
-- Mathlib.Order.Atoms
Pi.isAtomistic : ∀ {ι : Type u_4} {π : ι → Type u} [inst : (i : ι) → PartialOrder (π i)] [inst_1 : (i : ι) → OrderBot (π i)]
  [∀ (i : ι), IsAtomistic (π i)], IsAtomistic ((i : ι) → π i)
-- Mathlib.Order.Sublattice
Sublattice.mk_lt_mk : ∀ {α : Type u_2} [inst : Lattice α] {s t : Set α} (hs_sup : SupClosed s) (hs_inf : InfClosed s) (ht_sup : SupClosed t)
  (ht_inf : InfClosed t),
  { carrier := s, supClosed' := hs_sup, infClosed' := hs_inf } <
      { carrier := t, supClosed' := ht_sup, infClosed' := ht_inf } ↔
    s ⊂ t
-- Mathlib.Logic.Embedding.Basic
/-- If `e₁` and `e₂` are embeddings, then so is `Sum.map e₁ e₂`.  -/
Function.Embedding.sumMap : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → {δ : Type u_4} → (α ↪ β) → (γ ↪ δ) → α ⊕ γ ↪ β ⊕ δ
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
IsLUB.ciSup_eq : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {a : α} [Nonempty ι] {f : ι → α},
  IsLUB (Set.range f) a → ⨆ i, f i = a
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsUniformizer.zpowers_eq_valueGroup : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] {v : Valuation A Γ}
  [hv : v.IsRankOneDiscrete] {π : A} (hπ : v.IsUniformizer π),
  (MonoidWithZeroHom.ofClass v).valueGroup = Subgroup.zpowers (Units.mk0 (v π) ⋯)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
mul_inv_eq_mul_inv_iff : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a b c d : G₀}, b ≠ 0 → d ≠ 0 → (a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b)
-- Mathlib.Topology.EMetricSpace.Basic
/-- A sequentially complete pseudoemetric space is complete.  -/
EMetric.complete_of_cauchySeq_tendsto : ∀ {α : Type u} [inst : PseudoEMetricSpace α],
  (∀ (u : ℕ → α), CauchySeq u → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) → CompleteSpace α
-- Init.Data.UInt.Lemmas
UInt8.toNat_ofBitVec : ∀ {a : BitVec 8}, { toBitVec := a }.toNat = a.toNat
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (T : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ),
  (CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).obj T =
    CategoryTheory.Pretriangulated.Triangle.mk (Opposite.unop T).mor₂.op (Opposite.unop T).mor₁.op
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).counitIso.inv.app
          (Opposite.op (Opposite.unop T).obj₁))
        ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map (Opposite.unop T).mor₃.op))
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
/-- The subtype of monic polynomials.  -/
AlgebraicClosure.Monics : (k : Type u) → [Field k] → Type u
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.toMultiplicativeRight_symm_apply_symm_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : MulOneClass G] [inst_1 : AddZeroClass H] (f : G ≃* Multiplicative H) (a : H),
  (AddEquiv.toMultiplicativeRight.symm f).symm a = (MonoidHom.toAdditiveRight f.symm.toMonoidHom) a
-- Mathlib.Analysis.Normed.Group.InfiniteSum
/-- Variant of the direct comparison test for series:  if the norm of `f` is eventually bounded by a
real function `g` which is summable, then `f` is summable.  -/
Summable.of_norm_bounded_eventually : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E} {g : ι → ℝ},
  Summable g → (∀ᶠ (i : ι) in Filter.cofinite, ‖f i‖ ≤ g i) → Summable f
-- Mathlib.Data.Set.Function
Set.MapsTo.union : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} {f : α → β},
  Set.MapsTo f s₁ t → Set.MapsTo f s₂ t → Set.MapsTo f (s₁ ∪ s₂) t
-- Init.Grind.Ring.Envelope
_private.Init.Grind.Ring.Envelope.0.Lean.Grind.Ring.OfSemiring.r.match_1.splitter : (α : Type u_1) →
  (motive : α × α → α × α → Sort u_2) → (x x_1 : α × α) → ((a b c d : α) → motive (a, b) (c, d)) → motive x x_1
-- Mathlib.SetTheory.Ordinal.Notation
ONote.repr_scale : ∀ (x : ONote) [x.NF] (o : ONote) [o.NF], (x.scale o).repr = Ordinal.omega0 ^ x.repr * o.repr
-- Mathlib.Condensed.Light.Sequence
/-- Given a map `π : T ⟶ S ⊗ ℕ∪{∞}` and map `g : (free R) T.toCondensed ⟶ X`, the corresponding
map of free condensed R modules, construct a cocone for the parallel pair of both projections of
the pullback, which will descend down to a map `S ⊗ ℕ∪{∞} ⟶ X` by the universal property of
effective epimorphisms. The cocone is constructed by modifying `g` at the at the fibre over `∞`
using the retraction `r_inf`.  -/
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.cocone : (R : Type) →
  [inst : CommRing R] →
    {X : LightCondMod R} →
      {S T : LightProfinite} →
        (π : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj S LightProfinite.NatUnionInfty) →
          [CategoryTheory.Epi
                ((lightProfiniteToLightCondSet.comp (LightCondensed.free R)).map
                  (InternalProjectivityProof.cover✝ π))] →
            ((lightProfiniteToLightCondSet.comp (LightCondensed.free R)).obj T ⟶ X) →
              (r_inf :
                  T ⟶
                    InternalProjectivityProof.LightProfinite.fibre✝ OnePoint.infty
                      (CategoryTheory.CategoryStruct.comp π
                        (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty))) →
                (S ⟶
                    InternalProjectivityProof.LightProfinite.fibre✝ OnePoint.infty
                      (CategoryTheory.CategoryStruct.comp π
                        (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty))) →
                  CategoryTheory.CategoryStruct.comp
                        (InternalProjectivityProof.LightProfinite.fibreIncl✝ OnePoint.infty
                          (CategoryTheory.CategoryStruct.comp π
                            (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))
                        r_inf =
                      CategoryTheory.CategoryStruct.id
                        (InternalProjectivityProof.LightProfinite.fibre✝ OnePoint.infty
                          (CategoryTheory.CategoryStruct.comp π
                            (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty))) →
                    CategoryTheory.Limits.Cocone
                      ((CategoryTheory.Limits.parallelPair
                            (lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π))
                            (lightProfiniteToLightCondSet.map (CompHausLike.pullback.snd π π))).comp
                        (LightCondensed.free R))
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.sheafedSpaceObj_presheaf : ∀ (R : CommRingCat),
  (AlgebraicGeometry.Spec.sheafedSpaceObj R).presheaf = (AlgebraicGeometry.Spec.structureSheaf ↑R).obj
-- Init.Data.SInt.Lemmas
Int32.le_maxValue : ∀ (a : Int32), a ≤ Int32.maxValue
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.IsometryEquiv.mk.inj : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {inst : CommSemiring R} {inst_1 : AddCommMonoid M₁}
  {inst_2 : AddCommMonoid M₂} {inst_3 : Module R M₁} {inst_4 : Module R M₂} {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} {toLinearEquiv : M₁ ≃ₗ[R] M₂}
  {map_app' : ∀ (n m : M₁), (B₂ ((↑toLinearEquiv).toFun n)) ((↑toLinearEquiv).toFun m) = (B₁ n) m}
  {toLinearEquiv_1 : M₁ ≃ₗ[R] M₂}
  {map_app'_1 : ∀ (n m : M₁), (B₂ ((↑toLinearEquiv_1).toFun n)) ((↑toLinearEquiv_1).toFun m) = (B₁ n) m},
  { toLinearEquiv := toLinearEquiv, map_app' := map_app' } =
      { toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 } →
    toLinearEquiv = toLinearEquiv_1
-- Mathlib.RingTheory.WittVector.Domain
WittVector.shift_coeff : ∀ {p : ℕ} {R : Type u_1} (x : WittVector p R) (n k : ℕ), (x.shift n).coeff k = x.coeff (n + k)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_id_one : ∀ {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  [inst_2 : One F''] [NeZero 1], (fun x => x) =o[nhds 0] 1
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.instStarModule : ∀ {n : Type u_3} {α : Type v} {β : Type w} [inst : Star α] [inst_1 : Star β] [inst_2 : SMul α β] [StarModule α β],
  StarModule α (Matrix n n β)
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalGroup.ext : ∀ {G : Type u_1} [inst : Group G] {t t' : TopologicalSpace G},
  IsTopologicalGroup G → IsTopologicalGroup G → nhds 1 = nhds 1 → t = t'
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
instIsContMDiffRiemannianBundleOfNatWithTopENat : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {B : Type u_3} [inst_3 : TopologicalSpace B]
  [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F]
  {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_8 : (x : B) → NormedAddCommGroup (E x)]
  [inst_9 : (x : B) → InnerProductSpace ℝ (E x)] [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E]
  [IsContMDiffRiemannianBundle IB 1 F E], IsContMDiffRiemannianBundle IB 0 F E
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.mk : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  (∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] [Module.Finite R P] (N : Submodule R P),
      N.FG → Function.Injective ⇑(LinearMap.rTensor M N.subtype)) →
    Module.Flat R M
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_set : ∀ {M : Type u_4} [inst : Monoid M] (L : List M) (n : ℕ) (a : M),
  (L.set n a).prod = ((List.take n L).prod * if n < L.length then a else 1) * (List.drop (n + 1) L).prod
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
/-- If the measure `μ.trim hm` is sigma-finite, then the conditional expectation of a measurable set
with finite measure is integrable.  -/
MeasureTheory.integrable_condExpL2_indicator : ∀ {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E']
  [inst_2 : InnerProductSpace 𝕜 E'] [inst_3 : CompleteSpace E'] [NormedSpace ℝ E'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s)
  (hμs : μ s ≠ ⊤) (x : E'),
  MeasureTheory.Integrable (↑↑↑((MeasureTheory.condExpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x))) μ
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.coe_injective : ∀ {M : Type u_1} [inst : AddCommMonoid M] [IsAddTorsionFree M], Function.Injective DivisibleHull.coe
-- Mathlib.NumberTheory.LSeries.PrimesInAP
ArithmeticFunction.vonMangoldt.residueClass_nonneg : ∀ {q : ℕ} (a : ZMod q) (n : ℕ), 0 ≤ ArithmeticFunction.vonMangoldt.residueClass a n
-- Mathlib.Computability.DFA
/-- `M.evalFrom s x` evaluates `M` with input `x` starting from the state `s`.  -/
DFA.evalFrom : {α : Type u} → {σ : Type v} → DFA α σ → σ → List α → σ
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] (f : EsakiaHom α β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.norm_apply_eq_norm_coef : ∀ {𝕜 : Type u} {E : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {n : ℕ}, ‖p n‖ = ‖p.coeff n‖
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.reverse_toListRev_ensureTermination : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.ensureTermination.toListRev.reverse = it.toList
-- Mathlib.Algebra.Group.End
AddAut.coe_add : ∀ (M : Type u_2) [inst : Add M] (e₁ e₂ : AddAut M), ⇑(e₁ + e₂) = ⇑e₁ ∘ ⇑e₂
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_opow_le : ∀ (a b : Ordinal.{u_1}), (a ^ b).card ≤ max Cardinal.aleph0 (max a.card b.card)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.homCategory_comp_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {X Y Z : F ⟶ G} (Γ : CategoryTheory.Oplax.OplaxTrans.Hom X Y)
  (Δ : CategoryTheory.Oplax.OplaxTrans.Hom Y Z) (a : B),
  (CategoryTheory.CategoryStruct.comp Γ Δ).as.app a = CategoryTheory.CategoryStruct.comp (Γ.as.app a) (Δ.as.app a)
-- Mathlib.Data.FunLike.Basic
/-- This is not an instance to avoid slowing down every single `Subsingleton` typeclass search.  -/
DFunLike.subsingleton_dom : ∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] [IsEmpty α], Subsingleton F
-- Batteries.Data.List.Basic
/-- `dropInfix? l i` returns
`some (p, s)` if `l = p ++ i' ++ s` for some `i'` which is paiwise `==` to `i`,
and `none` otherwise.

Note that this is an inefficient implementation, and if computation time is a concern you should be
using the Knuth-Morris-Pratt algorithm as implemented in `Batteries.Data.List.Matcher`.
 -/
List.dropInfix? : {α : Type u_1} → [BEq α] → List α → List α → Option (List α × List α)
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.nonempty_of_lt : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C},
  P < Q → Q.Nonempty
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.toAdd_top : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderTop α], Multiplicative.toAdd ⊤ = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver.eq_1 : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X],
  CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X =
    {
      obj := fun J =>
        { fst := J.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G),
          snd := J.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G),
          iso :=
            J.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F ≪≫
              J.isoWhiskerLeft
                  (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                    (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G) ≪≫
                (J.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).symm },
      map := fun {J J'} F_1 =>
        { fst := CategoryTheory.Functor.whiskerRight F_1 (CategoryTheory.Limits.CategoricalPullback.π₁ F G),
          snd := CategoryTheory.Functor.whiskerRight F_1 (CategoryTheory.Limits.CategoricalPullback.π₂ F G), w := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Topology.Constructions.SumProd
nhds_inr : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (y : Y),
  nhds (Sum.inr y) = Filter.map Sum.inr (nhds y)
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.sigmaAll_apply : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
  FirstOrder.Language.BoundedFormula.sigmaAll ⟨n + 1, φ⟩ = ⟨n, φ.all⟩
-- Mathlib.Probability.Kernel.Defs
/-- **Alias** of `zero_apply`. -/
ProbabilityTheory.Kernel.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Mathlib.LinearAlgebra.Span.Basic
LinearEquiv.coord_self : ∀ (R : Type u_1) (M : Type u_4) [inst : Ring R] [inst_1 : IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inst_4 : Module.IsTorsionFree R M] (x : M) (h : x ≠ 0), (LinearEquiv.coord R M x h) ⟨x, ⋯⟩ = 1
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.AffineZariskiSite} {s : Set ↑(X.presheaf.obj (Opposite.op U.toOpens))}
  {f : V ⟶ U},
  (CategoryTheory.Sieve.generate (U.presieveOfSections s)).arrows f ↔ ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens