mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.constVAdd_zsmul : ∀ (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (z : ℤ) (v : V₁), AffineEquiv.constVAdd k P₁ (z • v) = AffineEquiv.constVAdd k P₁ v ^ z
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.descr : {α β σ : Type} → Lean.ScopedEnvExtension α β σ → Lean.ScopedEnvExtension.Descr α β σ
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
/-- Let `v` be an `(n + 1)`-tuple with two equal elements `v i = v j`, `i ≠ j`.
Let `w i` (resp., `w j`) be the vector `v` with `i`th (resp., `j`th) element removed.
Then `(-1) ^ i • f (w i) + (-1) ^ j • f (w j) = 0`.
This follows from the fact that these two vectors differ by a permutation of sign `(-1) ^ (i + j)`.

These are the only two nonzero terms in the proof of `map_eq_zero_of_eq`
in the definition of `AlternatingMap.alternatizeUncurryFin`.  -/
ContinuousAlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} (f : E [⋀^Fin n]→L[𝕜] F)
  {v : Fin (n + 1) → E} {i j : Fin (n + 1)},
  v i = v j → i ≠ j → (-1) ^ ↑i • f (i.removeNth v) + (-1) ^ ↑j • f (j.removeNth v) = 0
-- Mathlib.Analysis.Seminorm
Seminorm.comp_mono : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜] [inst_1 : SeminormedRing 𝕜₂]
  {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup E₂]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ E₂] {p q : Seminorm 𝕜₂ E₂} (f : E →ₛₗ[σ₁₂] E₂), p ≤ q → p.comp f ≤ q.comp f
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.ofHom_hom : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] (A B : TopRep k G)
  (f : A ⟶ B), TopRep.ofHom (TopRep.Hom.hom f) = f
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
/-- Being étale is multiplicative.  -/
AlgebraicGeometry.Etale.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.Etale
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `inv_lt_iff_one_lt_mul₀` for a version with multiplication on the other side.  -/
inv_lt_iff_one_lt_mul₀' : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀},
  0 < a → (a⁻¹ < b ↔ 1 < a * b)
-- Std.Time.Time.Unit.Minute
/-- Creates an `Ordinal` from a `Fin`, ensuring the value is within bounds.
 -/
Std.Time.Minute.Ordinal.ofFin : Fin 60 → Std.Time.Minute.Ordinal
-- Mathlib.FieldTheory.Perfect
/-- If `L / K` is an algebraic extension, `K` is a perfect field, then so is `L`.  -/
Algebra.IsAlgebraic.perfectField : ∀ (K : Type u_1) {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsAlgebraic K L]
  [PerfectField K], PerfectField L
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.map_comp_ofLE : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)}
  {A A' : DiscreteQuotient X} {B : DiscreteQuotient Y} (cond : DiscreteQuotient.LEComap f A B) (h : A' ≤ A),
  DiscreteQuotient.map f cond ∘ DiscreteQuotient.ofLE h = DiscreteQuotient.map f ⋯
-- Mathlib.Data.Holor
Holor.CPRankMax1.nil : ∀ {α : Type} [inst : Mul α] (x : Holor α []), x.CPRankMax1
-- Mathlib.Data.Finset.Basic
Finset.range_filter_eq : ∀ {n m : ℕ}, {x ∈ Finset.range n | x = m} = if m < n then {m} else ∅
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.univLevelPos : Lean.Meta.RecursorInfo → List Lean.Meta.RecursorUnivLevelPos
-- Lean.MetavarContext
/-- Low-level version of `setMVarUserName`.
It does not update the table `userNames`. Thus, `findUserName?` cannot see the modification.
It is meant for `mkForallFVars'` where we temporarily set the user facing name of metavariables to get more
meaningful binder names.
 -/
Lean.MetavarContext.setMVarUserNameTemporarily : Lean.MetavarContext → Lean.MVarId → Lean.Name → Lean.MetavarContext
-- Mathlib.Order.Filter.NAry
Filter.map₂_inf_subset_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g₁ g₂ : Filter β},
  Filter.map₂ m f (g₁ ⊓ g₂) ≤ Filter.map₂ m f g₁ ⊓ Filter.map₂ m f g₂
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- If `fn` is `UniformIntegrable`, then the family of a.e. limits of sequences of `fn` is
`UniformIntegrable`.  -/
MeasureTheory.UniformIntegrable.uniformIntegrable_of_ae_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {κ : Type u_4} (u : Filter κ) [u.NeBot] [u.IsCountablyGenerated]
  {fn : ι → α → β}, MeasureTheory.UniformIntegrable fn p μ → MeasureTheory.UniformIntegrable (fun f => ↑f) p μ
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.subgroupOf_eq_bot : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.subgroupOf K = ⊥ ↔ Disjoint H K
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.map_append : ∀ {α : Type u} {β : Type v} (f : α → β) (s t : Stream'.WSeq α),
  Stream'.WSeq.map f (s.append t) = (Stream'.WSeq.map f s).append (Stream'.WSeq.map f t)
-- Lean.Meta.Basic
Lean.Meta.resetDefEqPermCaches : Lean.MetaM Unit
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
BoxIntegral.Box.measure_coe_lt_top : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsLocallyFiniteMeasure μ],
  μ ↑I < ⊤
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.GetElem?.match_1.eq_2 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match none with
    | some e => h_1 e
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Star.StarAlgHom
/-- The class that directly extends `RingEquivClass` and `SMulHomClass`.

Mostly an implementation detail for the ⋆-algebra equivalence class
which is currently: `[NonUnitalAlgEquivClass]` and `[StarHomClass]`.
 -/
NonUnitalAlgEquivClass : (F : Type u_1) →
  (R : outParam (Type u_2)) →
    (A : outParam (Type u_3)) →
      (B : outParam (Type u_4)) →
        [Add A] → [Mul A] → [SMul R A] → [Add B] → [Mul B] → [SMul R B] → [EquivLike F A B] → Prop
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.cofibrations_rlp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)],
  (HomotopicalAlgebra.cofibrations C).rlp = HomotopicalAlgebra.trivialFibrations C
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.ofDual_bot : ∀ (α : Type u) [inst : Top α], OrderDual.ofDual ⊥ = ⊤
-- Mathlib.Analysis.Analytic.Composition
/-- Version of `AnalyticAt.comp` where point equality is a separate hypothesis.  -/
AnalyticAt.comp_of_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {y : F} {x : E},
  AnalyticAt 𝕜 g y → AnalyticAt 𝕜 f x → f x = y → AnalyticAt 𝕜 (g ∘ f) x
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- The action by an intermediate field is the action by the underlying field.  -/
IntermediateField.instSMulSubtypeMem : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → {X : Type u_4} → [SMul L X] → (F : IntermediateField K L) → SMul (↥F) X
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.fromAddMonoid.eq_1 : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {γ : Type u₁}
  [inst_2 : AddCommMonoid γ],
  DirectSum.fromAddMonoid = DirectSum.toAddMonoid fun i => AddMonoidHom.compHom (DirectSum.of β i)
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.copy_eq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A →ₗc[R] B) (f' : A → B) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsBlockSystem.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] (ℬ : Set (Set X)),
  AddAction.IsBlockSystem G ℬ = (Setoid.IsPartition ℬ ∧ ∀ ⦃B : Set X⦄, B ∈ ℬ → AddAction.IsBlock G B)
-- Batteries.Data.Fin.Lemmas
Fin.countP_zero : ∀ (p : Fin 0 → Bool), Fin.countP p = 0
-- Mathlib.ModelTheory.Graph
/-- The theory of simple graphs.  -/
FirstOrder.Language.Theory.simpleGraph : FirstOrder.Language.graph.Theory
-- Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
/-- The digamma function, defined as the logarithmic derivative of the Gamma function.  -/
Complex.digamma : ℂ → ℂ
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the right whiskering `whiskerRightIso η h`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.whiskerRightM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
    Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Lean.Data.PersistentArray
Lean.PersistentArray.tail : {α : Type u} → Lean.PersistentArray α → Array α
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- The exponential map as an equivalence between `G` and `(Gᵐ⁰)ˣ`.  -/
WithZero.expEquiv : {G : Type u_5} → [inst : AddGroup G] → G ≃ (WithZero (Multiplicative G))ˣ
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
UpperHalfPlane.upperHalfPlaneSet.eq_1 : UpperHalfPlane.upperHalfPlaneSet = {z | 0 < z.im}
-- Mathlib.Tactic.Algebra.Basic
Mathlib.Tactic.Algebra.BaseType.mk.sizeOf_spec : ∀ {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring «$R»)} {sA : Q(CommSemiring «$A»)}
  {sAlg : Q(Algebra «$R» «$A»)} (r : Q(«$R»)) (x : Mathlib.Tactic.Ring.ExSum q(«$sR») r),
  sizeOf (Mathlib.Tactic.Algebra.BaseType.mk r x) = 1 + sizeOf r + sizeOf x
-- Mathlib.MeasureTheory.Measure.Lebesgue.Complex
/-- Measurable equivalence between `ℂ` and `ℝ² = Fin 2 → ℝ`.  -/
Complex.measurableEquivPi : ℂ ≃ᵐ (Fin 2 → ℝ)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.State.mk.sizeOf_spec : ∀ (structs : Array Lean.Meta.Grind.AC.Struct) (opIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (exprToOpIds : Lean.PHashMap Lean.Meta.Sym.ExprPtr (List ℕ)) (steps : ℕ),
  sizeOf { structs := structs, opIdOf := opIdOf, exprToOpIds := exprToOpIds, steps := steps } =
    1 + sizeOf structs + sizeOf opIdOf + sizeOf exprToOpIds + sizeOf steps
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- A category "has a zero object" if it has an object which is both initial and terminal.  -/
CategoryTheory.Limits.HasZeroObject : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.RingTheory.PowerBasis
PowerBasis.map_dim : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {S' : Type u_7}
  [inst_3 : CommRing S'] [inst_4 : Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S'), (pb.map e).dim = pb.dim
-- Lean.Elab.Tactic.LibrarySearch
Lean.Elab.LibrarySearch.elabLibrarySearchConfig : Lean.Syntax →
  optParam Lean.Parser.Tactic.LibrarySearchConfig { } →
    optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Parser.Tactic.LibrarySearchConfig
-- Mathlib.Data.Rat.Star
NNRat.addSubmonoid_closure_range_pow : ∀ {n : ℕ}, n ≠ 0 → AddSubmonoid.closure (Set.range fun x => x ^ n) = ⊤
-- Init.Data.Vector.Lex
_private.Init.Data.Vector.Lex.0.Break.runK.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.mdifferentiable_denom_zpow : ∀ (g : GL (Fin 2) ℝ) (k : ℤ), MDiff fun x => UpperHalfPlane.denom g ↑x ^ k
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A split epi `f` coequalizes `(f ≫ section_ f)` and `(𝟙 X)`.
Here we build the cocone, and show in `isSplitEpiCoequalizes` that it is a colimit cocone.
 -/
CategoryTheory.Limits.coconeOfIsSplitEpi : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.IsSplitEpi f] →
          CategoryTheory.Limits.Cofork (CategoryTheory.CategoryStruct.id X)
            (CategoryTheory.CategoryStruct.comp f (CategoryTheory.section_ f))
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_eq_of_le : ∀ {R : Type u} [inst : NonAssocRing R] {s : Set R} {t : Subring R},
  s ⊆ ↑t → t ≤ Subring.closure s → Subring.closure s = t
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Given an element `x` of a topological space `M` over a semiring `R`, the natural continuous
linear map from `R` to `M` by taking multiples of `x`.  -/
ContinuousLinearMap.toSpanSingleton : (R₁ : Type u_1) →
  [inst : Semiring R₁] →
    {M₁ : Type u_4} →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] →
          [inst_3 : Module R₁ M₁] → [inst_4 : TopologicalSpace R₁] → [ContinuousSMul R₁ M₁] → M₁ → R₁ →L[R₁] M₁
-- Mathlib.Data.Int.Order.Lemmas
Int.natAbs_eq_iff_mul_self_eq : ∀ {a b : ℤ}, a.natAbs = b.natAbs ↔ a * a = b * b
-- Mathlib.CategoryTheory.Bicategory.SingleObj
/-- Promote a monoidal category to a bicategory with a single object.
(The objects of the monoidal category become the 1-morphisms,
with composition given by tensor product,
and the morphisms of the monoidal category become the 2-morphisms.)
 -/
CategoryTheory.MonoidalSingleObj : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → Type
-- Mathlib.Probability.Independence.Basic
/-- **Alias** of the forward direction of `ProbabilityTheory.iIndepFun_congr`. -/
ProbabilityTheory.iIndepFun.congr : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_10}
  {mβ : (i : ι) → MeasurableSpace (β i)} {f g : (i : ι) → Ω → β i},
  (∀ (i : ι), f i =ᵐ[μ] g i) → ProbabilityTheory.iIndepFun f μ → ProbabilityTheory.iIndepFun g μ
-- Mathlib.Data.Finset.Basic
Multiset.toFinset_nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α}, s.toFinset.Nonempty ↔ s ≠ 0
-- Mathlib.Analysis.ODE.Basic
/-- `IsIntegralCurveAt γ v t₀` means `γ : ℝ → E` is a local integral curve of `v` in a neighbourhood
containing `t₀`.  -/
IsIntegralCurveAt : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (ℝ → E) → (ℝ → E → E) → ℝ → Prop
-- Init.Data.String.Basic
String.Slice.Pos.cast_le_cast_iff : ∀ {s t : String.Slice} {pos pos' : s.Pos} {h : s.copy = t.copy}, pos.cast h ≤ pos'.cast h ↔ pos ≤ pos'
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasSum_of_isLUB : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α]
  [inst_3 : TopologicalSpace α] [OrderTopology α] {f : ι → α} (b : α),
  IsLUB (Set.range fun s => ∑ i ∈ s, f i) b → HasSum f b
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right}
  (hd : CategoryTheory.Limits.IsColimit d) {K₁ K₂ : CategoryTheory.Limits.Multicofork I} (f : K₁ ⟶ K₂),
  ((I.toSigmaCoforkFunctor hc hd).map f).hom = f.hom
-- Lean.DocString.Markdown
Lean.Doc.instInhabitedMdRendererState : Inhabited Lean.Doc.MdRendererState
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Makes the identity additive isomorphism from a proof two submonoids of an additive monoid are
equal.  -/
AddEquiv.addSubmonoidCongr : {M : Type u_1} → [inst : AddZeroClass M] → {S T : AddSubmonoid M} → S = T → ↥S ≃+ ↥T
-- Mathlib.Order.Cover
AntisymmRel.trans_wcovBy : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → b ⩿ c → a ⩿ c
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedExBase : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} → Inhabited ((e : Q(«$α»)) × Mathlib.Tactic.Ring.Common.ExBase bt sα e)
-- Init.Data.Nat.Lemmas
Nat.lt_mul_iff_one_lt_left : ∀ {b a : ℕ}, 0 < b → (b < a * b ↔ 1 < a)
-- Mathlib.Algebra.Quandle
Rack.left_cancel : ∀ {R : Type u_1} [inst : Rack R] (x : R) {y y' : R}, Shelf.act x y = Shelf.act x y' ↔ y = y'
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackRestrictIsoRestrict f U).hom (f ∣_ U) =
    CategoryTheory.Limits.pullback.snd f U.ι
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.constant.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.constant = 1
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Matrix.minpoly_toLin' : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  minpoly R (Matrix.toLin' M) = minpoly R M
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The function `ContinuousLinearEquiv.inverse` can be written in terms of `Ring.inverse` for the
ring of self-maps of the domain.  -/
ContinuousLinearMap.inverse_eq_ringInverse : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (e : M ≃L[R] M₂) (f : M →L[R] M₂), f.inverse = Ring.inverse (↑e.symm ∘SL f) ∘SL ↑e.symm
-- Mathlib.GroupTheory.Commensurable
AddSubgroup.Commensurable.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G), H.Commensurable K = (H.relIndex K ≠ 0 ∧ K.relIndex H ≠ 0)
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Given a function `g : β → γ` and a simple function `f : α →ₛ β`, `f.map g` return the simple
function `g ∘ f : α →ₛ γ`  -/
MeasureTheory.SimpleFunc.map : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → [inst : MeasurableSpace α] → (β → γ) → MeasureTheory.SimpleFunc α β → MeasureTheory.SimpleFunc α γ
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime_pow : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime]
  [hP₂ : P.LiesOver (Ideal.span {↑p})], P.ramificationIdx ℤ = p ^ k * (p - 1)
-- Mathlib.Analysis.Convex.PathConnected
JoinedIn.of_segment_subset : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] {x y : E} {s : Set E}, segment ℝ x y ⊆ s → JoinedIn s x y
-- Mathlib.Analysis.Complex.CanonicalDecomposition
_private.Mathlib.Analysis.Complex.CanonicalDecomposition.0.Complex.canonicalDecomposition_aux₁ : ∀ {R : ℝ} (F : Function.locallyFinsuppWithin (Metric.ball 0 R) ℤ),
  MeromorphicNFOn (∏ᶠ (u : ℂ), Complex.canonicalFactor R u ^ F u) (Metric.ball 0 R)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₂ → Std.ExtDHashMap.Const.get? (m₁ ∩ m₂) k = Std.ExtDHashMap.Const.get? m₁ k
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
/-- The source of the edge is `x₀`.  -/
SSet.Truncated.Edge.src_eq : ∀ {X : SSet.Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  (self : SSet.Truncated.Edge x₀ x₁),
  (CategoryTheory.ConcreteCategory.hom
        (X.map (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
      self.edge =
    x₀
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.toList.eq_1 : ∀ {α : Type u_1} (t : RBTree.RBNode α), t.toList = RBTree.RBNode.foldr (fun x1 x2 => x1 :: x2) t []
-- Mathlib.Analysis.Convex.StrictCombination
Affine.Simplex.dist_lt_of_mem_closedInterior_of_strictConvexSpace : ∀ {V : Type u_2} {P : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [StrictConvexSpace ℝ V]
  [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {r : ℝ} {p₀ p : P},
  p ∈ s.closedInterior →
    (∀ (i : Fin (n + 1)), p ≠ s.points i) → (∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r) → dist p p₀ < r
-- Init.Data.String.Iterate
String.Slice.ByteIterator : Type
-- Mathlib.Data.Int.ModEq
/-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`.  -/
Int.ModEq.cancel_left_div_gcd : ∀ {m a b c : ℤ}, 0 < m → c * a ≡ c * b [ZMOD m] → a ≡ b [ZMOD m / ↑(m.gcd c)]
-- Init.Control.Lawful.Basic
pure_id_seq : ∀ {f : Type u_1 → Type u_2} {α : Type u_1} [inst : Applicative f] [LawfulApplicative f] (x : f α), pure id <*> x = x
-- Init.Data.Vector.Attach
Vector.attach_congr : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n} (h : xs = ys), xs.attach = Vector.map (fun x => ⟨↑x, ⋯⟩) ys.attach
-- Lean.Meta.GeneralizeTelescope
Lean.Meta.GeneralizeTelescope.Entry.mk.inj : ∀ {expr type : Lean.Expr} {modified : Bool} {expr_1 type_1 : Lean.Expr} {modified_1 : Bool},
  { expr := expr, type := type, modified := modified } = { expr := expr_1, type := type_1, modified := modified_1 } →
    expr = expr_1 ∧ type = type_1 ∧ modified = modified_1
-- Mathlib.Topology.Sets.OpenCover
/-- (Pre)Irreducibility can be checked on an open cover with pairwise non-empty intersections.  -/
PreirreducibleSpace.of_isOpenCover : ∀ {X : Type u_1} {ι : Type u_2} [inst : TopologicalSpace X] {U : ι → TopologicalSpace.Opens X},
  Pairwise (Function.onFun (fun x1 x2 => ¬Disjoint x1 x2) U) →
    TopologicalSpace.IsOpenCover U → (∀ (i : ι), PreirreducibleSpace ↥(U i)) → PreirreducibleSpace X
-- Mathlib.Order.Interval.Finset.Fin
Fin.castLEEmb.congr_simp : ∀ {n m : ℕ} (h : n ≤ m), Fin.castLEEmb h = Fin.castLEEmb h
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLE?.go.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option α),
  Std.DTreeMap.Internal.Impl.getKeyLE?.go k best Std.DTreeMap.Internal.Impl.leaf = best
-- Init.Tactics
/-- Location specifications are used by many tactics that can operate on either the
hypotheses or the goal. It can have one of the forms:
* 'empty' is not actually present in this syntax, but most tactics use
  `(location)?` matchers. It means to target the goal only.
* `at h₁ ... hₙ`: target the hypotheses `h₁`, ..., `hₙ`
* `at h₁ h₂ ⊢`: target the hypotheses `h₁` and `h₂`, and the goal
* `at *`: target all hypotheses and the goal
 -/
Lean.Parser.Tactic.location : Lean.ParserDescr
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
IsSemilinearSet.biInter_finset : ∀ {M : Type u_1} {ι : Type u_3} [inst : AddCommMonoid M] [AddMonoid.FG M] {s : Finset ι} {t : ι → Set M},
  (∀ i ∈ s, IsSemilinearSet (t i)) → IsSemilinearSet (⋂ i ∈ s, t i)
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Arguments to callee (including fixed prefix)  -/
Lean.Elab.WF.GuessLex.RecCallWithContext.args : Lean.Elab.WF.GuessLex.RecCallWithContext → Array Lean.Expr
-- Init.Data.Array.Count
Array.count_eq_countP' : ∀ {α : Type u_1} [inst : BEq α] {a : α}, Array.count a = Array.countP fun x => x == a