mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ)
  {a b : B} {a' : C} (f : a ⟶ b) (g : G.obj b ⟶ a') {Z : F.obj a ⟶ a'}
  (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (θ.app a) (G.map f)) g ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (F.map f) (CategoryTheory.Bicategory.whiskerRight (Γ.app b) g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (θ.app b) g).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (θ.naturality f).hom g) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (η.app b) g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom g)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (Γ.app a) (G.map f)) g) h))
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.IsInitial.eq_1 : ∀ (o : Ordinal.{u_1}), o.IsInitial = (o.card.ord = o)
-- Mathlib.AlgebraicGeometry.Morphisms.IsIso
AlgebraicGeometry.isomorphisms_eq_isOpenImmersion_inf_surjective : CategoryTheory.MorphismProperty.isomorphisms AlgebraicGeometry.Scheme =
  AlgebraicGeometry.IsOpenImmersion ⊓ @AlgebraicGeometry.Surjective
-- Mathlib.Geometry.Manifold.Instances.Real
IccRightChart_extend_top : ∀ {x y : ℝ} [hxy : Fact (x < y)], ↑((IccRightChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) ⊤ = 0
-- Mathlib.Analysis.SpecialFunctions.Stirling
Stirling.stirlingSeq.eq_1 : ∀ (n : ℕ), Stirling.stirlingSeq n = ↑n.factorial / (√(2 * ↑n) * (↑n / Real.exp 1) ^ n)
-- Lean.Elab.PreDefinition.PartialFixpoint.Induction
/-- Returns true if `name` defined by `partial_fixpoint`, the first in its mutual group,
and all functions are defined using the `CCPO` instance for `Option`.
 -/
_private.Lean.Elab.PreDefinition.PartialFixpoint.Induction.0.Lean.Elab.PartialFixpoint.isOptionFixpoint : Lean.Environment → Lean.Name → Bool
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The `0` power series is the unique power series with infinite order.  -/
MvPowerSeries.weightedOrder_eq_top_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R},
  MvPowerSeries.weightedOrder w f = ⊤ ↔ f = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.maxEntry!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)], t₁.Equiv t₂ → t₁.maxEntry! = t₂.maxEntry!
-- Mathlib.Analysis.Normed.Field.Lemmas
DilationEquiv.mulRight_symm_apply : ∀ {α : Type u_1} [inst : NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α),
  (DilationEquiv.mulRight a ha).symm x = x * a⁻¹
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.nil_nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.Nil
-- Mathlib.Order.Defs.PartialOrder
/-- The relation `≤` on a preorder is reflexive.  -/
le_refl : ∀ {α : Type u_1} [inst : Preorder α] (a : α), a ≤ a
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.extract.match_1.splitter : (motive : Substring.Raw → String.Pos.Raw → String.Pos.Raw → Sort u_1) →
  (x : Substring.Raw) →
    (x_1 x_2 : String.Pos.Raw) →
      ((s : String) → (b e b' e' : String.Pos.Raw) → motive { str := s, startPos := b, stopPos := e } b' e') →
        motive x x_1 x_2
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ₀Iter.congr_simp : ∀ (i i_1 : ℕ) (e_i : i = i_1) {n m : ℕ} (hi : n + i = m), SimplexCategory.σ₀Iter i hi = SimplexCategory.σ₀Iter i_1 ⋯
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_le_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {k km : α}
  (hc : k ∈ t), t.min?.get ⋯ = km → (cmp km k).isLE = true
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.instQuotientIdealAlgebraMapSubmonoidMapRingHomAlgebraMap : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S] (I : Ideal R),
  IsLocalization (Algebra.algebraMapSubmonoid (R ⧸ I) M) (S ⧸ Ideal.map (algebraMap R S) I)
-- Mathlib.RingTheory.Ideal.Defs
Ideal.pow_mem_of_mem : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α) {a : α}, a ∈ I → ∀ (n : ℕ), 0 < n → a ^ n ∈ I
-- Mathlib.Data.Finset.Max
Finset.toDual_min' : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} (hs : s.Nonempty),
  OrderDual.toDual (s.min' hs) = (Finset.image (⇑OrderDual.toDual) s).max' ⋯
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressBegin.mk.injEq : ∀ (toWorkDoneProgressReport : Lean.Lsp.WorkDoneProgressReport) (title : String)
  (toWorkDoneProgressReport_1 : Lean.Lsp.WorkDoneProgressReport) (title_1 : String),
  ({ toWorkDoneProgressReport := toWorkDoneProgressReport, title := title } =
      { toWorkDoneProgressReport := toWorkDoneProgressReport_1, title := title_1 }) =
    (toWorkDoneProgressReport = toWorkDoneProgressReport_1 ∧ title = title_1)
-- Mathlib.Analysis.Normed.Group.Constructions
pi_norm_const_le : ∀ {ι : Type u_1} {E : Type u_2} [inst : Fintype ι] [inst_1 : SeminormedAddGroup E] (a : E), ‖fun x => a‖ ≤ ‖a‖
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobject_arrow'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
/-- Predicate on the triangle indices for the explicit triangles to be edge-disjoint.  -/
SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → Finset (α × β × γ) → Prop
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Unitization.concaveOn_of_concaveOn_inr_comp : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {f : A → A} {s : Set A},
  (∀ (x : A), IsSelfAdjoint (f x)) → ConcaveOn ℝ s (Unitization.inr ∘ f) → ConcaveOn ℝ s f
-- Mathlib.Algebra.Group.Prod
Prod.instSubtractionMonoid.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : SubtractionMonoid G] [inst_1 : SubtractionMonoid H],
  Prod.instSubtractionMonoid =
    { toSubNegMonoid := Prod.subNegMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.generator_mem_range : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] (K : Type u_3) [inst_1 : Field K] (w : Valuation K Γ)
  [inst_2 : w.IsRankOneDiscrete], ↑(Valuation.IsRankOneDiscrete.generator w) ∈ Set.range ⇑w
-- Mathlib.ModelTheory.Definability
Set.termDefinable₁_iff_exists_term : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {f : M → M},
  Set.TermDefinable₁ L f ↔ ∃ φ, f = (fun v => FirstOrder.Language.Term.realize v φ) ∘ Function.const Unit
-- Mathlib.Data.Int.GCD
/-- The extended GCD `a` value in the equation `gcd x y = x * a + y * b`.  -/
Int.gcdA : ℤ → ℤ → ℤ
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.isEmpty : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → Bool
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_self : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a : α}, Finset.uIcc a a = {a}
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.lift_tmul : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] (f : M →ₗ[A] N →ₗ[R] P) (x : M) (y : N),
  (TensorProduct.AlgebraTensorModule.lift f) (x ⊗ₜ[R] y) = (f x) y
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_leadingCoeff_sum_eq : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {D : A → B} {ι : Type u_7} {s : Finset ι} {i : ι} {f : ι → AddMonoidAlgebra R A} [inst_3 : AddZeroClass A],
  i ∈ s →
    (∀ j ∈ s, j ≠ i → AddMonoidAlgebra.supDegree D (f j) < AddMonoidAlgebra.supDegree D (f i)) →
      AddMonoidAlgebra.supDegree D (∑ j ∈ s, f j) = AddMonoidAlgebra.supDegree D (f i) ∧
        AddMonoidAlgebra.leadingCoeff D (∑ j ∈ s, f j) = AddMonoidAlgebra.leadingCoeff D (f i)
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.aemeasurable : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : TopologicalSpace E]
  [inst_1 : AddCommMonoid E] [inst_2 : Module ℝ E] [mE : MeasurableSpace E] {X : Ω → E},
  ProbabilityTheory.HasGaussianLaw X P → AEMeasurable X P
-- Mathlib.Algebra.Group.Action.Basic
/-- `MulAction.toPerm` is injective on faithful actions.  -/
MulAction.toPerm_injective : ∀ {α : Type u_5} {β : Type u_6} [inst : Group α] [inst_1 : MulAction α β] [FaithfulSMul α β],
  Function.Injective MulAction.toPerm
-- Mathlib.Data.PFunctor.Multivariate.M
TypeVec.splitFun.eq_1 : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : α.drop.Arrow α'.drop) (g : α.last → α'.last)
  (i : Fin2 n), TypeVec.splitFun f g i.fs = f i
-- Init.Data.UInt.Lemmas
UInt64.neg_sub : ∀ {a b : UInt64}, -(a - b) = b - a
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.checkSplitStatus : Lean.Meta.Grind.SplitInfo → Lean.Meta.Grind.GoalM Lean.Meta.Grind.SplitStatus
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyLT!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.Equiv t₂ → t₁.getKeyLT! k = t₂.getKeyLT! k
-- Init.Data.String.Substring
Substring.Raw.Internal.isEmptyImpl : Substring.Raw → Bool
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.lineDerivOpCLM_apply : ∀ {R : Type u_4} {V : Type u_5} {E : Type u_6} {F : Type u_7} [inst : Ring R] [inst_1 : AddCommGroup E]
  [inst_2 : Module R E] [inst_3 : AddCommGroup F] [inst_4 : Module R F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] [inst_7 : AddCommGroup V] [inst_8 : LineDeriv V E F] [inst_9 : LineDerivAdd V E F]
  [inst_10 : LineDerivSMul R V E F] [inst_11 : ContinuousLineDeriv V E F] (m : V) (x : E),
  (LineDeriv.lineDerivOpCLM R E m) x = LineDeriv.lineDerivOp m x
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_eval_neg : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ) (x : R),
  Polynomial.eval (-x) (Polynomial.Chebyshev.U R ↑n) =
    ↑↑(↑n).negOnePow * Polynomial.eval x (Polynomial.Chebyshev.U R ↑n)
-- Init.Data.Vector.MapIdx
Vector.exists_of_mem_mapIdx : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {f : ℕ → α → β} {b : β} {xs : Vector α n},
  b ∈ Vector.mapIdx f xs → ∃ i, ∃ (h : i < n), f i xs[i] = b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_insertMany_empty_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] {l : List (α × β)},
  List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
    (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)).size = l.length
-- Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
SimpleGraph.binomialRandom_apply : ∀ {V : Type u_1} (p : ↑unitInterval) [Countable V] (S : Set (SimpleGraph V)),
  (SimpleGraph.binomialRandom V p) S =
    (MeasureTheory.Measure.infinitePi fun e =>
        (unitInterval.toNNReal p • MeasureTheory.Measure.dirac ¬e.IsDiag) +
          unitInterval.toNNReal (unitInterval.symm p) • MeasureTheory.Measure.dirac False)
      ((fun G e => e ∈ G.edgeSet) '' S)
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- The colimit cokernel cofork of `(K.extend e).d i' j'` that is deduced from a
colimit cokernel cofork of `K.d i j`.  -/
HomologicalComplex.extend.rightHomologyData.isColimitCokernelCofork : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {i j : ι} →
                      {i' j' : ι'} →
                        (hj' : e.f j = j') →
                          (hi : c.prev j = i) →
                            (hi' : c'.prev j' = i') →
                              (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)) →
                                CategoryTheory.Limits.IsColimit cocone →
                                  CategoryTheory.Limits.IsColimit
                                    (HomologicalComplex.extend.rightHomologyData.cokernelCofork K e hj' hi hi' cocone)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- The tangent space at a point of the manifold `M`. It is just `E`. We could use instead
`(tangentBundleCore I M).toFiberBundleCore.fiber x`, but we use `E` to help the kernel.

The definition of `TangentSpace` is not reducible so that type class inference
does not pick wrong instances.
 -/
TangentSpace : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_2} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H → {M : Type u_3} → [inst : TopologicalSpace M] → [ChartedSpace H M] → M → Type u
-- Init.Data.List.Lemmas
List.exists_cons_of_length_pos : ∀ {α : Type u_1} {l : List α}, 0 < l.length → ∃ h t, l = h :: t
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] [CategoryTheory.IsCofiltered J],
      CategoryTheory.Limits.PreservesLimitsOfShape J F) →
    CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' h
-- Std.Data.DTreeMap.Basic
/-- Support for the `for` loop construct in `do` blocks. Iteration happens in ascending order.  -/
Std.DTreeMap.Const.forInUncurried : {α : Type u} →
  {cmp : α → α → Ordering} →
    {δ : Type w} →
      {m : Type w → Type w₂} →
        [Monad m] → {β : Type v} → (α × β → δ → m (ForInStep δ)) → δ → Std.DTreeMap α (fun x => β) cmp → m δ
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.mem_inf_iff : ∀ {α : Type u_1} [inst : LE α] {s t : UpperSet α} {a : α}, a ∈ s ⊓ t ↔ a ∈ s ∨ a ∈ t
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.subsingleton_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Submonoid R},
  Subsingleton (LocalizedModule S M) ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
-- Mathlib.Order.Preorder.Finite
OrderHom.eq_id_of_injective : ∀ {α : Type u_4} [inst : LinearOrder α] [Finite α] (f : α →o α), Function.Injective ⇑f → f = OrderHom.id
-- Mathlib.Data.List.Rotate
List.mem_rotate : ∀ {α : Type u} {l : List α} {a : α} {n : ℕ}, a ∈ l.rotate n ↔ a ∈ l
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_involutive : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (c : P) {R : ℝ}, R ≠ 0 → Function.Involutive (EuclideanGeometry.inversion c R)
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
/-- The diagonal object of a morphism `f : X ⟶ Y` is `Δ_{X/Y} := pullback f f`.  -/
CategoryTheory.Limits.pullback.diagonalObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasPullback f f] → C
-- Aesop.Forward.Match.Types
Aesop.CompleteMatch.mk.injEq : ∀ (clusterMatches clusterMatches_1 : Array Aesop.Match),
  ({ clusterMatches := clusterMatches } = { clusterMatches := clusterMatches_1 }) = (clusterMatches = clusterMatches_1)
-- Mathlib.GroupTheory.Solvable
map_derivedSeries_eq : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'},
  Function.Surjective ⇑f → ∀ (n : ℕ), Subgroup.map f (derivedSeries G n) = derivedSeries G' n
-- Mathlib.Computability.Primrec.Basic
Primrec.option_getD : ∀ {α : Type u_1} [inst : Primcodable α], Primrec₂ Option.getD
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_congr : ∀ {α : Type u} {β : Type v} (e : α ≃ β), Cardinal.toENat (Cardinal.mk α) = Cardinal.toENat (Cardinal.mk β)
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac : ∀ {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] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseRightKanExtension F L]
  [inst_5 : L.HasPointwiseRightKanExtension F],
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv)
      (CategoryTheory.CategoryStruct.comp (L.associator (L.pointwiseRightKanExtension F) G).inv
        (CategoryTheory.Functor.whiskerRight (L.pointwiseRightKanExtensionCounit F) G)) =
    L.pointwiseRightKanExtensionCounit (F.comp G)
-- Lean.Environment
Lean.PersistentEnvExtensionDescrCore.name : {α β σ : Type} → Lean.PersistentEnvExtensionDescrCore α β σ → Lean.Name
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsScalarTowerAtPrimeFractionRing_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {P : Ideal R} [inst_2 : P.IsPrime],
  IsScalarTower R (Localization.AtPrime P) (FractionRing R)
-- Mathlib.Logic.Encodable.Lattice
Encodable.iSup_decode₂ : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable β] [inst_1 : CompleteLattice α] (f : β → α),
  ⨆ i, ⨆ b ∈ Encodable.decode₂ β i, f b = ⨆ b, f b
-- Mathlib.Order.Interval.Set.Image
StrictAnti.image_Ico_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictAnti f → f '' Set.Ico a b ⊆ Set.Ioc (f b) (f a)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap'_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂), CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂ = γ.φK
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionParams.mk : Lean.Lsp.WorkDoneProgressParams →
  Lean.Lsp.PartialResultParams →
    Lean.Lsp.TextDocumentIdentifier → Lean.Lsp.Range → Lean.Lsp.CodeActionContext → Lean.Lsp.CodeActionParams
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.equiv_apply_euclideanSpace : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : EuclideanSpace 𝕜 ι),
  ((EuclideanSpace.basisFun ι 𝕜).equiv b (Equiv.refl ι)) x = ∑ i, x.ofLp i • b i
-- Mathlib.Data.Seq.Defs
Stream'.Seq.destruct_eq_none : ∀ {α : Type u} {s : Stream'.Seq α}, s.destruct = none → s = Stream'.Seq.nil
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- The canonical `R`-linear isomorphism between `WithVal v` and `S`, when `v : Valuation S Γ₀`.  -/
WithVal.linearEquiv : (R : Type u_1) →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] →
      [inst_1 : Ring R] →
        {S : Type u_3} → [inst_2 : Ring S] → [inst_3 : Module R S] → (v : Valuation S Γ₀) → WithVal v ≃ₗ[R] S
-- Lean.Elab.Util
Lean.Elab.instMonadMacroAdapterOfMonadLiftOfMonadQuotation : (m n : Type → Type) →
  [MonadLift m n] → [Lean.MonadQuotation n] → [Lean.Elab.MonadMacroAdapter m] → Lean.Elab.MonadMacroAdapter n
-- Mathlib.Algebra.Order.Group.Abs
eq_of_mabs_div_lt_all : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {x y : G},
  (∀ ε > 1, |x / y|ₘ < ε) → x = y
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.map_ofNat : ∀ {α : Type u} {β : Type v} [inst : AddMonoidWithOne α] {f : α → β} (n : ℕ) [inst_1 : n.AtLeastTwo],
  WithTop.map f (OfNat.ofNat n) = ↑(f (OfNat.ofNat n))
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.sup_eq_range : ∀ {N : Type u_4} [inst : AddCommMonoid N] (s t : AddSubmonoid N),
  s ⊔ t = AddMonoidHom.mrange (s.subtype.coprod t.subtype)
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.hasBasis_nhds_zero : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G],
  (nhds 0).HasBasis (fun V => V ∈ nhds 0) fun V => {f | ∀ (x : α), f x ∈ V}
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.liftEquiv_coe : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (N : AddSubgroup G) [nN : N.Normal]
  {φ : G →+ H} (hφ : Function.Surjective ⇑φ) (HN : N = φ.ker) (g : G), (QuotientAddGroup.liftEquiv N hφ HN) ↑g = φ g
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
/-- A **Delone set** consists of a set together with explicit radii
witnessing uniform discreteness and relative denseness.  -/
Delone.DeloneSet : (X : Type u_3) → [MetricSpace X] → Type u_3
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- If an element `p` of `FreeAddMonoid (R × Π i, s i)` lifts an element `x` of `⨂[R] i, s i`,
and if `a` is an element of `R`, then the list obtained by multiplying the first entry of each
element of `p` by `a` lifts `a • x`.
 -/
PiTensorProduct.lifts_smul : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {x : PiTensorProduct R fun i => s i} {p : FreeAddMonoid (R × ((i : ι) → s i))},
  p ∈ x.lifts → ∀ (a : R), (FreeAddMonoid.map fun y => (a * y.1, y.2)) p ∈ (a • x).lifts