mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.AEMeasurableOrder
/-- If a function `f : α → β` is such that the level sets `{f < p}` and `{q < f}` have measurable
supersets which are disjoint up to measure zero when `p < q`, then `f` is almost-everywhere
measurable. It is even enough to have this for `p` and `q` in a countable dense set.  -/
MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {β : Type u_2} [inst : CompleteLinearOrder β]
  [DenselyOrdered β] [inst_2 : TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β]
  [inst_5 : MeasurableSpace β] [BorelSpace β] (s : Set β),
  s.Countable →
    Dense s →
      ∀ (f : α → β),
        (∀ p ∈ s,
            ∀ q ∈ s,
              p < q →
                ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0) →
          AEMeasurable f μ
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.SearchState.mk.inj : ∀ {choiceStack : List Lean.Meta.Grind.EMatch.Choice} {instanceMap : Lean.Meta.Grind.EMatch.InstanceMap}
  {choiceStack_1 : List Lean.Meta.Grind.EMatch.Choice} {instanceMap_1 : Lean.Meta.Grind.EMatch.InstanceMap},
  { choiceStack := choiceStack, instanceMap := instanceMap } =
      { choiceStack := choiceStack_1, instanceMap := instanceMap_1 } →
    choiceStack = choiceStack_1 ∧ instanceMap = instanceMap_1
-- Std.Time.Date.PlainDate
/-- Returns the week-based year for the given `PlainDate`, using `firstDay` as the start of the week
and `minDays` as the minimum number of days in the first week of the year (default 4 for ISO 8601).
 -/
Std.Time.PlainDate.weekYear : Std.Time.PlainDate →
  optParam Std.Time.Weekday Std.Time.Weekday.monday →
    optParam (Std.Time.Internal.Bounded.LE 0 6)
        (Std.Time.Internal.Bounded.LE.mk 4 Std.Time.PlainDate.weekOfYear._proof_1) →
      Std.Time.Year.Offset
-- Mathlib.Analysis.Normed.Lp.PiLp
LinearIsometryEquiv.mk.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Semiring R] [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {E : Type u_11} {E₂ : Type u_12}
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (toLinearEquiv toLinearEquiv_1 : E ≃ₛₗ[σ₁₂] E₂) (e_toLinearEquiv : toLinearEquiv = toLinearEquiv_1)
  (norm_map' : ∀ (x : E), ‖toLinearEquiv x‖ = ‖x‖),
  { toLinearEquiv := toLinearEquiv, norm_map' := norm_map' } = { toLinearEquiv := toLinearEquiv_1, norm_map' := ⋯ }
-- Mathlib.Analysis.Complex.OperatorNorm
Complex.reCLM_nnnorm : ‖Complex.reCLM‖₊ = 1
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.unsafeRule.sizeOf_spec : ∀ (r : Aesop.UnsafeRule), sizeOf (Aesop.BaseRuleSetMember.unsafeRule r) = 1 + sizeOf r
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cyclesMap_comp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') {i'' j'' k'' : ι} (f'' : i'' ⟶ j'') (g'' : j'' ⟶ k'')
  (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g')
  (α' : CategoryTheory.ComposableArrows.mk₂ f' g' ⟶ CategoryTheory.ComposableArrows.mk₂ f'' g'')
  (α'' : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f'' g'') (n : ℤ),
  autoParam (CategoryTheory.CategoryStruct.comp α α' = α'')
      CategoryTheory.Abelian.SpectralObject.cyclesMap_comp._auto_1 →
    CategoryTheory.CategoryStruct.comp (X.cyclesMap f g f' g' α n) (X.cyclesMap f' g' f'' g'' α' n) =
      X.cyclesMap f g f'' g'' α'' n
-- Mathlib.Data.PNat.Defs
Nat.succPNat_coe : ∀ (n : ℕ), ↑n.succPNat = n.succ
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- The length-0 path at a vertex.  -/
SimpleGraph.Path.nil : {V : Type u} → {G : SimpleGraph V} → {u : V} → G.Path u u
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Given a collection of maps into the summands, we obtain a map into the biproduct.  -/
CategoryTheory.Limits.biproduct.lift : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {f : J → C} → [inst_2 : CategoryTheory.Limits.HasBiproduct f] → {P : C} → ((b : J) → P ⟶ f b) → (P ⟶ ⨁ f)
-- Mathlib.Tactic.CategoryTheory.Elementwise
/-- `elementwise_of% h`, where `h` is a proof of an equation `f = g` between
morphisms `X ⟶ Y` in a concrete category (possibly after a `∀` binder),
produces a proof of equation `∀ (x : X), f x = g x`, but with compositions fully
right associated and identities removed.

A typical example is using `elementwise_of%` to dynamically generate rewrite lemmas:
```lean
example (M N K : MonCat) (f : M ⟶ N) (g : N ⟶ K) (h : M ⟶ K) (w : f ≫ g = h) (m : M) :
    g (f m) = h m := by rw [elementwise_of% w]
```
In this case, `elementwise_of% w` generates the lemma `∀ (x : M), f (g x) = h x`.

Like the `@[elementwise]` attribute, `elementwise_of%` inserts a `ConcreteCategory`
instance argument if it can't synthesize a relevant `ConcreteCategory` instance.
(Technical note: The forgetful functor's universe variable is instantiated with a
fresh level metavariable in this case.)

One difference between `elementwise_of%` and `@[elementwise]` is that `@[elementwise]` by
default applies `simp` to both sides of the generated lemma to get something that is in simp
normal form. `elementwise_of%` does not do this.
 -/
Mathlib.Tactic.Elementwise.«termElementwise_of%_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.id_right : ∀ {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),
  (CategoryTheory.Limits.CatCospanTransform.id F G).right = CategoryTheory.Functor.id C
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.handlePlainGoal : Lean.Lsp.PlainGoalParams → Lean.Server.RequestM (Lean.Server.RequestTask (Option Lean.Lsp.PlainGoal))
-- Std.Time.Zoned.TimeZone
/-- Converts a `Timestamp` to a `WallTime` for a given timezone `offset`. The result is the local
civil time: `wall = UTC + offset`.
 -/
Std.Time.Timestamp.toWallTime : Std.Time.Timestamp → Std.Time.TimeZone.Offset → Std.Time.WallTime
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.forget_map : ∀ {W : Type v'} [inst : CategoryTheory.Category.{w', v'} W] [inst_1 : CategoryTheory.MonoidalCategory W] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory W C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory W D]
  (F : CategoryTheory.EnrichedFunctor W C D) {X Y : CategoryTheory.ForgetEnrichment W C} (f : X ⟶ Y),
  F.forget.map f =
    CategoryTheory.ForgetEnrichment.homOf W
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ForgetEnrichment.homTo W f)
        (F.map (CategoryTheory.ForgetEnrichment.to W X) (CategoryTheory.ForgetEnrichment.to W Y)))
-- Init.Data.BitVec.Lemmas
BitVec.concat_reverse_setWidth_msb_eq_reverse : ∀ {w : ℕ} {x : BitVec (w + 1)}, (BitVec.setWidth w x).reverse.concat x.msb = x.reverse
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_def : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G),
  ⁅H₁, H₂⁆ = Subgroup.closure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_le_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {k km : α}
  (hc : t.contains k = true), t.min?.get ⋯ = km → (cmp km k).isLE = true
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.coeFn_ofIsClosedGraph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_5} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {g : E →ₗ[𝕜] F} (hg : IsClosed ↑g.graph),
  ⇑(ContinuousLinearMap.ofIsClosedGraph hg) = ⇑g
-- Mathlib.Algebra.Homology.Localization
ComplexShape.quotient_isLocalization : ∀ {ι : Type u_1} (c : ComplexShape ι),
  (∀ (j : ι), ∃ i, c.Rel i j) →
    ∀ (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
      [CategoryTheory.Limits.HasBinaryBiproducts C],
      (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Arrow.changeProp_obj_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q W : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative] {P' Q' W' : CategoryTheory.MorphismProperty T}
  [inst_3 : Q'.IsMultiplicative] [inst_4 : W'.IsMultiplicative] (hPP' : P ≤ P') (hQQ' : Q ≤ Q') (hWW' : W ≤ W')
  (Y : P.Arrow Q W), ((CategoryTheory.MorphismProperty.Arrow.changeProp hPP' hQQ' hWW').obj Y).right = Y.right
-- Mathlib.GroupTheory.GroupAction.Hom
Pi.evalMulActionHom.eq_1 : ∀ {ι : Type u_1} {M : Type u_2} {X : ι → Type u_3} [inst : (i : ι) → SMul M (X i)] (i : ι),
  Pi.evalMulActionHom i = { toFun := Function.eval i, map_smul' := ⋯ }
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.user : Lean.Meta.Grind.EMatchTheoremKind
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_inf : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {p p' : NonUnitalSubring R} {x : R}, x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.rootSet_mapsTo : ∀ {T : Type w} [inst : CommRing T] {p : Polynomial T} [IsDomain T] {S : Type u_1} {S' : Type u_2} [inst_2 : CommRing S]
  [inst_3 : IsDomain S] [inst_4 : Algebra T S] [inst_5 : CommRing S'] [inst_6 : IsDomain S'] [inst_7 : Algebra T S']
  [Module.IsTorsionFree T S'] (f : S →ₐ[T] S'), Set.MapsTo (⇑f) (p.rootSet S) (p.rootSet S')
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasurableEmbedding.sigmaFinite_map : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {f : α → β},
  MeasurableEmbedding f → ∀ [MeasureTheory.SigmaFinite μ], MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.match_4.congr_eq_2 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (k : ℤ),
  x = Lean.Grind.CommRing.Expr.intCast k →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.intCast k => h_2 k
      | Lean.Grind.CommRing.Expr.natCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_2 k
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.node4L_lemma₅ : ∀ {a b c d : ℕ}, 3 * (b + c + 1 + d) ≤ 16 * a + 9 → 2 * d ≤ b + c + 1 → c ≤ 3 * b → c + d + 1 ≤ 3 * (a + b + 1)
-- Mathlib.Analysis.ODE.ExistUnique
/-- A version of `ODE_solution_unique_of_mem_Icc_right` for uniqueness in a closed interval whose
interior contains the initial time.  -/
ODE_solution_unique_of_mem_Icc : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal}
  {f g : ℝ → E} {a b t₀ : ℝ},
  (∀ t ∈ Set.Ioo a b, LipschitzOnWith K (v t) (s t)) →
    t₀ ∈ Set.Ioo a b →
      ContinuousOn f (Set.Icc a b) →
        (∀ t ∈ Set.Ioo a b, HasDerivAt f (v t (f t)) t) →
          (∀ t ∈ Set.Ioo a b, f t ∈ s t) →
            ContinuousOn g (Set.Icc a b) →
              (∀ t ∈ Set.Ioo a b, HasDerivAt g (v t (g t)) t) →
                (∀ t ∈ Set.Ioo a b, g t ∈ s t) → f t₀ = g t₀ → Set.EqOn f g (Set.Icc a b)
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.det_smul_adjugate_adjugate : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
  A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Eta-expanded form of `mvfderiv_smul` -/
mvfderiv_fun_smul : ∀ {𝕜 : 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_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {x : M} {a : M → 𝕜},
  MDiffAt a x → ∀ {g : M → F}, MDiffAt g x → (d% fun i => a i • g i) x = a x • d% g x + (d% a x).smulRight (g x)
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.lie_h_pow_toEnd_e : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {h e f : L}
  {m : M} {μ : R},
  IsSl2Triple h e f →
    ⁅h, m⁆ = μ • m →
      ∀ (n : ℕ), ⁅h, ((LieModule.toEnd R L M) e ^ n) m⁆ = (μ + 2 * ↑n) • ((LieModule.toEnd R L M) e ^ n) m
-- Mathlib.CategoryTheory.ComposableArrows.Three
CategoryTheory.ComposableArrows.threeδ₁Toδ₀_app_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {i j k l : C} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l)
  (f₁₂ : i ⟶ k) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂),
  (CategoryTheory.ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 1 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₂ f₁₂ f₃).obj 1)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- Bound for `|log x * x ^ t|` in the interval `(0, 1]`, for positive real `t`.  -/
Real.abs_log_mul_self_rpow_lt : ∀ (x t : ℝ), 0 < x → x ≤ 1 → 0 < t → |Real.log x * x ^ t| < 1 / t
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.instEssSurjMat_SingleObjMulOppositeEquivalenceSingleObjInverse : ∀ (R : Type) [inst : Ring R], (CategoryTheory.Mat.equivalenceSingleObjInverse R).EssSurj
-- Mathlib.MeasureTheory.Measure.Haar.DistribChar
/-- The distributive Haar character of a group `G` acting distributively on a group `A` is the
unique positive real number `Δ(g)` such that `μ (g • s) = Δ(g) * μ s` for all Haar
measures `μ : Measure A`, set `s : Set A` and `g : G`.  -/
MeasureTheory.distribHaarChar : {G : Type u_1} →
  (A : Type u_2) →
    [inst : Group G] →
      [inst_1 : AddCommGroup A] →
        [inst_2 : DistribMulAction G A] →
          [inst_3 : TopologicalSpace A] →
            [IsTopologicalAddGroup A] → [LocallyCompactSpace A] → [ContinuousConstSMul G A] → G →* NNReal
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- The natural map between pullback functors induced by `pullback.map`.  -/
CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q : CategoryTheory.MorphismProperty T} →
      [inst_1 : Q.IsMultiplicative] →
        [inst_2 : P.IsStableUnderComposition] →
          {X Y Z : T} →
            (f : X ⟶ Y) →
              (hPf : P f) →
                Q f →
                  (g : Y ⟶ Z) →
                    [inst_3 : P.IsStableUnderBaseChangeAlong f] →
                      [inst_4 : P.IsStableUnderBaseChangeAlong g] →
                        [inst_5 : Q.IsStableUnderBaseChange] →
                          [inst_6 : CategoryTheory.Limits.HasPullbacks T] →
                            (fg : optParam (X ⟶ Z) (CategoryTheory.CategoryStruct.comp f g)) →
                              (hfg :
                                  autoParam (CategoryTheory.CategoryStruct.comp f g = fg)
                                    CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback._auto_1) →
                                (CategoryTheory.MorphismProperty.Over.pullback P Q fg).comp
                                    (CategoryTheory.MorphismProperty.Over.map Q hPf) ⟶
                                  CategoryTheory.MorphismProperty.Over.pullback P Q g
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_maxKeyD_eq_maxKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {fallback : α} {he : Std.Internal.List.containsKey (Std.Internal.List.maxKeyD l fallback) l = true},
      Std.Internal.List.getKey (Std.Internal.List.maxKeyD l fallback) l he = Std.Internal.List.maxKey l ⋯
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_finsetSum_le : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] [inst_3 : ContinuousAdd V] {ι : Type u_3} (s : Finset ι)
  (μ : ι → MeasureTheory.VectorMeasure X V), (∑ i ∈ s, μ i).variation ≤ ∑ i ∈ s, (μ i).variation
-- Mathlib.Order.Monotone.Defs
Antitone.imp : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {a b : α},
  Antitone f → a ≤ b → f b ≤ f a
-- Mathlib.Order.Hom.Lattice
InfHomClass.toOrderHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : SemilatticeInf α]
  [inst_2 : SemilatticeInf β] [InfHomClass F α β], OrderHomClass F α β
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
ProbabilityTheory.iIndepFun.hasGaussianLaw_sum : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E]
  {ι : Type u_3} [inst_6 : Fintype ι] {X : ι → Ω → E},
  (∀ (i : ι), ProbabilityTheory.HasGaussianLaw (X i) P) →
    ProbabilityTheory.iIndepFun X P → ProbabilityTheory.HasGaussianLaw (∑ i, X i) P
-- Init.Data.Int.Order
Int.le_of_sub_le_sub_left : ∀ {a b c : ℤ}, c - a ≤ c - b → b ≤ a
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.zpow'_add : ∀ {α : Type u_1} [inst : GroupWithZero α] (a : α) (m n : ℤ),
  Mathlib.Tactic.FieldSimp.zpow' a (m + n) = Mathlib.Tactic.FieldSimp.zpow' a m * Mathlib.Tactic.FieldSimp.zpow' a n
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.GoodProducts.equiv_toFun_eq_eval : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I],
  (Profinite.NobelingProof.GoodProducts.equiv_range C).toFun =
    Set.rangeFactorization (Profinite.NobelingProof.GoodProducts.eval C)
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.imp_inf_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ θ : L.BoundedFormula α n},
  T.Imp φ (ψ ⊓ θ) ↔ T.Imp φ ψ ∧ T.Imp φ θ
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.one_hadamard_eq_one_iff : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : MulZeroOneClass α] {A : Matrix n n α},
  Matrix.hadamard 1 A = 1 ↔ A.diag = 1
-- Init.Data.Vector.Find
Vector.find?_push_eq_some : ∀ {α : Type} {n : ℕ} {a : α} {p : α → Bool} {b : α} {xs : Vector α n},
  Vector.find? p (xs.push a) = some b ↔ Vector.find? p xs = some b ∨ Vector.find? p xs = none ∧ p a = true ∧ a = b
-- Mathlib.Analysis.InnerProductSpace.Laplacian
tensorIteratedFDerivTwo.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  (e : E), tensorIteratedFDerivTwo 𝕜 f e = TensorProduct.lift (bilinearIteratedFDerivTwo 𝕜 f e)
-- Mathlib.Combinatorics.Graph.Delete
Graph.induce_vertexSet : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β), G.induce G.vertexSet = G
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.all_keys : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulHashable α]
  [EquivBEq α] {p : α → Bool}, m.WF → m.keys.all p = m.all fun a x => p a
-- Init.Tactics
/-- Applies the second constructor when
the goal is an inductive type with exactly two constructors, or fails otherwise.
```
example {p q : Prop} (h : q) : p ∨ q := by
  right
  exact h
```
 -/
Lean.Parser.Tactic.right : Lean.ParserDescr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {km : α}, t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ofLeftInverse_symm_apply : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {g : N →* G}
  (h : Function.LeftInverse ⇑g ⇑f) (x : ↥f.range), (MonoidHom.ofLeftInverse h).symm x = g ↑x
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mk'_smul_mk : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (T : Type u_1) [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : IsLocalization S T] (r : R) (m : M)
  (s s' : ↥S), IsLocalization.mk' T r s • LocalizedModule.mk m s' = LocalizedModule.mk (r • m) (s * s')
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- Constructing a bounded continuous function from a uniformly bounded
function on a discrete space, taking values in a normed group.  -/
BoundedContinuousFunction.ofNormedAddCommGroupDiscrete : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [DiscreteTopology α] →
        [inst_2 : SeminormedAddCommGroup β] →
          (f : α → β) → (C : ℝ) → (∀ (x : α), ‖f x‖ ≤ C) → BoundedContinuousFunction α β
-- Mathlib.Algebra.Polynomial.CancelLeads
Polynomial.dvd_cancelLeads_of_dvd_of_dvd : ∀ {R : Type u_1} [inst : CommRing R] {p q r : Polynomial R}, p ∣ q → p ∣ r → p ∣ q.cancelLeads r
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Scheme.instHasFiniteLimitsEtale : ∀ (X : AlgebraicGeometry.Scheme), CategoryTheory.Limits.HasFiniteLimits X.Etale
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId_inv_app_fst_app : ∀ {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] (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (X_2 : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F G X).inv.app X_1).fst.app X_2 =
    CategoryTheory.CategoryStruct.id (X_1.fst.obj X_2)
-- Mathlib.Topology.Homotopy.Lifting
IsQuotientCoveringMap.monodromy_eq_id_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {x : X} (e : ↑(p ⁻¹' {x}))
  {γ : FundamentalGroup X x}, ⋯.monodromy γ = id ↔ ⋯.monodromy γ e = e
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₃ = f.right.left
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitForall.go : Lean.LocalContext →
  Array Lean.Expr → Array Lean.Meta.LetToHave.Result✝ → Lean.Expr → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝