mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.eq_top_of_chromaticNumber_eq_card : ∀ {V : Type u} {G : SimpleGraph V} [inst : Fintype V], G.chromaticNumber = ↑(Fintype.card V) → G = ⊤
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup'_eq_iSup : ∀ {ι : Type u_3} (r : ι → ι → Prop) [inst : IsWellOrder ι r] (f : ι → Ordinal.{max u_3 u_4}),
  (Ordinal.type r).bsup (Ordinal.bfamilyOfFamily' r f) = iSup f
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.IsCardinalFiltered.mk : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular],
  (∀ {A : Type w} [inst_2 : CategoryTheory.SmallCategory A] (F : CategoryTheory.Functor A J),
      HasCardinalLT (CategoryTheory.Arrow A) κ → Nonempty (CategoryTheory.Limits.Cocone F)) →
    CategoryTheory.IsCardinalFiltered J κ
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableWithinAt.smul_const : ∀ {𝕜 : 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] {x : E}
  {s : Set E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
  DifferentiableWithinAt 𝕜 c s x → ∀ (f : F), DifferentiableWithinAt 𝕜 (fun y => c y • f) s x
-- Mathlib.Algebra.Torsor.Basic
Equiv.injective_pointReflection_left_of_injective_two_nsmul : ∀ {G : Type u_5} {P : Type u_6} [inst : AddCommGroup G] [inst_1 : AddTorsor G P],
  (Function.Injective fun x => 2 • x) → ∀ (y : P), Function.Injective fun x => (Equiv.pointReflection x) y
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- A path includes the data of `n + 1` 0-simplices in `X`.  -/
SSet.Truncated.Path₁.vertex : {X : SSet.Truncated 1} →
  {n : ℕ} →
    X.Path₁ n → Fin (n + 1) → X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Path₁._proof_1 })
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H}
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  (c : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.fiberwiseColimit G)),
  (CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit c).pt = c.pt
-- Mathlib.Data.ENat.Defs
ENat.recTopCoe_natCast : ∀ {C : ℕ∞ → Sort u_1} (d : C ⊤) (f : (a : ℕ) → C ↑a) (x : ℕ), ENat.recTopCoe d f ↑x = f x
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toArray_roo : ∀ {m n k : ℤ}, Array.map (fun x => x + k) (m<...n).toArray = ((m + k)<...n + k).toArray
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
/-- The functor
`HomotopyCategory.Plus.quotient C : CochainComplex.Plus C ⥤ HomotopyCategory.Plus C`
is induced by the functor `HomotopyCategory.quotient C (.up ℤ)` from `CochainComplex C ℤ`
to `HomotopyCategory C (.up ℤ)`.  -/
HomotopyCategory.Plus.quotientCompιIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (HomotopyCategory.Plus.quotient C).comp (HomotopyCategory.Plus.ι C) ≅
        (CochainComplex.Plus.ι C).comp (HomotopyCategory.quotient C (ComplexShape.up ℤ))
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.subst.inj : ∀ {x : Lean.Grind.Linarith.Var} {c₁ : Lean.Meta.Grind.Arith.Linear.EqCnstr}
  {c₂ : Lean.Meta.Grind.Arith.Linear.IneqCnstr} {x_1 : Lean.Grind.Linarith.Var}
  {c₁_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr} {c₂_1 : Lean.Meta.Grind.Arith.Linear.IneqCnstr},
  Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.subst x c₁ c₂ =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.subst x_1 c₁_1 c₂_1 →
    x = x_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E / F` is a separable extension of exponential characteristic `q`, if `{ u_i }` is a family
of elements of `E` which `F`-linearly spans `E`, then `{ u_i ^ (q ^ n) }` also `F`-linearly spans
`E` for any natural number `n`.  -/
Field.span_map_pow_expChar_pow_eq_top_of_isSeparable : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q n : ℕ) [hF : ExpChar F q]
  {ι : Type u_1} {v : ι → E} [Algebra.IsSeparable F E],
  Submodule.span F (Set.range v) = ⊤ → Submodule.span F (Set.range fun x => v x ^ q ^ n) = ⊤
-- Mathlib.Algebra.Algebra.Hom
AlgHomClass.toRingHom_toAlgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {F : Type u_4} [inst_5 : FunLike F A B] [inst_6 : AlgHomClass F R A B]
  (f : F), ↑↑f = ↑f
-- Mathlib.Algebra.Homology.LocalCohomology
/-- Local cohomology as the direct limit of `Ext^i(R/J', M)` over *all* ideals `J'` with radical
containing `J`.  -/
localCohomology.ofSelfLERadical : {R : Type u} → [inst : CommRing R] → Ideal R → ℕ → CategoryTheory.Functor (ModuleCat R) (ModuleCat R)
-- Init.Data.Vector.Lemmas
Vector.flatMap.eq_1 : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} (xs : Vector α n) (f : α → Vector β m),
  xs.flatMap f = Vector.mk (Array.flatMap (fun a => (f a).toArray) xs.toArray) ⋯
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedResolvableCompletionItem.default : Lean.Lsp.ResolvableCompletionItem
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_inter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        (m₁.inter! m₂).getKey! k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then m₁.getKey! k else default
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.atEnd.eq_1 : ∀ (s : String) (i : String.Pos.Raw), { s := s, i := i }.atEnd = decide (i.byteIdx ≥ s.rawEndPos.byteIdx)
-- Mathlib.Algebra.Order.SuccPred
Order.succ_iterate : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddMonoidWithOne α] [inst_2 : SuccAddOrder α] (x : α) (n : ℕ),
  Order.succ^[n] x = x + ↑n
-- Init.Data.String.Stream
instStreamRawChar : Std.Stream Substring.Raw Char
-- Mathlib.Probability.Process.FiniteDimensionalLaws
/-- If two processes are modifications of each other, then they have the same distribution.  -/
ProbabilityTheory.map_eq_of_forall_ae_eq : ∀ {T : Type u_1} {Ω : Type u_2} {𝓧 : T → Type u_3} {mΩ : MeasurableSpace Ω} {mα : (t : T) → MeasurableSpace (𝓧 t)}
  {X Y : (t : T) → Ω → 𝓧 t} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P],
  AEMeasurable (fun ω x => X x ω) P →
    AEMeasurable (fun ω x => Y x ω) P →
      (∀ (t : T), X t =ᵐ[P] Y t) →
        MeasureTheory.Measure.map (fun ω x => X x ω) P = MeasureTheory.Measure.map (fun ω x => Y x ω) P
-- Mathlib.Data.Set.Finite.Basic
Set.fintypeLENat : (n : ℕ) → Fintype ↑{i | i ≤ n}
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.divCoeffs.eq_1 : ∀ (k k_1 : ℤ), Int.Internal.Linear.Poly.divCoeffs k (Int.Internal.Linear.Poly.num k_1) = true
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.isIso_leftHomologyπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology], S.f = 0 → CategoryTheory.IsIso S.leftHomologyπ
-- Lean.Meta.Tactic.Grind.MatchCond
/-- Helper function for `isSatisfied`.
See `isSatisfied`.
 -/
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.isMatchCondFalseHyp : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Homeomorph.toMeasurableEquiv_coe : ∀ {γ : Type u_3} {γ₂ : Type u_4} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [inst_2 : BorelSpace γ]
  [inst_3 : TopologicalSpace γ₂] [inst_4 : MeasurableSpace γ₂] [inst_5 : BorelSpace γ₂] (h : γ ≃ₜ γ₂),
  ⇑h.toMeasurableEquiv = ⇑h
-- Mathlib.RingTheory.RingHom.OpenImmersion
RingHom.IsStandardOpenImmersion.containsIdentities : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => RingHom.IsStandardOpenImmersion
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.adjoin_mono : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {s t : Set A},
  s ⊆ t → StarAlgebra.adjoin R s ≤ StarAlgebra.adjoin R t
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.activateTheoremsCore : {α : Type} →
  [Lean.Meta.Grind.TheoremLike α] →
    Lean.Name →
      Lean.Meta.Grind.GoalM (Lean.Meta.Grind.TheoremsArray α) →
        (Lean.Meta.Grind.TheoremsArray α → Lean.Meta.Grind.GoalM Unit) →
          (α → Lean.Meta.Grind.GoalM Unit) → (α → Lean.Meta.Grind.GoalM Unit) → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- `⊓` commutes with pullback.  -/
CategoryTheory.Subobject.inf_pullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X Y : C}
  (g : X ⟶ Y) (f₁ f₂ : CategoryTheory.Subobject Y),
  (CategoryTheory.Subobject.pullback g).obj (f₁ ⊓ f₂) =
    (CategoryTheory.Subobject.pullback g).obj f₁ ⊓ (CategoryTheory.Subobject.pullback g).obj f₂
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.measure_sdiff_right : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t → μ (t \ s) = μ t
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version within a set at a point, but with full pullback.  -/
ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} {t : Set M'} {y₀ : M'} [CompleteSpace E]
  [inst_12 : IsManifold I 1 M] [inst_13 : IsManifold I' 1 M'],
  ContMDiffWithinAt I' I'.tangent m (fun x => ⟨x, V x⟩) t y₀ →
    ContMDiffAt I I' n f x₀ →
      (mfderiv% f x₀).IsInvertible →
        m + 1 ≤ n →
          f ⁻¹' t ∈ nhdsWithin x₀ s →
            y₀ = f x₀ → ContMDiffWithinAt I I.tangent m (fun x => ⟨x, VectorField.mpullback I I' f V x⟩) s x₀
-- Lean.Meta.Sym.Apply
/-- Computes which argument positions become new subgoals after applying a backward rule.

Arguments are excluded from `resultPos` if:
- They appear in the conclusion (will be determined by unification)
- They are instance arguments (will be synthesized)

The result is ordered with non-dependent arguments first, then dependent ones.
This ordering is the same one used for the `MetaM` `apply` tactic.
It improves the user experience: non-dependent goals can be solved in
any order, while dependent goals are often resolved by solving the non-dependent ones first.
Example: `Exists.intro` produces two subgoal `?h : ?p ?w` and `?w : ?α`. The goal `?h` appears
first because solving it often solves `?w`.
 -/
_private.Lean.Meta.Sym.Apply.0.Lean.Meta.Sym.mkResultPos : Lean.Meta.Sym.Pattern → List ℕ
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.le_union : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] (c : Set (IntermediateField.Lifts F E K))
  (hc : IsChain (fun x1 x2 => x1 ≤ x2) c) ⦃σ : IntermediateField.Lifts F E K⦄,
  σ ∈ c → σ ≤ IntermediateField.Lifts.union c hc
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.map_id : ∀ {R : Type u_2} {F : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid F] [inst_4 : TopologicalSpace F] [inst_5 : Module R F] [inst_6 : ContinuousAdd F]
  [inst_7 : ContinuousConstSMul R F] (C : ProperCone R F), ProperCone.map (ContinuousLinearMap.id R F) C = C
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_eq_zero_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {p : Polynomial R} {n : ℕ}, p.natDegree ≤ n → (p.homogenize n = 0 ↔ p = 0)
-- Mathlib.Tactic.Ring.Basic
/-- Decide if `x` is 1 and provide a proof if so.  -/
Mathlib.Tactic.Ring.RingCompute.isOne : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {x : Q(«$α»)} → Mathlib.Tactic.Ring.RatCoeff x → Option Q(Mathlib.Meta.NormNum.IsNat «$x» 1)
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.opRingEquiv.eq_1 : ∀ (R : Type u_2) [inst : Semiring R],
  Polynomial.opRingEquiv R =
    ((RingEquiv.op (Polynomial.toFinsuppIso R)).trans
          (AddMonoidAlgebra.opRingEquiv.trans
            (AddMonoidAlgebra.mapDomainRingEquiv Rᵐᵒᵖ AddOpposite.opAddEquiv.symm))).trans
      (Polynomial.toFinsuppIso Rᵐᵒᵖ).symm
-- Init.Data.Vector.Erase
Vector.getElem_eraseIdx_of_lt : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (w : i < n) {j : ℕ} (h : j < n - 1) (h' : j < i),
  (xs.eraseIdx i w)[j] = xs[j]
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.NullMeasurableSet.fundamentalInterior : ∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α) [Countable G]
  [inst_3 : MeasurableSpace α] [MeasurableConstSMul G α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.SMulInvariantMeasure G α μ],
  MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet (MeasureTheory.fundamentalInterior G s) μ
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.State.mk.inj : ∀ {structs : Array Lean.Meta.Grind.AC.Struct} {opIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {exprToOpIds : Lean.PHashMap Lean.Meta.Sym.ExprPtr (List ℕ)} {steps : ℕ} {structs_1 : Array Lean.Meta.Grind.AC.Struct}
  {opIdOf_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {exprToOpIds_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (List ℕ)} {steps_1 : ℕ},
  { structs := structs, opIdOf := opIdOf, exprToOpIds := exprToOpIds, steps := steps } =
      { structs := structs_1, opIdOf := opIdOf_1, exprToOpIds := exprToOpIds_1, steps := steps_1 } →
    structs = structs_1 ∧ opIdOf = opIdOf_1 ∧ exprToOpIds = exprToOpIds_1 ∧ steps = steps_1
-- Mathlib.Algebra.GroupWithZero.Prod
mulMonoidWithZeroHom_apply : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] (a : M₀ × M₀), mulMonoidWithZeroHom a = (↑mulMonoidHom).toFun a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {fallback : α}, t.getKey! (t.maxKeyD fallback) = t.maxKeyD fallback
-- Mathlib.SetTheory.ZFC.Rank
/-- For the rank of `⋃₀ x`, we only have `rank (⋃₀ x) ≤ rank x ≤ rank (⋃₀ x) + 1`.

This inequality is split into `rank_sUnion_le` and `le_succ_rank_sUnion`.  -/
ZFSet.rank_sUnion_le : ∀ (x : ZFSet.{u_1}), x.sUnion.rank ≤ x.rank
-- Init.Data.List.Sort.Lemmas
/-- The result of `mergeSort` is sorted,
as long as the comparison function is transitive (`le a b → le b c → le a c`)
and total in the sense that `le a b || le b a`.

The comparison function need not be irreflexive, i.e. `le a b` and `le b a` is allowed even when `a ≠ b`.
 -/
List.pairwise_mergeSort : ∀ {α : Type u_1} {le : α → α → Bool},
  (∀ (a b c : α), le a b = true → le b c = true → le a c = true) →
    (∀ (a b : α), (le a b || le b a) = true) → ∀ (l : List α), List.Pairwise (fun a b => le a b = true) (l.mergeSort le)
-- Mathlib.Analysis.Calculus.Deriv.Inverse
HasDerivAt.eventually_notMem : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜},
  HasDerivAt f f' x →
    f' ≠ 0 → ∀ (t : Set F), ¬AccPt (f x) (Filter.principal t) → ∀ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z ∉ t
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.negPart_eq_zero_of_not_isSelfAdjoint : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {a : A}, ¬IsSelfAdjoint a → a⁻ = 0
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X_pow_mul_injective : ∀ {R : Type u_1} [inst : Semiring R] {k : ℕ}, Function.Injective fun x => PowerSeries.X ^ k * x
-- Lean.Data.Lsp.Utf16
Lean.FileMap.lspRangeToUtf8Range : Lean.FileMap → Lean.Lsp.Range → Lean.Syntax.Range
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (G : CategoryTheory.Functor D K) [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit F G =
    CategoryTheory.NatIso.ofComponents
      (fun j =>
        CategoryTheory.Limits.limitObjIsoLimitCompEvaluation
            (F.comp ((CategoryTheory.Functor.whiskeringLeft D K C).obj G)) j ≪≫
          CategoryTheory.Limits.HasLimit.isoOfNatIso
              (F.isoWhiskerLeft (CategoryTheory.whiskeringLeftCompEvaluation G j)) ≪≫
            (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F (G.obj j)).symm)
      ⋯
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddLeftCancelSemigroup : {α : Type u_1} → [AddLeftCancelSemigroup α] → AddLeftCancelSemigroup (Colex α)
-- Lean.Meta.Tactic.Grind.Arith.ModelUtil
_private.Lean.Meta.Tactic.Grind.Arith.ModelUtil.0.Lean.Meta.Grind.Arith.pickUnusedValue.go : Lean.Meta.Grind.Goal → Std.HashMap Lean.Expr ℚ → Lean.Expr → Std.HashSet ℤ → ℤ → ℤ
-- Mathlib.FieldTheory.SeparableClosure
/-- `separableClosure` as a `ClosureOperator`.  -/
separableClosureOperator : (F : Type u) →
  (E : Type v) →
    [inst : Field F] → [inst_1 : Field E] → [inst_2 : Algebra F E] → ClosureOperator (IntermediateField F E)
-- Mathlib.Data.Sign.Basic
abs_mul_sign : ∀ {α : Type u} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (x : α), |x| * ↑(SignType.sign x) = x
-- Mathlib.Algebra.Group.PUnit
PUnit.instAdd_mathlib.eq_1 : PUnit.instAdd_mathlib = { add := fun x x_1 => PUnit.unit }
-- Mathlib.Data.Finset.Preimage
Equiv.image_symm_eq_preimage_of_finset : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] (e : α ≃ β) (s : Finset β),
  Finset.image (⇑e.symm) s = s.preimage ⇑e ⋯
-- Mathlib.Data.Set.Restrict
Set.MapsTo.coe_restrict : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t),
  Subtype.val ∘ Set.MapsTo.restrict f s t h = s.domRestrict f
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : TopologicalSpace.Opens X) (hs : Nonempty ↥s),
  (s.openPartialHomeomorphSubtypeCoe hs).target = ↑s
-- Init.Data.String.Basic
String.Pos.Raw.isValid_ofList : ∀ {l : List Char} {p : String.Pos.Raw},
  String.Pos.Raw.IsValid (String.ofList l) p ↔ ∃ i, p.byteIdx = (String.ofList (List.take i l)).utf8ByteSize
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.lintegral_edist_lt_top : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f g : α → β}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → ∫⁻ (a : α), edist (f a) (g a) ∂μ < ⊤
-- Std.Sat.AIG.Basic
/-- An And Inverter Graph together with a cache for subterm sharing.
 -/
Std.Sat.AIG : (α : Type) → [DecidableEq α] → [Hashable α] → Type
-- Lean.Data.Name
_private.Lean.Data.Name.0.Lean.Name.quickCmpImpl.unsafe_1 : Lean.Name → Lean.Name → Bool
-- Mathlib.RingTheory.Valuation.Archimedean
Valuation.instLinearOrderedCommGroupWithZeroMrange : {F : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : Field F] →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        {v : Valuation F Γ₀} → LinearOrderedCommGroupWithZero ↥(MonoidHom.mrange v)
-- Init.Data.Vector.Lemmas
Vector.toList_drop : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ}, (xs.drop i).toList = List.drop i xs.toList
-- Mathlib.Topology.Order.Hom.Esakia
/-- `EsakiaHomClass F α β` states that `F` is a type of lattice morphisms.

You should extend this class when you extend `EsakiaHom`.  -/
EsakiaHomClass : (F : Type u_6) →
  (α : outParam (Type u_7)) →
    (β : outParam (Type u_8)) →
      [TopologicalSpace α] → [Preorder α] → [TopologicalSpace β] → [Preorder β] → [FunLike F α β] → Prop
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.noConfusionType : Sort v✝ → Std.Time.Weekday → Std.Time.Weekday → Sort v✝
-- Mathlib.GroupTheory.Frattini
/-- The Frattini subgroup consists of "non-generating" elements in the following sense:

If a subgroup together with the Frattini subgroup generates the whole group,
then the subgroup is already the whole group.
 -/
frattini_nongenerating : ∀ {G : Type u_1} [inst : Group G] [IsCoatomic (Subgroup G)] {K : Subgroup G}, K ⊔ frattini G = ⊤ → K = ⊤
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- The antidiagonal of an element `n` is the finset of pairs `(i, j)` such that
`i + j = n`.  -/
Finset.HasAntidiagonal.antidiagonal : {A : Type u_1} → {inst : AddMonoid A} → [self : Finset.HasAntidiagonal A] → A → Finset (A × A)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β},
  m.WF →
    (Std.DHashMap.Raw.Const.modify m k f).getKeyD k' fallback =
      if (k == k') = true then if k ∈ m then k else fallback else m.getKeyD k' fallback
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Limits.PreservesLimit₂.mk : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} {G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)},
  (∀ {c₁ : CategoryTheory.Limits.Cone K₁} (hc₁ : CategoryTheory.Limits.IsLimit c₁) {c₂ : CategoryTheory.Limits.Cone K₂}
      (hc₂ : CategoryTheory.Limits.IsLimit c₂), Nonempty (CategoryTheory.Limits.IsLimit (G.mapCone₂ c₁ c₂))) →
    CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α}, (t₁ \ t₂).get? k = if k ∈ t₂ then none else t₁.get? k
-- Init.Data.Array.Attach
/-- Variant of `foldr_subtype` with side condition to check `stop = l.size`.  -/
Array.foldr_subtype' : ∀ {α : Type u_1} {β : Type u_2} {start : ℕ} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → β → β}
  {g : α → β → β} {x : β},
  (∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b) →
    start = xs.size → Array.foldr f x xs start = Array.foldr g x xs.unattach