mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k a : α} {fallback : β a} {v : β k},
      (Std.DTreeMap.Internal.Impl.insert! k v t).getD a fallback =
        if h : compare k a = Ordering.eq then cast ⋯ v else t.getD a fallback
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.heq_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z X' Y' Z' : C} {f : X ⟶ Y} {g : Y ⟶ Z}
  {f' : X' ⟶ Y'} {g' : Y' ⟶ Z'},
  X = X' →
    Y = Y' →
      Z = Z' → f ≍ f' → g ≍ g' → CategoryTheory.CategoryStruct.comp f g ≍ CategoryTheory.CategoryStruct.comp f' g'
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {k a : α} {v : β},
  Std.ExtDTreeMap.Const.get! (t.insert k v) a = if cmp k a = Ordering.eq then v else Std.ExtDTreeMap.Const.get! t a
-- Mathlib.Algebra.Star.Basic
/-- Closure under star.  -/
StarMemClass.star_mem : ∀ {S : Type u_1} {R : Type u_2} {inst : Star R} {inst_1 : SetLike S R} [self : StarMemClass S R] {s : S} {r : R},
  r ∈ s → star r ∈ s
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.seminormedAddGroup : {E : Type u_2} → [SeminormedAddGroup E] → SeminormedAddGroup (ULift.{u_5, u_2} E)
-- Init.System.IO
/-- Whether a file should be opened for reading, writing, creation and writing, or appending.

At the operating system level, this translates to the mode of a file handle (i.e., a set of `open`
flags and an `fdopen` mode).

None of the modes represented by this datatype translate line endings (i.e. `O_BINARY` on Windows).
Furthermore, they are not inherited across process creation (i.e. `O_NOINHERIT` on Windows and
`O_CLOEXEC` elsewhere).

**Operating System Specifics:**
* Windows:
  [`_open`](https://learn.microsoft.com/en-us/cpp/c-runtime-library/reference/open-wopen?view=msvc-170),
  [`_fdopen`](https://learn.microsoft.com/en-us/cpp/c-runtime-library/reference/fdopen-wfdopen?view=msvc-170)
* Linux: [`open`](https://linux.die.net/man/2/open), [`fdopen`](https://linux.die.net/man/3/fdopen)
 -/
IO.FS.Mode : Type
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- A chosen `S.LeftHomologyData` for a short complex `S` that has left homology  -/
CategoryTheory.ShortComplex.leftHomologyData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [S.HasLeftHomology] → S.LeftHomologyData
-- Init.Data.Ord.Basic
Ord.mk : {α : Type u} → (α → α → Ordering) → Ord α
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.fundamentalDomain_stdBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  ZSpan.fundamentalDomain (NumberField.mixedEmbedding.stdBasis K) =
    (Set.univ.pi fun x => Set.Ico 0 1) ×ˢ
      Set.univ.pi fun x => ⇑Complex.measurableEquivPi ⁻¹' Set.univ.pi fun x => Set.Ico 0 1
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbit.coe_vadd : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] {a : α} {m : M}
  {a' : ↑(AddAction.orbit M a)}, ↑(m +ᵥ a') = m +ᵥ ↑a'
-- Mathlib.Analysis.SpecificLimits.Normed
geom_series_eq_inverse : ∀ {R : Type u_4} [inst : NormedRing R] [HasSummableGeomSeries R] (x : R),
  ‖x‖ < 1 → ∑' (i : ℕ), x ^ i = Ring.inverse (1 - x)
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.labelledCopyCount_eq_zero : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V] [inst_1 : Fintype W],
  G.labelledCopyCount H = 0 ↔ H.Free G
-- Mathlib.Tactic.NormNum.Prime
Mathlib.Meta.NormNum.minFacHelper_1 : ∀ {n k k' : ℕ},
  k + 2 = k' → Mathlib.Meta.NormNum.MinFacHelper n k → n.minFac ≠ k → Mathlib.Meta.NormNum.MinFacHelper n k'
-- Mathlib.Data.Sum.Basic
Sum.inr_injective : ∀ {α : Type u} {β : Type v}, Function.Injective Sum.inr
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mrange_eq_top : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F}, MonoidHom.mrange f = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_neg : ∀ (x : ℝ), Real.arccos (-x) = Real.pi - Real.arccos x
-- Mathlib.Algebra.Group.PNatPowAssoc
ppow_add : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Pow M ℕ+] [PNatPowAssoc M] (k n : ℕ+) (x : M), x ^ (k + n) = x ^ k * x ^ n
-- Mathlib.Order.Category.Semilat
/-- The equivalence between `SemilatSupCat` and `SemilatInfCat` induced by `OrderDual` both ways.  -/
SemilatSupCatEquivSemilatInfCat : SemilatSupCat ≌ SemilatInfCat
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Poly.isZero.match_1.splitter : (motive : Nat.Internal.Linear.Poly → Sort u_1) →
  (p : Nat.Internal.Linear.Poly) →
    (Unit → motive []) → ((x : Nat.Internal.Linear.Poly) → (x = [] → False) → motive x) → motive p
-- Std.Net.Addr
Std.Net.instInhabitedIPv4Addr.default : Std.Net.IPv4Addr
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.instIsFractionRingPowerSeries : ∀ {K : Type u_2} [inst : Field K], IsFractionRing (PowerSeries K) (LaurentSeries K)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.coe_mul : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (e₁ e₂ : α ≃ᵢ α), ⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂
-- Lean.Parser.Do
Lean.Parser.Term.doExpr.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
HasEnoughRootsOfUnity.prim : ∀ {M : Type u_1} {inst : CommMonoid M} {n : ℕ} [self : HasEnoughRootsOfUnity M n], ∃ m, IsPrimitiveRoot m n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_ofList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  List.Pairwise (fun a b => (a.1 == b.1) = false) l → (Std.DHashMap.Raw.Const.ofList l).size = l.length
-- Mathlib.Tactic.GRewrite.Elab
/-- Function elaborating `GRewrite.Config`.  -/
_private.Mathlib.Tactic.GRewrite.Elab.0.Mathlib.Tactic.GRewrite.elabGRewriteConfig : Lean.Syntax →
  optParam Mathlib.Tactic.GRewrite.Config { } →
    optParam Bool true → Lean.Elab.Tactic.TacticM Mathlib.Tactic.GRewrite.Config
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.zero_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZeroClass N] (x : M), 0 x = 0
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod_cons : ∀ {M : Type u_3} [inst : CommMonoid M] (a : M) (s : Multiset M), (a ::ₘ s).prod = a * s.prod
-- Mathlib.Data.List.Basic
List.get_surjective_iff : ∀ {α : Type u} {l : List α}, Function.Surjective l.get ↔ ∀ (x : α), x ∈ l
-- Init.PropLemmas
And.imp_right : ∀ {a b c : Prop}, (a → b) → c ∧ a → c ∧ b
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.ι_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (c : C)
  (d : ↑(F.obj c)), (CategoryTheory.Grothendieck.ι F c).obj d = { base := c, fiber := d }
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection onto a subspace.  -/
Submodule.orthogonalProjectionOnto : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → (K : Submodule 𝕜 E) → [K.HasOrthogonalProjection] → E →L[𝕜] ↥K
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ : J.Point}
  (hom hom_1 : Φ₂.fiber ⟶ Φ₁.fiber), ({ hom := hom } = { hom := hom_1 }) = (hom = hom_1)
-- Mathlib.Algebra.Group.Basic
sub_zsmul : ∀ {G : Type u_3} [inst : AddGroup G] (a : G) (m n : ℤ), (m - n) • a = m • a + -(n • a)
-- Mathlib.Analysis.Analytic.CPolynomial
CPolynomialOn.add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  CPolynomialOn 𝕜 f s → CPolynomialOn 𝕜 g s → CPolynomialOn 𝕜 (f + g) s
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
ediam_smul_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedAddCommGroup 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E] (c : 𝕜) (s : Set E), Metric.ediam (c • s) ≤ ‖c‖₊ • Metric.ediam s
-- Mathlib.Algebra.Divisibility.Units
IsUnit.isRelPrime_right : ∀ {α : Type u_1} [inst : CommMonoid α] {x y : α}, IsUnit y → IsRelPrime x y
-- Mathlib.Analysis.Convex.Body
ConvexBody.coe_add : ∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V] [inst_3 : ContinuousAdd V]
  (K L : ConvexBody V), ↑(K + L) = ↑K + ↑L
-- Mathlib.Combinatorics.Derangements.Finite
/-- The number of derangements of an `n`-element set.  -/
numDerangements : ℕ → ℕ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.addMap_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P Q : Fin 3 → R),
  W'.addMap ⟦P⟧ ⟦Q⟧ = ⟦W'.add P Q⟧
-- Init.Data.Order.Lemmas
Std.lt_trichotomy : ∀ {α : Type u_1} [inst : LT α] [Std.Trichotomous fun x1 x2 => x1 < x2] (a b : α), a < b ∨ a = b ∨ b < a
-- Init.Data.Array.Lemmas
Array.any_eq : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, xs.any p = decide (∃ i, ∃ (h : i < xs.size), p xs[i] = true)
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- Negation in `ℤ√d`  -/
Zsqrtd.instNeg : {d : ℤ} → Neg (ℤ√d)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget.start : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {w : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget aig w → ℕ
-- Mathlib.Order.Filter.Bases.Basic
Filter.IsBasis.mem_filterBasis_iff : ∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) {U : Set α},
  U ∈ h.filterBasis ↔ ∃ i, p i ∧ s i = U
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero_aux2 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E),
  Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
      (nhds 0) →
    ∀ (t u : Set E),
      μ u ≠ 0 →
        ∀ (R : ℝ),
          0 < R →
            t ⊆ Metric.closedBall 0 R →
              Filter.Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
-- Mathlib.Topology.Order
TopologicalSpace.GenerateOpen.inter : ∀ {α : Type u} {g : Set (Set α)} (s t : Set α),
  TopologicalSpace.GenerateOpen g s → TopologicalSpace.GenerateOpen g t → TopologicalSpace.GenerateOpen g (s ∩ t)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.mk : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] →
        (toContinuousMap : C(α, β)) →
          (∃ C, ∀ (x y : α), dist (toContinuousMap.toFun x) (toContinuousMap.toFun y) ≤ C) →
            BoundedContinuousFunction α β
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The set of continuous functions is closed in the uniform convergence topology.
This is a simple wrapper over `TendstoUniformly.continuous`.  -/
UniformFun.isClosed_setOfPred_continuous : ∀ (α : Type u_1) {β : Type u_2} [inst : UniformSpace β] [inst_1 : TopologicalSpace α],
  IsClosed {f | Continuous (UniformFun.toFun f)}
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.wEquiv.refl : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : (MvQPF.P F).W α), MvQPF.WEquiv x x
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.comp_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₂ ⟶ S₃} {h₁ : S₁.RightHomologyData}
  {h₂ : S₂.RightHomologyData} {h₃ : S₃.RightHomologyData} (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
  (ψ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₂ h₃),
  (ψ.comp ψ').φH = CategoryTheory.CategoryStruct.comp ψ.φH ψ'.φH
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.instInhabitedTriangle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      [CategoryTheory.Limits.HasZeroObject C] →
        [CategoryTheory.Limits.HasZeroMorphisms C] → Inhabited (CategoryTheory.Pretriangulated.Triangle C)
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `none` if no such pair exists.
 -/
Std.ExtTreeMap.getEntryLT? : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → Option (α × β)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balance!_desc : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  l.Balanced →
    r.Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size ∨
          Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size →
        (Std.DTreeMap.Internal.Impl.balance! k v l r).size = l.size + 1 + r.size ∧
          (Std.DTreeMap.Internal.Impl.balance! k v l r).Balanced
-- Mathlib.Analysis.Analytic.Order
analyticOrderAt_mul_eq_top_of_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {z₀ : 𝕜},
  analyticOrderAt f z₀ = ⊤ → analyticOrderAt (f * g) z₀ = ⊤
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.measurableSet_mulSupport : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} [inst : One β] [inst_1 : TopologicalSpace β]
  [TopologicalSpace.MetrizableSpace β], MeasureTheory.StronglyMeasurable f → MeasurableSet (Function.mulSupport f)
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_left_congr : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {v : V} {p q : P}, inner ℝ v (p -ᵥ q) = 0 → (signedDist v) p = (signedDist v) q
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
/-- *Note: This is a very general combinator that requires an advanced understanding of monads, dependent
types and termination proofs. The variants `map` and `mapM` are easier to use and sufficient
for most use cases.*

If `it` is an iterator, then `it.mapWithPostcondition f` is another iterator that applies a monadic
function `f` to all values emitted by `it` and emits the result.

`f` is expected to return `PostconditionT n _`. The base iterator `it` being monadic in
`m`, `n` can be different from `m`, but `it.mapWithPostcondition f` expects a `MonadLiftT m n`
instance. The `PostconditionT` transformer allows the caller to intrinsically prove properties about
`f`'s return value in the monad `n`, enabling termination proofs depending on the specific behavior
of `f`.

**Marble diagram (without monadic effects):**

```text
it                          ---a --b --c --d -e ----⊥
it.mapWithPostcondition     ---a'--b'--c'--d'-e'----⊥
```

(given that `f a = pure a'`, `f b = pure b'` etc.)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is productive

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and
will always fail, then `it.mapWithPostcondition` will be finite even if `it` isn't.

In such situations, the missing instances can be proved manually if the postcondition bundled in
the `PostconditionT n` monad is strong enough. In the given example, a suitable postcondition might
be `fun _ => False`.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
Std.IterM.mapWithPostcondition : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      [inst : Monad n] →
        [inst_1 : MonadLiftT m n] →
          [Std.Iterator α m β] → (f : β → Std.Iterators.PostconditionT n γ) → Std.IterM m β → Std.IterM n γ
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.tag_mem_smul_span : ∀ {ι : Type u_1} (n : ℕ) [NeZero n] [inst : Finite ι] (ν : ι → ℤ),
  BoxIntegral.unitPartition.tag n ν ∈ (↑n)⁻¹ • Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supportedEquivFinsupp_symm_apply_coe_support_val : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set α) (a : ↑s →₀ M),
  (↑((Finsupp.supportedEquivFinsupp s).symm a)).support.val = Multiset.map Subtype.val a.support.val
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.variance_eval_multivariateGaussian : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ},
  S.PosSemidef →
    ∀ (i : ι), ProbabilityTheory.variance (fun x => x.ofLp i) (ProbabilityTheory.multivariateGaussian μ S) = S i i
-- Mathlib.Topology.Connected.PathConnected
ZerothHomotopy.mk_surjective : ∀ {X : Type u_1} [inst : TopologicalSpace X], Function.Surjective ZerothHomotopy.mk
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.of_forall_contains_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {t₁ t₂ : Std.DTreeMap.Raw α (fun x => Unit) cmp},
  t₁.WF → t₂.WF → (∀ (k : α), t₁.contains k = t₂.contains k) → t₁.Equiv t₂
-- Mathlib.Data.List.OffDiag
List.length_offDiag : ∀ {α : Type u_1} (l : List α), l.offDiag.length = l.length ^ 2 - l.length
-- Lean.Meta.Tactic.Grind.Core
/-- Adds a new heterogeneous equality `lhs ≍ rhs`. It assumes `lhs` and `rhs` have already been internalized.  -/
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.addHEq : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Init.Sym.DSimp.DSimprocDSL
/-- zeta reduction. That is, expands let-expressions.  -/
Lean.Parser.Sym.DSimp.zeta : Lean.ParserDescr
-- Init.Data.Fin.Lemmas
Fin.cast_castLE : ∀ {k m n : ℕ} (km : k ≤ m) (mn : m = n) (i : Fin k), Fin.cast mn (Fin.castLE km i) = Fin.castLE ⋯ i
-- Init.Data.Bool
Bool.or_not_self : ∀ (x : Bool), (x || !x) = true
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_hom_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (X : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ),
  (CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso C).hom.app X =
    ((CategoryTheory.Pretriangulated.Triangle.mk (Opposite.unop X).mor₁ (Opposite.unop X).mor₂
            (CategoryTheory.CategoryStruct.comp
              ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).unitIso.inv.app
                  (Opposite.op (Opposite.unop X).obj₃)).unop
              ((CategoryTheory.shiftFunctor C 1).map
                (CategoryTheory.CategoryStruct.comp
                  ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map (Opposite.unop X).mor₃.op).unop
                  ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).counitIso.inv.app
                      (Opposite.op (Opposite.unop X).obj₁)).unop)))).homMk
        (Opposite.unop X) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₁)
        (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₂)
        (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₃) ⋯ ⋯ ⋯).op
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CochainComplex.of.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] [inst_4 : DecidableEq α] (X : α → V)
  (d d_1 : (n : α) → X n ⟶ X (n + 1)) (e_d : d = d_1)
  (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d n) (d (n + 1)) = 0),
  CochainComplex.of X d sq = CochainComplex.of X d_1 ⋯
-- Mathlib.GroupTheory.MonoidLocalization.DivPairs
AddSubmonoid.subPairs_comap : ∀ {M : Type u_1} {G : Type u_2} {H : Type u_3} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G]
  [inst_2 : AddCommGroup H] (f : ⊤.LocalizationMap G) (g : ⊤.LocalizationMap H) (s : AddSubmonoid G),
  AddSubmonoid.subPairs g (AddSubmonoid.comap (g.addEquivOfLocalizations f).toAddMonoidHom s) =
    AddSubmonoid.subPairs f s
-- Mathlib.Algebra.Lie.Weights.Linear
/-- By Engel's theorem, if `M` is Noetherian, the shifted action `⁅x, m⁆ - χ x • m` makes the
`χ`-weight space into a nilpotent Lie module.  -/
LieModule.shiftedGenWeightSpace.instIsNilpotentSubtypeMemLieSubmoduleOfIsNoetherian : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [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]
  [inst_7 : LieRing.IsNilpotent L] (χ : L → R) [inst_8 : LieModule.LinearWeights R L M] [IsNoetherian R M],
  LieModule.IsNilpotent L ↥(LieModule.shiftedGenWeightSpace R L M χ)
-- Mathlib.FieldTheory.Fixed
FixedBy.intermediateField_mem_iff : ∀ {M : Type u} [inst : Monoid M] (K : Type u_1) (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction M F] (m : M)
  [inst_3 : Field K] [inst_4 : Algebra K F] [inst_5 : SMulCommClass M K F] (x : F),
  x ∈ FixedBy.intermediateField K F m ↔ m • x = x
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceRErase.congr_simp : ∀ {α : Type u} {β : α → Type v} (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (l l_1 : Std.DTreeMap.Internal.Impl α β) (e_l : l = l_1) (r r_1 : Std.DTreeMap.Internal.Impl α β) (e_r : r = r_1)
      (hlb : l.Balanced) (hrb : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size),
      Std.DTreeMap.Internal.Impl.balanceRErase k v l r hlb hrb hlr =
        Std.DTreeMap.Internal.Impl.balanceRErase k v_1 l_1 r_1 ⋯ ⋯ ⋯
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.compl₂.eq_1 : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddZeroClass Q] (f : M →+ N →+ P) (g : Q →+ N), f.compl₂ g = g.compHom'.comp f
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
/-- Monoid homomorphism mapping `w` to `fun v ↦ e (L v w)`.  -/
BoundedContinuousFunction.charMonoidHom : {V : Type u_1} →
  {W : Type u_2} →
    [inst : AddCommGroup V] →
      [inst_1 : Module ℝ V] →
        [inst_2 : TopologicalSpace V] →
          [inst_3 : AddCommGroup W] →
            [inst_4 : Module ℝ W] →
              [inst_5 : TopologicalSpace W] →
                {e : AddChar ℝ Circle} →
                  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} →
                    Continuous ⇑e →
                      (Continuous fun p => (L p.1) p.2) → Multiplicative W →* BoundedContinuousFunction V ℂ
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.semiring : {R₁ : Type u_1} →
  [inst : Semiring R₁] →
    {M₁ : Type u_4} →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] → [inst_3 : Module R₁ M₁] → [ContinuousAdd M₁] → Semiring (M₁ →L[R₁] M₁)
-- Lean.Environment
Lean.Kernel.Exception.letTypeMismatch : Lean.Kernel.Environment → Lean.LocalContext → Lean.Name → Lean.Expr → Lean.Expr → Lean.Kernel.Exception
-- Mathlib.RingTheory.Ideal.Height
IsLocalization.AtPrime.ringKrullDim_eq_height : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsPrime] (A : Type u_2) [inst_2 : CommRing A]
  [inst_3 : Algebra R A] [IsLocalization.AtPrime A I], ringKrullDim A = ↑I.height
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_zero : ∀ {a : ENNReal}, a ≠ 0 → a / 0 = ⊤