mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Types
Lean.Parser.ParserInfo.mk.inj : ∀ {collectTokens : List Lean.Parser.Token → List Lean.Parser.Token}
  {collectKinds : Lean.Parser.SyntaxNodeKindSet → Lean.Parser.SyntaxNodeKindSet} {firstTokens : Lean.Parser.FirstTokens}
  {collectTokens_1 : List Lean.Parser.Token → List Lean.Parser.Token}
  {collectKinds_1 : Lean.Parser.SyntaxNodeKindSet → Lean.Parser.SyntaxNodeKindSet}
  {firstTokens_1 : Lean.Parser.FirstTokens},
  { collectTokens := collectTokens, collectKinds := collectKinds, firstTokens := firstTokens } =
      { collectTokens := collectTokens_1, collectKinds := collectKinds_1, firstTokens := firstTokens_1 } →
    collectTokens = collectTokens_1 ∧ collectKinds = collectKinds_1 ∧ firstTokens = firstTokens_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α},
        Std.DHashMap.Internal.Raw₀.Const.get! (m₁.union m₂) k =
          Std.DHashMap.Internal.Raw₀.Const.getD m₂ k (Std.DHashMap.Internal.Raw₀.Const.get! m₁ k)
-- Mathlib.Order.Hom.Lattice
/-- Composition of `LatticeHom`s as a `LatticeHom`.  -/
LatticeHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Lattice α] →
        [inst_1 : Lattice β] → [inst_2 : Lattice γ] → LatticeHom β γ → LatticeHom α β → LatticeHom α γ
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.inradius_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  [inst_8 : NeZero n] (s : Affine.Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂), (s.map f.toAffineMap ⋯).inradius = s.inradius
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.instCategoryTruncated : (C : Type u_2) →
  [inst : CategoryTheory.Category.{u_1, u_2} C] →
    (n : ℕ) → CategoryTheory.Category.{u_1, max u_2 u_1} (CategoryTheory.CosimplicialObject.Truncated C n)
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Meromorphicity in normal form is a local property.  -/
meromorphicNFAt_congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {g : 𝕜 → E},
  f =ᶠ[nhds x] g → (MeromorphicNFAt f x ↔ MeromorphicNFAt g x)
-- Mathlib.RingTheory.ZMod.Torsion
ZMod.rootsOfUnity_eq_top : ∀ {p : ℕ} [Fact (Nat.Prime p)], rootsOfUnity (p - 1) (ZMod p) = ⊤
-- Init.Data.Fin.Lemmas
Fin.pred_le_pred_iff : ∀ {n : ℕ} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha ≤ b.pred hb ↔ a ≤ b
-- Lean.Server.AsyncList
Lean.AsyncList.delayed.inj : ∀ {ε : Type u} {α : Type v} {tl tl_1 : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α))},
  Lean.AsyncList.delayed tl = Lean.AsyncList.delayed tl_1 → tl = tl_1
-- Lean.Data.Lsp.Extra
/-- Range of lines in a document, including `start` but excluding `end`.
 -/
Lean.Lsp.LineRange : Type
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
Submodule.mem_toAffineSubspace : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {p : Submodule k V}
  {x : V}, x ∈ ↑p ↔ x ∈ p
-- ProofWidgets.Data.Html
/-- Interpolates an expression into a JSX literal  -/
ProofWidgets.Jsx.«proofWidgetsJsxChild{_}» : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Basic
/-- If `E` is an `F`-algebra, there exists an `F`-linear isomorphism from `F` to `E` (namely,
`E` is a free `F`-module of rank one), then the algebra map from `F` to `E` is bijective.  -/
bijective_algebraMap_of_linearEquiv : ∀ {F : Type u_1} {E : Type u_2} [inst : CommSemiring F] [inst_1 : Semiring E] [inst_2 : Algebra F E] (b : F ≃ₗ[F] E),
  Function.Bijective ⇑(algebraMap F E)
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
/-- The counit isomorphism of the equivalence  -/
CategoryTheory.Idempotents.KaroubiKaroubi.counitIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (CategoryTheory.Idempotents.KaroubiKaroubi.inverse C).comp
        (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Idempotents.Karoubi C)) ≅
      CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C))
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.instFaithfulSMulSubtypeMemSubalgebraSubalgebra : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] (D : Algebra.Smooth.DescentAux✝ A B),
  FaithfulSMul (↥(Algebra.Smooth.DescentAux.subalgebra✝ R D)) A
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.contains_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k k' : α} {f : Option β → Option β},
      (Std.DHashMap.Internal.Raw₀.Const.alter m k f).contains k' =
        if (k == k') = true then (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).isSome else m.contains k'
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- The structure sheaf on `Proj` 𝒜, valued in `CommRing`.  -/
AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) → [inst_3 : GradedRing 𝒜] → TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)
-- Mathlib.Topology.MetricSpace.HolderNorm
MemHolder.coe_nnHolderNorm_eq_eHolderNorm : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : EMetricSpace Y] {r : NNReal} {f : X → Y},
  MemHolder r f → ↑(nnHolderNorm r f) = eHolderNorm r f
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_rightInverse : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f : σ → τ} {g : τ → σ},
  Function.RightInverse f g → Function.RightInverse ⇑(MvPolynomial.rename f) ⇑(MvPolynomial.rename g)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_ne_empty_iff : ∀ {m n : ℕ}, (m...n).toArray ≠ #[] ↔ m < n
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.firstDiff_def : ∀ {E : ℕ → Type u_2} (x y : (n : ℕ) → E n), PiNat.firstDiff x y = if h : x ≠ y then Nat.find ⋯ else 0
-- Mathlib.Algebra.Quaternion
Quaternion.re_mul : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R),
  (a * b).re = a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.Path.cast_heq : ∀ {U : Type u_1} [inst : Quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Quiver.Path u v),
  Quiver.Path.cast hu hv p ≍ p
-- Mathlib.Topology.Order.OrderClosed
ContinuousAt.eventually_lt : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f g : β → α}
  [inst_3 : TopologicalSpace β] {x₀ : β},
  ContinuousAt f x₀ → ContinuousAt g x₀ → f x₀ < g x₀ → ∀ᶠ (x : β) in nhds x₀, f x < g x
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.neg_neg : ∀ {M : Type u} [inst : Lean.Grind.AddCommGroup M] (a : M), - -a = a
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.mem_saturation_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : AddSubmonoid M} {x : M}, x ∈ s.saturation ↔ ∃ y, x + y ∈ s
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.forall : ∀ {α : Type u} {p : Additive α → Prop}, (∀ (a : Additive α), p a) ↔ ∀ (a : α), p (Additive.ofMul a)
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.IsSolvable.solvable : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsSolvable L], ∃ k, LieAlgebra.derivedSeries R L k = ⊥
-- Mathlib.Topology.ExtendFrom
/-- If `f` is a function to a T₃ space `Y` which has a limit within `A` at any
point of a set `B ⊆ closure A`, then `extendFrom A f` is continuous on `B`.  -/
continuousOn_extendFrom : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [RegularSpace Y] {f : X → Y}
  {A B : Set X},
  B ⊆ closure A → (∀ x ∈ B, ∃ y, Filter.Tendsto f (nhdsWithin x A) (nhds y)) → ContinuousOn (extendFrom A f) B
-- Lean.Meta.HaveTelescope
Lean.Meta.HaveInfo.mk : Std.HashSet ℕ → Std.HashSet ℕ → Lean.LocalDecl → Lean.Level → Lean.Meta.HaveInfo
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instBEqDiagnosticRelatedInformation : BEq Lean.Lsp.DiagnosticRelatedInformation
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- **Alias** of `measurableSet_setOfPred`. -/
measurableSet_setOf : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p : α → Prop}, MeasurableSet {a | p a} ↔ Measurable p
-- Mathlib.Algebra.Homology.HomologySequence
CategoryTheory.ShortComplex.ShortExact.δ_eq : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j) {A : C} (x₃ : A ⟶ S.X₃.X i) (hx₃ : CategoryTheory.CategoryStruct.comp x₃ (S.X₃.d i j) = 0)
  (x₂ : A ⟶ S.X₂.X i),
  CategoryTheory.CategoryStruct.comp x₂ (S.g.f i) = x₃ →
    ∀ (x₁ : A ⟶ S.X₁.X j)
      (hx₁ : CategoryTheory.CategoryStruct.comp x₁ (S.f.f j) = CategoryTheory.CategoryStruct.comp x₂ (S.X₂.d i j))
      (k : ι) (hk : c.next j = k),
      CategoryTheory.CategoryStruct.comp (S.X₃.liftCycles x₃ j ⋯ hx₃)
          (CategoryTheory.CategoryStruct.comp (S.X₃.homologyπ i) (hS.δ i j hij)) =
        CategoryTheory.CategoryStruct.comp (S.X₁.liftCycles x₁ k hk ⋯) (S.X₁.homologyπ j)
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageParams.message : Lean.Lsp.ShowMessageParams → String
-- Mathlib.Algebra.Star.Unitary
Unitary.inv_mul_mem_iff : ∀ {G : Type u_2} [inst : Group G] [inst_1 : StarMul G] (a b : G), a⁻¹ * b ∈ unitary G ↔ a * star a = b * star b
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh_strictMono : StrictMono Real.arsinh
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
/-- The single functor `C ⥤ HomotopyCategory.Plus C` is induced by
`HomotopyCategory.singleFunctor C n : C ⥤ HomotopyCategory C (.up ℤ)`.  -/
HomotopyCategory.Plus.singleFunctorCompιIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        (n : ℤ) →
          (HomotopyCategory.Plus.singleFunctor C n).comp (HomotopyCategory.Plus.ι C) ≅
            HomotopyCategory.singleFunctor C n
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.isVanKampenColimit_extendCofan : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C)
  {c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ} {c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt},
  CategoryTheory.IsVanKampenColimit c₁ →
    CategoryTheory.IsVanKampenColimit c₂ →
      ∀ [∀ {Z : C} (i : Z ⟶ c₂.pt), CategoryTheory.Limits.HasPullback c₂.inr i]
        [CategoryTheory.Limits.HasFiniteCoproducts C],
        CategoryTheory.IsVanKampenColimit (CategoryTheory.extendCofan c₁ c₂)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.range_fromSpec : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U), Set.range ⇑hU.fromSpec = ↑U
-- Init.Data.BitVec.Lemmas
BitVec.getElem?_eq_none : ∀ {w n : ℕ} {l : BitVec w}, w ≤ n → l[n]? = none
-- Mathlib.Topology.Algebra.Group.Basic
instIsTopologicalGroupULift : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G],
  IsTopologicalGroup (ULift.{u_1, w} G)
-- Init.Prelude
/-- `a ||| b` computes the bitwise OR of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `|||` in identifiers is `or`. -/
HOr.hOr : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HOr α β γ] → α → β → γ
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Connected.boxProd : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β}, G.Connected → H.Connected → (G □ H).Connected
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toUInt16 = OfNat.ofNat n
-- Init.Prelude
USize.size_pos : 0 < USize.size
-- Init.Data.Range.Polymorphic.PRange
Std.Roc.instMembershipOfLEOfLT : {α : Type u} → [LE α] → [LT α] → Membership α (Std.Roc α)
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.associator_inv_apply : ∀ {X Y Z : Type u} {x : X} {y : Y} {z : Z},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) (x, y, z) =
    ((x, y), z)
-- Lean.Server.Utils
/-- URI where the document is located.  -/
Lean.Server.DocumentMeta.uri : Lean.Server.DocumentMeta → Lean.Lsp.DocumentUri
-- Lean.Setup
Lean.instFromJsonImportArtifacts : Lean.FromJson Lean.ImportArtifacts
-- Init.Data.String.Defs
List.utf8Encode_cons : ∀ {c : Char} {l : List Char}, (c :: l).utf8Encode = [c].utf8Encode ++ l.utf8Encode
-- Init.Data.Nat.MinMax
Nat.min_eq_min : ∀ {b : ℕ} (a : ℕ), a.min b = min a b
-- Mathlib.Algebra.GradedMonoid
/-- A version of `GradedMonoid.GMonoid` for internally graded objects.  -/
SetLike.GradedMonoid : {ι : Type u_1} → {R : Type u_2} → {S : Type u_3} → [SetLike S R] → [Monoid R] → [AddMonoid ι] → (ι → S) → Prop
-- Mathlib.Data.Set.Basic
Set.PiSetCoe.canLift' : ∀ (ι : Type u) (α : Type v) [Nonempty α] (s : Set ι), CanLift (↑s → α) (ι → α) (fun f i => f ↑i) fun x => True
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_eq_integral_of_support_subset : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ}
  {a b : ℝ}, Function.support f ⊆ Set.Ioc a b → ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.conv_eq_num_div_den : ∀ {K : Type u_1} {g : GenContFract K} {n : ℕ} [inst : DivisionRing K], g.convs n = g.nums n / g.dens n
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.toOrderTop : {α : Type u_3} → [self : LinearOrderedAddCommGroupWithTop α] → OrderTop α
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k fallback : α},
  (Std.HashMap.filterMap f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x_2 h' => (f x_2 m[x_2]).isSome).getD fallback
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.coe_symm_toLinearEquiv : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂),
  f.symm = f.symm.toLinearEquiv
-- Init.Data.SInt.Lemmas
ISize.toInt_div : ∀ (a b : ISize), (a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ System.Platform.numBits)
-- Mathlib.Algebra.Free
/-- Representation of an element of a free magma.  -/
FreeMagma.repr : {α : Type u} → [Repr α] → FreeMagma α → Std.Format
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.continuousWithinAt : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) {s : Set E} {x : E}, ContinuousWithinAt (⇑e) s x
-- Mathlib.Algebra.DirectSum.Internal
SetLike.GradeZero.coe_ofNat : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : Semiring R] [inst_1 : AddMonoid ι] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : SetLike.GradedMonoid A] (n : ℕ) [inst_5 : n.AtLeastTwo],
  ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalizer_empty : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.normalizer ∅ = ⊤
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.incidenceSet_inter_incidenceSet_of_adj : ∀ {V : Type u} (G : SimpleGraph V) {a b : V}, G.Adj a b → G.incidenceSet a ∩ G.incidenceSet b = {s(a, b)}
-- Mathlib.Order.Category.Semilat
SemilatSupCat.hasForgetToPartOrd : CategoryTheory.HasForget₂ SemilatSupCat PartOrd
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.instReprGenPatternInfo : Repr Lean.Meta.Grind.GenPatternInfo
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.forget₂_map : ∀ {R S : GrpCat} (f : R ⟶ S) (x : ↑((CategoryTheory.forget₂ GrpCat MonCat).obj R)),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ GrpCat MonCat).map f)) x =
    (CategoryTheory.ConcreteCategory.hom f) x
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_neg : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [inst : AddGroup R], ↑(-x) = -↑x
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.tensorUnit_carrier : ∀ (R : Type u) [inst : CommRing R], ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (CoalgCat R)).toModuleCat = R
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
/-- The shifted object in resolution by `1` degree.  -/
TopRep.resolution'X : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] →
      [inst_1 : Group G] →
        [inst_2 : TopologicalSpace k] →
          [inst_3 : TopologicalSpace G] → [IsTopologicalGroup G] → TopRep k G → ℕ → TopRep k G
-- Mathlib.Combinatorics.Graph.Basic
Graph.banana_inc : ∀ {α : Type u_1} {β : Type u_2} {x u v : α} {e : β} {edgeSet : Set β},
  (Graph.banana u v edgeSet).Inc e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v)
-- Mathlib.LinearAlgebra.LinearPMap
/-- The property that `f 0 = 0` in terms of the graph.  -/
LinearPMap.graph_fst_eq_zero_snd : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F) {x : E} {x' : F}, (x, x') ∈ f.graph → x = 0 → x' = 0
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The functions from an additive monoid `M` to itself equivariant with respect to
the right `M`-action are exactly left additions by elements of `M`.  -/
AddActionHom.End.addOppositeEquiv : {M : Type u_2} → [inst : AddMonoid M] → (M →ₑ[id] M) ≃+ M
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EquivalenceRelation.isEquivalenceRelation : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (h : CategoryTheory.EquivalenceRelation p₁ p₂), CategoryTheory.IsEquivalenceRelation p₁ p₂
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.ι.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.kernelCokernelCompSequence.ι f g =
    CategoryTheory.Limits.biprod.lift (CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp f g)) f)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_geom_sum : ∀ {R : Type u_1} [inst : CommSemiring R] {n : ℕ} {x : R},
  Polynomial.eval x (∑ i ∈ Finset.range n, Polynomial.X ^ i) = ∑ i ∈ Finset.range n, x ^ i
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- **Alias** of `MeasureTheory.setIntegral_eq_of_subset_of_forall_sdiff_eq_zero`.

---

If a function vanishes on `t \ s` with `s ⊆ t`, then its integrals on `s`
and `t` coincide if `t` is measurable.  -/
MeasureTheory.setIntegral_eq_of_subset_of_forall_diff_eq_zero : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasurableSet t → s ⊆ t → (∀ x ∈ t \ s, f x = 0) → ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k a : α}, (t.insert k).get! a = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.get! a
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_8} [inst : NormedAddCommGroup β]
  {T : Set α → β} {C : ℝ},
  MeasureTheory.DominatedFinMeasAdditive μ T C → ∀ {s : Set α}, MeasurableSet s → μ s = 0 → T s = 0
-- Mathlib.Data.Finset.Sym
Finset.sym2_univ : ∀ {α : Type u_1} [inst : Fintype α] (inst_1 : optParam (Fintype (Sym2 α)) Sym2.instFintype),
  Finset.univ.sym2 = Finset.univ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' fallback : α} {f : β k → β k},
  (t.modify k f).getKeyD k' fallback =
    if cmp k k' = Ordering.eq then if k ∈ t then k else fallback else t.getKeyD k' fallback
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.Saturate.below.of : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.Precoverage C}
  {motive : (X : C) → (a : CategoryTheory.Sieve X) → J.Saturate X a → Prop} (X : C) (S : CategoryTheory.Presieve X)
  (hS : S ∈ J.coverings X), CategoryTheory.Precoverage.Saturate.below ⋯
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- If `{Uᵢ}` covers `X`, this is the `0`-hypercover of `X ×[Z] Y` given by `{Uᵢ ×[Z] Y}`.  -/
CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      [J.IsStableUnderBaseChange] →
        {X : C} →
          (E : J.ZeroHypercover X) →
            {Y Z : C} →
              (f : X ⟶ Z) →
                (g : Y ⟶ Z) →
                  [inst_2 : CategoryTheory.Limits.HasPullback f g] →
                    [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.fst f g)] →
                      J.ZeroHypercover (CategoryTheory.Limits.pullback f g)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_iff_isSome_get? : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α}, a ∈ m ↔ (m.get? a).isSome = true
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
/-- If `f` is a nonarchimedean additive group seminorm on a commutative ring `α`, `n : ℕ`, and
`a b : α`, then we can find `m : ℕ` such that `m ≤ n` and
`f ((a + b) ^ n) ≤ (f (a ^ m)) * (f (b ^ (n - m)))`.  -/
IsNonarchimedean.add_pow_le : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {F : Type u_2} {α : Type u_3} [inst_2 : CommRing α]
  [inst_3 : FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] [SubmultiplicativeHomClass F α R] {f : F},
  IsNonarchimedean ⇑f → ∀ (n : ℕ) (a b : α), ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.instIsClosedUnderSubobjectsIsArtinianObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.isArtinianObject.IsClosedUnderSubobjects
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.leftUnitor_inv_app : ∀ {B C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B),
  (CategoryTheory.Bicategory.leftUnitor F).inv.toNatTrans.app X = CategoryTheory.eqToHom ⋯
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.affineBasisCover_map_range : ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X) (r : ↑⋯.choose),
  Set.range ⇑(X.affineBasisCover.f ⟨x, r⟩) = ⇑(X.affineCover.f x) '' (PrimeSpectrum.basicOpen r).carrier