mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.setOfPred_index_eq_univ : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] [P.IsIrreducible],
  {RootPairing.EmbeddedG2.long P, -RootPairing.EmbeddedG2.long P, RootPairing.EmbeddedG2.short P,
      -RootPairing.EmbeddedG2.short P, RootPairing.EmbeddedG2.shortAddLong P, -RootPairing.EmbeddedG2.shortAddLong P,
      RootPairing.EmbeddedG2.twoShortAddLong P, -RootPairing.EmbeddedG2.twoShortAddLong P,
      RootPairing.EmbeddedG2.threeShortAddLong P, -RootPairing.EmbeddedG2.threeShortAddLong P,
      RootPairing.EmbeddedG2.threeShortAddTwoLong P, -RootPairing.EmbeddedG2.threeShortAddTwoLong P} =
    Set.univ
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt64.size), (UInt64.ofNatClamp n).toBitVec = n#'hn
-- Mathlib.Topology.Constructions.SumProd
prod_eq_generateFrom : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  instTopologicalSpaceProd = TopologicalSpace.generateFrom {g | ∃ s t, IsOpen s ∧ IsOpen t ∧ g = s ×ˢ t}
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.ofComplex_apply : ∀ (z : UpperHalfPlane), ↑UpperHalfPlane.ofComplex ↑z = z
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.mem_commutator : ∀ {G : Type u_1} [inst : Group G] [hP : Group.IsPerfect G] {g : G}, g ∈ commutator G
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsStronglyCocartesian.fac_assoc : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCocartesian f φ]
  {S' : 𝒮} {b' : 𝒳} {g : S ⟶ S'} {f' : R ⟶ S'} (hf' : f' = CategoryTheory.CategoryStruct.comp f g) (φ' : a ⟶ b')
  [inst_3 : p.IsHomLift f' φ'] {Z : 𝒳} (h : b' ⟶ Z),
  CategoryTheory.CategoryStruct.comp φ
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCocartesian.map p f φ hf' φ') h) =
    CategoryTheory.CategoryStruct.comp φ' h
-- Mathlib.Tactic.Abel
/-- Construct the normal form representing a single term.  -/
Mathlib.Tactic.Abel.NormalExpr.term' : Lean.Expr × ℤ → ℕ × Lean.Expr → Mathlib.Tactic.Abel.NormalExpr → Mathlib.Tactic.Abel.M Mathlib.Tactic.Abel.NormalExpr
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.coe_top : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M], ↑⊤ = Set.univ
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.ord_mk_le_type : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] (s : Set α), (Cardinal.mk ↑s).ord ≤ Ordinal.type r
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.image_closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X),
  ⇑h '' closure s = closure (⇑h '' s)
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.genWeightSpace_genWeightSpaceOf_map_incl : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [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 : LieRing.IsNilpotent L] (x : L) (χ : L → R),
  LieSubmodule.map (LieModule.genWeightSpaceOf M (χ x) x).incl
      (LieModule.genWeightSpace (↥(LieModule.genWeightSpaceOf M (χ x) x)) χ) =
    LieModule.genWeightSpace M χ
-- Mathlib.Order.WithBot
WithBot.strictMono_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : WithBot α → β},
  StrictMono f ↔ (StrictMono fun a => f ↑a) ∧ ∀ (x : α), f ⊥ < f ↑x
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.refl_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} (C : HomologicalComplex V c), (HomotopyEquiv.refl C).hom = CategoryTheory.CategoryStruct.id C
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.empty_vecMul : ∀ {α : Type u} {o' : Type uₒ} [inst : NonUnitalNonAssocSemiring α] (v : Fin 0 → α) (B : Matrix (Fin 0) o' α),
  Matrix.vecMul v B = 0
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_5} {ε' : Type u_6}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [inst_2 : TopologicalSpace ε'] [inst_3 : ContinuousENorm ε']
  {f : α → ε} {g : α → ε'} {c : NNReal},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ) →
    ∀ {p : ℝ}, 0 < p → MeasureTheory.eLpNorm' f p μ ≤ c • MeasureTheory.eLpNorm' g p μ
-- Init.System.IOError
IO.Error.resourceBusy.sizeOf_spec : ∀ (osCode : UInt32) (details : String),
  sizeOf (IO.Error.resourceBusy osCode details) = 1 + sizeOf osCode + sizeOf details
-- Mathlib.Data.Finsupp.Order
Finsupp.support_inf : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsBotZeroClass α]
  [inst_3 : DecidableEq ι] (f g : ι →₀ α), (f ⊓ g).support = f.support ∩ g.support
-- Mathlib.Combinatorics.Additive.Convolution
Finset.card_inter_vadd_neg : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  (A ∩ (x +ᵥ -B)).card = A.addConvolution B x
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.evalCLM_apply : ∀ {α : Type u} {β : Type v} (𝕜 : Type u_2) [inst : PseudoMetricSpace 𝕜] [inst_1 : TopologicalSpace α]
  [inst_2 : PseudoMetricSpace β] [inst_3 : Semiring 𝕜] [inst_4 : AddCommMonoid β] [inst_5 : Module 𝕜 β]
  [inst_6 : IsBoundedSMul 𝕜 β] [inst_7 : BoundedAdd β] [inst_8 : ContinuousAdd β] (x : α)
  (f : BoundedContinuousFunction α β), (BoundedContinuousFunction.evalCLM 𝕜 x) f = f x
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k)
-- Aesop.RuleSet
Aesop.LocalRuleSet.applicableSafeRulesWith : Aesop.LocalRuleSet →
  Aesop.ForwardRuleMatches →
    Lean.MVarId → (Aesop.SafeRule → Bool) → Aesop.BaseM (Array (Aesop.IndexMatchResult Aesop.SafeRule))
-- Mathlib.FieldTheory.Normal.Defs
Normal.isIntegral : ∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K],
  Normal F K → ∀ (x : K), IsIntegral F x
-- Mathlib.Order.CompleteLattice.Basic
iSup_sum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : β ⊕ γ → α},
  ⨆ x, f x = (⨆ i, f (Sum.inl i)) ⊔ ⨆ j, f (Sum.inr j)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.jacobiMatrix_apply : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_3 : Fintype σ] [inst_4 : DecidableEq σ] (i j : σ),
  P.jacobiMatrix i j = (MvPolynomial.pderiv (P.map i)) (P.relation j)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.disjointUnion_source : ∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β) (hs : Disjoint e.source e'.source)
  (ht : Disjoint e.target e'.target) [inst : (x : α) → Decidable (x ∈ e.source)]
  [inst_1 : (y : β) → Decidable (y ∈ e.target)], (e.disjointUnion e' hs ht).source = e.source ∪ e'.source
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.re_pellZd : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), (Pell.pellZd a1 n).re = ↑(Pell.xn a1 n)
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
ContinuousLinearMapWOT.continuousWithinAt_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {α : Type u_4} [inst_7 : TopologicalSpace α] {f : α → E →WOT[𝕜] F} {s : Set α} {a : α},
  ContinuousWithinAt f s a ↔ ∀ (x : E) (y : F), ContinuousWithinAt (fun x_1 => inner 𝕜 y ((f x_1) x)) s a
-- Mathlib.Topology.Separation.Basic
/-- **Alias** of `Dense.sdiff_finset`.

---

Removing a finset from a dense set in a space without isolated points, one still
obtains a dense set.  -/
Dense.diff_finset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] {s : Set X},
  Dense s → ∀ (t : Finset X), Dense (s \ ↑t)
-- Mathlib.Order.OrderDual
OrderDual.instDecidableLE : (α : Type u_2) → [inst : LE α] → [h : DecidableLE α] → DecidableLE αᵒᵈ
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The kernel inclusion is natural.  -/
CategoryTheory.Limits.ker.ι : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasKernels C] → CategoryTheory.Limits.ker C ⟶ CategoryTheory.Arrow.leftFunc
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.hom_as_subtype : ∀ (M : Type u_1) [inst : Monoid M] (X : Type u) [inst_1 : MulAction M X] (p q : CategoryTheory.ActionCategory M X),
  (p ⟶ q) = { m // m • p.back = q.back }
-- Mathlib.Topology.MetricSpace.Dilation
/-- The `ratio` is equal to the distance ratio for any two points
with nonzero finite distance; `dist` version  -/
Dilation.ratio_unique_of_dist_ne_zero : ∀ {α : Type u_6} {β : Type u_7} {F : Type u_5} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] {f : F} {x y : α} {r : NNReal},
  dist x y ≠ 0 → dist (f x) (f y) = ↑r * dist x y → r = Dilation.ratio f
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdx!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited α] (x : ℕ),
  Std.DTreeMap.Internal.Impl.leaf.keyAtIdx! x =
    panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.keyAtIdx!" 503 16
      "Out-of-bounds access"
-- Init.Data.Vector.Lemmas
Vector.eq_of_mem_replicate : ∀ {α : Type u_1} {a b : α} {n : ℕ}, b ∈ Vector.replicate n a → b = a
-- Mathlib.Analysis.Convex.Segment
right_mem_openSegment_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {x y : E} [DenselyOrdered 𝕜] [Module.IsTorsionFree 𝕜 E],
  y ∈ openSegment 𝕜 x y ↔ x = y
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.sub_apply' : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_4} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] {M₂ : Type u_5} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} (f g : M →SL[σ₁₂] M₂) (x : M), (↑f - ↑g) x = f x - g x
-- Mathlib.Topology.Bornology.Basic
Bornology.isCobounded_univ : ∀ {α : Type u_2} {x : Bornology α}, Bornology.IsCobounded Set.univ
-- Mathlib.Analysis.LConvolution
MeasureTheory.lconvolution_assoc₀ : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] {f g k : G → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g μ →
      AEMeasurable k μ →
        MeasureTheory.lconvolution f (MeasureTheory.lconvolution g k μ) μ =
          MeasureTheory.lconvolution (MeasureTheory.lconvolution f g μ) k μ
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.instBEqAbsoluteLspSemanticToken : BEq Lean.Server.FileWorker.AbsoluteLspSemanticToken
-- Mathlib.Probability.Kernel.Composition.CompMap
ProbabilityTheory.Kernel.deterministic_comp_deterministic : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : β → γ} {g : γ → α} (hf : Measurable f) (hg : Measurable g),
  (ProbabilityTheory.Kernel.deterministic g hg).comp (ProbabilityTheory.Kernel.deterministic f hf) =
    ProbabilityTheory.Kernel.deterministic (g ∘ f) ⋯
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.xor_right_inj : ∀ {x y z : ℕ}, x ^^^ y = x ^^^ z ↔ y = z
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.curryRingEquiv_symm_single : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N] (m : M)
  (n : N) (r : R),
  AddMonoidAlgebra.curryRingEquiv.symm (AddMonoidAlgebra.single m (AddMonoidAlgebra.single n r)) =
    AddMonoidAlgebra.single (m, n) r
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageKind.notification.sizeOf_spec : sizeOf Lean.JsonRpc.MessageKind.notification = 1
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.quotKerTotalEquiv_symm_apply : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (a : Ω[S⁄R]),
  (KaehlerDifferential.quotKerTotalEquiv R S).symm a =
    (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential a
-- Mathlib.Data.Sym.Sym2
Sym2.mem_iff' : ∀ {α : Type u_1} {a b c : α}, Sym2.Mem a s(b, c) ↔ a = b ∨ a = c
-- Mathlib.Data.ENat.Basic
ENat.nat_induction : ∀ {motive : ℕ∞ → Prop} (a : ℕ∞),
  motive 0 → (∀ (n : ℕ), motive ↑n → motive ↑n.succ) → ((∀ (n : ℕ), motive ↑n) → motive ⊤) → motive a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∩ t₂)[k]? = if k ∈ t₂ then t₁[k]? else none
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
MvPolynomial.mem_image_comap_C_basicOpen : ∀ {R : Type u_2} [inst : CommRing R] {σ : Type u_1} (f : MvPolynomial σ R) (x : PrimeSpectrum R),
  x ∈ PrimeSpectrum.comap MvPolynomial.C '' ↑(PrimeSpectrum.basicOpen f) ↔ ∃ i, MvPolynomial.coeff i f ∉ x.asIdeal
-- Init.Data.Slice.Notation
/-- This typeclass indicates how to obtain slices of elements of `α` over ranges in the index type
`β`, the ranges being left-unbounded right-open.

The type of the resulting slices is `γ`.
 -/
Std.Rio.Sliceable : Type u → outParam (Type v) → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.Topology.DiscreteQuotient
/-- If `X` is a compact space, then we associate to any discrete quotient on `X` a finite set of
clopen subsets of `X`, given by the fibers of `proj`.

TODO: prove that these form a partition of `X`
 -/
DiscreteQuotient.finsetClopens : (X : Type u_2) →
  [inst : TopologicalSpace X] → [CompactSpace X] → DiscreteQuotient X → Finset (TopologicalSpace.Clopens X)
-- Init.Data.UInt.Lemmas
UInt64.mod_def : ∀ (a b : UInt64), a % b = { toBitVec := a.toBitVec % b.toBitVec }
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.MonoOver.top_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C), ⊤.arrow = CategoryTheory.CategoryStruct.id X
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Poly.denote.match_1.splitter : (motive : Lean.Grind.Linarith.Poly → Sort u_1) →
  (p : Lean.Grind.Linarith.Poly) →
    (Unit → motive Lean.Grind.Linarith.Poly.nil) →
      ((k : ℤ) →
          (v : Lean.Grind.Linarith.Var) →
            (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add k v p)) →
        motive p
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
/-- If `F` preserves the colimit of every `Discrete.functor f`, it preserves all colimits of shape
`Discrete J`.  -/
CategoryTheory.Limits.preservesColimitsOfShape_of_discrete : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} (F : CategoryTheory.Functor C D)
  [∀ (f : J → C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) F],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- **Alias** of the forward direction of `hasFDerivWithinAt_iff_isLittleO`. -/
HasFDerivWithinAt.isLittleO : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {s : Set E} {x : E},
  HasFDerivWithinAt f f' s x → (fun x' => f x' - f x - f' (x' - x)) =o[nhdsWithin x s] fun x' => x' - x
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
/-- An auxiliary `MetricSpace` instance on the upper half-plane. This instance has bad projection
to `TopologicalSpace`. We replace it later.  -/
UpperHalfPlane.metricSpaceAux : MetricSpace UpperHalfPlane
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_pair_le_right : ∀ {α : Type u_1} [inst : EDist α] {x y : α}, x ≠ y → {x, y}.einfsep ≤ edist y x
-- Mathlib.CategoryTheory.Sites.SheafHom
CategoryTheory.presheafHom_isSheafFor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  (F G : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.Sieve X)
  (hG :
    ⦃Y : C⦄ →
      (f : Y ⟶ X) → CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Sieve.pullback f S).arrows.cocone.op)),
  CategoryTheory.Presieve.IsSheafFor (CategoryTheory.presheafHom F G) S.arrows
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isSome_get?_iff_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, (t.get? a).isSome = true ↔ a ∈ t
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
IsIntegral.tmul : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (x : A) {y : B}, IsIntegral R y → IsIntegral A (x ⊗ₜ[R] y)
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.mem_support_cycleOf_iff : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} [inst : DecidableEq α] [inst_1 : Fintype α],
  y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshotInner.mk.inj : ∀ {α : Type} {toSnapshot : Lean.Language.Snapshot} {stx : Lean.Syntax} {inner? : Option (Lean.Language.SnapshotTask α)}
  {finished : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticFinishedSnapshot}
  {toSnapshot_1 : Lean.Language.Snapshot} {stx_1 : Lean.Syntax} {inner?_1 : Option (Lean.Language.SnapshotTask α)}
  {finished_1 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticFinishedSnapshot},
  { toSnapshot := toSnapshot, stx := stx, inner? := inner?, finished := finished } =
      { toSnapshot := toSnapshot_1, stx := stx_1, inner? := inner?_1, finished := finished_1 } →
    toSnapshot = toSnapshot_1 ∧ stx = stx_1 ∧ inner? = inner?_1 ∧ finished = finished_1
-- Init.Data.Float.Model.Unpacked.Operations.Sqrt
/-- Computes a `(mantissa, exponent)` pair for the square root with enough bits to populate the mantissa
for the given specification. Also returns an `Accuracy` stating how the returned pair relates to
the infinitely precise square root.
 -/
Float.Model.UnpackedFloat.sqrtCore : Float.Model.Format → ℕ → ℤ → ℕ × ℤ × Float.Model.UnpackedFloat.Accuracy
-- Init.Data.Int.Linear
Int.not_ge_eq : ∀ (a b : ℤ), (¬a ≥ b) = (a + 1 ≤ b)
-- Mathlib.CategoryTheory.Subfunctor.Subobject
CategoryTheory.Subfunctor.subobjectMk_range_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (X : CategoryTheory.Subobject F), CategoryTheory.Subobject.mk (CategoryTheory.Subfunctor.range X.arrow).ι = X
-- Lean.Parser.Extra
Lean.ppSpace.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getEntryDₘ_eq_getEntryD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α β} {fallback : (a : α) × β a},
  t.Ordered → Std.DTreeMap.Internal.Impl.getEntryDₘ k t fallback = Std.Internal.List.getEntryD k fallback t.toListModel
-- Mathlib.Order.KrullDimension
Order.coheight_nat : ∀ (n : ℕ), Order.coheight n = ⊤
-- Init.Data.Rat.Basic
Rat.instPowNat : Pow ℚ ℕ
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_iSup : ∀ {ι : Sort u_1} {M : Type u_2} [inst : MulOneClass M] (S : ι → Submonoid Mᵐᵒᵖ), (iSup S).unop = ⨆ i, (S i).unop
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.mem_of_models : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (p : T.CompleteType α) {φ : (L.withConstants α).Sentence},
  (L.lhomWithConstants α).onTheory T ⊨ᵇ φ → φ ∈ p
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.coe_inv_coe' : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c d : ↑S.objs} (p : c ⟶ d),
  ↑(CategoryTheory.inv p) = CategoryTheory.inv ↑p
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.norm_le_one : ∀ (z : Complex.UnitClosedDisc), ‖↑z‖ ≤ 1
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.isBounded : ∀ {ι : Type u_1} [Finite ι] (I : BoxIntegral.Box ι), Bornology.IsBounded ↑I
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.length_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  it.length = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => do
        let __do_lift ← it'.length
        pure { down := __do_lift.down + 1 }
      | Std.IterStep.skip it' => do
        let __do_lift ← it'.length
        pure { down := __do_lift.down }
      | Std.IterStep.done => pure { down := 0 }
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- An inner product with a sum on the right, `Finsupp` version.  -/
Finsupp.inner_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {M : Type u_5} [inst_3 : Zero M] (l : ι →₀ M) (v : ι → M → E) (x : E),
  inner 𝕜 x (l.sum v) = l.sum fun i a => inner 𝕜 x (v i a)
-- Mathlib.Order.Hom.Basic
/-- An order isomorphism respects `≤`.  -/
OrderIsoClass.map_le_map_iff : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : LE α} {inst_1 : LE β}
  {inst_2 : EquivLike F α β} [self : OrderIsoClass F α β] (f : F) {a b : α}, f a ≤ f b ↔ a ≤ b
-- Mathlib.LinearAlgebra.Basis.Defs
/-- A module over `R` with a finite basis is linearly equivalent to functions from its basis to `R`.
 -/
Module.Basis.equivFun : {ι : Type u_1} →
  {R : Type u_3} →
    {M : Type u_6} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [Finite ι] → Module.Basis ι R M → M ≃ₗ[R] ι → R
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.Hom.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
  [inst_1 : SizeOf C] (f : P.X ⟶ Q.X)
  (comm :
    autoParam (CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp f Q.p) = f)
      CategoryTheory.Idempotents.Karoubi.Hom.comm._autoParam),
  sizeOf { f := f, comm := comm } = 1 + sizeOf f + sizeOf comm
-- Mathlib.Analysis.Meromorphic.Basic
/-- The singular set of a meromorphic function is countable.
 -/
Meromorphic.countable_compl_analyticAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} [SecondCountableTopology 𝕜] [CompleteSpace E],
  Meromorphic f → {z | AnalyticAt 𝕜 f z}ᶜ.Countable
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_singleton : ∀ {α : Type u} {a : α} (ha : optParam {a}.Finite ⋯), ha.toFinset = {a}