mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.neg_toProd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (a : DoubleCentralizer 𝕜 A),
  (-a).toProd = -a.toProd
-- Init.Data.List.Lemmas
List.isEqv_eq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ : List α}, ((l₁.isEqv l₂ fun x1 x2 => x1 == x2) = true) = (l₁ = l₂)
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.basis_val : ∀ {R : Type u_1} [inst : Semiring R] {n : ℕ} (i : Fin n), ↑((Polynomial.degreeLT.basis R n) i) = Polynomial.X ^ ↑i
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A preadditive category with finite coproducts has finite biproducts.  -/
CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasFiniteCoproducts C], CategoryTheory.Limits.HasFiniteBiproducts C
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_congr : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k k' fallback : α}, (k == k') = true → m.getD k fallback = m.getD k' fallback
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singleton_sub_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] (a b : α), {a} - {b} = {a - b}
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.commTensorRight_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X X_1 : C),
  (CategoryTheory.Functor.Monoidal.commTensorRight F X).hom.app X_1 = CategoryTheory.Functor.LaxMonoidal.μ F X_1 X
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- An affine open cover of `X` consists of a family of open immersions into `X` from
spectra of rings.
 -/
AlgebraicGeometry.Scheme.AffineOpenCover : AlgebraicGeometry.Scheme → Type (max (v + 1) (u + 1))
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.j_mul_i : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (self : QuaternionAlgebra.Basis A c₁ c₂ c₃), self.j * self.i = c₂ • self.j - self.k
-- Mathlib.ModelTheory.Syntax
/-- A theory that indicates a structure is nonempty.  -/
FirstOrder.Language.nonemptyTheory : (L : FirstOrder.Language) → L.Theory
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.eraseListₘ.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (hd : α) (tl : List α) (h_1 : Unit → motive [])
  (h_2 : (hd : α) → (tl : List α) → motive (hd :: tl)),
  (match hd :: tl with
    | [] => h_1 ()
    | hd :: tl => h_2 hd tl) =
    h_2 hd tl
-- Mathlib.Combinatorics.Colex
Finset.Colex.toColex_empty : ∀ {α : Type u_1} [inst : PartialOrder α], toColex ∅ = ⊥
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.subtypeCongr.left_apply : ∀ {ε : Type u_9} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a })
  {a : ε} (h : p a), (ep.subtypeCongr en) a = ↑(ep ⟨a, h⟩)
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.reindex_comp : ∀ {n₁ n₂ n₃ : Type u} (i : n₁ ⟶ n₂) (j : n₂ ⟶ n₃) (S : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.AffineSpace.reindex
      (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp i j))) S =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.AffineSpace.reindex (⇑(CategoryTheory.ConcreteCategory.hom j)) S)
      (AlgebraicGeometry.AffineSpace.reindex (⇑(CategoryTheory.ConcreteCategory.hom i)) S)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.mk.inj : ∀ {V : Type v} {inst : CategoryTheory.Category.{w, v} V} {inst_1 : CategoryTheory.MonoidalCategory V} {C : Type u₁}
  {inst_2 : CategoryTheory.EnrichedCategory V C} {D : Type u₂} {inst_3 : CategoryTheory.EnrichedCategory V D}
  {obj : C → D} {map : (X Y : C) → (X ⟶[V] Y) ⟶ obj X ⟶[V] obj Y}
  {map_id :
    autoParam
      (∀ (X : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (map X X) = CategoryTheory.eId V (obj X))
      CategoryTheory.EnrichedFunctor.map_id._autoParam}
  {map_comp :
    autoParam
      (∀ (X Y Z : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (map X Z) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (map X Y) (map Y Z))
            (CategoryTheory.eComp V (obj X) (obj Y) (obj Z)))
      CategoryTheory.EnrichedFunctor.map_comp._autoParam}
  {obj_1 : C → D} {map_1 : (X Y : C) → (X ⟶[V] Y) ⟶ obj_1 X ⟶[V] obj_1 Y}
  {map_id_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (map_1 X X) = CategoryTheory.eId V (obj_1 X))
      CategoryTheory.EnrichedFunctor.map_id._autoParam}
  {map_comp_1 :
    autoParam
      (∀ (X Y Z : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (map_1 X Z) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (map_1 X Y) (map_1 Y Z))
            (CategoryTheory.eComp V (obj_1 X) (obj_1 Y) (obj_1 Z)))
      CategoryTheory.EnrichedFunctor.map_comp._autoParam},
  { obj := obj, map := map, map_id := map_id, map_comp := map_comp } =
      { obj := obj_1, map := map_1, map_id := map_id_1, map_comp := map_comp_1 } →
    obj = obj_1 ∧ map ≍ map_1
-- Mathlib.Data.Vector.Basic
_private.Mathlib.Data.Vector.Basic.0.List.Vector.elim.match_3.splitter : {α : Type u_1} →
  {n : ℕ} →
    (motive : List.Vector α n → Sort u_2) →
      (x : List.Vector α n) → ((l : List α) → (h : l.length = n) → motive ⟨l, h⟩) → motive x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.forIn_eq_forIn_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α × β → δ → m (ForInStep δ)} {init : δ}, forIn t init f = forIn t.toList init f
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsSymm.mk : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : R →+* R}
  {B : M →ₛₗ[I] M →ₗ[R] R}, (∀ (x y : M), I ((B x) y) = (B y) x) → B.IsSymm
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.biproduct_ι_comp_rightDistributor_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (f : J → C) (X : C) (j : J),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X)
      (CategoryTheory.rightDistributor f X).hom =
    CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j
-- Mathlib.Data.Int.Bitwise
Int.bodd_negOfNat : ∀ (n : ℕ), (Int.negOfNat n).bodd = n.bodd
-- Mathlib.Data.Set.Finite.Basic
Multiset.finite_toSet : ∀ {α : Type u} (s : Multiset α), {x | x ∈ s}.Finite
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of ring homs is said to be preserved by localization away
if `P` holds for `Rᵣ →+* Sᵣ` whenever `P` holds for `R →+* S`.  -/
RingHom.LocalizationAwayPreserves : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.Data.Complex.Basic
/-- The imaginary unit.  -/
Complex.I : ℂ
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.support_smul_subset : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] {V : Type u_8} [inst_1 : Zero V] [inst_2 : SMulZeroClass R V]
  (r : R) (x : HahnSeries Γ V), (r • x).support ⊆ x.support
-- Mathlib.RingTheory.Ideal.Maps
Ideal.apply_mem_of_equiv_iff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R} {f : R ≃+* S} {x : R},
  f x ∈ Ideal.map f I ↔ x ∈ I
-- Mathlib.Data.Set.Prod
Set.graphOn_univ_eq_range : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Set.graphOn f Set.univ = Set.range fun x => (x, f x)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.interSmallerFn.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Option ((a : α) × β a) → Sort u_3) →
      (x : Option ((a : α) × β a)) → ((kv' : (a : α) × β a) → motive (some kv')) → (Unit → motive none) → motive x
-- Init.Data.UInt.Bitwise
instAssociativeUInt8HXor : Std.Associative fun x1 x2 => x1 ^^^ x2
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.subcomplex_cast : ∀ {X : SSet} (s : X.S) {d : ℕ} (hd : s.dim = d), (s.cast hd).subcomplex = s.subcomplex
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.logSizeBallSeq.congr_simp : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] [inst_1 : DecidableEq T] (J J_1 : Finset T) (e_J : J = J_1)
  (hJ : J.Nonempty) (a a_1 : ENNReal),
  a = a_1 →
    ∀ (c c_1 : ENNReal),
      c = c_1 →
        ∀ (a_2 a_3 : ℕ),
          a_2 = a_3 → PairReduction.logSizeBallSeq J hJ a c a_2 = PairReduction.logSizeBallSeq J_1 ⋯ a_1 c_1 a_3
-- Mathlib.Algebra.Field.Basic
Lex.instDivisionSemiring : {K : Type u_1} → [DivisionSemiring K] → DivisionSemiring (Lex K)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorComm_zero_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] {X : C} (a : A),
  (CategoryTheory.shiftFunctorComm C a 0).hom.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C a).obj X))
      ((CategoryTheory.shiftFunctor C a).map ((CategoryTheory.shiftFunctorZero C A).inv.app X))
-- Mathlib.Algebra.Category.CommBialgCat
commBialgCatEquivComonCommAlgCat_functor_map_unop_hom : ∀ {R : Type u} [inst : CommRing R] {A B : CommBialgCat R} (f : A ⟶ B),
  ((commBialgCatEquivComonCommAlgCat R).functor.map f).unop.hom = (CommAlgCat.ofHom ↑(CommBialgCat.Hom.hom f)).op
-- Init.Data.SInt.Lemmas
Int16.toInt32_ofIntLE : ∀ {n : ℤ} (h₁ : Int16.minValue.toInt ≤ n) (h₂ : n ≤ Int16.maxValue.toInt),
  (Int16.ofIntLE n h₁ h₂).toInt32 = Int32.ofIntLE n ⋯ ⋯
-- Mathlib.Tactic.CategoryTheory.Elementwise
Mathlib.Tactic.Elementwise.hom_elementwise : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type u_3)} {x : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))}
  [inst_1 : CategoryTheory.ConcreteCategory C FC] {X Y : C} {f g : X ⟶ Y},
  f = g → ∀ (x_1 : CC X), (CategoryTheory.ConcreteCategory.hom f) x_1 = (CategoryTheory.ConcreteCategory.hom g) x_1
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.aestronglyMeasurable_condExpL1 : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] {f : α → F'},
  MeasureTheory.AEStronglyMeasurable (↑↑(MeasureTheory.condExpL1 hm μ f)) μ
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.variation_transpose_eq : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) [Nontrivial E],
  (∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖x‖₊ * ‖y‖₊) → (μ.transpose B).variation = μ.variation
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.mk.injEq : ∀ {α : Type u_1} (h : α) (s : Stream'.Seq (GenContFract.Pair α)) (h_1 : α) (s_1 : Stream'.Seq (GenContFract.Pair α)),
  ({ h := h, s := s } = { h := h_1, s := s_1 }) = (h = h_1 ∧ s = s_1)
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_mulHom_id : ∀ {α : Type u_2} [inst : NonUnitalNonAssocSemiring α], ↑(NonUnitalRingHom.id α) = MulHom.id α
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_eq_iff_right : ∀ {α : Type u} [inst : Monoid α] {a b : α} [inst_1 : Invertible a], ⅟a = b ↔ a * b = 1
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
/-- The conditional cdf is a measurable function of `a : α` for all `x : ℝ`.  -/
ProbabilityTheory.measurable_condCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (x : ℝ),
  Measurable fun a => ↑(ProbabilityTheory.condCDF ρ a) x
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubsemiring.copy.congr_simp : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (S S_1 : NonUnitalSubsemiring R) (e_S : S = S_1) (s s_1 : Set R)
  (e_s : s = s_1) (hs : s = ↑S), S.copy s hs = S_1.copy s_1 ⋯
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsFoelner.eventually_meas_ne_top : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X},
  IsFoelner G μ l F → ∀ᶠ (i : ι) in l, μ (F i) ≠ ⊤
-- Lean.Server.Utils
Lean.Server.DocumentMeta.mk.injEq : ∀ (uri : Lean.Lsp.DocumentUri) (mod : Lean.Name) (version : ℕ) (text : Lean.FileMap)
  (dependencyBuildMode : Lean.Lsp.DependencyBuildMode) (uri_1 : Lean.Lsp.DocumentUri) (mod_1 : Lean.Name)
  (version_1 : ℕ) (text_1 : Lean.FileMap) (dependencyBuildMode_1 : Lean.Lsp.DependencyBuildMode),
  ({ uri := uri, mod := mod, version := version, text := text, dependencyBuildMode := dependencyBuildMode } =
      { uri := uri_1, mod := mod_1, version := version_1, text := text_1,
        dependencyBuildMode := dependencyBuildMode_1 }) =
    (uri = uri_1 ∧ mod = mod_1 ∧ version = version_1 ∧ text = text_1 ∧ dependencyBuildMode = dependencyBuildMode_1)
-- Mathlib.Algebra.Algebra.Subalgebra.Matrix
/-- A version of `Set.matrix` for `Subalgebra`s.
Given a `Subalgebra` `S`, `S.matrix` is the `Subalgebra` of square matrices `m`
all of whose entries `m i j` belong to `S`.  -/
Subalgebra.matrix : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {n : Type u_3} →
            [inst_3 : Fintype n] → [inst_4 : DecidableEq n] → Subalgebra R A → Subalgebra R (Matrix n n A)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_succ_right_eq_push : ∀ {m n : ℕ}, m ≤ n → (m<...=n + 1).toArray = (m<...=n).toArray.push (n + 1)
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpoly_eq_of_basis : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ : L →ₗ[R] Module.End R M) [inst_5 : Fintype ι] [inst_6 : Fintype ιM] [inst_7 : DecidableEq ι]
  [inst_8 : Module.Free R M] [inst_9 : Module.Finite R M] (b : Module.Basis ι R L) [inst_10 : DecidableEq ιM]
  (bₘ : Module.Basis ιM R M),
  φ.polyCharpoly b =
    Polynomial.map (↑(MvPolynomial.bind₁ (LinearMap.toMvPolynomial b bₘ.end φ))) (Matrix.charpoly.univ R ιM)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- `ContinuousAlternatingMap.compContinuousLinearMap` as a bundled `LinearMap`.  -/
ContinuousAlternatingMap.compContinuousLinearMapₗ : {R : Type u_1} →
  {M : Type u_2} →
    {M' : Type u_3} →
      {N : Type u_4} →
        {ι : Type u_6} →
          [inst : CommSemiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : Module R M] →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : AddCommMonoid M'] →
                    [inst_5 : Module R M'] →
                      [inst_6 : TopologicalSpace M'] →
                        [inst_7 : AddCommMonoid N] →
                          [inst_8 : Module R N] →
                            [inst_9 : TopologicalSpace N] →
                              [inst_10 : ContinuousAdd N] →
                                [inst_11 : ContinuousConstSMul R N] →
                                  (M →L[R] M') → M' [⋀^ι]→L[R] N →ₗ[R] M [⋀^ι]→L[R] N
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.AEDisjoint.of_le : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t → ∀ {ν : MeasureTheory.Measure α}, ν ≤ μ → MeasureTheory.AEDisjoint ν s t
-- Init.Data.Array.Lemmas
Array.back!_eq_back? : ∀ {α : Type u_1} [inst : Inhabited α] {xs : Array α}, xs.back! = xs.back?.getD default
-- Mathlib.Data.Set.Card
Set.eq_univ_iff_ncard : ∀ {α : Type u_1} [Finite α] (s : Set α), s = Set.univ ↔ s.ncard = Nat.card α
-- Mathlib.Order.Monotone.Basic
StrictMono.ite : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β},
  StrictMono f →
    StrictMono g →
      ∀ {p : α → Prop} [inst_2 : DecidablePred p],
        (∀ ⦃x y : α⦄, x < y → p y → p x) → (∀ (x : α), f x ≤ g x) → StrictMono fun x => if p x then f x else g x
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.quotient : {G : Type u} →
  (X : Type v) →
    [inst : Group G] →
      [inst_1 : Monoid X] →
        [inst_2 : MulAction X G] → (H : Subgroup G) → [MulAction.QuotientAction X H] → MulAction X (G ⧸ H)
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.Prepartition.upper_sub_lower_of_mem_splitCenter : ∀ {ι : Type u_1} [inst : Fintype ι] {I J : BoxIntegral.Box ι},
  J ∈ BoxIntegral.Prepartition.splitCenter I → ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.coe_pointwise_smul : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M] (a : α) (S : Submodule R M),
  ↑(a • S) = a • ↑S
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_finsetSum : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : AddCommMonoid γ] [inst_3 : ContinuousAdd γ] {ι : Type u_5} (s : Finset ι) (f : ι → α →ₘ[μ] γ),
  ↑(∑ i ∈ s, f i) =ᵐ[μ] ∑ i ∈ s, ↑(f i)
-- Lean.Environment
Lean.instToStringModuleIdx : ToString Lean.ModuleIdx
-- Lean.Elab.Tactic.Monotonicity
Lean.Meta.Monotonicity.solveMonoStep : optParam ({α : Type} → Lean.Expr → Array Lean.Name → Lean.MetaM α) @Lean.Meta.Monotonicity.defaultFailK →
  Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Init.Data.List.Erase
List.exists_or_eq_self_of_eraseP : ∀ {α : Type u_1} (p : α → Bool) (l : List α),
  List.eraseP p l = l ∨ ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ List.eraseP p l = l₁ ++ l₂
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.ones_embedding : ∀ {n : ℕ} (i : Fin (Composition.ones n).length) (h : 0 < (Composition.ones n).blocksFun i),
  ((Composition.ones n).embedding i) ⟨0, h⟩ = ⟨↑i, ⋯⟩
-- Mathlib.RepresentationTheory.Rep.Res
Rep.instFaithfulResFunctor : ∀ {k : Type u} [inst : Semiring k] {G : Type v1} {H : Type v2} [inst_1 : Monoid G] [inst_2 : Monoid H] (f : H →* G),
  (Rep.resFunctor f).Faithful
-- Init.Data.UInt.Lemmas
UInt16.zero_mul : ∀ {a : UInt16}, 0 * a = 0
-- Mathlib.Analysis.Convex.Hull
convexHull_subset_affineSpan : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] (s : Set E), (convexHull 𝕜) s ⊆ ↑(affineSpan 𝕜 s)
-- Mathlib.Computability.Encoding
/-- A decoding function from `List Bool` to `ℕ`.  -/
Computability.decodeNat : List Bool → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_eq_two_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.edist u v = 2 ↔ u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
-- Mathlib.Analysis.Normed.Group.Basic
IndiscreteTopology.norm_eq_zero' : ∀ {E : Type u_5} [inst : SeminormedGroup E] [IndiscreteTopology E] (x : E), ‖x‖ = 0
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.forIn_filterMapWithPostcondition.match_1.eq_1 : ∀ {β₂ : Type u_1} (motive : Option β₂ → Sort u_2) (c : β₂) (h_1 : (c : β₂) → motive (some c))
  (h_2 : Unit → motive none),
  (match some c with
    | some c => h_1 c
    | none => h_2 ()) =
    h_1 c
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.D₂.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (j j' : ι₄)
  [inst_23 : HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄],
  HomologicalComplex.mapBifunctor₂₃.D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' =
    HomologicalComplex.mapBifunctor₂₃.D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j'
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The inverse of `rotation` is rotation by the negation of the angle.  -/
Orientation.rotation_symm : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle), (o.rotation θ).symm = o.rotation (-θ)
-- Mathlib.Data.Real.Basic
Real.ofCauchy.inj : ∀ {cauchy cauchy_1 : CauSeq.Completion.Cauchy abs}, { cauchy := cauchy } = { cauchy := cauchy_1 } → cauchy = cauchy_1
-- Mathlib.Analysis.Normed.Field.Basic
NormedDivisionRing.norm_le_one_of_discrete : ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] (x : 𝕜), ‖x‖ ≤ 1
-- Mathlib.Topology.Sheaves.Presheaf
/-- `restrict_tac` solves relations among subsets (copied from `aesop cat`)  -/
TopCat.Presheaf.restrict_tac : Lean.ParserDescr
-- Init.Data.Option.Lemmas
Option.getD_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) (o : Option α), (Option.map f o).getD (f x) = f (o.getD x)
-- Mathlib.Algebra.CharP.Lemmas
CharP.prime_ringChar : ∀ (R : Type u_1) [inst : Ring R] [NoZeroDivisors R] [Nontrivial R] [Finite R], Nat.Prime (ringChar R)
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.instMonoFNatι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) (n : ℕ),
  CategoryTheory.Mono (I.ι.f n)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.mk_smul_mk : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SetLike S M] [hS : SMulMemClass S R M] (s : S)
  (r : R) (x : M) (hx : x ∈ s), r • ⟨x, hx⟩ = ⟨r • x, ⋯⟩