mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Term
Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean_2 : Coe (Lean.TSyntax `Lean.Parser.Term.matchExprAltExpr) (Lean.TSyntax `Lean.Parser.Term.matchExprAlt)
-- Mathlib.Algebra.Notation.Indicator
Set.support_indicator : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {f : α → M},
  Function.support (s.indicator f) = s ∩ Function.support f
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.polarizationIn_Injective : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  (S : Type u_5) [inst_6 : CommRing S] [IsDomain R] [IsDomain S] [inst_9 : Algebra S R] [inst_10 : FaithfulSMul S R]
  [inst_11 : P.IsValuedIn S] [inst_12 : Module S M] [inst_13 : IsScalarTower S R M] [inst_14 : Module S N]
  [IsScalarTower S R N] [P.IsAnisotropic], Function.Injective ⇑(P.PolarizationIn S)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piCongrRight_refl : ∀ {ι : Type u_7} {R : ι → Type u_8} [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)],
  (RingEquiv.piCongrRight fun i => RingEquiv.refl (R i)) = RingEquiv.refl ((i : ι) → R i)
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- Make a `NameSet` containing all prefixes of `n`.  -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Lean.Name.prefixes : Lean.Name → Lean.NameSet
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_top : ∀ {R : Type u_1} [inst : CommRing R], ⊤.height = ⊤
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.tendsto_log_comp_add_sub_log : ∀ (y : ℝ), Filter.Tendsto (fun x => Real.log (x + y) - Real.log x) Filter.atTop (nhds 0)
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.mk.sizeOf_spec : ∀ (toLinOrd : LinOrd) [nonempty : Nonempty ↑toLinOrd] [fintype : Fintype ↑toLinOrd],
  sizeOf { toLinOrd := toLinOrd, nonempty := nonempty, fintype := fintype } =
    1 + sizeOf toLinOrd + sizeOf nonempty + sizeOf fintype
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.minpolyX_map : ∀ {K : Type u_1} [inst : Field K] (f : RatFunc K) (A : Type u_2) [inst_1 : CommRing A] [inst_2 : Algebra K A]
  [inst_3 : Algebra (↥K[f]) A] (B : Type u_3) [inst_4 : CommRing B] [inst_5 : Algebra K B] [inst_6 : Algebra (↥K[f]) B]
  [inst_7 : Algebra A B] [IsScalarTower K A B] [IsScalarTower (↥K[f]) A B],
  Polynomial.map (algebraMap A B) (f.minpolyX A) = f.minpolyX B
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.denote : Nat.Internal.Linear.Context → Nat.Internal.Linear.Expr → ℕ
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.flip.eq_1 : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {mM : AddZeroClass M} {mN : AddZeroClass N} {mP : AddCommMonoid P}
  (f : M →+ N →+ P),
  f.flip =
    { toFun := fun y => { toFun := fun x => (f x) y, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_right_split.eq_1 : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly) (k : ℕ),
  Int.Internal.Linear.cooper_right_split ctx p₁ p₂ k =
    (Int.Internal.Linear.Poly.denote' ctx
          (((p₁.tail.mul_k p₂.leadCoeff).combine (p₂.tail.mul_k (-p₁.leadCoeff))).addConst (-p₁.leadCoeff * ↑k)) ≤
        0 ∧
      p₂.leadCoeff ∣ Int.Internal.Linear.Poly.denote' ctx (p₂.tail.addConst ↑k))
-- Init.Data.Float.Float
instReprAtomFloat : ReprAtom Float
-- Mathlib.Analysis.Normed.Group.Basic
/-- An analogue of `norm_le_mul_norm_add` for the multiplication from the left.  -/
norm_le_mul_norm_add' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (u v : E), ‖v‖ ≤ ‖u * v‖ + ‖u‖
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.length_toList : ∀ {α : Type u} {r : Std.Ric α} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxc.HasSize α] [inst_5 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_7 : Std.Rxc.IsAlwaysFinite α] [Std.Rxc.LawfulHasSize α],
  r.toList.length = r.size
-- Mathlib.Algebra.QuadraticDiscriminant
/-- Discriminant of a quadratic  -/
discrim : {R : Type u_1} → [Ring R] → R → R → R → R
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.IsPath.below.nil : ∀ {F : PFunctor.{uA, uB}} {motive : (a : PFunctor.Approx.Path F) → (a_1 : F.M) → PFunctor.M.IsPath a a_1 → Prop}
  (x : F.M), PFunctor.M.IsPath.below ⋯
-- Mathlib.Analysis.Normed.Group.Constructions
pi_nnnorm_le_iff' : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (G i)] {x : (i : ι) → G i}
  {r : NNReal}, ‖x‖₊ ≤ r ↔ ∀ (i : ι), ‖x i‖₊ ≤ r
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
/-- A pairing for a subcomplex `A` of a simplicial set `X` consists of a partition
of the nondegenerate simplices of `X` not in `A` in two types (I) and (II) of simplices,
and a bijection between the type (II) simplices and the type (I) simplices.
See the introduction of the file
`Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean`.  -/
SSet.Subcomplex.Pairing : {X : SSet} → X.Subcomplex → Type u
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroupEmpty_equivariantMap_bijective : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α],
  Function.Bijective ⇑(SubAddAction.ofFixingAddSubgroup_equivariantMap M ∅)
-- Std.Data.TreeMap.Raw.Basic
/-- Computes the difference of the given tree maps.
This function always iterates through the smaller map.
 -/
Std.TreeMap.Raw.diff : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Std.TreeMap.Raw α β cmp → Std.TreeMap.Raw α β cmp
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.hp₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (self : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp self.chosenPullback.p₂ h₂₃.p₂ = self.p₃
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.mk : {α : Type u} → Option α → α → Std.Rxc.Iterator α
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_bijective : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂], Function.Bijective ContinuousLinearEquiv.symm
-- Mathlib.Computability.RecursiveIn
RecursiveIn.of_eq_tot : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {O : Set (ℕ →. ℕ)} {f : α →. σ}
  {g : α → σ}, RecursiveIn O f → (∀ (n : α), g n ∈ f n) → RecursiveIn O ↑g
-- Mathlib.Tactic.Abel
/-- Evaluate an expression into its `abel` normal form, by recursing into subexpressions.  -/
Mathlib.Tactic.Abel.eval : Lean.Expr → Mathlib.Tactic.Abel.M (Mathlib.Tactic.Abel.NormalExpr × Lean.Expr)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
/-- The pairs of parts of a partition `P` which are not `ε`-dense in a graph `G`. Note that we
dismiss the diagonal. We do not care whether `s` is `ε`-dense with itself.  -/
Finpartition.sparsePairs : {α : Type u_1} →
  {𝕜 : Type u_2} →
    [Field 𝕜] →
      [LinearOrder 𝕜] →
        [inst : DecidableEq α] →
          {A : Finset α} →
            Finpartition A → (G : SimpleGraph α) → [DecidableRel G.Adj] → 𝕜 → Finset (Finset α × Finset α)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- The Hausdorff dimension of a non-degenerate segment in a real normed space is 1.  -/
Real.dimH_segment : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {x y : E},
  x ≠ y → dimH (segment ℝ x y) = 1
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.preimage_iSup : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {ι : Sort u_1} (U : ι → Y.Opens),
  (TopologicalSpace.Opens.map f.base).obj (iSup U) = ⨆ i, (TopologicalSpace.Opens.map f.base).obj (U i)
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.mapDomain_vadd : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Monoid S] [inst_1 : Semiring R]
  [inst_2 : DistribMulAction S R] (f : M → N) (s : S) (x : AddMonoidAlgebra R M),
  AddMonoidAlgebra.mapDomain f (s • x) = s • AddMonoidAlgebra.mapDomain f x
-- Init.Data.Fin.Lemmas
Fin.castSucc_lt_last : ∀ {n : ℕ} (a : Fin n), a.castSucc < Fin.last n
-- Mathlib.Data.Nat.Upto
/-- The subtype of natural numbers `i` which have the property that
no `j` less than `i` satisfies `p`. This is an initial segment of the
natural numbers, up to and including the first value satisfying `p`.

We will be particularly interested in the case where there exists a value
satisfying `p`, because in this case the `>` relation is well-founded.  -/
Nat.Upto : (ℕ → Prop) → Type
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_iSup : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {ι : Sort u_1} (N : ι → LieSubmodule R L M),
  LieSubmodule.map f (⨆ i, N i) = ⨆ i, LieSubmodule.map f (N i)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.WalkingParallelFamily.Hom.id : {J : Type w} →
  (X : CategoryTheory.Limits.WalkingParallelFamily J) → CategoryTheory.Limits.WalkingParallelFamily.Hom J X X
-- Mathlib.Data.TwoPointing
/-- The `false`, `true` two-pointing of `Bool`.  -/
TwoPointing.bool : TwoPointing Bool
-- Mathlib.CategoryTheory.Category.RelCat
/-- The argument-swap isomorphism from `RelCat` to its opposite.  -/
CategoryTheory.RelCat.opFunctor : CategoryTheory.Functor CategoryTheory.RelCat CategoryTheory.RelCatᵒᵖ
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
diam_smul₀ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [NormSMulClass 𝕜 E] (c : 𝕜) (x : Set E), Metric.diam (c • x) = ‖c‖ * Metric.diam x
-- Mathlib.Order.Interval.Set.SuccPred
Set.Icc_pred_right_eq_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a b : α),
  Set.Icc a (Order.pred b) = Set.Ico a b
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.ofEq_h₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : φ₁ = φ₂),
  (CategoryTheory.ShortComplex.Homotopy.ofEq h).h₂ = 0
-- Mathlib.Order.PrimeIdeal
/-- A filter `F` is prime if its complement is an ideal.
 -/
Order.PFilter.IsPrime : {P : Type u_1} → [inst : Preorder P] → Order.PFilter P → Prop
-- Mathlib.Analysis.Normed.Lp.LpEquiv
coe_equiv_lpPiLp : ∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [inst_1 : Finite α]
  (f : ↥(lp E p)), (Equiv.lpPiLp f).ofLp = ↑f
-- Mathlib.CategoryTheory.Adjunction.Comma
/-- Given a right adjoint to `F`, we can construct a terminal object in each costructured arrow
category on `F`.  -/
CategoryTheory.mkTerminalOfRightAdjoint : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor D C) →
          {F : CategoryTheory.Functor C D} →
            (h : F ⊣ G) →
              (A : D) → CategoryTheory.Limits.IsTerminal (CategoryTheory.CostructuredArrow.mk (h.counit.app A))
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.abs_right : ∀ {R : Type u} [inst : CommRing R] [inst_1 : LinearOrder R] [AddLeftMono R] {x y : R}, IsCoprime x y → IsCoprime x |y|
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
/-- Lower estimate on the measure of the `ε`-cone in an `n`-dimensional normed space
divided by the measure of the ball.  -/
MeasureTheory.Measure.toSphereBallBound : ℕ → ℝ → NNReal
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.instHashableExpr_lean : Hashable Lean.Grind.AC.Expr
-- Batteries.Data.HashMap.Basic
/-- Similar to `insert`, but also returns a boolean flag indicating whether an existing entry has been
replaced with `a => b`.
```
def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.insert' "three" 3 = ({"one" => 1, "two" => 2, "three" => 3}, false)
hashMap.insert' "two" 0 = ({"one" => 1, "two" => 0}, true)
```
 -/
Batteries.HashMap.insert' : {α : Type u_1} →
  {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α β → α → β → Batteries.HashMap α β × Bool
-- Mathlib.Control.Monad.Cont
WriterT.callCC' : {m : Type u → Type v} →
  [Monad m] →
    [MonadCont m] → {α β ω : Type u} → [Monoid ω] → (MonadCont.Label α (WriterT ω m) β → WriterT ω m α) → WriterT ω m α
-- Mathlib.Order.LiminfLimsup
/-- Given an indexed family of sets `s j` over `j : Subtype p` and a function `f`, then
`liminfReparam j` is equal to `j` if `f` is bounded below on `s j`, and otherwise to some
index `k` such that `f` is bounded below on `s k` (if there exists one).
To ensure good measurability behavior, this index `k` is chosen as the minimal suitable index.
This function is used to write down a liminf in a measurable way,
in `Filter.HasBasis.liminf_eq_ciSup_ciInf` and `Filter.HasBasis.liminf_eq_ite`.  -/
Filter.liminfReparam : {α : Type u_1} →
  {ι : Type u_4} →
    {ι' : Type u_5} →
      [ConditionallyCompleteLinearOrder α] →
        (ι → α) →
          (ι' → Set ι) → (p : ι' → Prop) → [Countable (Subtype p)] → [Nonempty (Subtype p)] → Subtype p → Subtype p
-- Mathlib.Algebra.GroupWithZero.Defs
GroupWithZero.toInv : {G₀ : Type u} → [self : GroupWithZero G₀] → Inv G₀
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- To prove a property of a sum, it suffices to prove that
the property is additive and holds on summands.  -/
Finset.sum_induction : ∀ {ι : Type u_1} {s : Finset ι} {M : Type u_7} [inst : AddCommMonoid M] (f : ι → M) (p : M → Prop),
  (∀ (a b : M), p a → p b → p (a + b)) → p 0 → (∀ x ∈ s, p (f x)) → p (∑ x ∈ s, f x)
-- Init.Data.Range.Polymorphic.UInt
USize.instHasSize : Std.Rxc.HasSize USize
-- Init.Data.Fin.Lemmas
Fin.succ_inj : ∀ {n : ℕ} {a b : Fin n}, a.succ = b.succ ↔ a = b
-- Mathlib.RingTheory.Nilpotent.Defs
Commute.isNilpotent_mul_left : ∀ {R : Type u_1} {x y : R} [inst : Semiring R], Commute x y → IsNilpotent y → IsNilpotent (x * y)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The closure of the collection of elements of the form `prehaar K₀ U`,
for `U` open neighbourhoods of `1`, contained in `V`. The closure is taken in the space
`compacts G → ℝ`, with the topology of pointwise convergence.
We show that the intersection of all these sets is nonempty, and the Haar measure
on compact sets is defined to be an element in the closure of this intersection.  -/
MeasureTheory.Measure.haar.clPrehaar : {G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] → Set G → TopologicalSpace.OpenNhdsOf 1 → Set (TopologicalSpace.Compacts G → ℝ)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.comap_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] {f : BoundedLatticeHom α β},
  Monotone (BooleanSubalgebra.comap f)
-- Init.Data.Array.Lemmas
Array.contains_append : ∀ {α : Type u_1} [inst : BEq α] {xs ys : Array α} {x : α}, (xs ++ ys).contains x = (xs.contains x || ys.contains x)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.tsub_lt_tsub_left_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable (a - b) → b ≤ a → c < b → a - b < a - c
-- Init.Data.SInt.Lemmas
ISize.toInt16_ofNat' : ∀ {n : ℕ}, (ISize.ofNat n).toInt16 = Int16.ofNat n
-- Init.Data.Array.Monadic
Array.mapM_wfParam : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α} {f : α → m β},
  Array.mapM f (wfParam xs) = Array.mapM f xs.attach.unattach
-- Mathlib.Topology.ExtremallyDisconnected
CompactT2.Projective.extremallyDisconnected : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X] [T2Space X],
  CompactT2.Projective X → ExtremallyDisconnected X
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_unique : ∀ {m : Type u_2} {α : Type v} [inst : Unique m] [inst_1 : DecidableEq m] [inst_2 : Zero α] (d : m → α),
  Matrix.diagonal d = Matrix.of fun x x_1 => d default
-- Mathlib.Algebra.Group.Irreducible.Defs
/-- If an irreducible element factors, then one factor is a unit.  -/
Irreducible.isUnit_or_isUnit : ∀ {M : Type u_1} [inst : Monoid M] {p : M}, Irreducible p → ∀ ⦃a b : M⦄, p = a * b → IsUnit a ∨ IsUnit b
-- LeanSearchClient.LoogleSyntax
/-- The turnstyle uesd bin `#find`, unicode or ascii allowed  -/
LeanSearchClient.turnstyle : Lean.ParserDescr
-- Qq.Delab
Qq.Impl.pp.qq : Lean.Option Bool
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.pso_inv : ∀ (p : Type u_2) (q : Type u_3) (R : Type u₂) [inst : DecidableEq p] [inst_1 : DecidableEq q] [inst_2 : CommRing R]
  [inst_3 : Fintype p] [inst_4 : Fintype q] {i : R},
  i * i = -1 → LieAlgebra.Orthogonal.Pso p q R i * LieAlgebra.Orthogonal.Pso p q R (-i) = 1
-- Std.Sync.Channel
Std.CloseableChannel.Error.ofNat_ctorIdx : ∀ (x : Std.CloseableChannel.Error), Std.CloseableChannel.Error.ofNat x.ctorIdx = x
-- Init.Data.String.Iterate
String.Slice.RevByteIterator.instForInCharOfMonad : {m : Type u → Type v} → [Monad m] → ForIn m String.Slice Char
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote_ofVar : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (x : Lean.Grind.CommRing.Var),
  Lean.Grind.CommRing.Mon.denote ctx (Lean.Grind.CommRing.Mon.ofVar x) = Lean.Grind.CommRing.Var.denote ctx x
-- Lean.Util.FindLevelMVar
Lean.FindLevelMVar.Visitor : Type
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.ncard_vadd_set : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (a : G) (s : Set α),
  (a +ᵥ s).ncard = s.ncard
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc : ∀ {R : Type u} [inst : CommRing R] {S : Type u} [inst_1 : CommRing S] (f : R →+* S)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) {Z : CommRingCat}
  (h :
    CommRingCat.of
        ↑((AlgebraicGeometry.Spec.structureSheaf S).obj.obj
            (Opposite.op
              ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom (algebraMap R ↑((AlgebraicGeometry.Spec.structureSheaf R).obj.obj (Opposite.op U))))
      (CategoryTheory.CategoryStruct.comp
        (CommRingCat.ofHom
          (AlgebraicGeometry.StructureSheaf.comap f U
            ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U) ⋯))
        h) =
    CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom f)
      (CategoryTheory.CategoryStruct.comp
        (CommRingCat.ofHom
          (algebraMap S
            ↑((AlgebraicGeometry.Spec.structureSheaf S).obj.obj
                (Opposite.op
                  ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U)))))
        h)
-- Std.Http.Data.Method
Std.Http.Method.update.sizeOf_spec : sizeOf Std.Http.Method.update = 1
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom_inv_id : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom_inv_id._auto_1),
  CategoryTheory.CategoryStruct.comp (X.fromOpcycles f (CategoryTheory.CategoryStruct.id i₁) f ⋯ n₁)
      (X.opcyclesIsoH f n₀ n₁ hn₁).inv =
    CategoryTheory.CategoryStruct.id (X.opcycles f (CategoryTheory.CategoryStruct.id i₁) n₁)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instUniqueOfIsEmpty.eq_1 : ∀ {α : Type u} [inst : IsEmpty α], FreeGroup.instUniqueOfIsEmpty = { toInhabited := FreeGroup.instInhabited, uniq := ⋯ }
-- Mathlib.Algebra.Module.Torsion.Free
smul_right_injective : ∀ {R : Type u_1} (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R}
  [Module.IsTorsionFree R M] [IsCancelMulZero R], r ≠ 0 → Function.Injective fun x => r • x
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- A formal multilinear series over a field `𝕜`, from `E` to `F`, is given by a family of
multilinear maps from `E^n` to `F` for all `n`.  -/
FormalMultilinearSeries : (𝕜 : Type u_1) →
  (E : Type u_2) →
    (F : Type u_3) →
      [inst : Semiring 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : TopologicalSpace E] →
              [ContinuousAdd E] →
                [ContinuousConstSMul 𝕜 E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : Module 𝕜 F] →
                      [inst_8 : TopologicalSpace F] →
                        [ContinuousAdd F] → [ContinuousConstSMul 𝕜 F] → Type (max (max u_3 u_2) 0)
-- Plausible.Arbitrary
/-- Samples from the generator associated with the `Arbitrary` instance for a type,
using `size` as the size parameter for the generator.
To invoke this function, you will need to specify what type `α` is,
for example by doing `runArbitrary (α := Nat) 10`.  -/
Plausible.Arbitrary.runArbitrary : {α : Type} → [Plausible.Arbitrary α] → ℕ → IO α
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.unitOfList_cons : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {hd : α} {tl : List α},
  Std.DHashMap.Raw.Const.unitOfList (hd :: tl) = Std.DHashMap.Raw.Const.insertManyIfNewUnit (∅.insertIfNew hd ()) tl
-- Std.Http.Data.Extensions
_private.Std.Http.Data.Extensions.0.Std.Http.Extensions.mk.sizeOf_spec : ∀ (data : Std.TreeMap Lean.Name Dynamic Std.Http.Extensions.compareName), sizeOf { data := data } = 1 + sizeOf data
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- If two morphisms on `G` coincide on the elements of a basis, then they coincide.  -/
FreeGroupBasis.ext_hom : ∀ {ι : Type u_1} {G : Type u_3} {H : Type u_4} [inst : Group G] [inst_1 : Group H] (b : FreeGroupBasis ι G)
  (f g : G →* H), (∀ (i : ι), f (b i) = g (b i)) → f = g
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.union_vadd_inter_subset_union : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s₁ s₂ : Set α} {t₁ t₂ : Set β},
  (s₁ ∪ s₂) +ᵥ t₁ ∩ t₂ ⊆ (s₁ +ᵥ t₁) ∪ (s₂ +ᵥ t₂)
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.nonempty : ∀ {α : Type v} {s : Set α} [inst : LinearOrder α] [Nonempty α], IsClub s → s.Nonempty
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialLeftAdjoint_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D C) (X : F.PartialLeftAdjointSource),
  F.partialLeftAdjoint.obj X = F.partialLeftAdjointObj X
-- Mathlib.Order.Filter.Basic
Filter.eventually_congr : ∀ {α : Type u} {f : Filter α} {p q : α → Prop},
  (∀ᶠ (x : α) in f, p x ↔ q x) → ((∀ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, q x)