mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.root_apply_coroot : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K]
  {α : LieModule.Weight K (↥H) L}, α.IsNonZero → α (LieAlgebra.IsKilling.coroot α) = 2
-- Mathlib.Topology.Connected.PathConnected
IsPathConnected.add : ∀ {M : Type u_4} [inst : Add M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] {s t : Set M},
  IsPathConnected s → IsPathConnected t → IsPathConnected (s + t)
-- Mathlib.Combinatorics.SimpleGraph.Star
/-- The center vertex of a starGraph has degree (card V) - 1.  -/
SimpleGraph.degree_starGraph_center : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {r : V},
  (SimpleGraph.starGraph r).degree r = Fintype.card V - 1
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousAt_iff_le_liminf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : CompleteLinearOrder γ] {f : α → γ},
  LowerSemicontinuousAt f x ↔ f x ≤ Filter.liminf f (nhds x)
-- Init.MetaTypes
/-- When `true` (default: `true`) then switches to `dsimp` on dependent arguments
if there is no congruence theorem that would allow `simp` to visit them.
When `dsimp` is `false`, then the argument is not visited.
 -/
Lean.Meta.Simp.Config.dsimp : Lean.Meta.Simp.Config → Bool
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.sum_counit_tmul_map_eq : ∀ {R : Type u} {A : Type v} {ι : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] {B : Type u_4} [inst_4 : AddCommMonoid B] [inst_5 : Module R B] {F : Type u_5}
  [inst_6 : FunLike F A B] [LinearMapClass F R A B] (f : F) (a : A) {repr : Coalgebra.Repr R a ι},
  ∑ i ∈ repr.index, CoalgebraStruct.counit (repr.left i) ⊗ₜ[R] f (repr.right i) = 1 ⊗ₜ[R] f a
-- Batteries.Lean.EStateM
EStateM.run'_pure : ∀ {α σ ε : Type u_1} (x : α) (s : σ), (pure x).run' s = some x
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit.match_1.splitter : {n : ℕ} →
  (motive :
      Array Std.Tactic.BVDecide.LRAT.Internal.Assignment →
        Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1) →
    (x : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
      (x_1 : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
        ((assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
            (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → (b : Bool) → motive assignments (l, b)) →
          motive x x_1
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.comp_homologyMap_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  (h₁ : S₁.LeftHomologyData) (h₂ : S₂.RightHomologyData) {Z : C} (h : h₂.Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp h₁.π
      (CategoryTheory.CategoryStruct.comp h₁.homologyIso.inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ)
          (CategoryTheory.CategoryStruct.comp h₂.homologyIso.hom (CategoryTheory.CategoryStruct.comp h₂.ι h)))) =
    CategoryTheory.CategoryStruct.comp h₁.i
      (CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.CategoryStruct.comp h₂.p h))
-- Mathlib.RingTheory.Filtration
/-- The trivial `I`-filtration of `N`.  -/
Ideal.trivialFiltration : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (I : Ideal R) → Submodule R M → I.Filtration M
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.hasSum_derivWeierstrassP : ∀ (L : PeriodPair) (z : ℂ), HasSum (fun l => -2 / (z - ↑l) ^ 3) (L.derivWeierstrassP z)
-- Mathlib.Order.WellFoundedSet
Set.IsWF.not_lt_min : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α} {a : α} (hs : s.IsWF) (hn : s.Nonempty), a ∈ s → ¬a < hs.min hn
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_lt_aleph0_iff : ∀ {α : Type u}, Cardinal.mk α < Cardinal.aleph0 ↔ Finite α
-- Mathlib.Logic.Basic
dite_eq_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {c : α} {A : P → α} {B : ¬P → α},
  dite P A B = c ↔ (∃ (h : P), A h = c) ∨ ∃ (h : ¬P), B h = c
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H0π_comp_map_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {Z : ModuleCat k} (h : groupHomology B 0 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.H0π A)
      (CategoryTheory.CategoryStruct.comp (groupHomology.map f φ 0) h) =
    CategoryTheory.CategoryStruct.comp (Rep.Hom.toModuleCatHom φ)
      (CategoryTheory.CategoryStruct.comp (groupHomology.H0π B) h)
-- Init.Data.BitVec.Lemmas
BitVec.ule_iff_toNat_le : ∀ {w : ℕ} {x y : BitVec w}, x.ule y = true ↔ x.toNat ≤ y.toNat
-- Mathlib.SetTheory.ZFC.PSet
PSet.instUsesSetNotationForOrder : UsesSetNotationForOrder PSet.{u}
-- Init.Data.List.Lemmas
List.getLast.eq_def : ∀ {α : Type u} (x : List α) (x_1 : x ≠ []),
  x.getLast x_1 =
    match x, x_1 with
    | [], h => absurd ⋯ h
    | [a], x => a
    | head :: b :: as, x => (b :: as).getLast ⋯
-- Init.Data.Range.Polymorphic.RangeIterator
Std.IterM.DefaultConsumers.forIn'.wf.eq_1 : ∀ {m : Type w → Type w'} {α β : Type w} [inst : Std.Iterator α m β] {n : Type x → Type x'} [inst_1 : Monad n]
  (lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x)
  (PlausibleForInStep : β → γ → ForInStep γ → Prop) (wf : Std.IteratorLoop.WellFounded α m PlausibleForInStep)
  (it : Std.IterM m β) (init : γ) (P : β → Prop) (hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b)
  (f : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))),
  Std.IterM.DefaultConsumers.forIn'.wf lift γ PlausibleForInStep wf it init P hP f =
    (fun x => lift (Std.Shrink it.Step) γ x it.step) fun s =>
      match s.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => do
        let __do_lift ← f out ⋯ init
        match __do_lift with
          | ⟨ForInStep.yield c, property⟩ =>
            Std.IterM.DefaultConsumers.forIn'.wf lift γ PlausibleForInStep wf it' c P ⋯ f
          | ⟨ForInStep.done c, property⟩ => pure c
      | ⟨Std.IterStep.skip it', h⟩ => Std.IterM.DefaultConsumers.forIn'.wf lift γ PlausibleForInStep wf it' init P ⋯ f
      | ⟨Std.IterStep.done, property⟩ => pure init
-- Mathlib.Topology.Algebra.Monoid
Inseparable.add : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M] {a b c d : M},
  Inseparable a b → Inseparable c d → Inseparable (a + c) (b + d)
-- Mathlib.GroupTheory.Torsion
/-- Finite additive groups are torsion additive groups.  -/
isAddTorsion_of_finite : ∀ {G : Type u_1} [inst : AddGroup G] [Finite G], IsAddTorsion G
-- Mathlib.Algebra.Polynomial.Laurent
/-- The function `n ↦ T ^ n`, implemented as a sequence `ℤ → R[T;T⁻¹]`.

Using directly `T ^ n` does not work, since we want the exponents to be of Type `ℤ` and there
is no `ℤ`-power defined on `R[T;T⁻¹]`.  Using that `T` is a unit introduces extra coercions.
For these reasons, the definition of `T` is as a sequence.  -/
LaurentPolynomial.T : {R : Type u_1} → [inst : Semiring R] → ℤ → LaurentPolynomial R
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_iSup_of_directed : ∀ {G : Type u_1} [inst : Group G] {ι : Sort u_2} [hι : Nonempty ι] {K : ι → Subgroup G},
  Directed (fun x1 x2 => x1 ≤ x2) K → ∀ {x : G}, x ∈ iSup K ↔ ∃ i, x ∈ K i
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHomClass.toInfTopHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Lattice α] [inst_2 : Lattice β]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [BoundedLatticeHomClass F α β], InfTopHomClass F α β
-- Mathlib.Data.List.Sort
List.Pairwise.eq_of_mem_iff : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Antisymm r] [Std.Irrefl r] {l₁ l₂ : List α},
  List.Pairwise r l₁ → List.Pairwise r l₂ → (∀ (a : α), a ∈ l₁ ↔ a ∈ l₂) → l₁ = l₂
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
HomotopicalAlgebra.RightHomotopyClass.whitehead : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsCofibrant Y] [HomotopicalAlgebra.IsFibrant X]
  [HomotopicalAlgebra.IsFibrant Y] (f : X ⟶ Y) [HomotopicalAlgebra.WeakEquivalence f],
  ∃ g,
    HomotopicalAlgebra.RightHomotopyRel (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X) ∧
      HomotopicalAlgebra.RightHomotopyRel (CategoryTheory.CategoryStruct.comp g f) (CategoryTheory.CategoryStruct.id Y)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
isOpen_extChartAt_preimage' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M) {s : Set E},
  IsOpen s → IsOpen ((extChartAt I x).source ∩ ↑(extChartAt I x) ⁻¹' s)
-- Lean.Util.Trace
/-- Registers a trace class.

By default, trace classes are not inherited;
that is, `set_option trace.foo true` does not imply `set_option trace.foo.bar true`.
Calling ``registerTraceClass `foo.bar (inherited := true)`` enables this inheritance
on an opt-in basis.
 -/
Lean.registerTraceClass : Lean.Name → optParam Bool false → autoParam Lean.Name Lean.registerTraceClass._auto_1 → IO Unit
-- Lean.Meta.Tactic.Simp.SimpTheorems
_private.Lean.Meta.Tactic.Simp.SimpTheorems.0.Lean.Meta.isPerm : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive false) (h_2 : Unit → motive true),
  (match true with
    | false => h_1 ()
    | true => h_2 ()) =
    h_2 ()
-- Init.Data.Dyadic.Basic
Dyadic.toRat_eq_zero_iff : ∀ {x : Dyadic}, x.toRat = 0 ↔ x = 0
-- Mathlib.Data.Seq.Defs
/-- Coinductive principle for equality on sequences.
This is a version of `eq_of_bisim'` that requires proving only `s₁ = s₂`
instead of `s₁ = nil ∧ s₂ = nil` in `step`.  -/
Stream'.Seq.eq_of_bisim_strong : ∀ {α : Type u} {s₁ s₂ : Stream'.Seq α} (motive : Stream'.Seq α → Stream'.Seq α → Prop),
  motive s₁ s₂ →
    (∀ (s₁ s₂ : Stream'.Seq α),
        motive s₁ s₂ →
          s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = Stream'.Seq.cons x s₁' ∧ s₂ = Stream'.Seq.cons x s₂' ∧ motive s₁' s₂') →
      s₁ = s₂
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.of_one : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ],
  (GradedTensorProduct.of R 𝒜 ℬ) 1 = 1
-- Mathlib.Order.Bounded
Set.unbounded_le_inter_le : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
  Set.Unbounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a ≤ b}) ↔ Set.Unbounded (fun x1 x2 => x1 ≤ x2) s
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
CategoryTheory.Functor.EffectivePresentation.mk.injEq : ∀ {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 : CategoryTheory.Functor C D} {X : D} (p : C) (f : F.obj p ⟶ X)
  (effectiveEpi : CategoryTheory.EffectiveEpi f) (p_1 : C) (f_1 : F.obj p_1 ⟶ X)
  (effectiveEpi_1 : CategoryTheory.EffectiveEpi f_1),
  ({ p := p, f := f, effectiveEpi := effectiveEpi } = { p := p_1, f := f_1, effectiveEpi := effectiveEpi_1 }) =
    (p = p_1 ∧ f ≍ f_1)
-- Mathlib.RingTheory.FreeCommRing
instInhabitedFreeCommRing : (α : Type u_1) → Inhabited (FreeCommRing α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi : ∀ {θ : ℝ}, 0 ≤ θ → θ ≤ Real.pi → 0 ≤ (↑θ).sign
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
IsSelfAdjoint.nnnorm_add_eq_max : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {a b : A},
  IsSelfAdjoint a → IsSelfAdjoint b → a * b = 0 → ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊
-- Init.Data.BitVec.Basic
/-- Bitwise xor for bitvectors. Usually accessed via the `^^^` operator.

SMT-LIB name: `bvxor`.

Example:
* `0b1010#4 ^^^ 0b0110#4 = 0b1100#4`
 -/
BitVec.xor : {n : ℕ} → BitVec n → BitVec n → BitVec n
-- Lean.Parser.Command
Lean.Parser.Command.withWeakNamespace.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Vector.Lemmas
Vector.not_any_eq_all_not : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool}, (!xs.any p) = xs.all fun a => !p a
-- Mathlib.RingTheory.AlgebraTower
linearIndependent_smul : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [IsScalarTower R S A] {ι : Type u_5} {b : ι → S}
  {ι' : Type u_6} {c : ι' → A},
  LinearIndependent R b → LinearIndependent S c → LinearIndependent R fun p => b p.1 • c p.2
-- Mathlib.NumberTheory.ClassNumber.Finite
/-- The **class number theorem**: the class group of an integral closure `S` of `R` in an
algebraic extension `L` is finite if there is an admissible absolute value.

See also `ClassGroup.fintypeOfAdmissibleOfFinite` where `L` is a finite
extension of `K = Frac(R)`, supplying most of the required assumptions automatically.
 -/
ClassGroup.fintypeOfAdmissibleOfAlgebraic : {R : Type u_1} →
  {S : Type u_2} →
    [inst : EuclideanDomain R] →
      [inst_1 : CommRing S] →
        [inst_2 : IsDomain S] →
          [inst_3 : Algebra R S] →
            {abv : AbsoluteValue R ℤ} →
              {ι : Type u_5} →
                [DecidableEq ι] →
                  [Fintype ι] →
                    Module.Basis ι R S →
                      abv.IsAdmissible →
                        [Infinite R] →
                          [DecidableEq R] → [IsDedekindDomain S] → [Algebra.IsAlgebraic R S] → Fintype (ClassGroup S)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos : ∀ {x y : ℝ*}, x.InfinitePos → ¬y.Infinitesimal → 0 < y → (x * y).InfinitePos
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Submodule.inf_genEigenspace : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (p : Submodule R M) {k : ℕ∞} {μ : R} (hfp : ∀ x ∈ p, f x ∈ p),
  p ⊓ (f.genEigenspace μ) k = Submodule.map p.subtype ((Module.End.genEigenspace (LinearMap.restrict f hfp) μ) k)
-- Mathlib.Algebra.Lie.TensorProduct
/-- The tensor product of two Lie modules is a Lie module.  -/
TensorProduct.LieModule.lieModule : ∀ {R : Type u} [inst : CommRing R] {L : Type v} {M : Type w} {N : Type w₁} [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 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N], LieModule R L (TensorProduct R M N)
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EquivalenceRelation.transitivity₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.EquivalenceRelation p₁ p₂),
  CategoryTheory.CategoryStruct.comp self.t p₂ = CategoryTheory.CategoryStruct.comp self.c.snd p₂
-- Mathlib.Order.Defs.Unbundled
Std.Symm.decide : ∀ {α : Sort u_1} {r : α → α → Prop} [inst : DecidableRel r] [Std.Symm r], Std.Symm fun a b => decide (r a b) = true
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.mul_certC : Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Poly → ℕ → Bool
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Polynomial.Chebyshev.sumZeroes_T_of_not_dvd : ∀ {n : ℕ} {k : ℤ}, ¬2 * ↑n ∣ k → Polynomial.Chebyshev.sumZeroes n (Polynomial.Chebyshev.T ℝ k) = 0
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquivFunctorCompFstIso_inv_app_app : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor (A ⊕ A') B) (X_1 : A),
  (CategoryTheory.Sum.functorEquivFunctorCompFstIso.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj (Sum.inl X_1))
-- Mathlib.RingTheory.FinitePresentation
Algebra.FinitePresentation.iff : ∀ {R : Type w₁} {A : Type w₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.FinitePresentation R A ↔ ∃ n I x, I.FG
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_keysArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → (↑m).keysArray.size = (↑m).size
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.Iterators.Types.Zip.instIterator.match_3.eq_2 : ∀ {m : Type u_1 → Type u_2} {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type u_1}
  [inst_1 : Std.Iterator α₂ m β₂] (it : Std.IterM m (β₁ × β₂)) (motive : it.internalState.right.Step → Sort u_3)
  (it₂' : Std.IterM m β₂) (hp : it.internalState.right.IsPlausibleStep (Std.IterStep.skip it₂'))
  (h_1 :
    (it₂' : Std.IterM m β₂) →
      (out₂ : β₂) →
        (hp : it.internalState.right.IsPlausibleStep (Std.IterStep.yield it₂' out₂)) →
          motive ⟨Std.IterStep.yield it₂' out₂, hp⟩)
  (h_2 :
    (it₂' : Std.IterM m β₂) →
      (hp : it.internalState.right.IsPlausibleStep (Std.IterStep.skip it₂')) → motive ⟨Std.IterStep.skip it₂', hp⟩)
  (h_3 : (hp : it.internalState.right.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.skip it₂', hp⟩ with
    | ⟨Std.IterStep.yield it₂' out₂, hp⟩ => h_1 it₂' out₂ hp
    | ⟨Std.IterStep.skip it₂', hp⟩ => h_2 it₂' hp
    | ⟨Std.IterStep.done, hp⟩ => h_3 hp) =
    h_2 it₂' hp
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.of.eq_1 : ∀ (M : Type u) [inst : Monoid M], MonCat.of M = { carrier := M, str := inst }
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∈ m₂ → (m₁ \ m₂).get! k = default
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsExistential.below.ex : ∀ {L : FirstOrder.Language} {α : Type u'} {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsExistential → Prop}
  {n : ℕ} {φ : L.BoundedFormula α (n + 1)} (h : φ.IsExistential),
  FirstOrder.Language.BoundedFormula.IsExistential.below h →
    motive φ h → FirstOrder.Language.BoundedFormula.IsExistential.below ⋯
-- Mathlib.Analysis.InnerProductSpace.PiL2
DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] {V : ι → Submodule 𝕜 E}
  (hV : DirectSum.IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ)
  (w : PiLp 2 fun i => ↥(V i)), (hV.isometryL2OfOrthogonalFamily hV').symm w = ∑ i, ↑(w.ofLp i)
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.isPartition_splitMany : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Finset (ι × ℝ)), (BoxIntegral.Prepartition.splitMany I s).IsPartition
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.IsAlgebraic.algEquivEquivAlgHom_symm_apply : ∀ (K : Type u_1) (L : Type u_2) [inst : CommRing K] [inst_1 : IsDomain K] [inst_2 : Field L] [inst_3 : Algebra K L]
  [inst_4 : Module.IsTorsionFree K L] [inst_5 : Algebra.IsAlgebraic K L] (ϕ : L →ₐ[K] L),
  (Algebra.IsAlgebraic.algEquivEquivAlgHom K L).symm ϕ = AlgEquiv.ofBijective ϕ ⋯
-- Mathlib.Algebra.Algebra.NonUnitalHom
AlgHom.NonUnitalAlgHom.hasCoe : {R : Type u_2} →
  [inst : CommSemiring R] →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → CoeOut (A →ₐ[R] B) (A →ₙₐ[R] B)
-- Mathlib.Data.Set.Card
Set.nonempty_inter_compl_of_ncard_add_ncard_lt : ∀ {α : Type u_1} {s t : Set α}, s.ncard + t.ncard < Nat.card α → (sᶜ ∩ tᶜ).Nonempty
-- Init.Prelude
/-- Create syntax node with 6 children  -/
Lean.Syntax.node6 : Lean.SourceInfo →
  Lean.SyntaxNodeKind → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instReflVle : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R], Std.Refl fun x1 x2 => x1 ≤ᵥ x2
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_eq_none : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α},
  a ∉ t → Std.DTreeMap.Const.get? t a = none
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.ediam_image_le_of_subset : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s t : Set X}, HolderOnWith C r f s → t ⊆ s → Metric.ediam (f '' t) ≤ ↑C * Metric.ediam t ^ ↑r
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.instPreadditiveLocalization : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] →
      (W : CategoryTheory.MorphismProperty C) →
        [W.HasLeftCalculusOfFractions] → CategoryTheory.Preadditive W.Localization
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- If `f` is closable, then `f.closure` is the closure. Otherwise it is defined
as `f.closure = f`.  -/
LinearPMap.closure : {R : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module R E] →
              [inst_4 : Module R F] →
                [inst_5 : TopologicalSpace E] →
                  [inst_6 : TopologicalSpace F] →
                    [ContinuousAdd E] →
                      [ContinuousAdd F] →
                        [inst_9 : TopologicalSpace R] →
                          [ContinuousSMul R E] → [ContinuousSMul R F] → (E →ₗ.[R] F) → E →ₗ.[R] F
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_natCast : ∀ (n : ℕ∞), ⌈↑n⌉ₑ = n
-- Mathlib.FieldTheory.KummerPolynomial
root_X_pow_sub_C_pow : ∀ {K : Type u} [inst : Field K] (n : ℕ) (a : K),
  AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) ^ n = (AdjoinRoot.of (Polynomial.X ^ n - Polynomial.C a)) a
-- Mathlib.GroupTheory.Coxeter.Length
/-- The proposition that `i` is a right descent of `w`; that is, $\ell(w s_i) < \ell(w)$.  -/
CoxeterSystem.IsRightDescent : {B : Type u_1} → {W : Type u_2} → [inst : Group W] → {M : CoxeterMatrix B} → CoxeterSystem M W → W → B → Prop
-- Std.Time.Zoned.RecurringRule
/-- Recurring rule describing standard and DST zones, as found in a POSIX TZ string or TZif footer.
 -/
Std.Time.TimeZone.RecurringRule : Type
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_neg : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {S : Type u_1} [inst_1 : Ring S] (f : R →+* S) {x : S},
  Polynomial.eval₂ f x (-p) = -Polynomial.eval₂ f x p
-- Mathlib.Control.Random
Random.instBool : {m : Type → Type u_1} → [Monad m] → Random m Bool
-- Std.Http.Data.URI.Basic
/-- Extracts all query parameter values.
 -/
Std.Http.URI.Query.values : Std.Http.URI.Query → Array (Option Std.Http.URI.EncodedQueryParam)