mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.TensorBimod.middle_assoc' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T)
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (Bimod.TensorBimod.actLeft P Q) T.X)
      (Bimod.TensorBimod.actRight P Q) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator R.X (Bimod.TensorBimod.X P Q) T.X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (Bimod.TensorBimod.actRight P Q))
        (Bimod.TensorBimod.actLeft P Q))
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.of_subsingleton : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] [MeasurableSingletonClass α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {s : Set α},
  s.Subsingleton → ∀ {f : α → E}, MeasureTheory.IntegrableOn f s μ
-- Mathlib.Data.Int.Interval
Int.card_fintype_Icc_of_le : ∀ (a b : ℤ), a ≤ b + 1 → ↑(Fintype.card ↑(Set.Icc a b)) = b + 1 - a
-- Mathlib.Algebra.Group.Finsupp
Finsupp.support_add_single : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] {a : ι} {b : M} {f : ι →₀ M} (ha : a ∉ f.support),
  b ≠ 0 → (f + fun₀ | a => b).support = Finset.cons a f.support ha
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.ncard_sdiff'`.

---

This is the same as `ncard_sdiff` but we require `t` to be finite instead.  -/
Set.ncard_diff' : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → autoParam t.Finite Set.ncard_sdiff'._auto_1 → (t \ s).ncard = t.ncard - s.ncard
-- Mathlib.Algebra.Group.Units.Hom
Units.liftRight_inv_mul : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] {f : M →* N} {g : M → Nˣ}
  (h : ∀ (x : M), ↑(g x) = f x) (x : M), ↑((Units.liftRight f g h) x)⁻¹ * f x = 1
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.ofIso_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : CategoryTheory.SimplicialObject C}
  (s : X.Splitting) (e : X ≅ Y) (n : ℕ),
  (s.ofIso e).ι n = CategoryTheory.CategoryStruct.comp (s.ι n) (e.hom.app (Opposite.op { len := n }))
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanSingleton_mul_le_iff : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] {x : P} {I J : FractionalIdeal S P},
  FractionalIdeal.spanSingleton S x * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J
-- Mathlib.SetTheory.Cardinal.Defs
/-- **Alias** of `Cardinal.mk_congr`. -/
Equiv.cardinal_eq : ∀ {α β : Type u} (e : α ≃ β), Cardinal.mk α = Cardinal.mk β
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.atBot_basis_Iio : ∀ {α : Type u_3} [inst : Preorder α] [IsCodirectedOrder α] [Nonempty α] [NoMinOrder α],
  Filter.atBot.HasBasis (fun x => True) Set.Iio
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.instInhabitedFormatError : Inhabited Mathlib.Linter.FormatError✝
-- Lean.Server.Requests
Lean.Server.RequestM.runCommandElabM : {α : Type} →
  Lean.Server.Snapshots.Snapshot → Lean.Server.RequestT Lean.Elab.Command.CommandElabM α → Lean.Server.RequestM α
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableAt.comp_mdifferentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {s : Set M} {g : M' → M''}, MDiffAt g (f x) → MDiffAt[s] f x → MDiffAt[s] (g ∘ f) x
-- Lean.Meta.Tactic.Util
/-- Beta reduce the metavariable type head  -/
Lean.MVarId.headBetaType : Lean.MVarId → Lean.MetaM Unit
-- Mathlib.Algebra.Group.Equiv.Basic
/-- A multiplicative analogue of `Equiv.arrowCongr`,
where the equivalence between the targets is multiplicative.
 -/
MulEquiv.arrowCongr : {M : Type u_16} →
  {N : Type u_17} →
    {P : Type u_18} → {Q : Type u_19} → [inst : Mul P] → [inst_1 : Mul Q] → M ≃ N → P ≃* Q → (M → P) ≃* (N → Q)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.coe_rangeSRestrict : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (x : R),
  ↑(f.rangeSRestrict x) = f x
-- Mathlib.Data.Seq.Defs
Stream'.Seq.mem_cons : ∀ {α : Type u} (a : α) (s : Stream'.Seq α), a ∈ Stream'.Seq.cons a s
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_sdiff₀ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasureTheory.NullMeasurableSet t μ →
    MeasureTheory.IntegrableOn f s μ →
      t ⊆ s → ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ - ∫ (x : X) in t, f x ∂μ
-- Init.Data.Array.Nat
Array.sum_eq_zero_iff_forall_eq_nat : ∀ {xs : Array ℕ}, xs.sum = 0 ↔ ∀ x ∈ xs, x = 0
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
/-- The quadratic version of `LinearMap.sum_repr_mul_repr_mul`.  -/
QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : DecidableEq ι]
  (Q : QuadraticMap R M N) (bm : Module.Basis ι R M) (x : M),
  (Finsupp.linearCombination R (⇑Q ∘ ⇑bm)) (bm.repr x * bm.repr x) +
      ∑ p ∈ (bm.repr x).support.sym2 with ¬p.IsDiag,
        (Sym2.map (⇑(bm.repr x)) p).mul • QuadraticMap.polarSym2 (⇑Q) (Sym2.map (⇑bm) p) =
    Q x
-- Init.Data.Vector.Lemmas
Vector.set_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n) {i : ℕ} {x : α} (w : i < n),
  (Vector.mk xs h).set i x w = Vector.mk (xs.set i x ⋯) ⋯
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_pow : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [inst : Pow G M] (f : α → G) (n : M), ↑(f ^ n) = ↑f ^ n
-- Mathlib.Analysis.RCLike.Basic
RCLike.inv_im : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.im z⁻¹ = -RCLike.im z / RCLike.normSq z
-- Init.Data.Array.MinMax
Array.isSome_max?_of_mem : ∀ {α : Type u_1} {xs : Array α} [inst : Max α] {a : α}, a ∈ xs → xs.max?.isSome = true
-- Mathlib.Algebra.Star.Basic
IsUnit.star : ∀ {R : Type u} [inst : Monoid R] [inst_1 : StarMul R] {a : R}, IsUnit a → IsUnit (star a)
-- Mathlib.Order.Filter.Pointwise
Filter.bot_pow : ∀ {α : Type u_2} [inst : Monoid α] {n : ℕ}, n ≠ 0 → ⊥ ^ n = ⊥
-- Mathlib.Data.Set.Lattice.Image
Set.image2_sInter_right_subset : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Set α) (S : Set (Set β)) (f : α → β → γ),
  Set.image2 f t (⋂₀ S) ⊆ ⋂ s ∈ S, Set.image2 f t s
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.mem_sdiff_singleton_empty`. -/
Set.mem_diff_singleton_empty : ∀ {α : Type u_1} {s : Set α} {t : Set (Set α)}, s ∈ t \ {∅} ↔ s ∈ t ∧ s.Nonempty
-- Std.Http.Test.Helpers
/-- Assert `needle` does NOT appear in the response.
 -/
Std.Http.Internal.Test.assertAbsent : ByteArray → String → IO Unit
-- Init.Data.Array.Lemmas
List.mapM_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m β} {l : List α},
  Array.mapM f l.toArray = List.toArray <$> List.mapM f l
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.isOpenEmbedding' : ∀ {α : Type u_2} [inst : TopologicalSpace α] (U : TopologicalSpace.Opens α), Topology.IsOpenEmbedding Subtype.val
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.toList.eq_1 : ∀ {V : Type u} [inst : Quiver V] {a : V}, Quiver.Path.nil.toList = []
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.isEncodedQueryChar_isAscii : ∀ {r : UInt8 → Bool} (c : UInt8),
  Std.Http.URI.isEncodedQueryChar r c = true → Std.Http.Internal.Char.isAsciiByte c = true
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
opposite side.  -/
InnerProductGeometry.sin_angle_add_mul_norm_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → Real.sin (InnerProductGeometry.angle x (x + y)) * ‖x + y‖ = ‖y‖
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.nonempty : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α}, l.HasBasis p s → Nonempty ι
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp],
  t.isEmpty = false → ∀ {km fallback : α}, t.maxKeyD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Topology.Order.Compact
/-- A closed interval in a conditionally complete linear order is compact.  -/
ConditionallyCompleteLinearOrder.toCompactIccSpace : ∀ (α : Type u_2) [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α],
  CompactIccSpace α
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- Let `{x | p x}` be a subsemigroup of a commutative additive monoid `M`. Let `f : M → N` be a map
such that `f 0 = 0` and `f` is subadditive on `{x | p x}`, i.e. `p x → p y → f (x + y) ≤ f x + f y`.
Let `g i`, `i ∈ s`, be a finite family of elements of `M` such that `∀ i ∈ s, p (g i)`. Then
`f (∑ x ∈ s, g x) ≤ ∑ x ∈ s, f (g x)`.  -/
Finset.le_sum_of_subadditive_on_pred : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [inst_2 : Preorder N]
  [IsOrderedAddMonoid N] (f : M → N) (p : M → Prop),
  f 0 ≤ 0 →
    (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) →
      (∀ (x y : M), p x → p y → p (x + y)) →
        ∀ (g : ι → M) {s : Finset ι}, (∀ i ∈ s, p (g i)) → f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instSemiringQuotient : {R : Type u_1} → [inst : Semiring R] → (c : RingCon R) → Semiring c.Quotient
-- Mathlib.Order.RelClasses
/-- Construct a decidable linear order from a well-founded linear order.  -/
IsWellOrder.linearOrder : {α : Type u} → (r : α → α → Prop) → [IsWellOrder α r] → LinearOrder α
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_mem : ∀ {α : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s : Set α),
  ⊤ ∈ s → (∀ x ∈ s, ∀ y ∈ s, x ⊓ y ∈ s) → ∀ {ι : Type u_7} (t : Finset ι) (p : ι → α), (∀ i ∈ t, p i ∈ s) → t.inf p ∈ s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, t.isEmpty = true → ∀ {fallback : α}, (t.insertIfNew k v).minKeyD fallback = k
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.aut_inv : ∀ {S : Type u_1} {R : Type u_2} [inst : Mul R] [inst_1 : Add R] [inst_2 : Star R] [inst_3 : SMul S R] (f : R ≃⋆ₐ[S] R),
  f⁻¹ = f.symm
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.length_toList_rcc : ∀ {a b : ℕ}, (a...=b).toList.length = b + 1 - a
-- Mathlib.Data.List.Sym
List.mk_mem_sym2_iff : ∀ {α : Type u_1} {xs : List α} {a b : α}, s(a, b) ∈ xs.sym2 ↔ a ∈ xs ∧ b ∈ xs
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeries.StrictMonoOn : ∀ (G : Type u_1) [inst : Group G], StrictMonoOn (Subgroup.upperCentralSeries G) (Set.Iic (Group.nilpotencyClass G))
-- Mathlib.Data.TypeVec
TypeVec.toSubtype'.eq_1 : ∀ (n_2 : ℕ) (α_2 : TypeVec.{u} (n_2 + 1)) (p_2 : (α_2.prod α_2).Arrow (TypeVec.repeat (n_2 + 1) Prop)) (i : Fin2 n_2)
  (x_2 : { x // TypeVec.ofRepeat (p_2 i.fs (TypeVec.prod.mk i.fs x.1 x.2)) }),
  TypeVec.toSubtype' p_2 i.fs x_2 = TypeVec.toSubtype' (TypeVec.dropFun p_2) i x_2
-- Mathlib.Data.PFun
PFun.dom_eq : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β), f.Dom = {x | ∃ y, y ∈ f x}
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.SizedBalancedTree.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} {lb ub : ℕ} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)]
  (impl : Std.DTreeMap.Internal.Impl α β) (balanced_impl : impl.Balanced) (lb_le_size_impl : lb ≤ impl.size)
  (size_impl_le_ub : impl.size ≤ ub),
  sizeOf
      { impl := impl, balanced_impl := balanced_impl, lb_le_size_impl := lb_le_size_impl,
        size_impl_le_ub := size_impl_le_ub } =
    1 + sizeOf impl + sizeOf balanced_impl + sizeOf lb_le_size_impl + sizeOf size_impl_le_ub
-- Mathlib.Tactic.Bound
Mathlib.Tactic.Bound.min_le_of_left_le_or_right_le : ∀ {α : Type} [inst : LinearOrder α] {a b c : α}, a ≤ c ∨ b ≤ c → min a b ≤ c
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The essential image of `Under.post F` where `F` is full is the same as the essential image of
`F`.  -/
CategoryTheory.Functor.essImage_underPost : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {F : CategoryTheory.Functor T D} [F.Full] {Y : CategoryTheory.Under (F.obj X)},
  (CategoryTheory.Under.post F).essImage Y ↔ F.essImage Y.right
-- Mathlib.Data.Finsupp.Basic
Finsupp.extendDomain_support : ∀ {α : Type u_1} {M : Type u_12} [inst : Zero M] {P : α → Prop} [inst_1 : DecidablePred P] (f : Subtype P →₀ M),
  f.extendDomain.support = Finset.map (Function.Embedding.subtype P) f.support
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₈_of_isShortNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF], W.b₈ = -W.a₄ ^ 2
-- Std.Internal.Do.WP.Basic
/-- `StateT` lifts a `WPMonad` instance by adding a state argument.  -/
Std.Internal.Do.StateT.instWPMonad : {m : Type u → Type z} →
  {EPred : Type v} →
    {σ : Type u} →
      {Pred : Type w} →
        [inst : Monad m] →
          [inst_1 : Std.Internal.Do.Assertion Pred] →
            [inst_2 : Std.Internal.Do.Assertion EPred] →
              [Std.Internal.Do.WPMonad m Pred EPred] → Std.Internal.Do.WPMonad (StateT σ m) (σ → Pred) EPred
-- Mathlib.Order.Heyting.Basic
inf_sdiff_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b ⊓ a = a \ b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
/-- For 0 ≤ x we have x - x ^ 3 / 6 ≤ sin x.

This inequality is tight, in that the constant 6 is best possible.  -/
Real.sin_ge_sub_cube : ∀ {x : ℝ}, 0 ≤ x → x - x ^ 3 / 6 ≤ Real.sin x
-- Mathlib.Topology.Category.LightProfinite.Basic
instFaithfulLightDiagram'LightDiagramToLightFunctor : LightDiagram'.toLightFunctor.Faithful
-- Mathlib.Algebra.Group.Nat.Even
Nat.even_sub : ∀ {m n : ℕ}, n ≤ m → (Even (m - n) ↔ (Even m ↔ Even n))
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- The bicone constructed in `binaryBiconeOfSplitMonoOfCokernel` is a bilimit.
This is a version of the splitting lemma that holds in all preadditive categories.  -/
CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitMonoOfCokernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          [inst_2 : CategoryTheory.IsSplitMono f] →
            {c : CategoryTheory.Limits.CokernelCofork f} →
              (i : CategoryTheory.Limits.IsColimit c) →
                (CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).IsBilimit
-- Mathlib.Algebra.Category.Ring.Colimits
Quotient.map₂.congr_simp : ∀ {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} {γ : Sort u_4} {sc : Setoid γ} (f f_1 : α → β → γ)
  (e_f : f = f_1) (h : ∀ ⦃a₁ a₂ : α⦄, a₁ ≈ a₂ → ∀ ⦃b₁ b₂ : β⦄, b₁ ≈ b₂ → f a₁ b₁ ≈ f a₂ b₂) (a a_1 : Quotient sa),
  a = a_1 → ∀ (a_2 a_3 : Quotient sb), a_2 = a_3 → Quotient.map₂ f h a a_2 = Quotient.map₂ f_1 ⋯ a_1 a_3
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker_inv_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c)
  [inst_2 : CategoryTheory.Bicategory.LanLift.CommuteWith f g h],
  CategoryTheory.StructuredArrow.Hom.right
      (CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker f g h).inv =
    (CategoryTheory.Bicategory.LanLift.CommuteWith.isKan f g h).desc
      (CategoryTheory.Bicategory.lanLiftLeftLift f (CategoryTheory.CategoryStruct.comp h g))
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalDataValueExpr : Lean.Expr → Lean.MetaM Lean.DataValue
-- Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
MeasureTheory.instIsZeroOrProbabilityMeasure : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsZeroOneMeasure μ],
  MeasureTheory.IsZeroOrProbabilityMeasure μ
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.versoModuleDocExt : Lean.SimplePersistentEnvExtension Lean.VersoModuleDocs.Snippet Lean.VersoModuleDocs
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get!_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], k ∉ m₂ → (m₁ ∪ m₂).get! k = m₁.get! k
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanCompIso_inv_app_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  (CategoryTheory.Limits.spanCompIso F f g).inv.app CategoryTheory.Limits.WalkingSpan.zero =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.span (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingSpan.zero)
-- Mathlib.Order.Atoms
GaloisInsertion.isAtom_of_u_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α]
  [inst_3 : OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u), u ⊥ = ⊥ → ∀ {b : β}, IsAtom (u b) → IsAtom b
-- Mathlib.Algebra.Group.Defs
nsmul_eq_smul : ∀ {M : Type u_2} [inst : AddMonoid M] (n : ℕ) (x : M), NSMul.nsmul n x = n • x
-- Aesop.Index.Basic
Aesop.IndexingMode.brecOn_1.eq : ∀ {motive_1 : Aesop.IndexingMode → Sort u} {motive_2 : Array Aesop.IndexingMode → Sort u}
  {motive_3 : List Aesop.IndexingMode → Sort u} (t : Array Aesop.IndexingMode)
  (F_1 : (t : Aesop.IndexingMode) → t.below → motive_1 t)
  (F_2 : (t : Array Aesop.IndexingMode) → Aesop.IndexingMode.below_1 t → motive_2 t)
  (F_3 : (t : List Aesop.IndexingMode) → Aesop.IndexingMode.below_2 t → motive_3 t),
  Aesop.IndexingMode.brecOn_1 t F_1 F_2 F_3 = F_2 t (Aesop.IndexingMode.brecOn_1.go t F_1 F_2 F_3).2
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Twice the angle between a vector and its negation is 0.  -/
Orientation.two_zsmul_oangle_neg_self_right : ∀ {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), 2 • o.oangle x (-x) = 0
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerRight_whiskerLeft_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} (D : Type u_4) [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (F : CategoryTheory.Functor A B) {G H : CategoryTheory.Functor B C}
  (η : G ⟶ H) {Z : CategoryTheory.Functor (CategoryTheory.Join A D) (CategoryTheory.Join C D)}
  (h : CategoryTheory.Join.mapPair (F.comp H) (CategoryTheory.Functor.id D) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Join.mapWhiskerRight (F.whiskerLeft η) (CategoryTheory.Functor.id D)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompLeft D F G).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Join.mapPair F (CategoryTheory.Functor.id D)).whiskerLeft
          (CategoryTheory.Join.mapWhiskerRight η (CategoryTheory.Functor.id D)))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompLeft D F H).inv h))
-- Mathlib.Algebra.Category.Semigrp.Basic
CategoryTheory.Iso.magmaCatIsoToMulEquiv.eq_1 : ∀ {X Y : MagmaCat} (i : X ≅ Y),
  i.magmaCatIsoToMulEquiv = (MagmaCat.Hom.hom i.hom).toMulEquiv (MagmaCat.Hom.hom i.inv) ⋯ ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_eq_some_get! : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} [inst_3 : Inhabited (β a)], a ∈ m → m.get? a = some (m.get! a)
-- Mathlib.Order.Monotone.Basic
StrictAnti.compares : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictAnti f → ∀ {a b : α} {o : Ordering}, o.Compares (f a) (f b) ↔ o.Compares b a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_nsmul_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s : Finset α} {n : ℕ}, (n • s).card ≤ s.card ^ n
-- Mathlib.Order.Atoms
IsSimpleOrder.lt_top_iff_eq_bot : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [IsSimpleOrder α] {a : α}, a < ⊤ ↔ a = ⊥
-- Mathlib.Algebra.Module.Injective
Module.Baer.supExtensionOfMaxSingleton : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      (i : M →ₗ[R] N) → (M →ₗ[R] Q) → [Fact (Function.Injective ⇑i)] → N → Submodule R N
-- Mathlib.Tactic.Linter.TextBased
/-- Lint a collection of input strings if one of them contains trailing whitespace.  -/
Mathlib.Linter.TextBased.linter.trailingWhitespace : Lean.Option Bool