mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.foldM_iterM_id : ∀ {α β γ : Type u} {m : Type u → Type w} {Pred EPred : Type u} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_6 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.IterM Id β} {init : γ} {f : γ → β → m γ}
  (inv : Std.Internal.Do.Invariant it.toList.run γ Pred) {epost : EPred},
  (∀ (pref : List β) (cur : β) (suff : List β) (h : it.toList.run = pref ++ cur :: suff) (b : γ),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f b cur ⦃ fun b' =>
        inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'; epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := it.toList.run, property := ⋯ } init ⦄ Std.IterM.foldM f init it ⦃ fun b =>
      inv { «prefix» := it.toList.run, suffix := [], property := ⋯ } b; epost ⦄
-- Lean.Meta.Tactic.Grind.Intro
Lean.Meta.Grind.Action.intros : ℕ → Lean.Meta.Grind.Action
-- Mathlib.Algebra.GroupWithZero.Associated
Irreducible.dvd_iff : ∀ {M : Type u_1} [inst : Monoid M] {x y : M}, Irreducible x → (y ∣ x ↔ IsUnit y ∨ Associated x y)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α}, k ∉ t₁ → Std.DTreeMap.Const.get! (t₁ ∪ t₂) k = Std.DTreeMap.Const.get! t₂ k
-- Init.Data.Nat.Internal.Linear
/-- When encoding polynomials. We use `fixedVar` for encoding numerals.
The denotation of `fixedVar` is always `1`.  -/
Nat.Internal.Linear.fixedVar : ℕ
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.nndist_integral_add_measure_le_lintegral : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ ν : MeasureTheory.Measure α} {f : α → G},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable f ν → ↑(nndist (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂(μ + ν))) ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂ν
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.drop_add_eq : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n m : ℕ), p.drop (n + m) = ((p.drop n).drop m).copy ⋯ ⋯
-- Lean.Elab.Do.Legacy
/-- Convert `action _ e` instructions in `c` into `let y ← e; jmp _ jp (xs y)`.  -/
Lean.Elab.Term.Do.convertTerminalActionIntoJmp : Lean.Elab.Term.Do.Code → Lean.Name → Array Lean.Elab.Term.Do.Var → Lean.MacroM Lean.Elab.Term.Do.Code
-- Mathlib.Analysis.Calculus.Taylor
/-- **Taylor's theorem** with the Cauchy form of the remainder.

We assume that `f` is `n`-times continuously differentiable on the closed set `uIcc x₀ x` and
`n+1`-times differentiable on the open set `uIoo x₀ x`. Then there exists an `x' ∈ uIoo x₀ x` such
that
$$f(x) - (P_n f)(x₀, x) = \frac{f^{(n+1)}(x') (x - x')^n (x-x₀)}{n!},$$
where $P_n f$ denotes the Taylor polynomial of degree $n$ and $f^{(n+1)}$ is the $n+1$-th iterated
derivative.  -/
taylor_mean_remainder_cauchy : ∀ {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ},
  x₀ ≠ x →
    ContDiffOn ℝ (↑n) f (Set.uIcc x₀ x) →
      DifferentiableOn ℝ (iteratedDerivWithin n f (Set.uIcc x₀ x)) (Set.uIoo x₀ x) →
        ∃ x' ∈ Set.uIoo x₀ x,
          f x - taylorWithinEval f n (Set.uIcc x₀ x) x₀ x =
            iteratedDerivWithin (n + 1) f (Set.uIcc x₀ x) x' * (x - x') ^ n / ↑n.factorial * (x - x₀)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nonneg_add_lem : ∀ {d x y z w : ℕ},
  { re := ↑x, im := -↑y }.Nonneg →
    { re := -↑z, im := ↑w }.Nonneg → ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w }).Nonneg
-- Init.Data.Order.Lemmas
Std.instEquivBEqOfLawfulOrderBEqOfIsPreorder : ∀ {α : Type u} [inst : BEq α] [inst_1 : LE α] [Std.LawfulOrderBEq α] [Std.IsPreorder α], EquivBEq α
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.elabHeadersAux : Array Lean.Elab.Command.InductiveView →
  ℕ → Array Lean.Elab.Command.PreElabHeaderResult → Lean.Elab.TermElabM (Array Lean.Elab.Command.PreElabHeaderResult)
-- Mathlib.RingTheory.Polynomial.Subring
Polynomial.natDegree_toSubring : ∀ {R : Type u_1} [inst : Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T),
  (p.toSubring T hp).natDegree = p.natDegree
-- Mathlib.Order.Basic
ne_of_not_le : ∀ {α : Type u_2} [inst : Preorder α] {a b : α}, ¬a ≤ b → a ≠ b
-- Std.Data.ExtTreeMap.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.ExtTreeMap.toArray : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → Array (α × β)
-- Mathlib.Probability.Moments.ComplexMGF
/-- For `z : ℂ` with `z.re ∈ interior (integrableExpSet X μ)`, the n-th derivative of the function
`complexMGF X μ` at `z` is `μ[X ^ n * cexp (z * X)]`.  -/
ProbabilityTheory.iteratedDeriv_complexMGF : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ},
  z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (n : ℕ),
      iteratedDeriv n (ProbabilityTheory.complexMGF X μ) z =
        ∫ (x : Ω), (fun ω => ↑(X ω) ^ n * Complex.exp (z * ↑(X ω))) x ∂μ
-- Mathlib.Tactic.DepRewrite
_private.Mathlib.Tactic.DepRewrite.0.Mathlib.Tactic.DepRewrite.elabDepRewriteConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Mathlib.Tactic.DepRewrite.Config
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- Changing the hypothesis direction in `PiLp.single_eq_of_ne` for for ease of use by simp.  -/
PiLp.single_eq_of_ne' : ∀ (p : ENNReal) {ι : Type u_2} {β : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] {i i' : ι},
  i ≠ i' → ∀ (a : β i), (PiLp.single p i a).ofLp i' = 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Signature.mk : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Name → List Lean.Name → Lean.Expr → Array (Lean.Compiler.LCNF.Param pu) → Bool → Lean.Compiler.LCNF.Signature pu
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.mk : Bool → Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly → Nat.Internal.Linear.PolyCnstr
-- Mathlib.CategoryTheory.Shift.CommShift
/-- Auxiliary structure for `NatTrans.CommShift` when we need to
show a compatibility of a natural transformation `τ : F₁ ⟶ F₂` with
respect to the shift by a specific element `a`. See also
`NatTrans.CommShift.of_core`  -/
CategoryTheory.NatTrans.CommShiftCore : {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] →
        {F₁ F₂ : CategoryTheory.Functor C D} →
          (F₁ ⟶ F₂) →
            {A : Type u_5} →
              [inst_2 : AddMonoid A] →
                [inst_3 : CategoryTheory.HasShift C A] →
                  [inst_4 : CategoryTheory.HasShift D A] → [F₁.CommShift A] → [F₂.CommShift A] → A → Prop
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_zero_of_constantCoeff_zero : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {f : MvPowerSeries σ R}, MvPowerSeries.constantCoeff f = 0 → MvPowerSeries.subst 0 f = 0
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.IsContained.mono_left : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} {A' : SimpleGraph α},
  A ≤ A' → A'.IsContained B → A.IsContained B
-- Mathlib.Analysis.Calculus.VectorField
/-- The Lie bracket commutes with taking pullbacks. This requires the function to have symmetric
second derivative. Version in a complete space. One could also give a version avoiding
completeness but requiring that `f` is a local diffeomorphism. Variant where unique
differentiability and the invariance property are only required in a smaller set `u`.  -/
VectorField.pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt_of_eventuallyEq : ∀ {𝕜 : 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] {s : Set E}
  [CompleteSpace E] {f : E → F} {V W : F → F} {x : E} {t : Set F} {u : Set E},
  IsSymmSndFDerivWithinAt 𝕜 f s x →
    ContDiffWithinAt 𝕜 2 f s x →
      DifferentiableWithinAt 𝕜 V t (f x) →
        DifferentiableWithinAt 𝕜 W t (f x) →
          UniqueDiffOn 𝕜 u →
            x ∈ u →
              Set.MapsTo f u t →
                u =ᶠ[nhds x] s →
                  VectorField.pullbackWithin 𝕜 f (VectorField.lieBracketWithin 𝕜 V W t) s x =
                    VectorField.lieBracketWithin 𝕜 (VectorField.pullbackWithin 𝕜 f V s)
                      (VectorField.pullbackWithin 𝕜 f W s) s x
-- Mathlib.MeasureTheory.Measure.Doubling
IsUnifLocDoublingMeasure.measure_mul_le_scalingConstantOf_mul : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [inst_2 : IsUnifLocDoublingMeasure μ] {K : ℝ} {x : α} {t r : ℝ},
  t ∈ Set.Ioc 0 K →
    r ≤ IsUnifLocDoublingMeasure.scalingScaleOf μ K →
      μ (Metric.closedBall x (t * r)) ≤ ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K) * μ (Metric.closedBall x r)
-- Mathlib.Tactic.Widget.CongrM
/-- Display a widget panel allowing to generate a `congrm` call with holes specified by selecting
subexpressions in the goal.  -/
tacticCongrm? : Lean.ParserDescr
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  (MonoidWithZeroHom.ofClass Valued.v).valueGroup =
    (MonoidWithZeroHom.ofClass (IsDedekindDomain.HeightOneSpectrum.valuation K v)).valueGroup
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.instAdditiveObjWhiskeringLeft : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.Preadditive E] (F : CategoryTheory.Functor C D),
  ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).Additive
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inl_mul_inr : ∀ {R : Type u_1} {A : Type u_2} [inst : MulZeroClass R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : SMulZeroClass R A] (r : R) (a : A), Unitization.inl r * ↑a = ↑(r • a)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseOneOrTwoNum : Std.Internal.Parsec.String.Parser ℕ
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.id_compHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  (AlgebraicGeometry.Scheme.RationalMap.id X).compHom f = AlgebraicGeometry.Scheme.Hom.toRationalMap f
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingAfter_mem_set_of_ne_top : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω} [WellFoundedLT ι],
  MeasureTheory.hittingAfter u s n ω ≠ ⊤ → u (MeasureTheory.hittingAfter u s n ω).untopA ω ∈ s
-- Mathlib.Data.Setoid.Basic
Setoid.prod_apply : ∀ {α : Type u_1} {β : Type u_2} {r : Setoid α} {s : Setoid β} {x₁ x₂ : α} {y₁ y₂ : β},
  (r.prod s) (x₁, y₁) (x₂, y₂) ↔ r x₁ x₂ ∧ s y₁ y₂
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInlayHintOptions.fromJson : Lean.Json → Except String Lean.Lsp.InlayHintOptions
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flipping_functor_obj_obj_map : ∀ {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 (CategoryTheory.Functor D E)) (k : D) {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.Functor.flipping.functor.obj F).obj k).map f = (F.map f).app k
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.neg_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α], Function.Periodic f c → f (-c) = f 0
-- Mathlib.Order.Filter.Prod
/-- A fact that is eventually true about all pairs `l ×ˢ l` is eventually true about
all diagonal pairs `(i, i)`  -/
Filter.Eventually.diag_of_prod : ∀ {α : Type u_1} {f : Filter α} {p : α × α → Prop}, (∀ᶠ (i : α × α) in f ×ˢ f, p i) → ∀ᶠ (i : α) in f, p (i, i)
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- `MDifferentiableWithinAt I I' f s x` indicates that the function `f` between manifolds
has a derivative at the point `x` within the set `s`.
This is a generalization of `DifferentiableWithinAt` to manifolds.

We require continuity in the definition, as otherwise points close to `x` in `s` could be sent by
`f` outside of the chart domain around `f x`. Then the chart could do anything to the image points,
and in particular by coincidence `writtenInExtChartAt I I' x f` could be differentiable, while
this would not mean anything relevant.  -/
MDifferentiableWithinAt : {𝕜 : 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] →
              ModelWithCorners 𝕜 E H →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [ChartedSpace H M] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                ModelWithCorners 𝕜 E' H' →
                                  {M' : Type u_7} →
                                    [inst : TopologicalSpace M'] → [ChartedSpace H' M'] → (M → M') → Set M → M → Prop
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.Method.noConfusionType : Sort v✝ → Aesop.ScriptGenerated.Method → Aesop.ScriptGenerated.Method → Sort v✝
-- Mathlib.Data.List.Induction
_private.Mathlib.Data.List.Induction.0.List.bidirectionalRec.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (a : α) → motive [a])
  (h_3 : (a b : α) → (l : List α) → motive (a :: b :: l)),
  (match [] with
    | [] => h_1 ()
    | [a] => h_2 a
    | a :: b :: l => h_3 a b l) =
    h_1 ()
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.GoalContext.lctx₂ : Aesop.EqualUpToIds.GoalContext → Lean.LocalContext
-- Init.Data.Nat.Lemmas
Nat.div_lt_div_of_lt_of_dvd : ∀ {a b d : ℕ}, d ∣ b → a < b → a / d < b / d
-- Mathlib.Data.Set.Lattice
Set.iInter_mono : ∀ {α : Type u_1} {ι : Sort u_5} {s t : ι → Set α}, (∀ (i : ι), s i ⊆ t i) → ⋂ i, s i ⊆ ⋂ i, t i
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.addRight_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A : C} [inst_2 : CategoryTheory.AddGrpObj A] (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A),
  (CategoryTheory.AddGrpObj.addRight f).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) f))
      CategoryTheory.AddMonObj.add
-- Init.MetaTypes
Lean.Meta.DSimp.instInhabitedConfig : Inhabited Lean.Meta.DSimp.Config
-- Mathlib.FieldTheory.Galois.Infinite
InfiniteGalois.fixedField_fixingSubgroup : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (L : IntermediateField k K)
  [IsGalois k K], IntermediateField.fixedField L.fixingSubgroup = L
-- Lean.Declaration
/-- Reducibility hints guide the kernel's *lazy delta reduction* strategy. When the kernel encounters a
definitional equality constraint

           (f ...) =?= (g ...)

where `f` and `g` are definitions, it must decide which side to unfold. The rules (implemented in
`lazy_delta_reduction_step` in `src/kernel/type_checker.cpp`) are:

* If `f` and `g` have the **same hint kind**:
  - Both `.opaque` or both `.abbrev`: unfold both.
  - Both `.regular`: unfold the one with the **greater** height first. If their heights are equal
    (in particular, if `f` and `g` are the same definition), first try to compare their arguments
    for definitional equality (short-circuiting the unfolding if they match), then unfold both.
* If `f` and `g` have **different hint kinds**: unfold the one that is *not* `.opaque`, preferring to
  unfold `.abbrev` over `.regular`.

The `.regular` constructor carries a `UInt32` *definitional height*, which is computed by the
elaborator as one plus the maximum height of all `.regular` constants appearing in the definition's
body (see `getMaxHeight`). This means `.abbrev` and `.opaque` constants do not contribute to the
height. When creating declarations via meta-programming, the height can be specified manually.

The hints only affect performance — they control the order in which definitions are unfolded, but
never prevent the kernel from unfolding a definition during type checking.

The `ReducibilityHints` are not related to the `@[reducible]`/`@[irreducible]`/`@[semireducible]`
attributes. Those attributes are used by the elaborator to control which definitions tactics like
`simp`, `rfl`, and `dsimp` will unfold; they do not affect the kernel. Conversely,
`ReducibilityHints` are set when a declaration is added to the kernel and cannot be changed
afterwards.  -/
Lean.ReducibilityHints : Type
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.ContinuousMapGeneratedBy.mk : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y : Type v} →
        [inst_1 : TopologicalSpace Y] →
          {Z : Type v'} →
            [inst_2 : TopologicalSpace Z] →
              (toFun : Y → Z) → Topology.ContinuousGeneratedBy X toFun → Topology.ContinuousMapGeneratedBy X Y Z
-- Mathlib.Analysis.InnerProductSpace.JointEigenspace
/-- The joint eigenspaces of a pair of symmetric operators form an
`OrthogonalFamily`.  -/
LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {A B : E →ₗ[𝕜] E},
  A.IsSymmetric →
    B.IsSymmetric →
      OrthogonalFamily 𝕜 (fun i => ↥(Module.End.eigenspace A i.2 ⊓ Module.End.eigenspace B i.1)) fun i =>
        (Module.End.eigenspace A i.2 ⊓ Module.End.eigenspace B i.1).subtypeₗᵢ
-- Mathlib.Data.Seq.Defs
/-- Convert a sequence into a list, embedded in a computation to allow for
the possibility of infinite sequences (in which case the computation
never returns anything).  -/
Stream'.Seq.toList' : {α : Type u_1} → Stream'.Seq α → Computation (List α)
-- Std.Time.Format.Modifier
Std.Time.Modifier.O.sizeOf_spec : ∀ (presentation : Std.Time.OffsetO), sizeOf (Std.Time.Modifier.O presentation) = 1 + sizeOf presentation
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.decidableMemKer : {G : Type u_1} →
  [inst : AddGroup G] →
    {M : Type u_7} → [inst_1 : AddZeroClass M] → [DecidableEq M] → (f : G →+ M) → DecidablePred fun x => x ∈ f.ker
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiffWithinAt.norm_sq : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E}
  {s : Set G} {x : G} {n : WithTop ℕ∞}, ContDiffWithinAt ℝ n f s x → ContDiffWithinAt ℝ n (fun y => ‖f y‖ ^ 2) s x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The braiding isomorphism is symmetric.  -/
CategoryTheory.Limits.biprod.symmetry_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (P Q : C) {Z : C} (h : P ⊞ Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding P Q).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding Q P).hom h) =
    h
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.withTopCongr_toAddHom : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β), ↑e.withTopCongr = (↑e).withBotMap
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedDecl.default : Lean.IR.Decl
-- Mathlib.Topology.MetricSpace.Bounded
Metric.tendsto_dist_right_cobounded_atTop : ∀ {α : Type u} [inst : PseudoMetricSpace α] (c : α),
  Filter.Tendsto (fun x => dist x c) (Bornology.cobounded α) Filter.atTop
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The order of the sum of two formal power series
is at least the minimum of their orders.  -/
MvPowerSeries.min_order_le_add : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f g : MvPowerSeries σ R}, min f.order g.order ≤ (f + g).order
-- Mathlib.Order.Interval.Finset.Basic
Finset.nonempty_Ioi : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α], (Finset.Ioi a).Nonempty ↔ ¬IsMax a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [inst_4 : Inhabited α] {f : α → β → Bool} {k : α} (h : m.WF),
  (Std.DHashMap.Raw.filter f m).getKey! k =
    ((m.getKey? k).pfilter fun x h' => f x (Std.DHashMap.Raw.Const.get m x ⋯)).get!
-- Mathlib.Topology.Order.LiminfLimsup
/-- A continuous antitone function between (conditionally) complete linear ordered spaces sends a
`Filter.limsup` to the `Filter.liminf` of the images (if the filter is bounded from above and
frequently bounded from below).  -/
Antitone.map_limsup_of_continuousAt : ∀ {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [F.NeBot] [inst : ConditionallyCompleteLinearOrder R]
  [inst_1 : TopologicalSpace R] [OrderTopology R] [inst_3 : ConditionallyCompleteLinearOrder S]
  [inst_4 : TopologicalSpace S] [OrderTopology S] {f : R → S},
  Antitone f →
    ∀ (a : ι → R),
      ContinuousAt f (Filter.limsup a F) →
        autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F a) Antitone.map_limsup_of_continuousAt._auto_1 →
          autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F a) Antitone.map_limsup_of_continuousAt._auto_3 →
            f (Filter.limsup a F) = Filter.liminf (f ∘ a) F
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instContinuousMulCoeCofinite : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  [inst_1 : (i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] [inst_2 : (i : ι) → Mul (R i)]
  [inst_3 : ∀ (i : ι), MulMemClass (S i) (R i)] [∀ (i : ι), ContinuousMul (R i)],
  ContinuousMul (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) Filter.cofinite)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.CoextendScalars.mulAction : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) →
          (M : Type v) →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : Module R M] → MulAction S (↑((ModuleCat.restrictScalars f).obj (ModuleCat.of S S)) →ₗ[R] M)
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
/-- Let `b` be a basis of `M` indexed by a linearly ordered type `I` and `s` be a finset of `I`
of cardinality `n`. If we apply the linear form on `⋀[R]^n M` defined by `b` and `s`
to the exterior product of the `b i` for `i ∈ s`, then we get `1`.  -/
exteriorPower.ιMultiDual_apply_diag : ∀ (R : Type u_1) {M : Type u_3} (n : ℕ) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {I : Type u_5} [inst_3 : LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)),
  (exteriorPower.ιMultiDual R n b s) (exteriorPower.ιMulti_family R n (⇑b) s) = 1
-- Init.Sym.Lemmas
Lean.Sym.BitVec.eq_eq_false : ∀ {n : ℕ} (a b : BitVec n), decide (a = b) = false → (a = b) = False