mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_conjugation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z'),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
        (CategoryTheory.MonoidalCategoryStruct.associator X' Y' Z').inv)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFractionRel.symm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  {z₁ z₂ : W.LeftFraction X Y},
  CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂ → CategoryTheory.MorphismProperty.LeftFractionRel z₂ z₁
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen : ∀ (X : AlgebraicGeometry.Scheme) (U : X.Opens),
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))),
      ∃ n y, TopCat.Presheaf.restrictOpen y (X.basicOpen f) ⋯ = TopCat.Presheaf.restrictOpen f (X.basicOpen f) ⋯ ^ n * x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Replacing the third point by one on the same line but the opposite ray adds π to the oriented
angle.  -/
Sbtw.oangle_eq_add_pi_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₃' : P},
  Sbtw ℝ p₃ p₂ p₃' → p₁ ≠ p₂ → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃' + ↑Real.pi
-- Mathlib.Order.Category.Semilat
SemilatSupCat.dual_map : ∀ {x x_1 : SemilatSupCat} (a : SupBotHom x.X x_1.X), SemilatSupCat.dual.map a = SupBotHom.dual a
-- Mathlib.Topology.NhdsKer
mem_nhdsKer : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} {x : X},
  x ∈ nhdsKer s ↔ ∀ (U : Set X), IsOpen U → s ⊆ U → x ∈ U
-- Init.Data.UInt.Lemmas
USize.size_le_uint64Size : USize.size ≤ UInt64.size
-- Mathlib.Analysis.InnerProductSpace.Dual
/-- Maps a bounded sesquilinear form to its continuous linear map,
given by interpreting the form as a map `B : E →L⋆[𝕜] StrongDual 𝕜 E`
and dualizing the result using `toDual`.
 -/
InnerProductSpace.continuousLinearMapOfBilin : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → [CompleteSpace E] → (E →L⋆[𝕜] E →L[𝕜] 𝕜) → E →L[𝕜] E
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.instPartialOrder : {α : Type u_2} → [inst : TopologicalSpace α] → PartialOrder (TopologicalSpace.Clopens α)
-- Lean.Parser.Term
Lean.Parser.Term.sorry.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffMonoidMorphism.mk.sizeOf_spec : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {H' : Type u_5} [inst_4 : TopologicalSpace H']
  {E' : Type u_6} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {G : Type u_8} [inst_7 : TopologicalSpace G]
  [inst_8 : ChartedSpace H G] [inst_9 : Monoid G] {G' : Type u_9} [inst_10 : TopologicalSpace G']
  [inst_11 : ChartedSpace H' G'] [inst_12 : Monoid G'] [inst_13 : SizeOf 𝕜] [inst_14 : SizeOf H] [inst_15 : SizeOf E]
  [inst_16 : SizeOf H'] [inst_17 : SizeOf E'] [inst_18 : SizeOf G] [inst_19 : SizeOf G'] (toMonoidHom : G →* G')
  (contMDiff_toFun : ContMDiff I I' n (↑toMonoidHom).toFun),
  sizeOf { toMonoidHom := toMonoidHom, contMDiff_toFun := contMDiff_toFun } = 1 + sizeOf toMonoidHom
-- Mathlib.GroupTheory.Perm.DomMulAct
/-- The `invFun` component of `MulEquiv` from `MulAction.stabilizer (Perm α) f`
to the product of the `Equiv.Perm {a // f a = i}`.  -/
DomMulAct.stabilizerEquiv_invFun : {α : Type u_1} → {ι : Type u_2} → {f : α → ι} → ((i : ι) → Equiv.Perm { a // f a = i }) → α → α
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.homotopyEquivNondegComplex_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C], s.homotopyEquivNondegComplex.hom = s.toNondegComplex
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_roo_eq_zero_iff : ∀ {m n : ℤ} {i : ℕ}, (m<...n).toArray[i]! = 0 ↔ (n - (m + 1)).toNat ≤ i ∨ m + ↑i = -1
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_mul' : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  p.leadingCoeff * q.leadingCoeff ≠ 0 → (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
/-- The shadow of an initial segment is also an initial segment.  -/
Finset.Colex.IsInitSeg.shadow : ∀ {α : Type u_1} [inst : LinearOrder α] {𝒜 : Finset (Finset α)} {r : ℕ} [Finite α],
  Finset.Colex.IsInitSeg 𝒜 r → Finset.Colex.IsInitSeg 𝒜.shadow (r - 1)
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_bif_eq_bif : ∀ {w : ℕ} (d : Bool) (a b c : BitVec w),
  ((~~~bif d then a else b) == bif d then a else c) = bif d then ~~~a == a else ~~~b == c
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- If `X : Karoubi C`, then `X` is a retract of `((toKaroubi C).obj X.X)`.  -/
CategoryTheory.Idempotents.Karoubi.retract : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (X : CategoryTheory.Idempotents.Karoubi C) →
      CategoryTheory.Retract X ((CategoryTheory.Idempotents.toKaroubi C).obj X.X)
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
/-- Irreducibility is invariant under transpose.  -/
Matrix.IsIrreducible.transpose : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] {A : Matrix n n R},
  A.IsIrreducible → A.transpose.IsIrreducible
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.not_mem_edgeSet_of_isDiag : ∀ {V : Type u} (G : SimpleGraph V) {e : Sym2 V}, e.IsDiag → e ∉ G.edgeSet
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.self_le_maxKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α} {v : β k},
  (compare k (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.maxKey!).isLE = true
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.not_sqLe_succ : ∀ (c d y : ℕ), 0 < c → ¬Zsqrtd.SqLe (y + 1) c 0 d
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.continuous_projRestricts : ∀ {I : Type u} (C : Set (I → Bool)) {J K : I → Prop} [inst : (i : I) → Decidable (J i)]
  [inst_1 : (i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i),
  Continuous (Profinite.NobelingProof.ProjRestricts C h)
-- Mathlib.Computability.NFA
_private.Mathlib.Computability.NFA.0.NFA.Path.supp.match_1.splitter : {α : Type u_1} →
  {σ : Type u_2} →
    {M : NFA α σ} →
      (motive : (x : List α) → (t s : σ) → M.Path s t x → Sort u_3) →
        (x : List α) →
          (t s : σ) →
            (x_1 : M.Path s t x) →
              ((s : σ) → motive [] s s (NFA.Path.nil s)) →
                ((t s t_1 : σ) →
                    (a : α) →
                      (x : List α) →
                        (a_1 : t_1 ∈ M.step s a) →
                          (p : M.Path t_1 t x) → motive (a :: x) t s (NFA.Path.cons t_1 s t a x a_1 p)) →
                  motive x t s x_1
-- Mathlib.Analysis.Convex.Strict.Extreme
/-- **Alias** of `StrictConvex.sdiff_interior_subset_extremePoints`. -/
StrictConvex.diff_interior_subset_extremePoints : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid A]
  [inst_3 : Module 𝕜 A] [inst_4 : TopologicalSpace A] {C : Set A},
  StrictConvex 𝕜 C → C \ interior C ⊆ Set.extremePoints 𝕜 C
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The linear equivalence of weight spaces given by an equivalence of root pairings.  -/
RootPairing.Equiv.weightEquiv : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {ι₂ : Type u_5} →
                    {M₂ : Type u_6} →
                      {N₂ : Type u_7} →
                        [inst_5 : AddCommGroup M₂] →
                          [inst_6 : Module R M₂] →
                            [inst_7 : AddCommGroup N₂] →
                              [inst_8 : Module R N₂] →
                                (P : RootPairing ι R M N) → (Q : RootPairing ι₂ R M₂ N₂) → P.Equiv Q → M ≃ₗ[R] M₂
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
/-- Given `c : PullbackCone f g` in the category of types, this is
the canonical map `c.pt → Types.PullbackObj f g`.  -/
CategoryTheory.Limits.PullbackCone.toPullbackObj : {X Y S : Type v} →
  {f : X ⟶ S} →
    {g : Y ⟶ S} → (c : CategoryTheory.Limits.PullbackCone f g) → c.pt → CategoryTheory.Limits.Types.PullbackObj f g
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- To give a morphism in the under category, it suffices to give a morphism fitting in a
commutative triangle.  -/
CategoryTheory.Under.homMk : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} →
      {U V : CategoryTheory.Under X} →
        (f : U.right ⟶ V.right) →
          autoParam (CategoryTheory.CategoryStruct.comp U.hom f = V.hom) CategoryTheory.Under.homMk._auto_1 → (U ⟶ V)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Context.debug : Lean.Meta.Grind.Context → Bool
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.kahler_rightAngleRotation_left : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), (o.kahler (o.rightAngleRotation x)) y = -Complex.I * (o.kahler x) y
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Matrix.transpose_isTotallyUnimodular_iff : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] (A : Matrix m n R),
  A.transpose.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.glueDist_comm : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
  (x y : X ⊕ Y), Metric.glueDist Φ Ψ ε x y = Metric.glueDist Φ Ψ ε y x
-- Init.Data.List.Find
List.findIdx?_flatten : ∀ {α : Type u_1} {l : List (List α)} {p : α → Bool},
  List.findIdx? p l.flatten =
    Option.map
      (fun i => (List.map List.length (List.take i l)).sum + (Option.map (fun xs => List.findIdx p xs) l[i]?).getD 0)
      (List.findIdx? (fun x => x.any p) l)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof : Type
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.HasSupport.eventually_le_support : ∀ {β : Type u_2} {L : SummationFilter β} [self : L.HasSupport], ∀ᶠ (s : Finset β) in L.filter, ↑s ⊆ L.support
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerRight_η_ε : ∀ {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] (T : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.η F) T)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.ε F) T) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) T)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.iCyclesIso_hom_inv_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hj : c.next i = j) (h : K.d i j = 0)
  [inst_2 : K.HasHomology i] {Z : C} (h_1 : K.cycles i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.iCycles i)
      (CategoryTheory.CategoryStruct.comp (K.iCyclesIso i j hj h).inv h_1) =
    h_1
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precomposeId.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C},
  CategoryTheory.Limits.Cocone.precomposeId =
    CategoryTheory.NatIso.ofComponents'
      (fun s =>
        CategoryTheory.Limits.Cocone.extInv
          (CategoryTheory.Iso.refl
            ((CategoryTheory.Limits.Cocone.precompose (CategoryTheory.CategoryStruct.id F)).obj s).pt)
          ⋯)
      ⋯
-- Mathlib.Algebra.GCDMonoid.Basic
NormalizedGCDMonoid.toNormalizationMonoid : {α : Type u_2} → {inst : CommMonoidWithZero α} → [self : NormalizedGCDMonoid α] → NormalizationMonoid α
-- Std.Data.ByteSlice
/-- Folds a monadic operation from right to left over the bytes in a byte slice.

An accumulator of type `β` is constructed by starting with `init` and monadically combining each
byte of the byte slice with the current accumulator value in turn, moving from the end to the
start. The monad in question may permit early termination or repetition.

Examples:
```lean example
#eval (ByteArray.mk #[1, 2, 3]).toByteSlice.foldrM (init := 0) fun x acc =>
  some x.toNat + acc
```
```output
some 6
```
 -/
ByteSlice.foldrM : {β : Type v} → {m : Type v → Type w} → [Monad m] → (UInt8 → β → m β) → β → ByteSlice → m β
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_self_sub_bmod : ∀ {x : ℤ} {m : ℕ}, ↑m ∣ x - x.bmod m
-- Mathlib.Order.Ideal
/-- A non-empty directed union of ideals of sets in a preorder is an ideal.  -/
Order.isIdeal_sUnion_of_directedOn : ∀ {P : Type u_1} [inst : LE P] {C : Set (Set P)},
  (∀ I ∈ C, Order.IsIdeal I) → DirectedOn (fun x1 x2 => x1 ⊆ x2) C → C.Nonempty → Order.IsIdeal (⋃₀ C)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_congr_ae : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f g : α → G}, f =ᵐ[μ] g → ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- Quotients of locally path-connected spaces are locally path-connected.  -/
Quotient.locallyPathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] {s : Setoid X},
  LocallyPathConnectedSpace (Quotient s)
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.pairingIn_mul_eq_pairingIn_mul_swap : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) (i j : ι) [inst_9 : FaithfulSMul S R] [inst_10 : Module S M]
  [inst_11 : IsScalarTower S R M], P.pairingIn S j i * B.rootLength i = P.pairingIn S i j * B.rootLength j
-- Lean.Meta.Closure
Lean.Meta.Closure.MkValueTypeClosureResult.mk : Array Lean.Name →
  Lean.Expr → Lean.Expr → Array Lean.Level → Array Lean.Expr → Lean.Meta.Closure.MkValueTypeClosureResult
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' : α} {fallback : β k'} {f : β k → β k},
      (Std.DTreeMap.Internal.Impl.modify k f t).getD k' fallback =
        if heq : compare k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).getD fallback
        else t.getD k' fallback
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.namespace : Lean.Lsp.SemanticTokenType
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.foldr_eq_foldr_toList : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1 → α_1} {init : α_1} {s : RBTree.RBNode.Stream α},
  RBTree.RBNode.Stream.foldr f s init = List.foldr f init s.toList
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsAddKleinFour.addEquiv.eq_1 : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] [inst_2 : IsAddKleinFour G₁]
  [inst_3 : IsAddKleinFour G₂] (e : G₁ ≃ G₂) (he : e 0 = 0),
  IsAddKleinFour.addEquiv e he = IsAddKleinFour.addEquiv' e he ⋯
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Negating a rotation by π / 2 is equivalent to rotation by -π / 2.  -/
Orientation.neg_rotation_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V), -(o.rotation ↑(Real.pi / 2)) x = (o.rotation ↑(-Real.pi / 2)) x
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
/-- The pre-path object attached to `K : Plus C`.  -/
CochainComplex.Plus.prepathObject : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] → (K : CochainComplex.Plus C) → HomotopicalAlgebra.PrepathObject K
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsAddMonHom.isNormalHom_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H] {φ : H ⟶ G}
  [CategoryTheory.IsAddMonHom φ] [CategoryTheory.Mono φ],
  CategoryTheory.IsAddMonHom.Normal φ ↔
    ∃ ψ,
      CategoryTheory.CategoryStruct.comp ψ φ =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G φ)
          (CategoryTheory.AddGrpObj.addConj G)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingSpanOpEquiv_unitIso_inv_app : ∀ (X : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ),
  CategoryTheory.Limits.walkingSpanOpEquiv.unitIso.inv.app X = CategoryTheory.CategoryStruct.id X
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitDiagInfo.numCases : Lean.Meta.Grind.SplitDiagInfo → ℕ
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.isClassExpensive? : Lean.Expr → Lean.MetaM (Option Lean.Name)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A factorisation of a morphism `f = e ≫ m`, with `m` monic.  -/
CategoryTheory.Limits.MonoFactorisation : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → Type (max u v)
-- Mathlib.MeasureTheory.Measure.Content
/-- If `μ` is a regular content, then the measure induced by `μ` will agree with `μ`
on compact sets.  -/
MeasureTheory.Content.measure_eq_content_of_regular : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : MeasurableSpace G]
  [inst_2 : R1Space G] [inst_3 : BorelSpace G],
  μ.ContentRegular → ∀ (K : TopologicalSpace.Compacts G), μ.measure ↑K = μ K
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
/-- Given locally free data, this is the `QuasiCoherentData` where there are no relations.  -/
SheafOfModules.LocalGeneratorsData.quasiCoherentData : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] →
          [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} → (q : M.LocalGeneratorsData) → [q.IsLocallyFreeData] → M.QuasicoherentData
-- Init.Data.Vector.Find
Vector.findSome?_guard : ∀ {α : Type} {n : ℕ} {p : α → Bool} {xs : Vector α n}, Vector.findSome? (Option.guard p) xs = Vector.find? p xs
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub_nsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIocMod hp a (b - m • p) = toIocMod hp a b
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.preserves_pure : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  (η : ApplicativeTransformation F G) {α : Type u} (x : α), (fun {α} => η.app α) (pure x) = pure x
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.currying_unitIso_inv_app_app_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X_1 : C) (X_2 : D),
  ((CategoryTheory.Functor.currying.unitIso.inv.app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.id ((X.obj X_1).obj X_2)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.inf_ne_bot_of_ne_bot : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {I J : Ideal R} [I.IsTwoSided], I ≠ ⊥ → J ≠ ⊥ → I ⊓ J ≠ ⊥
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.nat : ℕ → Lean.Compiler.LCNF.LitValue
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.toAlgHom_apply : ∀ {R : CommRingCat} {A B : CategoryTheory.Under R} (f : A ⟶ B) (a : ↑A.right),
  (CommRingCat.toAlgHom f) a = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right f)) a
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.isReduced_iff_reduce_eq : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α], FreeAddGroup.IsReduced L ↔ FreeAddGroup.reduce L = L
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.card : ∀ (p n : ℕ) {R : Type u_2} [inst : Fintype R], Fintype.card (TruncatedWittVector p n R) = Fintype.card R ^ n
-- Mathlib.Algebra.Group.Pi.Lemmas
MonoidHom.compLeft_apply : ∀ {α : Type u_5} {β : Type u_6} [inst : MulOneClass α] [inst_1 : MulOneClass β] (f : α →* β) (I : Type u_7) (h : I → α)
  (a : I), (f.compLeft I) h a = (⇑f ∘ h) a
-- Mathlib.Tactic.Widget.StringDiagram
/-- The list of nodes associated with a 2-morphism. The position is counted from the
specified natural numbers.  -/
Mathlib.Tactic.BicategoryLike.WhiskerRight.nodes : ℕ → ℕ → ℕ → Mathlib.Tactic.BicategoryLike.WhiskerRight → List Mathlib.Tactic.Widget.StringDiagram.Node
-- Mathlib.GroupTheory.Subgroup.Center
/-- An additive group is commutative if the center is the whole group.  -/
AddGroup.addCommGroupOfCenterEqTop : {G : Type u_1} → [inst : AddGroup G] → AddSubgroup.center G = ⊤ → AddCommGroup G