mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mul_mem_cancel_right : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x y : G}, x ∈ H → (y * x ∈ H ↔ y ∈ H)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.singleton_vadd_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] (a : α) (b : β), {a} +ᵥ {b} = {a +ᵥ b}
-- Mathlib.Logic.Equiv.Basic
/-- A family of equivalences `∀ a, β₁ a ≃ β₂ a` generates an equivalence between `∀ a, β₁ a` and
`∀ a, β₂ a`.  -/
Equiv.piCongrRight : {α : Sort u_1} →
  {β₁ : α → Sort u_9} → {β₂ : α → Sort u_10} → ((a : α) → β₁ a ≃ β₂ a) → ((a : α) → β₁ a) ≃ ((a : α) → β₂ a)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.eq_zero' : ∀ {G : Type u_1} [inst : AddMonoid G] [IsAddTorsionFree G] {a : G}, IsOfFinAddOrder a → a = 0
-- Mathlib.Data.Finsupp.Defs
Finsupp.embDomain_apply_self : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_4} [inst : Zero M] (f : α ↪ β) (v : α →₀ M) (a : α),
  (Finsupp.embDomain f v) (f a) = v a
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
/-- This holds true for all `x : ℂ` because of the junk values `0 / 0 = 0` and `arg 0 = 0`.  -/
Complex.arg_div_self : ∀ (x : ℂ), (x / x).arg = 0
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.map_iInf_le : ∀ {α : Type u_1} {ι : Sort u_2} {β : Type u_3} (f : α → β) (m : ι → MeasureTheory.OuterMeasure α),
  (MeasureTheory.OuterMeasure.map f) (⨅ i, m i) ≤ ⨅ i, (MeasureTheory.OuterMeasure.map f) (m i)
-- Lean.Server.Completion.CompletionUtils
_private.Lean.Server.Completion.CompletionUtils.0.Lean.String.charactersIn.go : String → String → String.Pos.Raw → String.Pos.Raw → Bool
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_inter_ne_top_of_left_ne_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α}, μ s ≠ ⊤ → μ (s ∩ t) ≠ ⊤
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inr_v_snd_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + 1 = q)
  {Z : C} (h : L.X p ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.snd φ).v q p ⋯) h) =
    h
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkNatTrans_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  {F F' : CategoryTheory.Functor (CategoryTheory.Join C D) E}
  (αₗ : (CategoryTheory.Join.inclLeft C D).comp F ⟶ (CategoryTheory.Join.inclLeft C D).comp F')
  (αᵣ : (CategoryTheory.Join.inclRight C D).comp F ⟶ (CategoryTheory.Join.inclRight C D).comp F')
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
          ((CategoryTheory.Prod.snd C D).whiskerLeft αᵣ) =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).whiskerLeft αₗ)
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F'))
      _auto_108✝)
  (d : D), (CategoryTheory.Join.mkNatTrans αₗ αᵣ h).app (CategoryTheory.Join.right d) = αᵣ.app d
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.checkToFieldDefEq? : Option Lean.Expr →
  Option Lean.Expr → Option Lean.Expr → Lean.Name → Lean.Level → Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.gluedCover_t' : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).t' x y z = AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] {f : (a : α) → β a → γ a}, (Std.DTreeMap.Raw.map f t).size = t.size
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for monotonicity of addition on the right,
namely `a₁ ≤ a₂ → a₁ + b ≤ a₂ + b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedAddMonoid`.  -/
AddRightMono : (M : Type u_1) → [Add M] → [LE M] → Prop
-- Mathlib.Topology.Connected.LocallyConnected
IsOpen.locallyConnectedSpace : ∀ {α : Type u} [inst : TopologicalSpace α] [LocallyConnectedSpace α] {U : Set α}, IsOpen U → LocallyConnectedSpace ↑U
-- Mathlib.Order.WellFoundedSet
Finset.wellFoundedOn : ∀ {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] (s : Finset α), (↑s).WellFoundedOn r
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyItem.tags? : Lean.Lsp.CallHierarchyItem → Option (Array Lean.Lsp.SymbolTag)
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.coeff_ofScalars : ∀ {𝕜 : Type u_3} [inst : NontriviallyNormedField 𝕜] {p : ℕ → 𝕜} {n : ℕ},
  (FormalMultilinearSeries.ofScalars 𝕜 p).coeff n = p n
-- Mathlib.MeasureTheory.Measure.Decomposition.Hahn
/-- A set where `μ ≤ ν` (and the reverse inequality on the complement),
defined via measurable set and measure restriction comparisons.  -/
MeasureTheory.IsHahnDecomposition : {α : Type u_1} → {mα : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → Set α → Prop
-- Mathlib.Analysis.Convex.BetweenList
List.wbtw_cons : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {p : P} {l : List P},
  List.Wbtw R (p :: l) ↔ List.Pairwise (Wbtw R p) l ∧ List.Wbtw R l
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.rankOne_eq_zero : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {F : Type u_8} [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {x : E} {y : F},
  ((InnerProductSpace.rankOne 𝕜) x) y = 0 ↔ x = 0 ∨ y = 0
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum, over the image of an embedding, equals a weighted
sum with the same points and weights over the original
`Finset`.  -/
Finset.weightedVSubOfPoint_map : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} {ι₂ : Type u_5} (s₂ : Finset ι₂) (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) (b : P),
  ((Finset.map e s₂).weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint (p ∘ ⇑e) b) (w ∘ ⇑e)
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.apply_mem_target : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] {f : Equidecomp X G} {x : X},
  x ∈ f.source → ↑f.toPartialEquiv x ∈ f.target
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (r : R) (s : σ →₀ ℕ),
  (MvPolynomial.monomial s) r ∈ MvPolynomial.homogeneousSubmodule σ R 1 ^ Finsupp.degree s
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.mk : {α : Type u_6} →
  [inst : MeasurableSpace α] →
    (toOuterMeasure : MeasureTheory.OuterMeasure α) →
      (∀ ⦃f : ℕ → Set α⦄,
          (∀ (i : ℕ), MeasurableSet (f i)) →
            Pairwise (Function.onFun Disjoint f) → toOuterMeasure (⋃ i, f i) = ∑' (i : ℕ), toOuterMeasure (f i)) →
        toOuterMeasure.trim ≤ toOuterMeasure → MeasureTheory.Measure α
-- Init.Data.List.Nat.Sublist
List.append_sublist_of_sublist_right : ∀ {α : Type u_1} {xs ys zs : List α}, zs.Sublist ys → ((xs ++ ys).Sublist zs ↔ xs = [] ∧ ys = zs)
-- Mathlib.Analysis.Convex.Between
Convex.mem_of_wbtw : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [IsOrderedRing R] {p₀ p₁ p₂ : V} {s : Set V},
  Convex R s → Wbtw R p₀ p₁ p₂ → p₀ ∈ s → p₂ ∈ s → p₁ ∈ s
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential in a Banach algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has strict Fréchet derivative
`1 : 𝔸 →L[𝕂] 𝔸` at zero.  -/
hasStrictFDerivAt_exp_zero : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : RCLike 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸], HasStrictFDerivAt NormedSpace.exp 1 0
-- Std.Data.DTreeMap.Internal.WF.Lemmas
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.SameKeys : {α : Type u} →
  {β : α → Type v} → {β' : α → Type u_1} → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β' → Prop
-- Mathlib.LinearAlgebra.LinearPMap
/-- `f.coprod g` is the partially defined linear map defined on `f.domain × g.domain`,
and sending `p` to `f p.1 + g p.2`.  -/
LinearPMap.coprod : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} →
                  [inst_4 : AddCommGroup F] →
                    {G : Type u_6} →
                      [inst_5 : AddCommGroup G] →
                        [inst_6 : Module R F] → [inst_7 : Module S G] → (E →ₛₗ.[σ] G) → (F →ₛₗ.[σ] G) → E × F →ₛₗ.[σ] G
-- Mathlib.Data.Set.Finite.Basic
/-- A `Fintype` instance for inserting an element into a `Set` using the
corresponding `insert` function on `Finset`. This requires `DecidableEq α`.
There is also `Set.fintypeInsert'` when `a ∈ s` is decidable.  -/
Set.fintypeInsert : {α : Type u} → (a : α) → (s : Set α) → [DecidableEq α] → [Fintype ↑s] → Fintype ↑(insert a s)
-- Mathlib.CategoryTheory.Presentable.Limits
CategoryTheory.IsCardinalPresentable.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X X_1 : C),
  X = X_1 →
    ∀ (κ κ_1 : Cardinal.{w}) (e_κ : κ = κ_1) [inst_1 : Fact κ.IsRegular],
      CategoryTheory.IsCardinalPresentable X κ = CategoryTheory.IsCardinalPresentable X_1 κ_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, k ∈ t₂ → (t₁ ∩ t₂).getKey! k = t₁.getKey! k
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
Filter.EventuallyEq.lineDerivWithin_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f f₁ : E → F}
  {s : Set E} {x v : E}, f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sSameSide_self_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x : P}, s.SSameSide x x ↔ (↑s).Nonempty ∧ x ∉ s
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.mapBinaryBicone_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C}
  (b : CategoryTheory.Limits.BinaryBicone X Y), (F.mapBinaryBicone b).pt = F.obj b.pt
-- Mathlib.LinearAlgebra.Orientation
/-- The value of `Orientation.map` when the index type has the cardinality of a basis, in terms
of `f.det`.  -/
Module.Basis.map_orientation_eq_det_inv_smul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_4} [Finite ι] (e : Module.Basis ι R M)
  (x : Orientation R M ι) (f : M ≃ₗ[R] M), (Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Irreducible.coe_ne_zero : ∀ {M₀ : Type u_1} {S : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : SetLike S M₀] [inst_2 : SubmonoidClass S M₀]
  {s : S} {x : ↥s}, Irreducible x → ↑x ≠ 0
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The inverse of a ContinuousAddEquiv.  -/
ContinuousAddEquiv.symm : {M : Type u_1} →
  {N : Type u_2} →
    [inst : TopologicalSpace M] →
      [inst_1 : TopologicalSpace N] → [inst_2 : Add M] → [inst_3 : Add N] → M ≃ₜ+ N → N ≃ₜ+ M
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- A family of MulHom's `f a : γ →ₙ* β a` defines a MulHom `MulHom.pi f : γ →ₙ* Π a, β a`
given by `MulHom.pi f x b = f b x`.  -/
MulHom.pi : {I : Type u} →
  {f : I → Type v} →
    [inst : (i : I) → Mul (f i)] → {γ : Type w} → [inst_1 : Mul γ] → ((i : I) → γ →ₙ* f i) → γ →ₙ* (i : I) → f i
-- Lean.Data.Lsp.Diagnostics
/-- Represents a related message and source code location for a diagnostic.
This should be used to point to code locations that cause or are related to
a diagnostics, e.g when duplicating a symbol in a scope.  -/
Lean.Lsp.DiagnosticRelatedInformation : Type
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.HasReverse.mk : {V : Type u_2} → [inst : Quiver V] → ({a b : V} → (a ⟶ b) → (b ⟶ a)) → Quiver.HasReverse V
-- Mathlib.Probability.ProbabilityMassFunction.Monad
/-- The measure of a set under `p.bind f` is the sum over `a : α`
of the probability of `a` under `p` times the measure of the set under `f a`.  -/
PMF.toMeasure_bind_apply : ∀ {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β) (s : Set β) [inst : MeasurableSpace β],
  MeasurableSet s → (p.bind f).toMeasure s = ∑' (a : α), p a * (f a).toMeasure s
-- Mathlib.RingTheory.Perfection
ModP.mul_ne_zero_of_pow_p_ne_zero : ∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K],
  v.Integers O → ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x y : ModP O p}, x ^ p ≠ 0 → y ^ p ≠ 0 → x * y ≠ 0
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.negRev_negRev : ∀ {α : Type u} {L₁ : List (α × Bool)}, FreeAddGroup.negRev (FreeAddGroup.negRev L₁) = L₁
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.instFiniteCarrierObjFiniteEtale : ∀ (R : Type u) [inst : CommRing R] (S : CommAlgCat.FiniteEtale R), Module.Finite R ↑S.obj
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- The map sending `x` to `[1, x; 0, 1]` (bundled as an `AddChar`).  -/
Matrix.GeneralLinearGroup.upperRightHom : {R : Type u_1} → [inst : Ring R] → AddChar R (GL (Fin 2) R)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.restrictAppIso_inv_map_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  {U V : X.Opens} (hUV : Opposite.op V ⟶ Opposite.op U)
  (x : ↑(M.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj V)))),
  (CategoryTheory.ConcreteCategory.hom ((M.restrict f).presheaf.map hUV))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M V).inv) x) =
    (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).inv)
      ((CategoryTheory.ConcreteCategory.hom (M.presheaf.map (CategoryTheory.homOfLE ⋯).op)) x)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.coe_rangeRestrict : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] [inst_8 : RingHomSurjective σ₁₂]
  (f : M₁ →SL[σ₁₂] M₂), ⇑f.rangeRestrict = Set.rangeFactorization ⇑f
-- Mathlib.Logic.Equiv.Basic
/-- A specialization of `sigmaSigmaSubtype` to the case where the second base
does not depend on the first, and the property being checked for is simple
equality. Useful e.g. when `γ` is `Hom` inside a category.  -/
Equiv.sigmaSigmaSubtypeEq : {α : Type u_9} →
  {β : Type u_10} → {γ : α → β → Type u_11} → (a : α) → (b : β) → { s // s.fst = a ∧ s.snd.fst = b } ≃ γ a b
-- Mathlib.Util.Superscript
/-- Map from "special" (e.g. superscript) characters to "normal" characters.  -/
Mathlib.Tactic.Superscript.Mapping.toNormal : Mathlib.Tactic.Superscript.Mapping → Std.HashMap Char Char
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- A functorial factorization in the category `C` extends to the functor category `J ⥤ C`.  -/
CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      W₁.FunctorialFactorizationData W₂ →
        (J : Type u_3) →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} J] →
            (W₁.functorCategory J).FunctorialFactorizationData (W₂.functorCategory J)
-- Mathlib.Algebra.Module.ZLattice.Basic
Module.Basis.ofZLatticeBasis.congr_simp : ∀ (K : Type u_1) [inst : NormedField K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  [inst_3 : HasSolidNorm K] [inst_4 : FloorRing K] {E : Type u_2} [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace K E] [inst_7 : FiniteDimensional K E] [inst_8 : ProperSpace E] (L : Submodule ℤ E)
  [inst_9 : DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L] (b b_1 : Module.Basis ι ℤ ↥L),
  b = b_1 → Module.Basis.ofZLatticeBasis K L b = Module.Basis.ofZLatticeBasis K L b_1
-- Mathlib.Algebra.Exact.Basic
MonoidHom.mulExact_of_comp_of_mem_range : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Group M] [inst_1 : Group N] [inst_2 : Group P] {f : M →* N}
  {g : N →* P}, g.comp f = 1 → (∀ (x : N), g x = 1 → x ∈ f.range) → Function.MulExact ⇑f ⇑g
-- Std.Data.ExtTreeSet.Basic
/-- Transforms a list into a tree set.  -/
Std.ExtTreeSet.ofList : {α : Type u} → List α → (cmp : autoParam (α → α → Ordering) Std.ExtTreeSet.ofList._auto_1) → Std.ExtTreeSet α cmp
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.coe_algebraMap_valuationSubring_eq : ∀ {K : outParam (Type u_5)} {L : outParam (Type u_6)} {Γ₀ : outParam (Type u_7)} {Γ₁ : outParam (Type u_8)}
  [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_4 : LinearOrderedCommGroupWithZero Γ₁] (vK : Valuation K Γ₀) (vL : Valuation L Γ₁) [inst_5 : vK.HasExtension vL]
  (x : ↥vK.valuationSubring), ↑((algebraMap ↥vK.valuationSubring ↥vL.valuationSubring) x) = (algebraMap K L) ↑x
-- Mathlib.Logic.Function.Iterate
Function.Commute.iterate_self : ∀ {α : Type u} (f : α → α) (n : ℕ), Function.Commute f^[n] f
-- Mathlib.Algebra.FreeMonoid.Basic
/-- A variant of `List.prod` that has `[x].prod = x` true definitionally.
The purpose is to make `FreeMonoid.lift_eval_of` true by `rfl`.  -/
FreeMonoid.prodAux : {M : Type u_6} → [Monoid M] → List M → M
-- Mathlib.CategoryTheory.Sites.Sieves
/-- a map in the source category which has to be in the presieve  -/
CategoryTheory.Presieve.FunctorPushforwardStructure.premap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {X : C} →
            {S : CategoryTheory.Presieve X} →
              {Y : D} →
                {f : Y ⟶ F.obj X} → (self : CategoryTheory.Presieve.FunctorPushforwardStructure F S f) → self.preobj ⟶ X
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalSubsemiring.unitization_range : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : SetLike S R] [hSR : NonUnitalSubsemiringClass S R]
  (s : S), (NonUnitalSubsemiring.unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure ↑s)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Right.neg_le_self : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : Preorder α] [AddRightMono α] {a : α}, 0 ≤ a → -a ≤ a
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.toFunLifted.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (S : Type v) [inst_5 : CommSemiring S] [inst_6 : Algebra R S]
  (f : M →ₚₗ[R] N) (s : Finset S) (p : TensorProduct R (MvPolynomial (Fin s.card) R) M),
  PolynomialLaw.toFunLifted S f ⟨s, p⟩ =
    (LinearMap.rTensor N (PolynomialLaw.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_lt_mk : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk a < ArchimedeanClass.mk b ↔ ∀ (n : ℕ), n • |b| < |a|
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.smulCommClass_symm_self : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} [inst : Semiring S] [inst_1 : DistribSMul R S] [inst_2 : Add M]
  [SMulCommClass S R S], SMulCommClass (AddMonoidAlgebra S M) R (AddMonoidAlgebra S M)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
CategoryTheory.Sheaf.hasFilteredColimitsOfSize : ∀ {C : Type u} {A : Type u₁} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J A]
  [CategoryTheory.Limits.HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} A],
  CategoryTheory.Limits.HasFilteredColimitsOfSize.{v₂, u₂, max u v₁, max (max (max u₁ u) v₁) v}
    (CategoryTheory.Sheaf J A)
-- Mathlib.Topology.Instances.Matrix
IsOpen.matrix : ∀ {m : Type u_4} {n : Type u_5} {R : Type u_8} [Finite m] [Finite n] [inst : TopologicalSpace R] {S : Set R},
  IsOpen S → IsOpen S.matrix
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.comp_measurable : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {α' : Type u_8} [inst_2 : MeasurableSpace α'] {f : α → α'} {g : α' → ε},
  MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ) → Measurable f → MeasureTheory.Integrable (g ∘ f) μ
-- Lean.Parser.Level
Lean.Parser.Level.max : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kronecker_assoc' : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} {q : Type u_13} {r : Type u_14}
  [inst : Semigroup α] (A : Matrix l m α) (B : Matrix n p α) (C : Matrix q r α),
  (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B) C).submatrix
      ⇑(Equiv.prodAssoc l n q).symm ⇑(Equiv.prodAssoc m p r).symm =
    Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) B C)
-- Batteries.Tactic.PrintOpaques
Batteries.Tactic.CollectOpaques.State.mk : Lean.NameSet → Array Lean.Name → Batteries.Tactic.CollectOpaques.State
-- Mathlib.Topology.IsLocalHomeomorph
/-- A function `f : X → Y` satisfies `IsLocalHomeomorphOn f s` if each `x ∈ s` is contained in
the source of some `e : OpenPartialHomeomorph X Y` with `f = e`.  -/
IsLocalHomeomorphOn : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Set X → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- Given a rank `j` cell `c` for a rank function `f` for a proper
pairing of a subcomplex of a simplicial set, this is
the nondegenerate simplex in `f.sigmaStdSimplex j`
not in the image of `f.m j : f.sigmaHorn j ⟶ f.sigmaStdSimplex j`
which corresponds to the `c.index`th-face of `c.type₁`.  -/
SSet.Subcomplex.Pairing.RankFunction.Cell.type₂ : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          (f : P.RankFunction ι) → [inst_1 : P.IsProper] → {j : ι} → f.Cell j → (SSet.Subcomplex.range (f.m j)).N