mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner
MeasureTheory.StronglyMeasurable.inner : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {x : MeasurableSpace α} {f g : α → E},
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun t => inner 𝕜 (f t) (g t)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.removeLoops_isNonloop_eq : ∀ {α : Type u_1} {M : Matroid α}, M.removeLoops.IsNonloop = M.IsNonloop
-- Init.Data.String.Lemmas.Splits
String.Pos.splits : ∀ {s : String} (p : s.Pos), p.Splits (s.sliceTo p).copy (s.sliceFrom p).copy
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.RingCompute.mk.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)}
  [inst : (a : Q(«$α»)) → SizeOf (BaseType a)] (toRingCompare : Mathlib.Tactic.Ring.Common.RingCompare BaseType)
  (add :
    {x y : Q(«$α»)} →
      BaseType x →
        BaseType y →
          Lean.MetaM
            (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» + «$y») ×
              Option Q(Mathlib.Meta.NormNum.IsNat («$x» + «$y») 0)))
  (mul :
    {x y : Q(«$α»)} → BaseType x → BaseType y → Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» * «$y»)))
  (cast :
    (v : Lean.Level) →
      (β : Q(Type v)) →
        Q(CommSemiring «$β») →
          (x : Q(SMul «$β» «$α»)) →
            (x_1 : Q(«$β»)) →
              Mathlib.Tactic.AtomM
                ((y : Q(«$α»)) ×
                  Mathlib.Tactic.Ring.Common.ExSum BaseType sα q(«$y») × Q(∀ (a : «$α»), «$x_1» • a = «$y» * a)))
  (neg :
    {x : Q(«$α»)} →
      (rα : Q(CommRing «$α»)) → BaseType x → Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(-«$x»)))
  (pow :
    {x : Q(«$α»)} →
      {b : Q(ℕ)} →
        BaseType x →
          Mathlib.Tactic.Ring.Common.ExProdNat q(«$b») →
            OptionT Lean.MetaM (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» ^ «$b»)))
  (inv :
    {x : Q(«$α»)} →
      Option Q(CharZero «$α») →
        (fα : Q(Semifield «$α»)) →
          BaseType x → Mathlib.Tactic.AtomM (Option (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x»⁻¹))))
  (derive :
    (x : Q(«$α»)) →
      Lean.MetaM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum BaseType sα) q(«$x»)))
  (isOne : {x : Q(«$α»)} → BaseType x → Option Q(Mathlib.Meta.NormNum.IsNat «$x» 1))
  (one : Mathlib.Tactic.Ring.Common.Result BaseType q(Nat.rawCast 1)),
  sizeOf
      { toRingCompare := toRingCompare, add := add, mul := mul, cast := cast, neg := neg, pow := pow, inv := inv,
        derive := derive, isOne := isOne, one := one } =
    1 + sizeOf toRingCompare + sizeOf one
-- Init.Data.String.Subslice
String.Slice.Subslice.toString_eq : ∀ {s : String.Slice}, String.Slice.Subslice.toString = String.Slice.copy ∘ String.Slice.Subslice.toSlice
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.instCommShiftOppositeOpOpEquivalenceInt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ],
  (CategoryTheory.opOpEquivalence C).CommShift ℤ
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.DirectLimit.le_partialEquivLimit : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Type u_1}
  [inst_2 : Preorder ι] [inst_3 : Nonempty ι] [inst_4 : IsDirectedOrder ι] (S : ι →o L.PartialEquiv M N) (i : ι),
  S i ≤ FirstOrder.Language.DirectLimit.partialEquivLimit S
-- Mathlib.Order.Partition.Finpartition
Finpartition.instFintypeOfDecidableEq : {α : Type u_1} →
  [inst : Lattice α] → [inst_1 : OrderBot α] → [Fintype α] → [DecidableEq α] → (a : α) → Fintype (Finpartition a)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.app_one_eq_π : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Cofork f g),
  t.ι.app CategoryTheory.Limits.WalkingParallelPair.one = t.π
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_zero : ∀ (α : Type u_1) (G : Type u_5) [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α}, ∫ (x : α), 0 ∂μ = 0
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The division in the Ore localization `X[S⁻¹]`, as a fraction of an element of `X` and `S`.  -/
OreLocalization.«term_/ₒ_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsReflection.inv : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W},
  cs.IsReflection t → t⁻¹ = t
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {fallback : α}, t.getKeyD t.maxKey! fallback = t.maxKey!
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.insertListIfNew : {α : Type u} → {β : α → Type v} → [BEq α] → List ((a : α) × β a) → List ((a : α) × β a) → List ((a : α) × β a)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.toRange_ι_assoc : ∀ {X Y : SSet} (f : X ⟶ Y) {Z : SSet} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.toRange f)
      (CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.range f).ι h) =
    CategoryTheory.CategoryStruct.comp f h
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.maxEntryD : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → (a : α) × β a → (a : α) × β a
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.mk.sizeOf_spec : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : SizeOf E] [inst_5 : SizeOf F] (toFun : E → F) (smooth' : ContDiff ℝ (↑⊤) toFun)
  (decay' : ∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n toFun x‖ ≤ C),
  sizeOf { toFun := toFun, smooth' := smooth', decay' := decay' } = 1 + sizeOf smooth'
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.foldM_filter : ∀ {α β δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad n]
  [LawfulMonad n] [inst_4 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → Bool} {g : δ → β → n δ}
  {init : δ} {it : Std.Iter β},
  Std.Iter.foldM g init (Std.Iter.filter f it) =
    Std.Iter.foldM (fun d b => if f b = true then g d b else pure d) init it
-- Mathlib.Topology.Closure
IsClosed.frontier_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → frontier s = s \ interior s
-- Mathlib.Logic.Basic
not_forall₂_of_exists₂_not : ∀ {α : Sort u_1} {p : α → Prop} {P : (x : α) → p x → Prop}, (∃ x, ∃ (h : p x), ¬P x h) → ¬∀ (x : α) (h : p x), P x h
-- Mathlib.CategoryTheory.Abelian.Ext
ChainComplex.linearYonedaObj_X : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C] [inst_1 : CategoryTheory.Abelian C] {α : Type u_3}
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] (X : ChainComplex C α) (A : Type u_4) [inst_4 : Ring A]
  [inst_5 : CategoryTheory.Linear A C] (Y : C) (i : α),
  (X.linearYonedaObj A Y).X i = ((CategoryTheory.linearYoneda A C).obj Y).obj (Opposite.op (X.X i))
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.symbol.inj : ∀ {prio prio_1 : ℕ}, Lean.Meta.Grind.AttrKind.symbol prio = Lean.Meta.Grind.AttrKind.symbol prio_1 → prio = prio_1
-- Lean.Data.AssocList
Lean.AssocList.cons.inj : ∀ {α : Type u} {β : Type v} {key : α} {value : β} {tail : Lean.AssocList α β} {key_1 : α} {value_1 : β}
  {tail_1 : Lean.AssocList α β},
  Lean.AssocList.cons key value tail = Lean.AssocList.cons key_1 value_1 tail_1 →
    key = key_1 ∧ value = value_1 ∧ tail = tail_1
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
MonoidWithZero.coe_inverse : ∀ {M : Type u_8} [inst : CommMonoidWithZero M], ⇑MonoidWithZero.inverse = Ring.inverse
-- Mathlib.RingTheory.Noetherian.Orzech
IsNoetherian.equivPUnitOfProdInjective_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type w} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : IsNoetherian R M] (f : M × N →ₗ[R] M)
  (i : Function.Injective ⇑f) (x : N), (IsNoetherian.equivPUnitOfProdInjective f i) x = PUnit.unit
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α},
  k ∈ Std.ExtDHashMap.Const.unitOfList l ↔ l.contains k = true
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l →
        ∀
          {h' :
            (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).contains
                k' =
              true},
          (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey k' h' =
            k
-- Std.Time.Format.DateFormat
/-- English (US) locale.
 -/
Std.Time.DateFormat.enUS : Std.Time.DateFormat
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- Use `mk_start_snd_eq_head_edges` to rewrite in the reverse direction.  -/
SimpleGraph.Walk.head_edges_eq_mk_start_snd : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : p.edges ≠ []), p.edges.head hp = s(v, p.snd)
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_dvd_iff_zsmul_eq_zero : ∀ {G : Type u_1} [inst : AddGroup G] {x : G} {i : ℤ}, ↑(addOrderOf x) ∣ i ↔ i • x = 0
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_le_sub_iff_left : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] [AddRightMono α] {b c : α} (a : α),
  a - b ≤ a - c ↔ c ≤ b
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiableWithinAt_neg_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s : (x : B) → E x}
  {u : Set B} {x₀ : B}, MDiffAt[u] (T% s) x₀ → (MDiffAt[u] fun x => ⟨x, (-s) x⟩) x₀
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumElim_isExpansionOn : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L')
  (M : Type u_1) [inst : L.Structure M] [inst_1 : L'.Structure M] [inst_2 : L''.Structure M] [ϕ.IsExpansionOn M]
  [ψ.IsExpansionOn M], (ϕ.sumElim ψ).IsExpansionOn M
-- Mathlib.Data.Multiset.Fintype
Multiset.fintypeCoe : {α : Type u_1} → [inst : DecidableEq α] → {m : Multiset α} → Fintype m.ToType
-- Mathlib.FieldTheory.IsPerfectClosure
pow_expChar_pow_inj_of_pNilradical_eq_bot : ∀ (R : Type u_1) [inst : CommRing R] (p : ℕ) [ExpChar R p],
  pNilradical R p = ⊥ → ∀ (n : ℕ), Function.Injective fun x => x ^ p ^ n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol.mk.inj : ∀ {sym sym_1 : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol},
  Lean.Lsp.DocumentSymbol.mk sym = Lean.Lsp.DocumentSymbol.mk sym_1 → sym = sym_1
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.All.ins : ∀ {α : Type u_1} {p : α → Prop} {cmp : α → α → Ordering} {x : α} {t : RBTree.RBNode α},
  p x → RBTree.RBNode.All p t → RBTree.RBNode.All p (RBTree.RBNode.ins cmp x t)
-- Mathlib.RepresentationTheory.Induced
/-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear map
`(Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G` sending `⟦h ⊗ₜ a⟧ ⊗ₜ b` to `⟦a ⊗ ρ(h)(b)⟧` for all
`h : H`, `a : A`, and `b : B`.  -/
Rep.coinvariantsTensorIndHom : {k : Type u} →
  [inst : CommRing k] →
    {G H : Type u} →
      [inst_1 : Group G] →
        [inst_2 : Group H] →
          (φ : G →* H) →
            (A : Rep.{u, u, u} k G) →
              (B : Rep.{u, u, u} k H) →
                ((Rep.coinvariantsTensor k H).obj (Rep.ind φ A)).obj B ⟶
                  ((Rep.coinvariantsTensor k G).obj A).obj (Rep.res φ B)
-- Mathlib.Data.Finset.Basic
Finset.disjoint_filter : ∀ {α : Type u_1} {s : Finset α} {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q],
  Disjoint (Finset.filter p s) (Finset.filter q s) ↔ ∀ x ∈ s, p x → ¬q x
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.forget_createsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat),
  AddGrpCat.forget_createsLimit F =
    CategoryTheory.createsLimitOfNatIso
      (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ AddGrpCat AddMonCat).comp (CategoryTheory.forget AddMonCat)))
-- Lean.Elab.InfoTree.Main
Lean.Elab.DocElabInfo.format : Lean.Elab.ContextInfo → Lean.Elab.DocElabInfo → Std.Format
-- Init.Prelude
MonadFunctor.mk : {m : semiOutParam (Type u → Type v)} →
  {n : Type u → Type w} → ({α : Type u} → ({β : Type u} → m β → m β) → n α → n α) → MonadFunctor m n
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c) (i j : ι),
  (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K).X.d i j = (K.d i j).f
-- Mathlib.RingTheory.Perfection
PerfectionMap.injective : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u₁} [inst_1 : CommSemiring R] [inst_2 : CharP R p] {P : Type u₂}
  [inst_3 : CommSemiring P] [inst_4 : CharP P p] [inst_5 : PerfectRing P p] {π : P →+* R},
  PerfectionMap p π →
    ∀ ⦃x y : P⦄, (∀ (n : ℕ), π ((⇑(frobeniusEquiv P p).symm)^[n] x) = π ((⇑(frobeniusEquiv P p).symm)^[n] y)) → x = y
-- Mathlib.GroupTheory.HNNExtension
/-- Every `ReducedWord` is the product of an element of the group and a word made up
of letters each of which is in the transversal. `head` is that element of the base group.  -/
HNNExtension.NormalWord.ReducedWord.head : {G : Type u_1} → [inst : Group G] → {A B : Subgroup G} → HNNExtension.NormalWord.ReducedWord G A B → G
-- Mathlib.Algebra.Order.Round
round_eq_iff : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] {x : α}
  {n : ℤ}, round x = n ↔ x ∈ Set.Ico (↑n - 1 / 2) (↑n + 1 / 2)
-- Mathlib.Topology.Sheaves.Sheaf
/-- The presheaf valued in `Unit` over any topological space is a sheaf.
 -/
TopCat.Presheaf.isSheaf_unit : ∀ {X : TopCat} (F : TopCat.Presheaf (CategoryTheory.Discrete Unit) X), F.IsSheaf
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.mk₀_comp_extMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (f : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m) (hf : CategoryTheory.CategoryStruct.comp f (R.cocomplex.d n m) = 0)
  {X' : C} (g : X' ⟶ X),
  (CategoryTheory.Abelian.Ext.mk₀ g).comp (R.extMk f m hm hf) ⋯ =
    R.extMk (CategoryTheory.CategoryStruct.comp g f) m hm ⋯
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.preimage_inf : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U V : Y.Opens},
  (TopologicalSpace.Opens.map f.base).obj (U ⊓ V) =
    (TopologicalSpace.Opens.map f.base).obj U ⊓ (TopologicalSpace.Opens.map f.base).obj V
-- Mathlib.Topology.Algebra.Module.PerfectPairing
/-- Given a perfect pairing between `M` and `N`, we may interchange the roles of `M` and `N`.  -/
LinearMap.flip.instIsContPerfPair : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : TopologicalSpace R]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : TopologicalSpace M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : TopologicalSpace N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsContPerfPair], p.flip.IsContPerfPair
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.singleton_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] (t : Set β) (b : β), {b} -ᵥ t = (fun x => b -ᵥ x) '' t
-- Init.Control.Lawful.Instances
ReaderT.instLawfulFunctor : ∀ {m : Type u_1 → Type u_2} {ρ : Type u_1} [inst : Monad m] [LawfulFunctor m], LawfulFunctor (ReaderT ρ m)
-- Init.Data.List.Lex
List.lex_asymm : ∀ {α : Type u_1} {r : α → α → Prop},
  (∀ {x y : α}, r x y → ¬r y x) → ∀ {l₁ l₂ : List α}, List.Lex r l₁ l₂ → ¬List.Lex r l₂ l₁
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.mapRingHom_id`. -/
MonoidAlgebra.mapRangeRingHom_id : ∀ {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : Monoid M],
  MonoidAlgebra.mapRingHom M (RingHom.id R) = RingHom.id (MonoidAlgebra R M)
-- Mathlib.Geometry.Euclidean.MongePoint
/-- Suppose we are given a triangle `t₁`, and replace one of its
vertices by its orthocenter, yielding triangle `t₂` (with vertices not
necessarily listed in the same order).  Then the orthocenter of `t₂`
is the vertex of `t₁` that was replaced.  -/
Affine.Triangle.orthocenter_replace_orthocenter_eq_point : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {t₁ t₂ : Affine.Triangle ℝ P} {i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        j₁ ≠ j₂ →
          j₁ ≠ j₃ →
            j₂ ≠ j₃ →
              t₂.points j₁ = t₁.orthocenter →
                t₂.points j₂ = t₁.points i₂ → t₂.points j₃ = t₁.points i₃ → t₂.orthocenter = t₁.points i₁
-- Mathlib.CategoryTheory.Limits.Filtered
CategoryTheory.Limits.hasFilteredColimitsOfSize_of_univLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [UnivLE.{w, w₂}] [UnivLE.{w', w₂'}]
  [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w₂', w₂, v, u} C],
  CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, v, u} C
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getCast?.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a a_1 : α) (b : β a_1)
  (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getCast? a (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    if h : (a_1 == a) = true then some (cast ⋯ b) else Std.DHashMap.Internal.AssocList.getCast? a es
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.instHasOfPostcompPropertyLocalEpiIsLocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C},
  P.localEpi.HasOfPostcompProperty P.isLocal
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- A sort. Universe levels are ignored.  -/
Lean.Meta.RefinedDiscrTree.Key.sort : Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Arithmetic progressions can be pushed forward along bijective 2-Freiman homs.  -/
IsMulFreimanHom.mulRothNumber_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : CommMonoid α] [inst_2 : CommMonoid β]
  [inst_3 : DecidableEq β] {A : Finset α} {B : Finset β} {f : α → β},
  IsMulFreimanHom 2 (↑A) (↑B) f → Set.BijOn f ↑A ↑B → mulRothNumber B ≤ mulRothNumber A
-- Mathlib.Data.Set.Lattice
Set.iUnion_inter_subset : ∀ {ι : Sort u_12} {α : Type u_13} {s t : ι → Set α}, ⋃ i, s i ∩ t i ⊆ (⋃ i, s i) ∩ ⋃ i, t i
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by weight, non-strict inequality
version: if the total weight of a finite set of pigeons is less than or equal to `n • b`, they are
sorted into some pigeonholes, and for all but `n > 0` pigeonholes the total weight of the pigeons
there is nonnegative, then for at least one of these `n` pigeonholes, the total weight of the
pigeons in this pigeonhole is less than or equal to `b`.  -/
Finset.exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M}
  {b : M} [inst_1 : AddCommMonoid M] [inst_2 : LinearOrder M] [IsOrderedCancelAddMonoid M],
  (∀ y ∉ t, 0 ≤ ∑ x ∈ s with f x = y, w x) →
    t.Nonempty → ∑ x ∈ s, w x ≤ t.card • b → ∃ y ∈ t, ∑ x ∈ s with f x = y, w x ≤ b
-- Mathlib.Combinatorics.Graph.Delete
Graph.restrict_eq_self_iff : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (E₀ : Set β), G.restrict E₀ = G ↔ G.edgeSet ⊆ E₀
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasWidePullbacks_opposite_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Limits.HasWidePullbacks Cᵒᵖ ↔ CategoryTheory.Limits.HasWidePushouts C
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.toAddSubgroup_mono : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], Monotone NonUnitalSubring.toAddSubgroup
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.eval_add_of_sq_eq_zero : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R) (x y : R),
  y ^ 2 = 0 → Polynomial.eval (x + y) p = Polynomial.eval x p + Polynomial.eval x (Polynomial.derivative p) * y
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε' : Type u_8} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddMonoid ε'] [ContinuousAdd ε'] {f g : α → ε'},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → MeasureTheory.Integrable (f + g) μ
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.pu32 : Std.Internal.Parsec.ByteArray.Parser UInt32
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
WithBot.ciSup_empty : ∀ {α : Type u_1} {ι : Sort u_4} [inst : Preorder α] [IsEmpty ι] [inst_2 : SupSet α] (f : ι → WithBot α), ⨆ i, f i = ⊥
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.nhds_basis_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α}, (nhds x).HasBasis (fun x => 0 < x) (Metric.ball x)
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Computation.BisimO.match_1.splitter : {α : Type u_1} →
  (motive : α ⊕ Computation α → α ⊕ Computation α → Sort u_2) →
    (x x_1 : α ⊕ Computation α) →
      ((a a' : α) → motive (Sum.inl a) (Sum.inl a')) →
        ((s s' : Computation α) → motive (Sum.inr s) (Sum.inr s')) →
          ((x x_2 : α ⊕ Computation α) →
              (∀ (a a' : α), x = Sum.inl a → x_2 = Sum.inl a' → False) →
                (∀ (s s' : Computation α), x = Sum.inr s → x_2 = Sum.inr s' → False) → motive x x_2) →
            motive x x_1
-- Mathlib.FieldTheory.Normal.Basic
/-- An intersection of normal extensions is normal.  -/
IntermediateField.normal_iInf : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] {ι : Type u_3}
  [hι : Nonempty ι] (t : ι → IntermediateField F K) [h : ∀ (i : ι), Normal F ↥(t i)], Normal F ↥(⨅ i, t i)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂'_compl₁₂ : ∀ {n : Type u_11} {m : Type u_12} {n' : Type u_13} {m' : Type u_14} {R : Type u_16} [inst : CommSemiring R]
  [inst_1 : Fintype n] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : DecidableEq m] [inst_5 : Fintype n']
  [inst_6 : Fintype m'] [inst_7 : DecidableEq n'] [inst_8 : DecidableEq m'] (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R)
  (l : (n' → R) →ₗ[R] n → R) (r : (m' → R) →ₗ[R] m → R),
  (LinearMap.toMatrix₂' R) (B.compl₁₂ l r) =
    (LinearMap.toMatrix' l).transpose * (LinearMap.toMatrix₂' R) B * LinearMap.toMatrix' r