mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {a : α}, m.contains a = false → m[a]! = default
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.coeFn_empty : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω), ν ∅ = 0
-- Init.Data.List.Lemmas
List.ext_getElem?_iff : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ = l₂ ↔ ∀ (i : ℕ), l₁[i]? = l₂[i]?
-- Init.Data.UInt.Lemmas
USize.ofNat.eq_1 : ∀ (n : ℕ), USize.ofNat n = { toBitVec := BitVec.ofNat System.Platform.numBits n }
-- ProofWidgets.Presentation.Expr
/-- Register an Expr presenter. It must have the type `ProofWidgets.ExprPresenter`.  -/
ProofWidgets.exprPresenters : Lean.TagAttribute
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Finsupp.linearIndependent_single_iff : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {φ : ι → Type u_4} {f : (i : ι) → φ i → M},
  (LinearIndependent R fun ix => fun₀ | ix.fst => f ix.fst ix.snd) ↔ ∀ (i : ι), LinearIndependent R (f i)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_roo_eq_zero_iff : ∀ {m n : ℤ} {i : ℕ}, (m<...n).toList[i]! = 0 ↔ (n - (m + 1)).toNat ≤ i ∨ m + ↑i = -1
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], (m₁ \ m₂)[k]! = if k ∈ m₂ then default else m₁[k]!
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
summableUniformly_iff_hasSumUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α],
  SummableUniformly f ↔ HasSumUniformly f fun x => ∑' (i : ι), f i x
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.HasAnchor : Type u → Type u
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainBotCoeff_chainTopIdx : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  RootPairing.chainBotCoeff i (RootPairing.chainTopIdx i j) =
    RootPairing.chainBotCoeff i j + RootPairing.chainTopCoeff i j
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.Cache.mk.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {sα : Q(CommSemiring «$α»)} (rα : Option Q(CommRing «$α»))
  (dsα : Option Q(Semifield «$α»)) (czα : Option Q(CharZero «$α»)),
  sizeOf { rα := rα, dsα := dsα, czα := czα } = 1 + sizeOf rα + sizeOf dsα + sizeOf czα
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- See `Multipliable.congr_cofinite` for a version allowing the functions to
disagree on a finite set.  -/
Multipliable.congr : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β}, Multipliable f L → (∀ (b : β), f b = g b) → Multipliable g L
-- Lean.Server.FileWorker.SignatureHelp
/-- Cursor is in the position of the trailing whitespace of some term. Medium precedence.
Ensures that `fun otherFun <cursor>` yields the signature help of `fun`, not `otherFun`.
 -/
Lean.Server.FileWorker.SignatureHelp.CandidateKind.termArg : Lean.Server.FileWorker.SignatureHelp.CandidateKind
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_neg_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), inner 𝕜 x (-y) = -inner 𝕜 x y
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coe_neg`. -/
CuspForm.coe_neg : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Neg F] [inst_2 : Neg β]
  [IsNegApply F α β] (f : F), ⇑(-f) = -⇑f
-- Mathlib.CategoryTheory.Monad.Limits
/-- If `C` has limits then any coreflective subcategory has limits.  -/
CategoryTheory.hasLimits_of_coreflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (R : CategoryTheory.Functor D C) [CategoryTheory.Coreflective R]
  [CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₁, u₁} C], CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₂, u₂} D
-- Mathlib.Data.Finset.Basic
Finset.toList_empty : ∀ {α : Type u_1}, ∅.toList = []
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.unop_i₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Cᵒᵖ} (P : HomotopicalAlgebra.PrepathObject A),
  P.unop.i₁ = P.p₁.unop
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.initial_of_initial_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.Initial] [(F.comp G).Initial], G.Initial
-- Mathlib.Order.Minimal
MaximalFor.minimal_of_strictAntiOn : ∀ {α : Type u_2} {β : Type u_3} {P : α → Prop} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {g : α → β},
  StrictAntiOn g (Set.ofPred P) → MaximalFor P g x → Minimal P x
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideCoequalizer.cotrident_π : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y))
  [inst_1 : CategoryTheory.Limits.HasWideCoequalizer f],
  (CategoryTheory.Limits.wideCoequalizer.cotrident f).π = CategoryTheory.Limits.wideCoequalizer.π f
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- Given `f` a linear map into multilinear maps, then the derivative
of `x ↦ f (a x) (b₁ x, ..., bₙ x)` at `x` applied to a vector `v` is given by
`f (a' v) (b₁ x, ...., bₙ x) + ∑ i, f a (b₁ x, ..., b'ᵢ v, ..., bₙ x)`.  -/
HasFDerivAt.linear_multilinear_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {ι : Type u_2}
  {G : ι → Type u_3} [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)]
  [inst_7 : Fintype ι] {H : Type u_4} [inst_8 : NormedAddCommGroup H] [inst_9 : NormedSpace 𝕜 H]
  [inst_10 : DecidableEq ι] {a : H → E} {a' : H →L[𝕜] E} {b : (i : ι) → H → G i} {b' : (i : ι) → H →L[𝕜] G i} {x : H},
  HasFDerivAt a a' x →
    (∀ (i : ι), HasFDerivAt (b i) (b' i) x) →
      ∀ (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F),
        HasFDerivAt (fun y => (f (a y)) fun i => b i y)
          ((f.flipMultilinear fun i => b i x) ∘SL a' + ∑ i, (f (a x)).toContinuousLinearMap (fun j => b j x) i ∘SL b' i)
          x
-- Mathlib.Data.Finset.Lattice.Fold
Finset.ofDual_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s : Finset β) (f : β → αᵒᵈ),
  OrderDual.ofDual (s.sup f) = s.inf (⇑OrderDual.ofDual ∘ f)
-- Mathlib.Order.Hom.WithTopBot
WithBot.toDualTopEquiv.eq_1 : ∀ {α : Type u_1} [inst : LE α], WithBot.toDualTopEquiv = OrderIso.refl (WithBot αᵒᵈ)
-- Mathlib.RingTheory.LocalRing.Module
/-- [Stacks Tag 02M9](https://stacks.math.columbia.edu/tag/02M9) -/
Module.free_of_flat_of_finrank_eq : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [Finite (MaximalSpectrum R)] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.Finite R M] [Module.Flat R M] (n : ℕ),
  (∀ (P : MaximalSpectrum R), Module.finrank (R ⧸ P.asIdeal) (TensorProduct R (R ⧸ P.asIdeal) M) = n) → Module.Free R M
-- Init.Data.Array.Basic
Array.isEqvAux : {α : Type u} → (xs ys : Array α) → xs.size = ys.size → (α → α → Bool) → (i : ℕ) → i ≤ xs.size → Bool
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (h : μ.MutuallySingular ν),
  MeasurableSet h.nullSet
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.ofMatroid_lt_iff : ∀ {α : Type u_1} {M M' : Matroid α}, { toMatroid := M } < { toMatroid := M' } ↔ M.IsStrictRestriction M'
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.forM_eq_forM : ∀ {α : Type u} {m : Std.HashSet.Raw α} {m' : Type v → Type w} [inst : Monad m'] [LawfulMonad m']
  {f : α → m' PUnit.{v + 1}}, Std.HashSet.Raw.forM f m = forM m f
-- Lean.Elab.MutualInductive
/-- The constraint `u ≤ ?r + k` is represented by `levels[u] := k`.
When `k` is negative, this represents `u + (-k) ≤ ?r`.
The level `u` is either a parameter, metavariable, or `Level.zero`.

When `k ≥ 0`, this is potentially a "bad" level constraint.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AccLevelState.levels : Lean.Elab.Command.AccLevelState✝ → Lean.LevelMap ℤ
-- Mathlib.Analysis.Normed.Group.Basic
ne_zero_of_norm_ne_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a : E}, ‖a‖ ≠ 0 → a ≠ 0
-- Mathlib.Analysis.Normed.Algebra.Exponential
Prod.snd_exp : ∀ {𝔸 : Type u_1} {𝔹 : Type u_2} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] [inst_3 : NormedRing 𝔹]
  [NormedAlgebra ℚ 𝔹] [CompleteSpace 𝔹] (x : 𝔸 × 𝔹), (NormedSpace.exp x).2 = NormedSpace.exp x.2
-- Lean.CoreM
Lean.instMonadDeclNameGeneratorOfMonadLift : {m n : Type → Type} → [MonadLift m n] → [Lean.MonadDeclNameGenerator m] → Lean.MonadDeclNameGenerator n
-- Init.Data.String.Subslice
String.Slice.Subslice.cast.congr_simp : ∀ {s t : String.Slice} (h : s.copy = t.copy) (sl sl_1 : s.Subslice),
  sl = sl_1 → String.Slice.Subslice.cast h sl = String.Slice.Subslice.cast h sl_1
-- Mathlib.Order.SupClosed
latticeClosure.eq_1 : ∀ {α : Type u_3} [inst : Lattice α], latticeClosure = ClosureOperator.ofCompletePred IsSublattice ⋯
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1CLM_of_aestronglyMeasurable' : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)]
  [inst_3 : CompleteSpace F'] (f : ↥(MeasureTheory.Lp F' 1 μ)),
  MeasureTheory.AEStronglyMeasurable (↑↑f) μ → (MeasureTheory.condExpL1CLM F' hm μ) f = f
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.fst_map_id_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) {f : β → γ},
  Measurable f → (κ.map fun a => (a, f a)).fst = κ
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_apply_anti : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] (u : ι → Ω → β) (n m : ι)
  (ω : Ω), Antitone fun x => MeasureTheory.hittingBtwn u x n m ω
-- Lean.Server.Completion.CompletionUtils
Lean.String.charactersIn : String → String → Bool
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.ι₁_desc_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F K : HomologicalComplex C c} [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder]
  (φ₀ φ₁ : K ⟶ F) (h : Homotopy φ₀ φ₁) {Z : HomologicalComplex C c} (h_1 : F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₁ K)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.desc φ₀ φ₁ h) h_1) =
    CategoryTheory.CategoryStruct.comp φ₁ h_1
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuousWithinAt_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {x : α} {s : Set α},
  UpperSemicontinuousWithinAt f s x ↔ ∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, f x' ≥ y) → f x ≥ y
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instZero : {R : Type u_3} → {A : Type u_4} → [Zero R] → [Zero A] → Zero (Unitization R A)
-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
TensorialAt.mkHom₂_apply_eq_extend : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {F' : Type u_7}
  [inst_13 : NormedAddCommGroup F'] [inst_14 : NormedSpace 𝕜 F'] {V' : M → Type u_8}
  [inst_15 : TopologicalSpace (Bundle.TotalSpace F' V')] [inst_16 : (x : M) → AddCommGroup (V' x)]
  [inst_17 : (x : M) → Module 𝕜 (V' x)] [inst_18 : (x : M) → TopologicalSpace (V' x)] [inst_19 : FiberBundle F' V']
  {A : Type u_9} [inst_20 : AddCommGroup A] [inst_21 : Module 𝕜 A] [inst_22 : VectorBundle 𝕜 F V]
  [inst_23 : VectorBundle 𝕜 F' V'] [inst_24 : CompleteSpace 𝕜] [inst_25 : FiniteDimensional 𝕜 F]
  [inst_26 : FiniteDimensional 𝕜 F'] [inst_27 : ContMDiffVectorBundle 1 F V I]
  [inst_28 : ContMDiffVectorBundle 1 F' V' I] [inst_29 : TopologicalSpace A] [inst_30 : IsTopologicalAddGroup A]
  [inst_31 : ContinuousSMul 𝕜 A] {Φ : ((x : M) → V x) → ((x : M) → V' x) → A} {x : M}
  (hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun x => Φ x τ) x)
  (hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (Φ σ) x) (σ : V x) (τ : V' x),
  (⋯ σ) τ = Φ (FiberBundle.extend F σ) (FiberBundle.extend F' τ)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.toList_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} {f : α → β → Bool},
  t.WF →
    Std.DTreeMap.Raw.Const.toList (Std.DTreeMap.Raw.filter f t) =
      List.filter (fun p => f p.1 p.2) (Std.DTreeMap.Raw.Const.toList t)
-- Lean.Widget.UserWidget
Lean.Widget.instFromJsonGetWidgetSourceParams : Lean.FromJson Lean.Widget.GetWidgetSourceParams
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.isOpenEmbedding_mk : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsOpenEmbedding ⇑DomAddAct.mk
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instAddCommSemigroupQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : SMul S M] → [inst_1 : AddCommSemigroup M] → (c : ModuleCon S M) → AddCommSemigroup (ModuleCon.Quotient M c)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toListRev_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {it : Std.IterM m β},
  it.toListRev = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => do
        let __do_lift ← it'.toListRev
        pure (__do_lift ++ [out])
      | Std.IterStep.skip it' => it'.toListRev
      | Std.IterStep.done => pure []
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instIsRightCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsRightCancelAdd α], IsRightCancelAdd αᵒᵈ
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkAppS₆ : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] →
    [Monad m] → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The space of multilinear maps over an algebra over `R` is a module over `R`, for the pointwise
addition and scalar multiplication.  -/
MultilinearMap.instModule : {R : Type uR} →
  {S : Type uS} →
    {ι : Type uι} →
      {M₁ : ι → Type v₁} →
        {M₂ : Type v₂} →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : (i : ι) → Module R (M₁ i)] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M₂] →
                    [inst_5 : Semiring S] →
                      [inst_6 : Module S M₂] → [SMulCommClass R S M₂] → Module S (MultilinearMap R M₁ M₂)
-- Init.Data.String.Basic
String.Pos.toSlice_le_toSlice_iff : ∀ {s : String} {p q : s.Pos}, p.toSlice ≤ q.toSlice ↔ p ≤ q
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_inj : ∀ {o₁ o₂ : Ordinal.{u_1}}, Cardinal.preBeth o₁ = Cardinal.preBeth o₂ ↔ o₁ = o₂
-- Mathlib.Algebra.Order.Monovary
/-- Two functions monovary iff the rearrangement inequality holds.  -/
monovary_iff_smul_rearrangement : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β},
  Monovary f g ↔ ∀ (i j : ι), f i • g j + f j • g i ≤ f i • g i + f j • g j
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
ofAdd_image_zmultiples_eq_zpowers_ofAdd : ∀ {A : Type u_2} [inst : AddGroup A] {x : A},
  ⇑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x) = ↑(Subgroup.zpowers (Multiplicative.ofAdd x))
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.toGeneratedByTopCat_map_apply : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y Z : ContinuousGeneratedByCat X} (f : Y ⟶ Z)
  (y : Topology.WithGeneratedByTopology X ↑Y),
  (CategoryTheory.ConcreteCategory.hom (ContinuousGeneratedByCat.toGeneratedByTopCat.map f)) y =
    Topology.WithGeneratedByTopology.equiv.symm
      ((CategoryTheory.ConcreteCategory.hom f) (Topology.WithGeneratedByTopology.equiv y))
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.drop.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_succ : ∀ {w i : ℕ} (x : BitVec w), BitVec.setWidth (i + 1) x = BitVec.cons (x.getLsbD i) (BitVec.setWidth i x)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.toEquiv_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), (↑e.symm).toEquiv = (↑e).symm
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet.isProbabilityMeasure : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set Ω},
  ProbabilityTheory.iIndepSet s μ → MeasureTheory.IsProbabilityMeasure μ
-- Mathlib.Data.Seq.Defs
Stream'.Seq.destruct_cons : ∀ {α : Type u} (a : α) (s : Stream'.Seq α), (Stream'.Seq.cons a s).destruct = some (a, s)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.hasProduct_unique : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [Nonempty β] [Subsingleton β] (f : β → C),
  CategoryTheory.Limits.HasProduct f
-- Mathlib.Data.Finset.Image
Finset.iterate_image : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α] (f : α → α) (n : ℕ),
  (Finset.image f)^[n] s = Finset.image f^[n] s
-- Mathlib.CategoryTheory.Sites.Localization
/-- SGA 4 III 1.2 (ii) => (i)  -/
CategoryTheory.Presieve.IsSheaf.comp_of_W_map_of_adjunction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_3, u_3} D] {K : CategoryTheory.GrothendieckTopology D}
  [inst_2 : CategoryTheory.LocallySmall.{w, v_1, u_1} C] {F : CategoryTheory.Functor C D}
  {H : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type w)) (CategoryTheory.Functor Dᵒᵖ (Type w))}
  (adj : H ⊣ (CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)).obj F.op),
  (∀ ⦃X : C⦄ ⦃S : CategoryTheory.Sieve X⦄,
      S ∈ J X → K.W (H.map (CategoryTheory.Sieve.shrinkFunctor.{w, v_1, u_1} S).ι)) →
    ∀ (G : CategoryTheory.Functor Dᵒᵖ (Type w)),
      CategoryTheory.Presieve.IsSheaf K G → CategoryTheory.Presieve.IsSheaf J (F.op.comp G)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Icc_eq_integral_Ioc : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x y : X} [MeasureTheory.NullSingletonClass μ],
  ∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ioc x y, f t ∂μ
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instNonUnitalSeminormedCommRing : {α : Type u} →
  [inst : TopologicalSpace α] →
    {R : Type u_1} →
      [inst_1 : NonUnitalSeminormedCommRing R] → NonUnitalSeminormedCommRing (BoundedContinuousFunction α R)
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.indep_iff_forall_notMem_closure_sdiff'`.

---

An alternative version of `Matroid.indep_iff_forall_notMem_closure_sdiff` where the
hypothesis that `I ⊆ M.E` is contained in the RHS rather than the hypothesis.  -/
Matroid.indep_iff_forall_notMem_closure_diff' : ∀ {α : Type u_2} {M : Matroid α} {I : Set α}, M.Indep I ↔ I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_mul_le_of_le : ∀ {R : Type u} {n m : ℕ} [inst : Semiring R] {p q : Polynomial R},
  p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n
-- Mathlib.Probability.ProductMeasure
/-- The product measure is the projective limit of the partial product measures. This ensures
uniqueness and expresses the value of the product measure applied to cylinders.  -/
MeasureTheory.Measure.isProjectiveLimit_infinitePi : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)],
  MeasureTheory.IsProjectiveLimit (MeasureTheory.Measure.infinitePi μ) fun I => MeasureTheory.Measure.pi fun i => μ ↑i
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Hom.id.eq_1 : ∀ (a : SimplexCategory), SimplexCategory.Hom.id a = SimplexCategory.Hom.mk OrderHom.id
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Combinatorics.Quiver.Path.Vertices
/-- The head of the vertices list is the start vertex  -/
Quiver.Path.vertices_head? : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), p.vertices.head? = some a
-- Init.Data.Option.Lemmas
Option.join_eq_none_iff : ∀ {α : Type u_1} {o : Option (Option α)}, o.join = none ↔ o = none ∨ o = some none
-- Init.Data.UInt.Bitwise
USize.ofBitVec_shiftRight_mod : ∀ (a : BitVec System.Platform.numBits) (b : ℕ),
  { toBitVec := a >>> (b % System.Platform.numBits) } = { toBitVec := a } >>> USize.ofNat b
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.instPseudoMetricSpace : {𝕜 : Type u_1} →
  {V : Type u_3} →
    {W : Type u_4} →
      {Q : Type u_6} →
        [inst : SeminormedAddCommGroup V] →
          [inst_1 : SeminormedAddCommGroup W] →
            [inst_2 : NontriviallyNormedField 𝕜] →
              [inst_3 : NormedSpace 𝕜 V] →
                [inst_4 : NormedSpace 𝕜 W] →
                  [inst_5 : PseudoMetricSpace Q] → [inst_6 : NormedAddTorsor W Q] → PseudoMetricSpace (V →ᴬ[𝕜] Q)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Ring.mulFn? : Lean.Meta.Grind.Arith.CommRing.Ring → Option Lean.Expr
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.tendsto_zero_of_tendsto : ∀ {α : Type u_1} {E' : Type u_6} {𝕜 : Type u_15} [inst : SeminormedAddCommGroup E'] [inst_1 : NormedDivisionRing 𝕜]
  {u : α → E'} {v : α → 𝕜} {l : Filter α} {y : 𝕜}, u =o[l] v → Filter.Tendsto v l (nhds y) → Filter.Tendsto u l (nhds 0)