mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.sum_measure_le_measure_univ : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset ι} {t : ι → Set α},
  (∀ i ∈ s, MeasureTheory.NullMeasurableSet (t i) μ) →
    (↑s).Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) t) → ∑ i ∈ s, μ (t i) ≤ μ Set.univ
-- Mathlib.Order.Interval.Finset.Defs
Finset.card_Icc_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (x y : α × β),
  (Finset.Icc x y).card = (Finset.Icc x.1 y.1).card * (Finset.Icc x.2 y.2).card
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖᵒᵖ)
  (n m : ℤ) (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app._auto_1),
  (CategoryTheory.Functor.commShiftIso (CategoryTheory.unopUnop C) n).hom.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app X).unop.unop
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).inv.app (Opposite.unop X)).unop
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
/-- The cohomology class of a cocycle.  -/
CochainComplex.HomComplex.CohomologyClass.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} → CochainComplex.HomComplex.Cocycle K L n → CochainComplex.HomComplex.CohomologyClass K L n
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
DirectSum.toAddMonoidAlgebra_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f g : DirectSum ι fun x => M), (f + g).toAddMonoidAlgebra = f.toAddMonoidAlgebra + g.toAddMonoidAlgebra
-- Init.Data.UInt.Lemmas
USize.toUSize_toUInt64 : ∀ (n : USize), n.toUInt64.toUSize = n
-- Mathlib.Data.Set.Restrict
Set.image_domRestrict : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α), s.domRestrict f '' Subtype.val ⁻¹' t = f '' (t ∩ s)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_eq_some_minKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {fallback : α},
  l.isEmpty = false → Std.Internal.List.minKey? l = some (Std.Internal.List.minKeyD l fallback)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] {U : X.Opens} {x : ↥X},
  f x ∈ (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U ↔ x ∈ U
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.map_update_add : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) [inst_5 : DecidableEq ι] (i : ι)
  (u v : s i →ₗ[R] t i),
  PiTensorProduct.map (Function.update f i (u + v)) =
    PiTensorProduct.map (Function.update f i u) + PiTensorProduct.map (Function.update f i v)
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedMonoid.toMonoid : {E : Type u_8} → {inst : TopologicalSpace E} → [self : ESeminormedMonoid E] → Monoid E
-- Mathlib.NumberTheory.Real.Irrational
Irrational.natCast_sub : ∀ {x : ℝ}, Irrational x → ∀ (m : ℕ), Irrational (↑m - x)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A too large block is equal to `univ`  -/
MulAction.IsBlock.eq_univ_of_card_lt : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] [MulAction.IsPretransitive G X] {B : Set X}
  [hX : Finite X], MulAction.IsBlock G B → Nat.card X < B.ncard * 2 → B = Set.univ
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum_top : ∀ {V : Type u_1}, (SimpleGraph.completeGraph V).vertexCoverNum = ENat.card V - 1
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_neg_eq_zero : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b : α}, IsAddUnit b → (a + -b = 0 ↔ a = b)
-- Init.Data.Dyadic.Basic
/-- Shift a dyadic number right by `i` bits.  -/
Dyadic.shiftRight : Dyadic → ℤ → Dyadic
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
CategoryTheory.ShortComplex.ShortExact.extClass_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact)
  (f : S₁ ⟶ S₂),
  h₁.extClass.comp (CategoryTheory.Abelian.Ext.mk₀ f.τ₁) ⋯ = (CategoryTheory.Abelian.Ext.mk₀ f.τ₃).comp h₂.extClass ⋯
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₃₂.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.d₃₂ A =
    ModuleCat.ofHom
      ((Finsupp.lsum k) fun g =>
        Finsupp.lsingle (g.2.1, g.2.2) ∘ₗ A.ρ g.1⁻¹ - Finsupp.lsingle (g.1 * g.2.1, g.2.2) +
            Finsupp.lsingle (g.1, g.2.1 * g.2.2) -
          Finsupp.lsingle (g.1, g.2.1))
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
CategoryTheory.MorphismProperty.Over.mk.congr_simp : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) {X A : T} (f f_1 : A ⟶ X) (e_f : f = f_1) (hf : P f),
  CategoryTheory.MorphismProperty.Over.mk Q f hf = CategoryTheory.MorphismProperty.Over.mk Q f_1 ⋯
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.inf : ∀ {β : Type u_1} {t₁ t₂ : TopologicalSpace β} {B₁ B₂ : Set (Set β)},
  TopologicalSpace.IsTopologicalBasis B₁ →
    TopologicalSpace.IsTopologicalBasis B₂ →
      TopologicalSpace.IsTopologicalBasis (Set.image2 (fun x1 x2 => x1 ∩ x2) B₁ B₂)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
instCompleteLatticeWithBot.eq_1 : ∀ {α : Type u_1} [inst : CompleteLattice α],
  instCompleteLatticeWithBot =
    { toLattice := WithBot.lattice, toSupSet := WithBot.instSupSet, isLUB_sSup := ⋯, toInfSet := WithBot.instInfSet,
      isGLB_sInf := ⋯, toBoundedOrder := WithBot.instBoundedOrder }
-- Mathlib.Data.Matrix.Basic
/-- `Matrix.transpose` as an `AlgEquiv` to the opposite ring.

See also `AlgEquiv.mopMatrix` for a version that doesn't require `α` to have commutative
multiplication, by taking its opposite.  -/
Matrix.transposeAlgEquiv : (m : Type u_2) →
  (R : Type u_7) →
    (α : Type u_11) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring α] →
          [inst_2 : Fintype m] →
            [inst_3 : DecidableEq m] → [inst_4 : Algebra R α] → Matrix m m α ≃ₐ[R] (Matrix m m α)ᵐᵒᵖ
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hasRightKanExtension : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F}
  (h : E.IsPointwiseRightKanExtension), L.HasRightKanExtension F
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.ExtensionState.mk.injEq : ∀ (casesTypes : Lean.Meta.Grind.CasesTypes) (extThms : Lean.Meta.Grind.ExtTheorems) (funCC : Lean.NameSet)
  (ematch : Lean.Meta.Grind.Theorems Lean.Meta.Grind.EMatchTheorem)
  (inj : Lean.Meta.Grind.Theorems Lean.Meta.Grind.InjectiveTheorem) (casesTypes_1 : Lean.Meta.Grind.CasesTypes)
  (extThms_1 : Lean.Meta.Grind.ExtTheorems) (funCC_1 : Lean.NameSet)
  (ematch_1 : Lean.Meta.Grind.Theorems Lean.Meta.Grind.EMatchTheorem)
  (inj_1 : Lean.Meta.Grind.Theorems Lean.Meta.Grind.InjectiveTheorem),
  ({ casesTypes := casesTypes, extThms := extThms, funCC := funCC, ematch := ematch, inj := inj } =
      { casesTypes := casesTypes_1, extThms := extThms_1, funCC := funCC_1, ematch := ematch_1, inj := inj_1 }) =
    (casesTypes = casesTypes_1 ∧ extThms = extThms_1 ∧ funCC = funCC_1 ∧ ematch = ematch_1 ∧ inj = inj_1)
-- Mathlib.Data.Finset.Pairwise
List.pairwise_of_coe_toFinset_pairwise : ∀ {α : Type u_1} [inst : DecidableEq α] {r : α → α → Prop} {l : List α},
  (↑l.toFinset).Pairwise r → l.Nodup → List.Pairwise r l
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- A function is `C^(n + 1)` on an open domain if and only if it is
differentiable there, and its derivative (expressed with `fderiv`) is `C^n`.  -/
contDiffOn_succ_iff_fderiv_of_isOpen : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞},
  IsOpen s →
    (ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ⊤ → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (fderiv 𝕜 f) s)
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
_private.Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite.0.SimpleGraph.IsPathGraph3Compl.pathGraph3ComplEmbedding.match_1.eq_3 : ∀ (motive : Fin 3 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2),
  (match 2 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()) =
    h_3 ()
-- Mathlib.Algebra.Star.RingQuot
/-- Transfer a `StarRing` instance through a quotient, if the quotient is invariant to `star`  -/
RingQuot.starRing : {R : Type u} →
  [inst : Semiring R] →
    [inst_1 : StarRing R] → (r : R → R → Prop) → (∀ (a b : R), r a b → r (star a) (star b)) → StarRing (RingQuot r)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Model
Lean.Meta.Grind.Arith.Linear.getAssignment? : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr → Option ℚ
-- Mathlib.Data.List.Basic
_private.Mathlib.Data.List.Basic.0.List.getLastI.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (head b : α) (h_1 : Unit → motive []) (h_2 : (a : α) → motive [a])
  (h_3 : (head b : α) → motive [head, b]) (h_4 : (head head_1 : α) → (l : List α) → motive (head :: head_1 :: l)),
  (match [head, b] with
    | [] => h_1 ()
    | [a] => h_2 a
    | [head, b] => h_3 head b
    | head :: head_1 :: l => h_4 head head_1 l) =
    h_3 head b
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.trans_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ φ₃ : S₁ ⟶ S₂} (h₁₂ : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h₂₃ : CategoryTheory.ShortComplex.Homotopy φ₂ φ₃), (h₁₂.trans h₂₃).h₀ = h₁₂.h₀ + h₂₃.h₀
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.one_le_coe : ∀ {α : Type u_1} [inst : LE α] {a : α} [inst_1 : One α], 1 ≤ ↑a ↔ 1 ≤ a
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.toHomeomorph_uniformEquivProd : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [inst : UniformSpace α] [inst_1 : UniformSpace β],
  (WithLp.uniformEquivProd p α β).toHomeomorph = WithLp.homeomorphProd p α β
-- Init.Tactics
/-- If `thm` is a theorem `a = b`, then as a rewrite rule,
* `thm` means to replace `a` with `b`, and
* `← thm` means to replace `b` with `a`.
 -/
Lean.Parser.Tactic.rwRule : Lean.ParserDescr
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.quotient_inverts_homotopyEquivalences : ∀ {ι : Type u_2} (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι), (HomologicalComplex.homotopyEquivalences V c).IsInvertedBy (HomotopyCategory.quotient V c)
-- Lean.Server.AsyncList
Lean.AsyncList.brecOn_2.eq : ∀ {ε : Type u} {α : Type v} {motive_1 : Lean.AsyncList ε α → Sort u_1}
  {motive_2 : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α)) → Sort u_1}
  {motive_3 : Task (Except ε (Lean.AsyncList ε α)) → Sort u_1} {motive_4 : Except ε (Lean.AsyncList ε α) → Sort u_1}
  (t : Task (Except ε (Lean.AsyncList ε α))) (F_1 : (t : Lean.AsyncList ε α) → t.below → motive_1 t)
  (F_2 : (t : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_1 t → motive_2 t)
  (F_3 : (t : Task (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_2 t → motive_3 t)
  (F_4 : (t : Except ε (Lean.AsyncList ε α)) → Lean.AsyncList.below_3 t → motive_4 t),
  Lean.AsyncList.brecOn_2 t F_1 F_2 F_3 F_4 = F_3 t (Lean.AsyncList.brecOn_2.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Order.Defs.LinearOrder
LinearOrder.mk : {α : Type u_2} →
  [toPartialOrder : PartialOrder α] →
    [toMin : Min α] →
      [toMax : Max α] →
        [toOrd : Ord α] →
          (∀ (a b : α), a ≤ b ∨ b ≤ a) →
            (toDecidableLE : DecidableLE α) →
              (toDecidableEq : DecidableEq α) →
                (toDecidableLT : DecidableLT α) →
                  autoParam (∀ (a b : α), a ⊓ b = if a ≤ b then a else b) LinearOrder.min_def._autoParam →
                    autoParam (∀ (a b : α), a ⊔ b = if a ≤ b then b else a) LinearOrder.max_def._autoParam →
                      autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b)
                          LinearOrder.compare_eq_compareOfLessAndEq._autoParam →
                        LinearOrder α
-- Lean.Meta.Closure
Lean.Meta.Closure.MkValueTypeClosureResult.levelParams : Lean.Meta.Closure.MkValueTypeClosureResult → Array Lean.Name
-- Init.PropLemmas
Bool.ite_then_true_eq_false : ∀ {p : Prop} [inst : Decidable p] {x : Bool}, (if p then true else x) = false ↔ ¬p ∧ x = false
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.valMinAbs_neg_of_ne_half : ∀ {n : ℕ} {a : ZMod n}, 2 * a.val ≠ n → (-a).valMinAbs = -a.valMinAbs
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.zero_compLinearMap : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (g : M₂ →ₗ[R] M), AlternatingMap.compLinearMap 0 g = 0
-- Mathlib.Topology.MetricSpace.Ultra.Basic
/-- The `dist : X → X → ℝ` respects the ultrametric inequality
of `dist(x, z) ≤ max (dist(x,y)) (dist(y,z))`.  -/
IsUltrametricDist : (X : Type u_2) → [Dist X] → Prop
-- Mathlib.RingTheory.TensorProduct.Basic
/-- Universal property of the base change of algebra.

An algebra map from the base change is equivalent to an algebra map over the base ring.

In categorical terms, this is an adjunction between:
1. `A ↦ S ⊗[R] A`, a functor `R-Alg ⥤ S-Alg` (the base change).
2. `B ↦ B`, a functor `S-Alg ⥤ R-Alg` (the restriction).
 -/
AlgHom.liftEquiv : (R : Type u_4) →
  (S : Type u_5) →
    (A : Type u_6) →
      (B : Type u_7) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Semiring A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R A] →
                  [inst_5 : Algebra S B] →
                    [inst_6 : Algebra R S] →
                      [inst_7 : Algebra R B] → [IsScalarTower R S B] → (A →ₐ[R] B) ≃ (TensorProduct R S A →ₐ[S] B)
-- Init.Data.SInt.Lemmas
ISize.neg_neg : ∀ {a : ISize}, - -a = a
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.MorphismProperty.isIso_fst'_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.MorphismProperty C}
  {G : CategoryTheory.Functor Cᵒᵖ (Type v₁)},
  P ≤ CategoryTheory.MorphismProperty.monomorphisms C →
    ∀ {X : C} {f : CategoryTheory.yoneda.obj X ⟶ G} (hf : P.presheaf f), CategoryTheory.IsIso (⋯.fst' f)
-- Mathlib.Data.DFinsupp.Order
DFinsupp.le_def : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → LE (α i)] {f g : Π₀ (i : ι), α i},
  f ≤ g ↔ ∀ (i : ι), f i ≤ g i
-- Mathlib.Data.DFinsupp.Module
DFinsupp.smul_apply : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : (i : ι) → SMulZeroClass γ (β i)]
  (b : γ) (v : Π₀ (i : ι), β i) (i : ι), (b • v) i = b • v i
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.ofFractionRing_div : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p q : FractionRing (Polynomial K)),
  { toFractionRing := p / q } = { toFractionRing := p } / { toFractionRing := q }
-- Mathlib.RingTheory.WittVector.Complete
WittVector.ker_constantCoeff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [CharP k p] [PerfectRing k p],
  RingHom.ker WittVector.constantCoeff = Ideal.span {↑p}
-- Init.Data.List.Lemmas
List.foldl_ite_left : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} [inst : DecidablePred P] {l : List α} {f : β → α → β} {init : β},
  List.foldl (fun sofar a => if P a then f sofar a else sofar) init l =
    List.foldl f init (List.filter (fun b => decide (P b)) l)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- **Alias** of `ContinuousLinearMapWOT.ofCLM_apply`. -/
ContinuousLinearMap.toWOT_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] {A : E →SL[σ] F} {x : E},
  (ContinuousLinearMapWOT.ofCLM A) x = A x
-- Mathlib.Algebra.Lie.Classical
/-- When `i ≠ j`, the single-element matrices are elements of `sl n R`.

Along with some elements produced by `singleSubSingle`, these form a natural basis of `sl n R`.  -/
LieAlgebra.SpecialLinear.single : {n : Type u_1} →
  {R : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → (i j : n) → i ≠ j → R →ₗ[R] ↥(LieAlgebra.SpecialLinear.sl n R)
-- Init.Core
_private.Init.Core.0.Quotient.rel_of_eq : ∀ {α : Sort u} {s : Setoid α} {q₁ q₂ : Quotient s}, q₁ = q₂ → Quotient.rel✝ q₁ q₂
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.GuessLexRel.lt : Lean.Elab.WF.GuessLex.GuessLexRel
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
/-- The error of the trapezoidal integration from `a` to `a` is zero.  -/
trapezoidal_error_eq : ∀ (f : ℝ → ℝ) (N : ℕ) (a : ℝ), trapezoidal_error f N a a = 0
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.isAcyclic_iff_free_cycleGraph : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic ↔ ∀ n ≥ 3, (SimpleGraph.cycleGraph n).Free G
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- Lift two variable maps to completions.  -/
AbstractCompletion.map₂ : {α : Type uα} →
  [inst : UniformSpace α] →
    (pkg : AbstractCompletion.{vα, uα} α) →
      {β : Type uβ} →
        [inst_1 : UniformSpace β] →
          (pkg' : AbstractCompletion.{u_1, uβ} β) →
            {γ : Type uγ} →
              [inst_2 : UniformSpace γ] →
                (pkg'' : AbstractCompletion.{vγ, uγ} γ) → (α → β → γ) → pkg.space → pkg'.space → pkg''.space
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.IsTopCompl.continuous_projection : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (self : Submodule.IsTopCompl p q), Continuous ⇑(p.projection q ⋯)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.inner_rid_rid : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : TensorProduct 𝕜 E 𝕜), inner 𝕜 ((TensorProduct.rid 𝕜 E) x) ((TensorProduct.rid 𝕜 E) y) = inner 𝕜 x y
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousWithinAt_iff_limsup_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [inst_1 : CompleteLinearOrder γ]
  {f : α → γ}, UpperSemicontinuousWithinAt f s x ↔ Filter.limsup f (nhdsWithin x s) ≤ f x
-- Mathlib.Algebra.Order.Group.Abs
mabs_div_le_iff : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b c : G},
  |a / b|ₘ ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany?_one : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a : α},
  Std.PRange.succMany? 1 a = Std.PRange.succ? a
-- Mathlib.Order.Monotone.Defs
StrictAntiOn.comp_strictMonoOn : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α} {t : Set β}, StrictAntiOn g t → StrictMonoOn f s → Set.MapsTo f s t → StrictAntiOn (g ∘ f) s
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.apply_inv_self : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (e : α ≃ᵢ α) (x : α), e (e⁻¹ x) = x
-- Mathlib.Data.Set.Image
/-- A common special case of `image_congr`  -/
Set.image_congr' : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {s : Set α}, (∀ (x : α), f x = g x) → f '' s = g '' s
-- Std.Data.ExtTreeMap.Basic
/-- Support for the `for` loop construct in `do` blocks. Iteration happens in ascending order.  -/
Std.ExtTreeMap.forIn : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} →
        {m : Type w → Type w₂} →
          [inst : Monad m] →
            [LawfulMonad m] → [Std.TransCmp cmp] → (α → β → δ → m (ForInStep δ)) → δ → Std.ExtTreeMap α β cmp → m δ
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_eq'' : ∀ {Ω : Type u_1} {ι : Type u_3} [inst : Nonempty ι] {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E}
  [inst_1 : LinearOrder ι] [inst_2 : LocallyFiniteOrderBot ι] [inst_3 : AddCommMonoid E] (n : ι),
  MeasureTheory.stoppedProcess u τ n = {a | ↑n ≤ τ a}.indicator (u n) + ∑ i < n, {ω | τ ω = ↑i}.indicator (u i)
-- Mathlib.Order.SupClosed
supClosed_preimage_toDual : ∀ {α : Type u_3} [inst : Lattice α] {s : Set αᵒᵈ}, SupClosed (⇑OrderDual.toDual ⁻¹' s) ↔ InfClosed s
-- Mathlib.Algebra.Order.BigOperators.Group.List
/-- See also `List.single_le_prod`.  -/
List.le_prod_of_mem : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [CanonicallyOrderedMul M] {xs : List M} {x : M},
  x ∈ xs → x ≤ xs.prod
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIso_hom_app : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (X : D),
  (CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIso C D).hom.app X =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso X).hom
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.mk : {α : Type u_5} →
  {β : Type u_6} →
    (toFun : α → β) →
      (invFun : β → α) →
        (source : Set α) →
          (target : Set β) →
            (∀ ⦃x : α⦄, x ∈ source → toFun x ∈ target) →
              (∀ ⦃x : β⦄, x ∈ target → invFun x ∈ source) →
                (∀ ⦃x : α⦄, x ∈ source → invFun (toFun x) = x) →
                  (∀ ⦃x : β⦄, x ∈ target → toFun (invFun x) = x) → PartialEquiv α β
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.ofAddUnits_inf_addUnits : ∀ {M : Type u_1} [inst : AddMonoid M] (S T : AddSubgroup (AddUnits M)), (S.ofAddUnits ⊓ T.ofAddUnits).addUnits = S ⊓ T
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instIsLocalizationPrimeComplAsIdealSubtypeMemValuationSubringValuationSubringAtPrime : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsLocalization v.asIdeal.primeCompl ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K v)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_f : ∀ {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.snakeInput f g).L₁.f = CategoryTheory.Limits.biprod.inl