mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.ofSet_coe : ∀ {α : Type u_1} (s : Set α), ↑(PartialEquiv.ofSet s) = id
-- Mathlib.ModelTheory.Substructures
/-- The equivalence between a substructure `s` and its image `s.map f.toHom`, where `f` is an
embedding.  -/
FirstOrder.Language.Embedding.substructureEquivMap : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          (f : L.Embedding M N) → (s : L.Substructure M) → L.Equiv ↥s ↥(FirstOrder.Language.Substructure.map f.toHom s)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.instSliceableImplUnitRicSlice : {α : Type u} →
  [inst : Ord α] →
    Std.Ric.Sliceable (Std.DTreeMap.Internal.Impl α fun x => Unit) α (Std.DTreeMap.Internal.Unit.RicSlice α)
-- Lean.Parser.Term
Lean.Parser.Term.showRhs.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.CompleteLattice.Basic
iSup_false : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : False → α}, iSup s = ⊥
-- Lean.Meta.Match.Match
Lean.Meta.Match.MkMatcherInput.mk.inj : ∀ {matcherName : Lean.Name} {matchType : Lean.Expr} {discrInfos : Array Lean.Meta.Match.DiscrInfo}
  {lhss : List Lean.Meta.Match.AltLHS} {isSplitter : Option Lean.Meta.Match.Overlaps} {matcherName_1 : Lean.Name}
  {matchType_1 : Lean.Expr} {discrInfos_1 : Array Lean.Meta.Match.DiscrInfo} {lhss_1 : List Lean.Meta.Match.AltLHS}
  {isSplitter_1 : Option Lean.Meta.Match.Overlaps},
  { matcherName := matcherName, matchType := matchType, discrInfos := discrInfos, lhss := lhss,
        isSplitter := isSplitter } =
      { matcherName := matcherName_1, matchType := matchType_1, discrInfos := discrInfos_1, lhss := lhss_1,
        isSplitter := isSplitter_1 } →
    matcherName = matcherName_1 ∧
      matchType = matchType_1 ∧ discrInfos = discrInfos_1 ∧ lhss = lhss_1 ∧ isSplitter = isSplitter_1
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_mono_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ ν : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] (f : α → ε),
  ν ≤ μ → MeasureTheory.eLpNorm f p ν ≤ MeasureTheory.eLpNorm f p μ
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_true : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, P ∨ ⌜True⌝ ⊣⊢ₛ ⌜True⌝
-- Init.Data.List.Sort.Impl
List.MergeSort.Internal.splitRevAt_eq : ∀ {α : Type u_1} (i : ℕ) (l : List α), List.MergeSort.Internal.splitRevAt i l = ((List.take i l).reverse, List.drop i l)
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
/-- The embedding from the even subalgebra with an extra dimension into the original algebra.  -/
CliffordAlgebra.ofEven : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (Q : QuadraticForm R M) → ↥(CliffordAlgebra.even (CliffordAlgebra.EquivEven.Q' Q)) →ₐ[R] CliffordAlgebra Q
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimTargetView.mk.sizeOf_spec : ∀ (hIdent? : Option Lean.Ident) (term : Lean.Syntax),
  sizeOf { hIdent? := hIdent?, term := term } = 1 + sizeOf hIdent? + sizeOf term
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- If `f` is surjective, then the kernel of `f ⊗ (id B)` is generated by the kernel of `f`  -/
Algebra.TensorProduct.rTensor_ker : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A : Type u_6}
  {B : Type u_7} {C : Type u_8} [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Ring C] [inst_6 : Algebra R A]
  [inst_7 : Algebra R B] [inst_8 : Algebra R C] [inst_9 : Algebra S A] [inst_10 : Algebra S B]
  [inst_11 : IsScalarTower R S A] [inst_12 : IsScalarTower R S B] (f : A →ₐ[S] B),
  Function.Surjective ⇑f →
    RingHom.ker (Algebra.TensorProduct.map f (AlgHom.id R C)) =
      Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f)
-- Mathlib.Combinatorics.Graph.Basic
Graph.edgeSet_copy : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) {vertexSet : Set α} {edgeSet : Set β} {IsLink : β → α → α → Prop}
  (hvertexSet : G.vertexSet = vertexSet) (hedgeSet : G.edgeSet = edgeSet)
  (hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y), (G.copy hvertexSet hedgeSet hIsLink).edgeSet = edgeSet
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_mul : ∀ {α : Type u_1} [inst : Mul α] (a b : αᵒᵈ), OrderDual.ofDual (a * b) = OrderDual.ofDual a * OrderDual.ofDual b
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `neg_apply`. -/
QuadraticMap.neg_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Neg β}
  {inst_2 : Neg F} [self : IsNegApply F α β] (f : F) (x : α), (-f) x = -f x
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Sum.isGeneratedBy`. -/
Sum.deltaGeneratedSpace : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {Z : Type v'} [inst_1 : TopologicalSpace Z] [Topology.IsGeneratedBy X Y] [Topology.IsGeneratedBy X Z],
  Topology.IsGeneratedBy X (Y ⊕ Z)
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
/-- If `F` is a pseudofunctor from `Cᵒᵖ` to `Cat`, and `M` and `N` are objects in
`F.obj (.mk (op S))`, this is the presheaf of morphisms from `M` to `N`: it sends
an object `T : Over S` corresponding to a morphism `p : X ⟶ S` to the type
of morphisms $p^* M ⟶ p^* N$.  -/
CategoryTheory.Pseudofunctor.presheafHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {S : C} →
        ↑(F.obj { as := Opposite.op S }) →
          ↑(F.obj { as := Opposite.op S }) → CategoryTheory.Functor (CategoryTheory.Over S)ᵒᵖ (Type v')
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDecl.mk.inj : ∀ {declName : Lean.Name} {keys : Array Lean.Meta.SimpTheoremKey} {declName_1 : Lean.Name}
  {keys_1 : Array Lean.Meta.SimpTheoremKey},
  { declName := declName, keys := keys } = { declName := declName_1, keys := keys_1 } →
    declName = declName_1 ∧ keys = keys_1
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- The possibilities we distinguish to delaborate the finset indexing a big operator:
* `finset s` corresponds to `∑ x ∈ s, f x`
* `univ` corresponds to `∑ x, f x`
* `Iio n`/`Iic n`/`Ioi n`/`Ici n` corresponds to the intervals that are elaborated by sums.
 -/
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult : Type
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.EqnInfo.value : Lean.Elab.Structural.EqnInfo → Lean.Expr
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
CategoryTheory.Sheaf.instIsMonoidalFunctorOppositeIsSheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A],
  CategoryTheory.ObjectProperty.IsMonoidal (CategoryTheory.Presheaf.IsSheaf J)
-- Mathlib.Data.Finsupp.Multiset
Multiset.toFinsupp_symm_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (f : α →₀ ℕ), Multiset.toFinsupp.symm f = Finsupp.toMultiset f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} (h : t.WF), (Std.TreeMap.Raw.filter f t)[k]? = t[k]?.pfilter fun x h' => f (t.getKey k ⋯) x
-- Mathlib.Topology.Separation.Lemmas
/-- Countable subsets of metric spaces are totally disconnected.  -/
Set.Countable.isTotallyDisconnected : ∀ {X : Type u_1} [inst : MetricSpace X] {s : Set X}, s.Countable → IsTotallyDisconnected s
-- Mathlib.NumberTheory.Divisors
Nat.divisorsAntidiagonalList_zero : Nat.divisorsAntidiagonalList 0 = []
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.comp_symm : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B), (↑e).comp ↑e.symm = BialgHom.id R B
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_hom_app_assoc : ∀ {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.shiftFunctorCompIsoId_op_hom_app._auto_1)
  {Z : Cᵒᵖ} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId Cᵒᵖ n m hnm).hom.app X) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor Cᵒᵖ m).map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).hom.app
          (Opposite.op ((CategoryTheory.shiftFunctor C m).obj (Opposite.unop X))))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).inv.app (Opposite.unop X)).op h))
-- Mathlib.Analysis.Convex.Between
Wbtw.swap_left_iff : ∀ {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] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V] {x y z : P},
  Wbtw R x y z → (Wbtw R y x z ↔ x = y)
-- Init.Data.SInt.Lemmas
Int32.toInt64_le : ∀ {a b : Int32}, a.toInt64 ≤ b.toInt64 ↔ a ≤ b
-- Mathlib.SetTheory.Ordinal.Notation
/-- We can extend the fast growing hierarchy one more step to `ε₀` itself, using `ω ^ (ω ^ (⋯ ^ ω))`
as the fundamental sequence converging to `ε₀` (which is not an `ONote`). Extending the fast
growing hierarchy beyond this requires a definition of fundamental sequence for larger ordinals.  -/
ONote.fastGrowingε₀ : ℕ → ℕ
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_ofHom : ∀ {R : Type u} [inst : Ring R] {X Y : Type v} [inst_1 : AddCommGroup X] [inst_2 : Module R X] [inst_3 : AddCommGroup Y]
  [inst_4 : Module R Y] (f : X →ₗ[R] Y), ModuleCat.Hom.hom (ModuleCat.ofHom f) = f
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorAdd'.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n₁ n₂ n₁₂ : ℤ)
  (h : n₁ + n₂ = n₁₂), CochainComplex.shiftFunctorAdd' C n₁ n₂ n₁₂ h = CochainComplex.shiftFunctorAdd' C n₁ n₂ n₁₂ h
-- Mathlib.Order.Basic
/-- Pull back a `Preorder` instance along an injective function.

See note [reducible non-instances].  -/
Function.Injective.preorder : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder β] →
      [inst_1 : LE α] →
        [inst_2 : LT α] → (f : α → β) → (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) → (∀ {x y : α}, f x < f y ↔ x < y) → Preorder α
-- Mathlib.Data.Part
Part.ret_eq_some : ∀ {α : Type u_1} (a : α), pure a = Part.some a
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
IsTranscendenceBasis.mvPolynomial' : ∀ (ι : Type u) (R : Type u_1) [inst : CommRing R] [Nonempty ι], IsTranscendenceBasis R MvPolynomial.X
-- Mathlib.Order.Interval.Set.Defs
Set.Iio_def : ∀ {α : Type u_1} [inst : Preorder α] (a : α), {x | x < a} = Set.Iio a
-- Std.Data.DTreeMap.Internal.Lemmas
/-- Variant of `get!_map` that holds without `LawfulEqOrd`.  -/
Std.DTreeMap.Internal.Impl.Const.get!_map' : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] [inst_1 : Inhabited γ] {f : α → β → γ} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.map f t) k =
    (Option.pmap (fun v h => f (t.getKey k h) v) (Std.DTreeMap.Internal.Impl.Const.get? t k) ⋯).get!
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.Section.equivComp_apply : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (σ : S.Section)
  (equiv : S.Equiv S') (a : G), (σ.equivComp equiv) a = equiv (σ a)
-- Mathlib.Tactic.FunProp.ToBatteries
/-- For `#[x₁, .., xₙ]` create `(x₁, .., xₙ)`.
 -/
Mathlib.Meta.FunProp.mkProdElem : Array Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.ReservedNameAction
/-- Similar to `realizeGlobalConstNoOverloadCore`, but also executes reserved name actions.
 -/
Lean.realizeGlobalConstNoOverloadCore : Lean.Name → Lean.CoreM Lean.Name
-- Std.Do.PredTrans
Std.Do.PredTrans.apply_pushExcept : ∀ {ps : Std.Do.PostShape} {α ε : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)}
  (x : Std.Do.PredTrans ps (Except ε α)),
  (Std.Do.PredTrans.pushExcept x).apply Q =
    x.apply
      (fun x =>
        match x with
        | Except.ok a => Q.1 a
        | Except.error e => Q.2.1 e,
        Q.2.2)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
  [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] {X' Y' : D}
  (f' g' : X' ⟶ Y') [inst_5 : CategoryTheory.Limits.HasCoequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y')
  (wf : CategoryTheory.CategoryStruct.comp (G.map f) q = CategoryTheory.CategoryStruct.comp p f')
  (wg : CategoryTheory.CategoryStruct.comp (G.map g) q = CategoryTheory.CategoryStruct.comp p g') {Z : D}
  (h : CategoryTheory.Limits.colimit (CategoryTheory.Limits.parallelPair f' g') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (G.map f) (G.map g) f' g' p q wf wg))
          h)) =
    CategoryTheory.CategoryStruct.comp q
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f' g') h)
-- Lean.Setup
/-- `import all`; whether to import and expose all data saved by the module.  -/
Lean.Import.importAll : Lean.Import → Bool
-- Mathlib.Topology.Sheaves.PUnit
TopCat.Presheaf.isSheaf_on_punit_of_isTerminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : TopCat.Presheaf C (TopCat.of PUnit.{u_1 + 1}))
  (it : CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥))), F.IsSheaf
-- Lean.Meta.WHNF
Lean.Meta.smartUnfoldingMatchAlt? : Lean.Expr → Option Lean.Expr
-- Mathlib.Order.Filter.AtTopBot.Map
OrderIso.tendsto_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β),
  Filter.Tendsto (⇑e) Filter.atTop Filter.atTop
-- Mathlib.Topology.ContinuousOn
ContinuousAt.comp₂_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] {f : β × γ → δ} {g : α → β} {h : α → γ} {x : α}
  {s : Set α},
  ContinuousAt f (g x, h x) →
    ContinuousWithinAt g s x → ContinuousWithinAt h s x → ContinuousWithinAt (fun x => f (g x, h x)) s x
-- Mathlib.Algebra.Ring.IsFormallyReal
/-- The subsemigroup of sums of squares of nonzero elements.  -/
AddSubsemigroup.sumNonzeroSq : (R : Type u_1) → [inst : AddMonoid R] → [Mul R] → AddSubsemigroup R
-- Mathlib.CategoryTheory.Comma.Basic
/-- The canonical functor from `Comma L R` to `(Comma R.op L.op)ᵒᵖ`.  -/
CategoryTheory.Comma.opFunctor : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                CategoryTheory.Functor (CategoryTheory.Comma L R) (CategoryTheory.Comma R.op L.op)ᵒᵖ
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.lift_of_comp_eq_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), (FreeAddMonoid.lift fun x => FreeAddMonoid.of (f x)) = FreeAddMonoid.map f
-- Std.Data.HashMap.Basic
/-- Returns `true` if the hash map contains no mappings.

Note that if your `BEq` instance is not reflexive or your `Hashable` instance is not
lawful, then it is possible that this function returns `false` even though is not possible
to get anything out of the hash map.
 -/
Std.HashMap.isEmpty : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → Bool
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_inter_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.mopAlgEquivOp_symm_apply : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) (a : ↥S.op), S.mopAlgEquivOp.symm a = MulOpposite.op (S.addEquivOp.symm a)
-- Mathlib.Algebra.Group.WithOne.Map
WithZero.map₂_bot_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (b : WithZero β), WithZero.map₂ f 0 b = 0
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen : ∀ {R : Type u} [inst : CommSemiring R] {s : Set (PrimeSpectrum R)},
  IsClopen s → ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(PrimeSpectrum.basicOpen e) ∧ sᶜ = ↑(PrimeSpectrum.basicOpen f)
-- Init.Data.Range.Polymorphic.PRange
Std.Rxc.IsAlwaysFinite.mk : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α],
  (∀ (init hi : α), ∃ n, (Std.PRange.succMany? n init).elim True fun x => ¬x ≤ hi) → Std.Rxc.IsAlwaysFinite α
-- Mathlib.Dynamics.FixedPoints.Basic
Function.IsFixedPt.perm_inv : ∀ {α : Type u_1} {x : α} {e : Equiv.Perm α}, Function.IsFixedPt (⇑e) x → Function.IsFixedPt (⇑e⁻¹) x
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.nhds_eq_principal_Iic : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLowerSet α] (a : α),
  nhds a = Filter.principal (Set.Iic a)
-- Mathlib.Algebra.Category.Grp.Limits
/-- If `J` is `u`-small, the forgetful functor from `CommGrpCat.{u}` to `CommMonCat.{u}`
preserves limits of shape `J`.  -/
CommGrpCat.forget₂CommMon_preservesLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget₂ CommGrpCat CommMonCat)
-- Init.Data.Fin.Lemmas
Fin.succ_castSucc : ∀ {n : ℕ} (i : Fin n), i.castSucc.succ = i.succ.castSucc
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
/-- The polar coordinates are an open partial homeomorphism in `ℝ^2`, mapping `(r cos θ, r sin θ)`
to `(r, θ)`. It is a homeomorphism between `ℝ^2 - (-∞, 0]` and `(0, +∞) × (-π, π)`.  -/
polarCoord : OpenPartialHomeomorph (ℝ × ℝ) (ℝ × ℝ)
-- Mathlib.Order.CompleteLattice.Basic
biInf_ge_eq_iInf : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} [inst_1 : Preorder ι] {f : ι → α},
  ⨅ i, ⨅ j, ⨅ (_ : j ≥ i), f j = ⨅ i, f i
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- The weights sum to 1.  -/
Convexity.StdSimplex.total : ∀ {R : Type u} [inst : LE R] [inst_1 : AddCommMonoid R] [inst_2 : One R] {M : Type v} (self : Convexity.StdSimplex R M),
  (self.weights.sum fun x r => r) = 1
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimits F],
  CategoryTheory.Limits.ReflectsFiniteColimits F
-- Mathlib.Order.Completion
DedekindCut.instTotalLe : ∀ {α : Type u_1} [inst : LinearOrder α], Std.Total fun x1 x2 => x1 ≤ x2
-- Init.Core
DoResultSBC.continue.inj : ∀ {α σ : Type u} {a a_1 : σ}, DoResultSBC.continue a = DoResultSBC.continue a_1 → a = a_1
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.CompatibleSMul.mk : ∀ {R : Type u_1} {R' : Type u_4} [inst : CommSemiring R] [inst_1 : Monoid R'] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : DistribMulAction R' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : DistribMulAction R' N],
  (∀ (r : R') (m : M) (n : N), (r • m) ⊗ₜ[R] n = m ⊗ₜ[R] (r • n)) → TensorProduct.CompatibleSMul R R' M N
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.mono_cokernelDesc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [S.HasHomology] [inst_3 : CategoryTheory.Limits.HasCokernel S.f],
  S.Exact → CategoryTheory.Mono (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)
-- Mathlib.Analysis.Normed.Group.Basic
NormedCommGroup.nhds_basis_norm_lt : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (x : E), (nhds x).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y / x‖ < ε}
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.mk : {X : SSet} →
  {x₀ x₁ : X.obj (Opposite.op { len := 0 })} →
    {hom : SSet.Edge x₀ x₁} →
      (inv : SSet.Edge x₁ x₀) →
        hom.CompStruct inv (SSet.Edge.id x₀) → inv.CompStruct hom (SSet.Edge.id x₁) → hom.InvStruct
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toLinearIsometry_injective : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
  [inst_7 : Module R₂ E₂], Function.Injective LinearIsometryEquiv.toLinearIsometry
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.resetAnchors : Lean.Meta.Grind.GrindM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback.instIsSplitMonoDiagonal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f f],
  CategoryTheory.IsSplitMono (CategoryTheory.Limits.pullback.diagonal f)
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.refl_symm : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X], (DilationEquiv.refl X).symm = DilationEquiv.refl X
-- Mathlib.Data.Num.Basic
/-- `ofNat n` is the `PosNum` corresponding to `n`, except for `ofNat 0 = 1`.  -/
PosNum.ofNat : ℕ → PosNum
-- Mathlib.Computability.DFA
DFA.symm_reindex : ∀ {α : Type u} {σ : Type v} {σ' : Type u_2} (g : σ ≃ σ'), (DFA.reindex g).symm = DFA.reindex g.symm
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.lim_inv : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Field β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [inst_5 : CauSeq.IsComplete β abv] {f : CauSeq β abv}
  (hf : ¬f.LimZero), (f.inv hf).lim = f.lim⁻¹
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.substFunc.match_1.eq_1 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u_3}
  (motive : L.Term α → ({n : ℕ} → L.Functions n → L'.Term (Fin n)) → Sort u_6) (a : α)
  (x : {n : ℕ} → L.Functions n → L'.Term (Fin n))
  (h_1 : (a : α) → (x : {n : ℕ} → L.Functions n → L'.Term (Fin n)) → motive (FirstOrder.Language.var a) x)
  (h_2 :
    (l : ℕ) →
      (f : L.Functions l) →
        (ts : Fin l → L.Term α) →
          (tf : {n : ℕ} → L.Functions n → L'.Term (Fin n)) → motive (FirstOrder.Language.func f ts) tf),
  (match FirstOrder.Language.var a, x with
    | FirstOrder.Language.var a, x => h_1 a x
    | FirstOrder.Language.func f ts, tf => h_2 l f ts tf) =
    h_1 a x
-- Mathlib.Data.Set.Monotone
Set.antitoneOn_insert_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  AntitoneOn f (insert a s) ↔ (∀ b ∈ s, b ≤ a → f a ≤ f b) ∧ (∀ b ∈ s, a ≤ b → f b ≤ f a) ∧ AntitoneOn f s