mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.HausdorffDimension
ContinuousLinearEquiv.dimH_preimage : ∀ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (e : E ≃L[𝕜] F) (s : Set F),
  dimH (⇑e ⁻¹' s) = dimH s
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_insert : ∀ {α : Type u} [inst : Semiring α] (x : α) (s : Set α), Ideal.span (insert x s) = Ideal.span {x} ⊔ Ideal.span s
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.le_op_iff : ∀ {R : Type u_2} [inst : NonAssocRing R] {S₁ : Subring Rᵐᵒᵖ} {S₂ : Subring R}, S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.apply_def : ∀ {α : Type u_2} {ι : Type u_3} (l : Combinatorics.Line α ι) (x : α), ↑l x = fun i => (l.idxFun i).getD x
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_sub_uIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a - x) '' Set.uIcc b c = Set.uIcc (a - b) (a - c)
-- Mathlib.Analysis.Complex.Spectrum
_private.Mathlib.Analysis.Complex.Spectrum.0.QuasispectrumRestricts.termσₙ : Lean.ParserDescr
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.Precheck.Context : Type
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.satAssignment_inl : ∀ {aig : Std.Sat.AIG ℕ} {assign1 : ℕ → Bool} {x : ℕ},
  Std.Sat.AIG.toCNF.cnfSatAssignment✝ aig assign1 (x + aig.decls.size) = assign1 x
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Given two measures `μ` and `ν`, `measurableLE μ ν` is the set of measurable
functions `f`, such that, for all measurable sets `A`, `∫⁻ x in A, f x ∂μ ≤ ν A`.

This is useful for the Lebesgue decomposition theorem.  -/
MeasureTheory.Measure.LebesgueDecomposition.measurableLE : {α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → Set (α → ENNReal)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctorMapIso_hom : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  {F F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))} (e : F ≅ F')
  (I₁ : Type u_7) (I₂ : Type u_8) (I₃ : Type u_9),
  (CategoryTheory.GradedObject.mapTrifunctorMapIso e I₁ I₂ I₃).hom =
    CategoryTheory.GradedObject.mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃
-- Mathlib.Algebra.Module.Projective
Function.Surjective.surjective_linearMapComp_left : ∀ {R : Type u_1} [inst : Semiring R] {P : Type u_2} [inst_1 : AddCommMonoid P] [inst_2 : Module R P] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_4} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  [Module.Projective R P] {f : M →ₗ[R] P}, Function.Surjective ⇑f → Function.Surjective fun g => f ∘ₗ g
-- Aesop.Tree.Data
Aesop.Rapp.setIntroducedMVars : Aesop.UnorderedArraySet Lean.MVarId → Aesop.Rapp → Aesop.Rapp
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ici : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => a * x) ⁻¹' Set.Ici b = Set.Ici (b / a)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
Commute.cfcₙHom : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A]
  [inst_3 : Module 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : TopologicalSpace A]
  [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [T2Space A] {a b : A} (ha : p a),
  Commute a b → Commute (star a) b → ∀ (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜), Commute ((cfcₙHom ha) f) b
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_le_one' : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a b : α}, a / b ≤ 1 ↔ a ≤ b
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.instReprMRefinePat : Repr Lean.Parser.Tactic.MRefinePat
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.eq_of_left : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → Function.IsFixedPt (⇑f) x → x = y
-- Mathlib.Algebra.Group.Action.Defs
MulDistribMulAction.toMulAction : {M : Type u_9} →
  {N : Type u_10} → {inst : Monoid M} → {inst_1 : Monoid N} → [self : MulDistribMulAction M N] → MulAction M N
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_neg_right : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F), inner 𝕜 x (-y) = -inner 𝕜 x y
-- Mathlib.Data.Vector3
Fin2.add.eq_def : ∀ {n : ℕ} (i : Fin2 n) (x : ℕ),
  i.add x =
    match x with
    | 0 => i
    | k.succ => (i.add k).fs
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.instToForwardSearcher_1 : {pat : String} → String.Slice.Pattern.ToForwardSearcher pat String.Slice.Pattern.ForwardSliceSearcher
-- Mathlib.Algebra.Order.UpperLower
IsUpperSet.mul_right : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s t : Set α},
  IsUpperSet s → IsUpperSet (s * t)
-- Mathlib.Order.Cover
CovBy.irrefl : ∀ {α : Type u_1} [inst : Preorder α], Std.Irrefl fun x1 x2 => x1 ⋖ x2
-- Lean.DocString.Types
Lean.Doc.instOrdInline.ord : {i : Type u_1} → [Ord i] → Lean.Doc.Inline i → Lean.Doc.Inline i → Ordering
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.NonlinearRightInverse.mk.sizeOf_spec : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {f : E →SL[σ] F} [inst_6 : SizeOf 𝕜] [inst_7 : SizeOf 𝕜']
  [inst_8 : SizeOf E] [inst_9 : SizeOf F] (toFun : F → E) (nnnorm : NNReal)
  (bound' : ∀ (y : F), ‖toFun y‖ ≤ ↑nnnorm * ‖y‖) (right_inv' : ∀ (y : F), f (toFun y) = y),
  sizeOf { toFun := toFun, nnnorm := nnnorm, bound' := bound', right_inv' := right_inv' } = 1 + sizeOf nnnorm
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewRawFact.mk.injEq : ∀ (proof prop : Lean.Expr) (generation : ℕ) (splitSource : Lean.Meta.Grind.SplitSource)
  (ematchDiagSource : Lean.Meta.Grind.EMatchDiagSource) (proof_1 prop_1 : Lean.Expr) (generation_1 : ℕ)
  (splitSource_1 : Lean.Meta.Grind.SplitSource) (ematchDiagSource_1 : Lean.Meta.Grind.EMatchDiagSource),
  ({ proof := proof, prop := prop, generation := generation, splitSource := splitSource,
        ematchDiagSource := ematchDiagSource } =
      { proof := proof_1, prop := prop_1, generation := generation_1, splitSource := splitSource_1,
        ematchDiagSource := ematchDiagSource_1 }) =
    (proof = proof_1 ∧
      prop = prop_1 ∧ generation = generation_1 ∧ splitSource = splitSource_1 ∧ ematchDiagSource = ematchDiagSource_1)
-- Init.Data.SInt.Lemmas
ISize.toInt16_ofInt : ∀ {n : ℤ}, (ISize.ofInt n).toInt16 = Int16.ofInt n
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mul_subset_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s₁ s₂ t₁ t₂ : Finset α}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ * t₁ ⊆ s₂ * t₂
-- Mathlib.Analysis.Convex.Quasiconvex
QuasiconvexOn.monotone_comp : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {β : Type u_6} {γ : Type u_7} [inst_4 : LinearOrder β] [inst_5 : Preorder γ] {s : Set E}
  {f : E → β} {g : β → γ}, Monotone g → QuasiconvexOn 𝕜 s f → QuasiconvexOn 𝕜 s (g ∘ f)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenspace_nat : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ}, (f.genEigenspace μ) ↑k = ((f - μ • 1) ^ k).ker
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- The eigenspaces of a self-adjoint operator are mutually orthogonal.  -/
LinearMap.IsSymmetric.orthogonalFamily_eigenspaces : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E},
  T.IsSymmetric →
    OrthogonalFamily 𝕜 (fun μ => ↥(Module.End.eigenspace T μ)) fun μ => (Module.End.eigenspace T μ).subtypeₗᵢ
-- Mathlib.Data.Nat.Prime.Basic
/-- **Alias** of the reverse direction of `Nat.coprime_two_left`. -/
Odd.coprime_two_left : ∀ {n : ℕ}, Odd n → Nat.Coprime 2 n
-- Std.Data.DTreeMap.Internal.Operations
/-- The tree is balanced.  -/
Std.DTreeMap.Internal.Impl.BalancedTree.balanced_impl : ∀ {α : Type u} {β : α → Type v} (self : Std.DTreeMap.Internal.Impl.BalancedTree α β), self.impl.Balanced
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.incMatrix.congr_simp : ∀ (R : Type u_1) {α : Type u_2} (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ [inst : Zero R] [inst_1 : One R] {inst_2 : DecidableEq α} [inst_3 : DecidableEq α] {inst_4 : DecidableRel G.Adj}
      [inst_5 : DecidableRel G_1.Adj] (a a_1 : α),
      a = a_1 → ∀ (a_2 a_3 : Sym2 α), a_2 = a_3 → SimpleGraph.incMatrix R G a a_2 = SimpleGraph.incMatrix R G_1 a_1 a_3
-- Mathlib.Algebra.Order.Floor.Div
floorDiv_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : FloorDiv α β] (b : β), b ⌊/⌋ 0 = 0
-- Mathlib.Data.ENat.Basic
ENat.instSuccAddOrder : SuccAddOrder ℕ∞
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app : ∀ {X : AlgebraicGeometry.Scheme} (X_1 : X.Opensᵒᵖ),
  AlgebraicGeometry.Scheme.restrictFunctorΓ.hom.app X_1 = X.presheaf.map (CategoryTheory.eqToHom ⋯)
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.BorelCantelli.process.eq_1 : ∀ {Ω : Type u_2} (s : ℕ → Set Ω) (n : ℕ),
  MeasureTheory.BorelCantelli.process s n = ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso.congr_simp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p p_1 : CategoryTheory.Functor 𝒳 𝒮) (e_p : p = p_1) {R R' S : 𝒮} {a a' b : 𝒳} {f f_1 : R ⟶ S} (e_f : f = f_1)
  {f' f'_1 : R' ⟶ S} (e_f' : f' = f'_1) {g g_1 : R' ≅ R} (e_g : g = g_1)
  (h : f' = CategoryTheory.CategoryStruct.comp g.hom f) (φ φ_1 : a ⟶ b) (e_φ : φ = φ_1) (φ' φ'_1 : a' ⟶ b)
  (e_φ' : φ' = φ'_1) [inst_2 : p.IsStronglyCartesian f φ] [inst_3 : p.IsStronglyCartesian f' φ'],
  CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso p h φ φ' =
    CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso p_1 ⋯ φ_1 φ'_1
-- Mathlib.Analysis.Normed.Ring.Basic
MulOpposite.normOneClass : ∀ {α : Type u_2} [inst : SeminormedAddCommGroup α] [inst_1 : One α] [NormOneClass α], NormOneClass αᵐᵒᵖ
-- Batteries.Lean.NameMapAttribute
/-- The description of the attribute  -/
Lean.NameMapAttributeImpl.descr : {α : Type} → Lean.NameMapAttributeImpl α → String
-- Mathlib.Algebra.Star.Unitary
Unitary.instInhabitedSubtypeMemSubmonoidUnitary : {R : Type u_1} → [inst : Monoid R] → [inst_1 : StarMul R] → Inhabited ↥(unitary R)
-- Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Subgroup.Commensurable.properlyDiscontinuousSMul_iff : ∀ {Γ : Type u_1} {α : Type u_2} [inst : Group Γ] [inst_1 : TopologicalSpace α] [inst_2 : MulAction Γ α]
  [ContinuousConstSMul Γ α] {G H : Subgroup Γ},
  G.Commensurable H → (ProperlyDiscontinuousSMul (↥G) α ↔ ProperlyDiscontinuousSMul (↥H) α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.isLocalMax_T_real : ∀ {n k : ℕ},
  n ≠ 0 →
    0 < k →
      k < n →
        Even k → IsLocalMax (fun x => Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n)) (Real.cos (↑k * Real.pi / ↑n))
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.list_prod_map_rpow' : ∀ {ι : Type u_1} (l : List ι) (f : ι → NNReal) (r : ℝ), (List.map (fun x => f x ^ r) l).prod = (List.map f l).prod ^ r
-- Mathlib.Data.List.Permutation
_private.Mathlib.Data.List.Permutation.0.Nat.factorial.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyGE?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → ∀ {k : α}, Std.DTreeMap.Internal.Impl.getKeyGE? k t₁ = Std.DTreeMap.Internal.Impl.getKeyGE? k t₂
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.cancel_counitInv_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : D} (f f' : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y) = CategoryTheory.CategoryStruct.comp f' (e.counitInv.app Y) ↔
    f = f'
-- Mathlib.Order.Lattice
Monotone.of_map_inf_le_left : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst_1 : Preorder β] {f : α → β},
  (∀ (x y : α), f (x ⊓ y) ≤ f x) → Monotone f
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
nonZeroDivisorsLeft_eq_nonZeroDivisors : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀], nonZeroDivisorsLeft M₀ = nonZeroDivisors M₀
-- Mathlib.Algebra.DualNumber
DualNumber.coe_lift_symm_apply : ∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (F : DualNumber A →ₐ[R] B),
  ↑(DualNumber.lift.symm F) = (F.comp (TrivSqZeroExt.inlAlgHom R A A), F DualNumber.eps)
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.State.mk : Std.HashMap.Raw Lean.Meta.Canonicalizer.ExprVisited UInt64 →
  Std.HashMap UInt64 (List Lean.Expr) → Lean.Meta.Canonicalizer.State
-- Mathlib.Algebra.GroupWithZero.Units.Basic
mul_inv_eq_iff_eq_mul₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, b ≠ 0 → (a * b⁻¹ = c ↔ a = c * b)
-- Mathlib.Order.Hom.WithTopBot
/-- Any `OrderTop` is equivalent to `WithTop` of the subtype excluding `⊤`.

See also `Equiv.optionSubtypeNe`.  -/
WithTop.subtypeOrderIso : {α : Type u_1} →
  [inst : PartialOrder α] → [inst_1 : OrderTop α] → [DecidablePred fun x => x = ⊤] → WithTop { a // a ≠ ⊤ } ≃o α
-- Mathlib.Algebra.Order.Ring.Abs
one_le_sq_iff_one_le_abs : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α), 1 ≤ a ^ 2 ↔ 1 ≤ |a|
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Finset.Nat.antidiagonalTuple_zero_right : ∀ (k : ℕ), Finset.Nat.antidiagonalTuple k 0 = {0}
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHint.deferredResolution : Lean.Elab.InlayHint → Lean.Elab.InlayHintInfo → Lean.MetaM Lean.Elab.InlayHintInfo
-- Lean.Data.AssocList
Lean.AssocList.toList : {α : Type u} → {β : Type v} → Lean.AssocList α β → List (α × β)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.inclusion_inclusion : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {E F G : IntermediateField K L} (hEF : E ≤ F) (hFG : F ≤ G) (x : ↥E),
  (IntermediateField.inclusion hFG) ((IntermediateField.inclusion hEF) x) = (IntermediateField.inclusion ⋯) x
-- Mathlib.Data.Set.Lattice
Set.directedOn_sUnion : ∀ {α : Type u_1} {r : α → α → Prop} {S : Set (Set α)},
  DirectedOn (fun x1 x2 => x1 ⊆ x2) S → (∀ x ∈ S, DirectedOn r x) → DirectedOn r (⋃₀ S)
-- Init.Data.String.Bootstrap
Substring.Raw.Internal.prev : Substring.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.coe_rangeRestrict : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (g : G),
  ↑(f.rangeRestrict g) = f g
-- ProofWidgets.Presentation.Expr
/-- Whether the output HTML has inline (think something which fits in the space normally occupied
by an `Expr`, e.g. LaTeX) or block (think large diagram which needs dedicated space) layout.  -/
ProofWidgets.ExprPresenter.layoutKind : ProofWidgets.ExprPresenter → ProofWidgets.LayoutKind
-- Init.Data.UInt.Bitwise
UInt8.toBitVec_not : ∀ {a : UInt8}, (~~~a).toBitVec = ~~~a.toBitVec
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcL_apply : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  (a_1 : C(↑(spectrum R a), R)), (cfcL ha) a_1 = (cfcHom ha) a_1
-- Init.Tactics
/-- An erasure specification `-thm` says to remove `thm` from the simp set  -/
Lean.Parser.Tactic.simpErase : Lean.ParserDescr
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- A data-bearing typeclass which distinguishes a pair of roots whose pairing is `-3`. This is a
sufficient condition for the span of this pair of roots to be a `𝔤₂` root system.  -/
RootPairing.EmbeddedG2 : {ι : 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] → RootPairing ι R M N → Type u_1
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_inv : ∀ {α : Type u_1} {m : Type u_3} [inst : CommRing α] [inst_1 : StarRing α] [inst_2 : Fintype m] [inst_3 : DecidableEq m]
  (A : Matrix m m α) [Invertible A], A⁻¹.IsHermitian ↔ A.IsHermitian
-- Mathlib.Tactic.Linarith.NNRealPreprocessor
/-- **Alias** of `Mathlib.Tactic.Linarith.mkToRealNonnegProof?`.

---

If `e : ℝ≥0`, returns a proof of `0 ≤ (e : ℝ)`.  -/
Mathlib.Tactic.Linarith.mk_toReal_nonneg_prf : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic.0.Real.sqrtTwoAddSeries.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The completion of `K` with respect to its `v`-adic valuation, defined as a one-field structure
wrapping the uniform-space completion `(v.valuation K).Completion`.  -/
IsDedekindDomain.HeightOneSpectrum.adicCompletion : {R : Type u_1} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [IsFractionRing R K] → IsDedekindDomain.HeightOneSpectrum R → Type u_2
-- Mathlib.Topology.Category.LightProfinite.AsLimit
/-- `S.asLimitCone` is indeed a limit cone.  -/
LightProfinite.asLimit : (S : LightProfinite) → CategoryTheory.Limits.IsLimit S.asLimitCone
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_preimage_equiv_lift : ∀ {α : Type u} {β : Type v} (f : α ≃ β) (s : Set β),
  Cardinal.lift.{v, u} (Cardinal.mk ↑(⇑f ⁻¹' s)) = Cardinal.lift.{u, v} (Cardinal.mk ↑s)
-- Mathlib.Algebra.Order.Field.Basic
one_half_pos : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α], 0 < 1 / 2
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A cofan over `f : β → C` consists of a collection of maps from every `f b` to an object `P`.  -/
CategoryTheory.Limits.Cofan : {β : Type w} → {C : Type u} → [CategoryTheory.Category.{v, u} C] → (β → C) → Type (max (max w u) v)
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToHom_trans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y = Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) (CategoryTheory.eqToHom q) = CategoryTheory.eqToHom ⋯
-- Lean.Language.Basic
Lean.Language.instMonadLiftProcessingMProcessingTIO : MonadLift Lean.Language.ProcessingM (Lean.Language.ProcessingT IO)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Local notation for the positive elements of a type `α`.  -/
_private.Mathlib.Algebra.Order.GroupWithZero.Defs.0.«termα>0» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.Module
Matrix.Module.smul_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (N : Matrix ι ι R) (v : ι → M) (i : ι), (N • v) i = ∑ j, N i j • v j
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Special case of product model with corners, which is trivial on the second factor. This shows up
as the model to tangent bundles.  -/
ModelWithCorners.tangent : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type w} →
            [inst_3 : TopologicalSpace H] → ModelWithCorners 𝕜 E H → ModelWithCorners 𝕜 (E × E) (ModelProd H E)
-- Mathlib.Data.Set.MemPartition
memPartitionSet.eq_2 : ∀ {α : Type u_1} (f : ℕ → Set α) (n : ℕ),
  memPartitionSet f n.succ = fun a => if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- The functor `shrinkCoyoneda.{w}` followed by the evaluation
at `Y : C` and `uliftFunctor.{v}` identifies to `yoneda.obj Y` followed
by `uliftFunctor.{w}`.  -/
CategoryTheory.shrinkCoyonedaCompEvaluationCompUliftFunctorIsoUliftFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      (Y : C) →
        CategoryTheory.shrinkCoyoneda.{w, v, u}.comp
            (((CategoryTheory.evaluation C (Type w)).obj Y).comp CategoryTheory.uliftFunctor.{v, w}) ≅
          (CategoryTheory.yoneda.obj Y).comp CategoryTheory.uliftFunctor.{w, v}
-- Mathlib.Topology.PartitionOfUnity
/-- If `X` is a normal topological space and `U i`, `i : ι`, is a locally finite open covering of a
closed set `s`, then there exists a `BumpCovering ι X s` that is subordinate to `U`. If `X` is a
paracompact space, then the assumption `hf : LocallyFinite U` can be omitted, see
`BumpCovering.exists_isSubordinate`.  -/
BumpCovering.exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [LocallyCompactSpace X] [T2Space X],
  IsCompact s →
    ∀ (U : ι → Set X),
      (∀ (i : ι), IsOpen (U i)) →
        LocallyFinite U → s ⊆ ⋃ i, U i → ∃ f, f.IsSubordinate U ∧ ∀ (i : ι), HasCompactSupport ⇑(f i)
-- Mathlib.Order.Filter.CountablyGenerated
Filter.countable_biInf_principal_eq_seq_iInf : ∀ {α : Type u_1} {B : Set (Set α)}, B.Countable → ∃ x, ⨅ t ∈ B, Filter.principal t = ⨅ i, Filter.principal (x i)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.checkNoImmediateColon.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.extendRight.instIsScalarTowerSubtypeMem_2 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (M : Type u_3) [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [inst_6 : IsScalarTower K L M]
  {R : Type u_4} {S : Type u_5} [inst_7 : CommRing R] [inst_8 : CommRing S] [inst_9 : Algebra S ↥F]
  [inst_10 : Algebra S M] [inst_11 : IsScalarTower S (↥F) M] [inst_12 : Algebra R S] [inst_13 : Algebra R ↥F]
  [inst_14 : Algebra R M] [inst_15 : IsScalarTower R (↥F) M] [IsScalarTower R S M], IsScalarTower R S ↥(F.extendRight M)
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.lintegral_bind : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : MeasureTheory.Measure α}
  {μ : α → MeasureTheory.Measure β} {f : β → ENNReal},
  AEMeasurable μ m → AEMeasurable f (m.bind μ) → ∫⁻ (x : β), f x ∂m.bind μ = ∫⁻ (a : α), ∫⁻ (x : β), f x ∂μ a ∂m
-- Mathlib.Topology.Algebra.WithZeroTopology
WithZeroTopology.hasBasis_nhds_units : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ), (nhds ↑γ).HasBasis (fun x => True) fun x => {↑γ}