mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.Hom.mk.sizeOf_spec : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {X Y : F.Grothendieck}
  [inst_1 : SizeOf 𝒮] (base : X.base ⟶ Y.base) (fiber : (F.map base.toLoc).toFunctor.obj X.fiber ⟶ Y.fiber),
  sizeOf { base := base, fiber := fiber } = 1 + sizeOf base + sizeOf fiber
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.State.canon : Lean.Meta.Sym.State → Lean.Meta.Sym.Canon.State
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
/-- A comonoid object in the category of `R`-modules has a natural comultiplication
and counit.  -/
CoalgCat.ofComonObjCoalgebraStruct : {R : Type u} → [inst : CommRing R] → (X : ModuleCat R) → [CategoryTheory.ComonObj X] → CoalgebraStruct R ↑X
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Multiplying by a unit `a` of the ring `R` is a linear equivalence.  -/
LinearEquiv.smulOfUnit : {R : Type u_1} →
  {M : Type u_5} → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Rˣ → M ≃ₗ[R] M
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_filterMap_le_size : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ}, (Std.HashMap.filterMap f m).size ≤ m.size
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.AddConstAsyncResult.exportedKind? : Lean.Environment.AddConstAsyncResult → Option Lean.ConstantKind
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multicospanMapIso_hom_app : ∀ {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] {J : CategoryTheory.Limits.MulticospanShape}
  (d : CategoryTheory.Limits.MulticospanIndex J C) (F : CategoryTheory.Functor C D)
  (X : CategoryTheory.Limits.WalkingMulticospan J),
  (d.multicospanMapIso F).hom.app X =
    (match X with
      | CategoryTheory.Limits.WalkingMulticospan.left a => CategoryTheory.Iso.refl (F.obj (d.left a))
      | CategoryTheory.Limits.WalkingMulticospan.right a => CategoryTheory.Iso.refl (F.obj (d.right a))).hom
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- The sheaf of smooth functions from `M` to
`A`, for `A` an abelian additive Lie group, as a sheaf of abelian additive groups.  -/
smoothSheafAddCommGroup : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              ModelWithCorners 𝕜 EM HM →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [ChartedSpace HM M] →
                                  (A : Type u) →
                                    [inst_9 : TopologicalSpace A] →
                                      [inst_10 : ChartedSpace H A] →
                                        [inst_11 : AddCommGroup A] →
                                          [LieAddGroup I (↑⊤) A] → TopCat.Sheaf AddCommGrpCat (TopCat.of M)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.intercalateTR.go.eq_2 : ∀ {α : Type u_1} (sep : Array α) (a : List α) (a_1 : Array α) (y : List α) (xs : List (List α)),
  List.intercalateTR.go✝ sep a (y :: xs) a_1 = List.intercalateTR.go✝ sep y xs (a_1 ++ a ++ sep)
-- Mathlib.RingTheory.Ideal.IsPrimary
Ideal.isPrimary_finsetInf : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_3} {s : Finset ι} {f : ι → Ideal R} {i : ι},
  i ∈ s →
    (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) → (∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical) → (s.inf f).IsPrimary
-- Init.Data.Option.Basic
/-- Returns `none` if a value doesn't satisfy a Boolean predicate, or the value itself otherwise.

From the perspective of `Option` as computations that might fail, this function is a run-time
assertion operator in the `Option` monad.

Examples:
 * `Option.guard (· > 2) 1 = none`
 * `Option.guard (· > 2) 5 = some 5`
 -/
Option.guard : {α : Type u_1} → (α → Bool) → α → Option α
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.Martingale.ae_not_tendsto_atTop_atTop : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Martingale f ℱ μ →
    (∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) →
      ∀ᵐ (ω : Ω) ∂μ, ¬Filter.Tendsto (fun n => f n ω) Filter.atTop Filter.atTop
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.isLocalization_away_of_isAffine : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (r : ↑(X.presheaf.obj (Opposite.op ⊤))),
  IsLocalization.Away r ↑(X.presheaf.obj (Opposite.op (X.basicOpen r)))
-- Mathlib.Algebra.Category.ModuleCat.InjectiveDimension
ModuleCat.hasInjectiveDimensionLE_iff_of_semiLinearEquiv : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] {R' : Type u'} [inst_2 : Ring R'] (eR : R ≃+* R') [Small.{v', u'} R']
  {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N) (n : ℕ),
  CategoryTheory.HasInjectiveDimensionLE M n ↔ CategoryTheory.HasInjectiveDimensionLE N n
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [Countable ι] (hτ : MeasureTheory.IsStoppingTime f τ) (i : ι), MeasurableSet {ω | τ ω < ↑i}
-- Init.Data.List.Erase
List.eraseIdx_append_of_lt_length : ∀ {α : Type u_1} {l : List α} {k : ℕ}, k < l.length → ∀ (l' : List α), (l ++ l').eraseIdx k = l.eraseIdx k ++ l'
-- Mathlib.Data.Nat.Factorization.Basic
Nat.factorization_le_factorization_mul_left : ∀ {a b : ℕ}, b ≠ 0 → a.factorization ≤ (a * b).factorization
-- Lean.Declaration
Lean.ConstantVal.levelParams : Lean.ConstantVal → List Lean.Name
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.instReprIndGroupInst : Repr Lean.Elab.Structural.IndGroupInst
-- Mathlib.Order.Max
not_isMin_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ¬IsMin a ↔ ∃ b, b < a
-- Mathlib.Computability.TuringMachine.Computable
/-- type of stack elements  -/
Turing.FinTM2.Γ : (self : Turing.FinTM2) → self.K → Type
-- Mathlib.Order.Filter.ENNReal
ENNReal.liminf_mul_const_of_ne_zero_of_ne_top : ∀ {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal},
  a ≠ 0 → a ≠ ⊤ → Filter.liminf (fun x => u x * a) f = a * Filter.liminf u f
-- Mathlib.Tactic.FastInstance
/-- Throw an error for `makeFastInstance`. The trace is a list of fields.
Note: with the current implementation, this might not be accurate for multi-structure types,
since `makeFastInstance` just uses `ClassName.paramName` for the trace.
 -/
_private.Mathlib.Tactic.FastInstance.0.Mathlib.Elab.FastInstance.error : {α : Type} → Array Lean.Name → Lean.MessageData → Lean.MetaM α
-- Lean.Environment
/-- Indicates whether the environment is being used in an exported context, i.e. whether it should
provide access to only the data to be imported by other modules participating in the module
system. Apart from controlling access, some operations such as `mkAuxDeclName` may also change
their output based on this flag.

By default, `isExporting` is set to false when command elaborators are invoked such that they have
access to the full local environment. Use `with(out)Exporting` to modify based on context. For
example, `elabDeclaration` sets it based on `(← getScope).isPublic` on the top level, then
`elabMutualDef` may switch from public to private when e.g. entering the proof of a theorem.
 -/
Lean.Environment.isExporting : Lean.Environment → Bool
-- Init.Data.SInt.Bitwise
Int32.shiftLeft_xor : ∀ {a b c : Int32}, (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.funCC : Lean.Name → Lean.Meta.Grind.Entry
-- Init.Data.Range.Polymorphic.UInt
USize.instLawfulHasSize_2 : Std.Rxi.LawfulHasSize USize
-- Mathlib.Topology.Constructions
continuous_pi : ∀ {X : Type u} {ι : Type u_5} {A : ι → Type u_6} [inst : TopologicalSpace X] [T : (i : ι) → TopologicalSpace (A i)]
  {f : X → (i : ι) → A i}, (∀ (i : ι), Continuous fun a => f a i) → Continuous f
-- Mathlib.Topology.Algebra.SeparationQuotient.Hom
SeparationQuotient.liftContinuousAddCommMonoidHom_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : AddCommMonoid M]
  [inst_3 : ContinuousAdd M] [inst_4 : AddCommMonoid N] (f : M →ₜ+ N) (hf : ∀ (x y : M), Inseparable x y → f x = f y)
  (x : M), (SeparationQuotient.liftContinuousAddMonoidHom f hf) (SeparationQuotient.mk x) = f x
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.compContinuousLinearMap_comp : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} {H : Type y} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F]
  [inst_10 : ContinuousConstSMul 𝕜 F] [inst_11 : AddCommMonoid G] [inst_12 : Module 𝕜 G] [inst_13 : TopologicalSpace G]
  [inst_14 : ContinuousAdd G] [inst_15 : ContinuousConstSMul 𝕜 G] [inst_16 : AddCommMonoid H] [inst_17 : Module 𝕜 H]
  [inst_18 : TopologicalSpace H] [inst_19 : ContinuousAdd H] [inst_20 : ContinuousConstSMul 𝕜 H]
  (p : FormalMultilinearSeries 𝕜 G H) (u₁ : F →L[𝕜] G) (u₂ : E →L[𝕜] F),
  (p.compContinuousLinearMap u₁).compContinuousLinearMap u₂ = p.compContinuousLinearMap (u₁ ∘SL u₂)
-- Mathlib.Topology.Maps.Basic
IsClosedMap.closure_image_eq_of_continuous : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f → Continuous f → ∀ (s : Set X), closure (f '' s) = f '' closure s
-- Lean.Meta.Sym.Simp.SimpM
/-- Cache mapping expressions (by pointer equality) to their simplified results.  -/
Lean.Meta.Sym.Simp.Cache : Type
-- Init.Data.Nat.Gcd
Nat.gcd_div_gcd_div_gcd_of_pos_right : ∀ {n m : ℕ}, 0 < m → (n / n.gcd m).gcd (m / n.gcd m) = 1
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
summableLocallyUniformlyOn_iff_hasSumLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  SummableLocallyUniformlyOn f s ↔ HasSumLocallyUniformlyOn f (fun x => ∑' (i : ι), f i x) s
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- `PowerSeries.IsWeierstrassDivisorAt g I` is a `Prop` which asserts that the `n`-th coefficient
of `g` is a unit, where `n` is the order of the
image of `g` in `(A / I)⟦X⟧` (defined to be zero if such image is zero, in which case
it's mathematically not considered).

This property guarantees that if the ring is `I`-adic complete, then `g` can be used as a divisor
in Weierstrass division (`PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod`).  -/
PowerSeries.IsWeierstrassDivisorAt : {A : Type u_1} → [inst : CommRing A] → PowerSeries A → Ideal A → Prop
-- Mathlib.Topology.EMetricSpace.Defs
/-- Fixed size neighborhoods of the diagonal belong to the uniform structure  -/
edist_mem_uniformity : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {ε : ENNReal}, 0 < ε → {p | edist p.1 p.2 < ε} ∈ uniformity α
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.instAddSubtypeMem : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → (I : TwoSidedIdeal R) → Add ↥I
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
hasSum_unop : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {f : β → αᵐᵒᵖ} {a : αᵐᵒᵖ}, HasSum (fun a => MulOpposite.unop (f a)) (MulOpposite.unop a) L ↔ HasSum f a L
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.setStateImpl : {σ : Type} → Lean.EnvExtension σ → Array Lean.EnvExtensionState → σ → Array Lean.EnvExtensionState
-- Lean.Data.Lsp.Internal
/-- Shortened representation of `RefIdent` for more compact serialization.  -/
Lean.Lsp.RefIdent.RefIdentJsonRepr : Type
-- Mathlib.Order.Hom.Order
OrderHom.instSemilatticeInf : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : SemilatticeInf β] → SemilatticeInf (α →o β)
-- Mathlib.Topology.Connected.LocallyPathConnected
AlexandrovDiscrete.locallyPathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [AlexandrovDiscrete X], LocallyPathConnectedSpace X
-- Mathlib.Order.Filter.Prod
Filter.prod_iInf_left : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [Nonempty ι] {f : ι → Filter α} {g : Filter β},
  (⨅ i, f i) ×ˢ g = ⨅ i, f i ×ˢ g
-- Mathlib.RingTheory.Ideal.Quotient.Operations
RingEquiv.quotientBot_mk : ∀ {R : Type u_1} [inst : Ring R] (r : R), (RingEquiv.quotientBot R) ((Ideal.Quotient.mk ⊥) r) = r
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.instCategoryMonad : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Category.{max u₁ v₁, max u₁ v₁} (CategoryTheory.Monad C)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.insert_iff : ∀ {α : outParam (Type u)} {β : outParam (Type v)} {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w}
  {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (f : σ) (c1 c2 : β),
  c2 ∈ Std.Tactic.BVDecide.LRAT.Internal.Formula.toList (Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c1) ↔
    c2 = c1 ∨ c2 ∈ Std.Tactic.BVDecide.LRAT.Internal.Formula.toList f
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filter_not_contains : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k fallback : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getKeyD k (List.filter (fun p => !l₂.contains p.fst) l₁) fallback =
      if l₂.contains k = true then fallback else Std.Internal.List.getKeyD k l₁ fallback
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_eq_toLinearMap : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) {f : ρ.IntertwiningMap σ}, ↑f = f.toLinearMap
-- Init.Grind.AC
Lean.Grind.AC.imp_eq : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) (lhs rhs : Lean.Grind.AC.Expr) (s : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Expr.denote ctx lhs = Lean.Grind.AC.Seq.denote ctx s →
    Lean.Grind.AC.Expr.denote ctx rhs = Lean.Grind.AC.Seq.denote ctx s →
      Lean.Grind.AC.Expr.denote ctx lhs = Lean.Grind.AC.Expr.denote ctx rhs
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overMapPullbackId_inv_app_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] (X : C) (X_1 : CategoryTheory.Sheaf (J.over X) A)
  (X_2 : (CategoryTheory.Over X)ᵒᵖ),
  ((J.overMapPullbackId A X).inv.app X_1).hom.app X_2 =
    X_1.obj.map ((CategoryTheory.Over.mapId X).hom.app (Opposite.unop X_2)).op
-- Init.Data.Iterators.Basic
Std.IterM.IsPlausibleIndirectSuccessorOf.below.cons_right : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {a : Std.IterM m β}
  {motive : (a_1 : Std.IterM m β) → a.IsPlausibleIndirectSuccessorOf a_1 → Prop} {it' it : Std.IterM m β}
  (h' : a.IsPlausibleIndirectSuccessorOf it') (h : it'.IsPlausibleSuccessorOf it),
  Std.IterM.IsPlausibleIndirectSuccessorOf.below h' → motive it' h' → Std.IterM.IsPlausibleIndirectSuccessorOf.below ⋯
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Fields to not automatically synthesize handlers for, in addition to those keys
already appearing in `handlers`.  -/
Lean.Elab.ConfigEval.EvalConfigItemView.omitFields : Lean.Elab.ConfigEval.EvalConfigItemView → Array (Lean.Ident × Lean.Name)
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Mulinv-mul-mul version.  -/
Finset.ruzsa_triangle_inequality_mulInv_mul_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] (A B C : Finset G),
  (A * C⁻¹).card * B.card ≤ (A * B).card * (C * B).card
-- Init.Data.Array.Basic
/-- Replaces the first occurrence of `a` with `b` in an array. The modification is performed in-place
when the reference to the array is unique. Returns the array unmodified when `a` is not present.

Examples:
* `#[1, 2, 3, 2, 1].replace 2 5 = #[1, 5, 3, 2, 1]`
* `#[1, 2, 3, 2, 1].replace 0 5 = #[1, 2, 3, 2, 1]`
* `#[].replace 2 5 = #[]`
 -/
Array.replace : {α : Type u} → [BEq α] → Array α → α → α → Array α
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- For even `k ≥ 3`, the rank of `𝒮ℒ` modular forms is one more than the rank of
cusp forms.  -/
ModularForm.rank_eq_one_add_rank_cuspForm : ∀ {k : ℕ},
  3 ≤ k →
    Even k →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
        1 + Module.rank ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSet.eq_1 : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} (s t : Set Ω) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.IndepSet s t μ =
    ProbabilityTheory.Kernel.IndepSet s t (ProbabilityTheory.Kernel.const Unit μ) (MeasureTheory.Measure.dirac ())
-- Mathlib.ModelTheory.Order
FirstOrder.Language.IsOrdered.mk : {L : FirstOrder.Language} → L.Relations 2 → L.IsOrdered
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- The function `n ↦ Λ n / n` restricted to primes in an invertible residue class
is not summable. This then implies that there must be infinitely many such primes.  -/
ArithmeticFunction.vonMangoldt.not_summable_residueClass_prime_div : ∀ {q : ℕ} [NeZero q] {a : ZMod q},
  IsUnit a → ¬Summable fun n => (if Nat.Prime n then ArithmeticFunction.vonMangoldt.residueClass a n else 0) / ↑n
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.norm.eq_def : ∀ (p : Lean.Grind.Linarith.Poly),
  p.norm =
    match p with
    | Lean.Grind.Linarith.Poly.nil => Lean.Grind.Linarith.Poly.nil
    | Lean.Grind.Linarith.Poly.add k v p => Lean.Grind.Linarith.Poly.insert k v p.norm
-- Mathlib.Data.Set.Prod
Set.singleton_pi' : ∀ {ι : Type u_1} {α : ι → Type u_2} (i : ι) (t : (i : ι) → Set (α i)), {i}.pi t = {x | x i ∈ t i}
-- Mathlib.Order.Fin.Basic
Fin.rev_top : ∀ {n : ℕ} [inst : NeZero n], ⊤.rev = ⊥
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- The walk obtained by removing the first dart of a walk. A nil walk stays nil.  -/
SimpleGraph.Walk.tail : {V : Type u} → {G : SimpleGraph V} → {u v : V} → (p : G.Walk u v) → G.Walk p.snd v
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.instIsEquivalenceMat_SingleObjMulOppositeEquivalenceSingleObjInverse : ∀ (R : Type) [inst : Ring R], (CategoryTheory.Mat.equivalenceSingleObjInverse R).IsEquivalence
-- Mathlib.Data.Finsupp.Defs
Finsupp.support_mapRange_of_injective : ∀ {ι : Type u_3} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] {e : M → N} (he0 : e 0 = 0)
  (f : ι →₀ M), Function.Injective e → (Finsupp.mapRange e he0 f).support = f.support
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.le_ofFunction : ∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {μ : MeasureTheory.OuterMeasure α},
  μ ≤ MeasureTheory.OuterMeasure.ofFunction m m_empty ↔ ∀ (s : Set α), μ s ≤ m s
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.image_Ioc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (a b : α),
  ⇑e '' Set.Ioc a b = Set.Ioc (e a) (e b)
-- Mathlib.Data.PNat.Factors
PrimeMultiset.prod_ofPNatMultiset : ∀ (v : Multiset ℕ+) (h : ∀ p ∈ v, p.Prime), (PrimeMultiset.ofPNatMultiset v h).prod = v.prod
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.neg_eq_mul_neg_one : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (a : α), -a = a * -1
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSeq.iSup_eq : ∀ {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)}, Ordinal.IsFundamentalSeq f → 1 < a → ⨆ i, ↑(f i) = o
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.Lan.CommuteWith.of_isKan_whisker : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] (t : CategoryTheory.Bicategory.LeftExtension f g) {x : B}
  (h : c ⟶ x) (H : (t.whisker h).IsKan) (i : t.whisker h ≅ (CategoryTheory.Bicategory.lanLeftExtension f g).whisker h),
  CategoryTheory.Bicategory.Lan.CommuteWith f g h
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.mul_right : ∀ {α : Type u_1} [inst : CommMonoid α] {a b c : α}, FiniteMultiplicity a (b * c) → FiniteMultiplicity a c
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
/-- For a `WeierstrassCurve` defined over a ring of characteristic = 3,
there is an explicit change of variables of it to `Y² = X³ + a₄X + a₆`
(`WeierstrassCurve.IsShortNF`) if its j = 0.
This is in fact given by `WeierstrassCurve.toCharNeTwoNF`.  -/
WeierstrassCurve.toShortNFOfCharThree : {R : Type u_1} → [inst : CommRing R] → WeierstrassCurve R → [CharP R 3] → WeierstrassCurve.VariableChange R
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.instInhabitedSubterminalsOfHasTerminal : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasTerminal C] → Inhabited (CategoryTheory.Subterminals C)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
/-- **Alias** of `CategoryTheory.Functor.coverPreserving_restrictedTopology`.

---

If `G` is locally fully faithful and locally cover dense, `G` is cover-preserving w.r.t. the
restricted topology.  -/
CategoryTheory.Functor.inducedTopology_coverPreserving : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K],
  CategoryTheory.CoverPreserving (G.restrictedTopology K) K G
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      [inst_1 : W₁.IsMultiplicative] →
        [inst_2 : W₂.IsMultiplicative] →
          {α : Type u_2} →
            [inst_3 : LinearOrder α] →
              [inst_4 : OrderBot α] →
                [inst_5 : SuccOrder α] →
                  [inst_6 : WellFoundedLT α] →
                    (deg : C → α) →
                      (∀ {X Y : C} (f : X ⟶ Y),
                          W₁ f → ¬CategoryTheory.MorphismProperty.identities C f → deg Y < deg X) →
                        (∀ {X Y : C} (f : X ⟶ Y),
                            W₂ f → ¬CategoryTheory.MorphismProperty.identities C f → deg X < deg Y) →
                          (∀ {X Y : C} (f : X ⟶ Y), Nonempty (Unique (W₁.MapFactorizationData W₂ f))) →
                            HomotopicalAlgebra.ReedyStructure W₁ W₂ α
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_sum : ∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  (f : R →+* S₁) (g : σ → S₁) (s : Finset S₂) (p : S₂ → MvPolynomial σ R),
  MvPolynomial.eval₂ f g (∑ x ∈ s, p x) = ∑ x ∈ s, MvPolynomial.eval₂ f g (p x)