mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- The cofan `cofan₃MapBifunctor₁₂BifunctorMapObj` is a colimit, see the induced isomorphism
`mapBifunctorComp₁₂MapObjIso`.  -/
CategoryTheory.GradedObject.isColimitCofan₃MapBifunctor₁₂BifunctorMapObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₁₂ : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] →
                    (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) →
                      (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) →
                        {I₁ : Type u_7} →
                          {I₂ : Type u_8} →
                            {I₃ : Type u_9} →
                              {J : Type u_10} →
                                {r : I₁ × I₂ × I₃ → J} →
                                  (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) →
                                    (X₁ : CategoryTheory.GradedObject I₁ C₁) →
                                      (X₂ : CategoryTheory.GradedObject I₂ C₂) →
                                        (X₃ : CategoryTheory.GradedObject I₃ C₃) →
                                          [inst_5 :
                                              (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj
                                                    X₂).HasMap
                                                ρ₁₂.p] →
                                            [inst_6 :
                                                (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
                                                          (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁
                                                            X₂)).obj
                                                      X₃).HasMap
                                                  ρ₁₂.q] →
                                              [H :
                                                  CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂
                                                    X₃] →
                                                (j : J) →
                                                  CategoryTheory.Limits.IsColimit
                                                    (CategoryTheory.GradedObject.cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂
                                                      G ρ₁₂ X₁ X₂ X₃ j)
-- Mathlib.Algebra.Group.PNatPowAssoc
ppow_mul : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Pow M ℕ+] [PNatPowAssoc M] (x : M) (m n : ℕ+), x ^ (m * n) = (x ^ m) ^ n
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.cast_mulConst_mul_card : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {𝕜 : Type u_3} [inst_2 : Semifield 𝕜] [CharZero 𝕜]
  (A B : Finset G), ↑(A.mulConst B) * ↑A.card = ↑(A * B).card
-- Init.Data.String.Basic
String.Slice.Pos.ofReplaceStart : {s : String.Slice} → {p₀ : s.Pos} → (s.sliceFrom p₀).Pos → s.Pos
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.congr_mul.sizeOf_spec : ∀ {R : Type u} [inst : Rack R] [inst_1 : SizeOf R] {a b a' b' : Rack.PreEnvelGroup R}
  (ha : Rack.PreEnvelGroupRel' R a a') (hb : Rack.PreEnvelGroupRel' R b b'),
  sizeOf (ha.congr_mul hb) = 1 + sizeOf a + sizeOf b + sizeOf a' + sizeOf b' + sizeOf ha + sizeOf hb
-- Init.Grind.Module.Basic
/-- If `k * a ≠ k * b` then `k ≠ 0` or `a ≠ b`. -/
Lean.Grind.NoNatZeroDivisors.no_nat_zero_divisors : ∀ {α : Type u} {inst : Lean.Grind.NatModule α} [self : Lean.Grind.NoNatZeroDivisors α] (k : ℕ) (a b : α),
  k ≠ 0 → k • a = k • b → a = b
-- Mathlib.Order.WithBot
/-- Function that sends an element of `WithBot α` to `α`,
with an arbitrary default value for `⊥`.  -/
WithBot.unbotA : {α : Type u_1} → [Nonempty α] → WithBot α → α
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
/-- The natural representation of the Weyl group on the coroot space.  -/
RootPairing.weylGroupCorootRep : {ι : 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] → (P : RootPairing ι R M N) → Representation R (↥P.weylGroup.op) N
-- Lean.Elab.DeclModifiers
Lean.Elab.instReprComputeKind : Repr Lean.Elab.ComputeKind
-- Mathlib.Data.Set.Constructions
FiniteInter.finiteInterClosure.below : {α : Type u_1} →
  {S : Set (Set α)} →
    {motive : (a : Set α) → FiniteInter.finiteInterClosure S a → Prop} →
      {a : Set α} → FiniteInter.finiteInterClosure S a → Prop
-- Init.Data.Array.Lemmas
Array.getElem_extract_loop_ge : ∀ {α : Type u_1} {i : ℕ} {xs ys : Array α} {size start : ℕ} (hge : i ≥ ys.size)
  (h : i < (Array.extract.loop xs size start ys).size),
  (Array.extract.loop xs size start ys)[i] = xs[start + i - ys.size]
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.triangleOfSESδ.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact),
  DerivedCategory.triangleOfSESδ hS =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.inv (DerivedCategory.Q.map (CochainComplex.mappingCone.descShortComplex S)))
      (CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map (CochainComplex.mappingCone.triangle S.f).mor₃)
        ((CategoryTheory.Functor.commShiftIso DerivedCategory.Q 1).hom.app S.X₁))
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
TopCat.toSSetObj₁Equiv.eq_1 : ∀ {X : TopCat},
  TopCat.toSSetObj₁Equiv =
    (X.toSSetObjEquiv (Opposite.op { len := 1 })).trans
      { toFun := fun f => TopCat.ofHom (f.comp ↑TopCat.stdSimplexHomeomorphI.symm),
        invFun := fun f => (TopCat.Hom.hom f).comp ↑TopCat.stdSimplexHomeomorphI, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.RingTheory.Regular.RegularSequence
/-- Regular sequences can be inductively characterized by:
* The empty sequence is regular on any nonzero module.
* If `r` is regular on `M` and `rs` is a regular sequence on `M⧸rM` then the
  sequence obtained from `rs` by prepending `r` is regular on `M`.

This is the induction principle produced by the inductive definition above.
The motive will usually be valued in `Prop`, but `Sort*` works too.  -/
RingTheory.Sequence.IsRegular.recIterModByRegular : {R : Type u_1} →
  [inst : CommRing R] →
    {motive :
        (M : Type v) →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → (rs : List R) → RingTheory.Sequence.IsRegular M rs → Sort u_7} →
      ((M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → [inst_3 : Nontrivial M] → motive M [] ⋯) →
        ({M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] →
                (r : R) →
                  (rs : List R) →
                    (h1 : IsSMulRegular M r) →
                      (h2 : RingTheory.Sequence.IsRegular (QuotSMulTop r M) rs) →
                        motive (QuotSMulTop r M) rs h2 → motive M (r :: rs) ⋯) →
          {M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] → {rs : List R} → (h : RingTheory.Sequence.IsRegular M rs) → motive M rs h
-- Mathlib.Analysis.InnerProductSpace.Adjoint
isStarProjection_iff_eq_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {p : E →L[𝕜] E},
  IsStarProjection p ↔ ∃ K, ∃ (x : K.HasOrthogonalProjection), p = K.starProjection
-- Mathlib.Analysis.Convex.Deriv
/-- Reformulation of `ConvexOn.le_slope_of_hasDerivAt` using `deriv`  -/
ConvexOn.deriv_le_slope : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  ConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableAt ℝ f x → deriv f x ≤ slope f x y
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryClass.isometry : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂]
  [inst_4 : Module R E] [inst_5 : Module R₂ E₂] [inst_6 : FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕),
  Isometry ⇑f
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α),
  BoundedVariationOn f s = (eVariationOn f s ≠ ⊤)
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  k ∈ Std.HashSet.ofList l ↔ l.contains k = true
-- Lean.Data.JsonRpc
/-- The method does not exist / is not available.  -/
Lean.JsonRpc.ErrorCode.methodNotFound : Lean.JsonRpc.ErrorCode
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List α} {k k' : α},
      cmp k k' = Ordering.eq →
        k ∉ t →
          List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
            k ∈ l → (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).getKey? k' = some k
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_le_of_le_toReal : ∀ {a : ℝ} {b : ENNReal}, a ≤ b.toReal → ENNReal.ofReal a ≤ b
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.restrict_measure_eq : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω),
  ↑(μ.restrict A) = (↑μ).restrict A
-- Init.Data.UInt.Lemmas
UInt8.sub_add_cancel : ∀ (a b : UInt8), a - b + b = a
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.eq_top_of_isIndContained_top : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V}, G.IsIndContained (SimpleGraph.completeGraph W) → G = ⊤
-- Mathlib.Order.OrderIsoNat
Infinite.natEmbedding.congr_simp : ∀ (α : Type u_4) [inst : Infinite α], Infinite.natEmbedding α = Infinite.natEmbedding α
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.ext_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {C₁ C₂ : ConvexCone R M}, C₁ = C₂ ↔ ∀ (x : M), x ∈ C₁ ↔ x ∈ C₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → ∀ {h' : k' ∈ t.insertMany l}, (t.insertMany l).get k' h' = cast ⋯ v
-- Std.Http.Data.Chunk
Std.Http.Chunk.ExtensionValue.mk.inj : ∀ {value : String}
  {isValidExtensionValue :
    autoParam (Std.Http.Chunk.IsValidExtensionValue value)
      Std.Http.Chunk.ExtensionValue.isValidExtensionValue._autoParam}
  {value_1 : String}
  {isValidExtensionValue_1 :
    autoParam (Std.Http.Chunk.IsValidExtensionValue value_1)
      Std.Http.Chunk.ExtensionValue.isValidExtensionValue._autoParam},
  { value := value, isValidExtensionValue := isValidExtensionValue } =
      { value := value_1, isValidExtensionValue := isValidExtensionValue_1 } →
    value = value_1
-- Mathlib.Analysis.InnerProductSpace.PiL2
finrank_euclideanSpace_fin : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {n : ℕ}, Module.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n
-- Mathlib.Data.ENNReal.Basic
ENNReal.none_eq_top : none = ⊤
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_biUnion : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set (Submodule R M)), Submodule.span R (⋃ S ∈ s, ↑S) = sSup s
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.instIsMonHomHomBraiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C] {X Y : C} [inst_3 : CategoryTheory.MonObj X]
  [inst_4 : CategoryTheory.MonObj Y], CategoryTheory.IsMonHom (β_ X Y).hom
-- Mathlib.RingTheory.DedekindDomain.Instances
instFiniteLocalizationAlgebraMapSubmonoidPrimeCompl : ∀ {R : Type u_1} (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] {P : Ideal R} [inst_4 : P.IsPrime] [inst_5 : Algebra S T] [inst_6 : Algebra R T]
  [inst_7 : IsScalarTower R S T] [Module.Finite S T],
  Module.Finite (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
    (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))
-- Std.Internal.UV.UDP
/-- Enables or disables broadcasting on a UDP socket.
 -/
Std.Internal.UV.UDP.Socket.setBroadcast : Std.Internal.UV.UDP.Socket → Bool → IO Unit
-- Mathlib.Order.Antichain
/-- The intersection of an antichain and a chain is subsingleton.  -/
inter_subsingleton_of_isAntichain_of_isChain : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, IsAntichain r s → IsChain r t → (s ∩ t).Subsingleton
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If a `E ⋙ F` has a colimit, and `E` is an equivalence, we can construct a colimit of `F`.
 -/
CategoryTheory.Limits.hasColimit_of_equivalence_comp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} (e : K ≌ J)
  [CategoryTheory.Limits.HasColimit (e.functor.comp F)], CategoryTheory.Limits.HasColimit F
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Function.Injective.mulActionHom_embedding_apply : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : Group H] [inst_3 : MulAction H β] {σ : G → H} {f : α →ₑ[σ] β} {ι : Type u_5} (hf : Function.Injective ⇑f)
  {x : ι ↪ α} {i : ι}, ((Function.Injective.mulActionHom_embedding ι hf) x) i = f (x i)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The tangent of an angle in a right-angled triangle as a ratio of sides.  -/
EuclideanGeometry.tan_oangle_right_of_oangle_eq_pi_div_two : ∀ {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},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → (EuclideanGeometry.oangle p₂ p₃ p₁).tan = dist p₁ p₂ / dist p₃ p₂
-- Mathlib.Probability.Process.Adapted
MeasureTheory.stronglyAdapted_const : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {β : Type u_4} [inst_1 : TopologicalSpace β]
  (f : MeasureTheory.Filtration ι m) (x : β), MeasureTheory.StronglyAdapted f fun x_1 x_2 => x
-- Mathlib.Data.Int.ModEq
Int.modEq_zero_iff : ∀ {a b : ℤ}, a ≡ b [ZMOD 0] ↔ a = b
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
SSet.homologyFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (R : C) [inst_3 : CategoryTheory.CategoryWithHomology C] (n : ℕ) (X : SSet),
  (SSet.homologyFunctor R n).obj X = X.homology R n
-- Mathlib.RingTheory.RingHom.Locally
/-- If `P` is local on the target, then `Locally P` coincides with `P`.  -/
RingHom.locally_iff_of_localizationSpanTarget : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] => P) →
      ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
        RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => P) f ↔ P f
-- Init.Data.Vector.Lemmas
Vector.foldr_eq_foldl_reverse : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → β → β} {b : β},
  Vector.foldr f b xs = Vector.foldl (fun x y => f y x) b xs.reverse
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.instEssSurjLocalizationQ : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C}, W.Q.EssSurj
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.harmonicContOnCl_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {s : Set E} {c : F},
  InnerProductSpace.HarmonicContOnCl (fun x => c) s
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.homOfLE_op_comp_eqToHom : ∀ {X : Type u} [inst : Preorder X] {a b c : X} (hab : b ≤ a) (hbc : Opposite.op b = Opposite.op c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hab).op (CategoryTheory.eqToHom hbc) =
    (CategoryTheory.homOfLE ⋯).op
-- Mathlib.ModelTheory.Order
FirstOrder.Language.noTopOrderSentence.eq_1 : ∀ (L : FirstOrder.Language) [inst : L.IsOrdered],
  L.noTopOrderSentence = (((FirstOrder.Language.var ∘ Sum.inr) 1).le ((FirstOrder.Language.var ∘ Sum.inr) 0)).not.ex.all
-- Mathlib.FieldTheory.Extension
IntermediateField.exists_algHom_of_splits : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K],
  (∀ (s : E), IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) →
    ∀ {L : IntermediateField F E} (f : ↥L →ₐ[F] K), ∃ φ, φ.comp L.val = f
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypePreimage_symm_apply_coe : ∀ {α : Sort u_1} {β : Sort u_4} (p : α → Prop) [inst : DecidablePred p] (x₀ : { a // p a } → β) (x : { a // ¬p a } → β)
  (a : α), ↑((Equiv.subtypePreimage p x₀).symm x) a = if h : p a then x₀ ⟨a, h⟩ else x ⟨a, h⟩
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.ninePointCircle_center_mem_affineSpan : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n),
  s.ninePointCircle.center ∈ affineSpan ℝ (Set.range s.points)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.insertManyIfNew_list_equiv_foldl : ∀ {α : Type u} {β : α → Type v} (m₁ : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {l : List ((a : α) × β a)},
  (↑↑(m₁.insertManyIfNew l)).Equiv (List.foldl (fun acc p => acc.insertIfNew p.fst p.snd) (↑m₁) l)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.MatcherInfo.getNumDiscrEqs : Lean.Meta.MatcherInfo → ℕ
-- Mathlib.Topology.MetricSpace.Basic
MulOpposite.instMetricSpace.eq_1 : ∀ {α : Type u_2} [inst : MetricSpace α], MulOpposite.instMetricSpace = MetricSpace.induced MulOpposite.unop ⋯ inst
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f₁ f₂ : E →L[𝕜] F),
  ContinuousLinearMap.lTensor G (f₁ + f₂) = ContinuousLinearMap.lTensor G f₁ + ContinuousLinearMap.lTensor G f₂
-- Mathlib.Computability.TuringMachine.PostTuringMachine
cond.match_1.congr_eq_1 : ∀ (motive : Bool → Sort u_1) (c : Bool) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  c = true →
    (match c with
      | true => h_1 ()
      | false => h_2 ()) ≍
      h_1 ()
-- Mathlib.Data.FP.Basic
FP.Float.div : [C : FP.FloatCfg] → FP.RMode → FP.Float → FP.Float → FP.Float
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.toList_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} [LawfulMonad m] {xs : Vector β n},
  (xs.iterM m).toList = pure xs.toList
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquivClass.toAlgEquivClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : Semiring A} {inst_2 : TopologicalSpace A} {inst_3 : Semiring B} {inst_4 : TopologicalSpace B}
  {inst_5 : Algebra R A} {inst_6 : Algebra R B} {inst_7 : EquivLike F A B} [self : ContinuousAlgEquivClass F R A B],
  AlgEquivClass F R A B
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionList.isIncomplete : Lean.Lsp.CompletionList → Bool
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_iSup_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {ι : Type u_5} {f : M →ₙ* N},
  Function.Injective ⇑f → ∀ (S : ι → Subsemigroup M), Subsemigroup.comap f (⨆ i, Subsemigroup.map f (S i)) = iSup S
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The functor `ComposableArrows C n ⥤ ComposableArrows D n` induced by `G : C ⥤ D`
commutes with `opEquivalence`.  -/
CategoryTheory.Functor.mapComposableArrowsOpIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (G : CategoryTheory.Functor C D) →
          (n : ℕ) →
            (G.mapComposableArrows n).comp (CategoryTheory.ComposableArrows.opEquivalence D n).functor.rightOp ≅
              (CategoryTheory.ComposableArrows.opEquivalence C n).functor.rightOp.comp (G.op.mapComposableArrows n).op
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instCommRing : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] →
      [inst_1 : PartialOrder S] → [inst_2 : CommRing R] → (v : AbsoluteValue R S) → CommRing (WithAbs v)
-- Aesop.Rule.Forward
/-- The rule's name. Should be unique among all rules in a rule set.  -/
Aesop.ForwardRule.name : Aesop.ForwardRule → Aesop.RuleName
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.comp_null : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel β γ} {s : Set γ} (a : α),
  MeasurableSet s → (((η.comp κ) a) s = 0 ↔ (fun y => (η y) s) =ᵐ[κ a] 0)
-- Mathlib.Topology.MetricSpace.Gluing
Metric.le_glueDist_inl_inr : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
  (x : X) (y : Y), ε ≤ Metric.glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y)
-- Mathlib.Data.Nat.PrimeFin
Nat.primeFactors.eq_1 : ∀ (n : ℕ), n.primeFactors = n.primeFactorsList.toFinset
-- Mathlib.FieldTheory.RatFunc.Basic
/-- `FractionRing.isScalarTower_liftAlgebra` specialized to `R⟮X⟯`.  -/
RatFunc.isScalarTower_liftAlgebra : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : Field L] [inst_2 : IsDomain R]
  [inst_3 : Algebra (Polynomial R) L] [inst_4 : FaithfulSMul (Polynomial R) L],
  IsScalarTower (Polynomial R) (RatFunc R) L
-- Mathlib.Analysis.Convex.Side
AffineEquiv.wOppSide_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : CommRing R]
  [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V]
  [inst_5 : AddTorsor V P] [inst_6 : AddCommGroup V'] [inst_7 : Module R V'] [inst_8 : AddTorsor V' P']
  {s : AffineSubspace R P} {x y : P} (f : P ≃ᵃ[R] P'), (AffineSubspace.map (↑f) s).WOppSide (f x) (f y) ↔ s.WOppSide x y
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
/-- The proposed colimit cocone is a colimit in `ModuleCat R`.  -/
ModuleCat.FilteredColimits.colimitCoconeIsColimit : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [inst_2 : CategoryTheory.IsFiltered J] →
          (F : CategoryTheory.Functor J (ModuleCat R)) →
            CategoryTheory.Limits.IsColimit (ModuleCat.FilteredColimits.colimitCocone F)