mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.BlockMem.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] (a : X),
  AddAction.BlockMem G a = { B // a ∈ B ∧ AddAction.IsBlock G B }
-- Mathlib.Data.Vector.Basic
_private.Mathlib.Data.Vector.Basic.0.List.Vector.mOfFn.match_1.eq_2 : ∀ {m : Type u_3 → Type u_2} {α : Type u_3} (motive : (x : ℕ) → (Fin x → m α) → Sort u_1) (n : ℕ) (f : Fin (n + 1) → m α)
  (h_1 : (x : Fin 0 → m α) → motive 0 x) (h_2 : (n : ℕ) → (f : Fin (n + 1) → m α) → motive n.succ f),
  (match n.succ, f with
    | 0, x => h_1 x
    | n.succ, f => h_2 n f) =
    h_2 n f
-- Mathlib.AlgebraicGeometry.Limits
/-- If `X` and `Y` are open disjoint and covering open subschemes of `S`,
`S` is the disjoint union of `X` and `Y`.  -/
AlgebraicGeometry.nonempty_isColimit_binaryCofanMk_of_isCompl : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsOpenImmersion g],
  IsCompl (AlgebraicGeometry.Scheme.Hom.opensRange f) (AlgebraicGeometry.Scheme.Hom.opensRange g) →
    Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f g))
-- Mathlib.Combinatorics.Quiver.Prefunctor
/-- A morphism of quivers. As we will later have categorical functors extend this structure,
we call it a `Prefunctor`.  -/
Prefunctor : (V : Type u₁) → [Quiver V] → (W : Type u₂) → [Quiver W] → Type (max (max (max u₁ u₂) v₁) v₂)
-- Mathlib.RingTheory.Congruence.Basic
RingCon.Quotient.eq_1 : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (c : RingCon R), c.Quotient = Quotient c.toSetoid
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.π_comp_cokernelIsoOfEq_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasCokernel g]
  (h : f = g) {Z : C} (h_1 : CategoryTheory.Limits.cokernel f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelIsoOfEq h).inv h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) h_1
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLE.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_3 ()
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM : Type → Type
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀)
  {Z_1 : AlgebraicGeometry.Scheme} (h : 𝒰.X i ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) h
-- Mathlib.Data.Num.ZNum
ZNum.zeroLEOneClass : ZeroLEOneClass ZNum
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the forward direction of `upperHemicontinuousAt_iff_forall_isOpen`. -/
UpperHemicontinuousAt.forall_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {x : α} [inst_1 : TopologicalSpace β],
  UpperHemicontinuousAt f x → ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhds x, f x' ⊆ u
-- Init.Data.List.OfFn
List.ofFn.eq_1 : ∀ {α : Type u_1} {n : ℕ} (f : Fin n → α), List.ofFn f = Fin.foldr n (fun x1 x2 => f x1 :: x2) []
-- Std.Http.Data.Body.Full
/-- A body backed by a fixed, mutex-protected `ByteArray`.

The data is consumed on the first read. Once consumed (or explicitly closed), the body
behaves as a closed, empty channel.
 -/
Std.Http.Body.Full : Type
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- If a submodule has maximal dimension in a finite-dimensional space, then it is equal to the
whole space.  -/
Submodule.eq_top_of_finrank_eq : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] {S : Submodule K V}, Module.finrank K ↥S = Module.finrank K V → S = ⊤
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- The degree of a vertex is at most the number of edges.  -/
SimpleGraph.degree_le_card_edgeFinset : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)] [inst_1 : Fintype ↑G.edgeSet],
  G.degree v ≤ G.edgeFinset.card
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.instDecidableEqHom.decEq : {ι : Type u_1} → {a a_1 : CategoryTheory.Pairwise ι} → [DecidableEq ι] → (x x_1 : a.Hom a_1) → Decidable (x = x_1)
-- Lean.Util.Recognizers
Lean.Expr.isEq : Lean.Expr → Bool
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.conjExponent : ∀ {p : NNReal}, 1 < p → p.HolderConjugate p.conjExponent
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- `h.homEquiv` acts like an "object comprehension" operator: it maps any characteristic map
`f : X ⟶ Ω` to the associated subobject of `X`, obtained by pulling back `h.Ω₀` along `f`.  -/
CategoryTheory.SubobjectRepresentableBy.homEquiv_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {X : C} (f : X ⟶ Ω),
  h.homEquiv f = (CategoryTheory.Subobject.pullback f).obj h.Ω₀
-- Mathlib.Data.Set.PowersetCard
/-- Complement of `Finset`s as an equivalence on `Set.powersetCard`.  -/
Set.powersetCard.compl : {α : Type u_1} →
  {n : ℕ} →
    [DecidableEq α] →
      [inst : Fintype α] → {m : ℕ} → m + n = Fintype.card α → ↑(Set.powersetCard α n) ≃ ↑(Set.powersetCard α m)
-- Mathlib.CategoryTheory.Monoidal.Braided.PushoutObjObj
/-- In a braided monoidal category, from a `Functor.PushoutObjObj` structure for
the bifunctor `curriedTensor` and two morphism `f₁` and `f₂`, one may
obtain a similar structure for `f₂` and `f₁`.  -/
CategoryTheory.Functor.PushoutObjObj.flipTensor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        {X₁ Y₁ X₂ Y₂ : C} →
          {f₁ : X₁ ⟶ Y₁} →
            {f₂ : X₂ ⟶ Y₂} →
              (CategoryTheory.MonoidalCategory.curriedTensor C).PushoutObjObj f₁ f₂ →
                (CategoryTheory.MonoidalCategory.curriedTensor C).PushoutObjObj f₂ f₁
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
_private.Lean.Meta.Tactic.Simp.Arith.Nat.Basic.0.Nat.Internal.Linear.Expr.applyPerm.go : Lean.Perm → Nat.Internal.Linear.Expr → Nat.Internal.Linear.Expr
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C} {J : Type w}
  [inst_2 : CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {j₀ : J} (y : X ⟶ Y.obj j₀)
  (j : CategoryTheory.Under j₀),
  (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F y).obj j =
    CategoryTheory.MonoOver.mk
      ((CategoryTheory.Limits.kernel.ι (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y)).app j)
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.alternatingWord_succ' : ∀ {B : Type u_1} (i i' : B) (m : ℕ),
  CoxeterSystem.alternatingWord i i' (m + 1) = (if Even m then i' else i) :: CoxeterSystem.alternatingWord i i' m
-- Mathlib.Analysis.Complex.AbsMax
/-- If two complex differentiable functions `f g : E → F` are equal on the boundary of a bounded set
`U`, then they are equal on `U`.  -/
Complex.eqOn_of_eqOn_frontier : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [Nontrivial E] {f g : E → F} {U : Set E},
  Bornology.IsBounded U → DiffContOnCl ℂ f U → DiffContOnCl ℂ g U → Set.EqOn f g (frontier U) → Set.EqOn f g U
-- Lean.Data.Lsp.Client
Lean.Lsp.instFromJsonRegistrationParams.fromJson : Lean.Json → Except String Lean.Lsp.RegistrationParams
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.toNegMemClass : ∀ {S : Type u_3} {G : outParam (Type u_4)} {inst : SubNegMonoid G} {inst_1 : SetLike S G} [self : AddSubgroupClass S G],
  NegMemClass S G
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
Float.Model.UnpackedFloat.pack.match_1.congr_eq_4 : ∀ (motive : Float.Model.UnpackedFloat → Sort u_1) (x : Float.Model.UnpackedFloat)
  (h_1 : Unit → motive Float.Model.UnpackedFloat.notANumber)
  (h_2 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.infinity s))
  (h_3 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.zero s))
  (h_4 :
    (s : Float.Model.UnpackedFloat.Sign) →
      (m : ℕ) → (e : ℤ) → (mantissa_pos : 0 < m) → motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos))
  (s : Float.Model.UnpackedFloat.Sign) (m : ℕ) (e : ℤ) (mantissa_pos : 0 < m),
  x = Float.Model.UnpackedFloat.finite s m e mantissa_pos →
    (match x with
      | Float.Model.UnpackedFloat.notANumber => h_1 ()
      | Float.Model.UnpackedFloat.infinity s => h_2 s
      | Float.Model.UnpackedFloat.zero s => h_3 s
      | Float.Model.UnpackedFloat.finite s m e mantissa_pos => h_4 s m e mantissa_pos) ≍
      h_4 s m e mantissa_pos
-- Mathlib.RingTheory.Lasker
Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {s : Finset (Submodule R M)},
  s.inf id = N →
    (∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary) →
      ∃ t,
        t.inf id = N ∧
          (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
            (↑t).Pairwise (Function.onFun (fun x1 x2 => x1 ≠ x2) fun J => (J.colon Set.univ).radical) ∧
              ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_sdiff_null : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {s t : Set α}, μ t = 0 → μ (s \ t) = μ s
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.join_meet_right : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.join (Lean.Order.meet P Q) R = Lean.Order.meet (Lean.Order.join P R) (Lean.Order.join Q R)
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Bundle.Pretrivialization.continuousAlternatingMap.congr_simp : ∀ (𝕜 : Type u_1) (ι : Type u_2) [inst : NontriviallyNormedField 𝕜] {B : Type u_3} [inst_1 : TopologicalSpace B]
  {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_5}
  [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜 (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₁ x)] [inst_13 : FiberBundle F₁ E₁]
  [inst_14 : (x : B) → TopologicalSpace (E₂ x)] [inst_15 : FiberBundle F₂ E₂]
  (e₁ e₁_1 : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e_e₁ : e₁ = e₁_1)
  (e₂ e₂_1 : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) (e_e₂ : e₂ = e₂_1)
  [inst_16 : Bundle.Trivialization.IsLinear 𝕜 e₁] [inst_17 : Bundle.Trivialization.IsLinear 𝕜 e₂],
  Bundle.Pretrivialization.continuousAlternatingMap 𝕜 ι e₁ e₂ =
    Bundle.Pretrivialization.continuousAlternatingMap 𝕜 ι e₁_1 e₂_1
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_pair_eq_inf : ∀ {α : Type u_1} [inst : EDist α] {x y : α}, x ≠ y → {x, y}.einfsep = min (edist x y) (edist y x)
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.mk.sizeOf_spec : ∀ {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]
  [inst_7 : SizeOf R] [inst_8 : SizeOf A] [inst_9 : SizeOf B] (toLinearMap : A →ₗ[R] B)
  (counit_comp : CoalgebraStruct.counit ∘ₗ toLinearMap = CoalgebraStruct.counit)
  (map_comp_comul :
    TensorProduct.map toLinearMap toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ toLinearMap),
  sizeOf { toLinearMap := toLinearMap, counit_comp := counit_comp, map_comp_comul := map_comp_comul } =
    1 + sizeOf toLinearMap + sizeOf counit_comp + sizeOf map_comp_comul
-- Batteries.Data.DList.Basic
/-- `O(1)` (`apply` is `O(1)`). A `DList α` corresponding to the list `[a]`.  -/
Batteries.DList.singleton : {α : Type u} → α → Batteries.DList α
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneRightOpOfCocone_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.coneRightOpOfCocone c).π = CategoryTheory.NatTrans.rightOp c.ι
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
ExteriorAlgebra.liftAlternating_comp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {N' : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup N'] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R N'] (g : N →ₗ[R] N') (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
  (ExteriorAlgebra.liftAlternating fun i => g.compAlternatingMap (f i)) = g ∘ₗ ExteriorAlgebra.liftAlternating f
-- Mathlib.Data.Finset.Insert
Finset.cons_swap : ∀ {α : Type u_1} {s : Finset α} {a b : α} (hb : b ∉ s) (ha : a ∉ Finset.cons b s hb),
  Finset.cons a (Finset.cons b s hb) ha = Finset.cons b (Finset.cons a s ⋯) ⋯
-- Mathlib.Topology.Order.OrderClosed
Iio_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b < a → Set.Iio a ∈ nhds b
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- If `W₁ : MorphismProperty C₁` and `W₂ : MorphismProperty C₂`, a `LocalizerMorphism W₁ W₂`
is the datum of a functor `C₁ ⥤ C₂` which sends morphisms in `W₁` to morphisms in `W₂`  -/
CategoryTheory.LocalizerMorphism : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        CategoryTheory.MorphismProperty C₁ → CategoryTheory.MorphismProperty C₂ → Type (max (max (max u₁ u₂) v₁) v₂)
-- Mathlib.RingTheory.PrincipalIdealDomain
Submodule.IsPrincipal.map : ∀ {R : Type u} {M : Type v} {N : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] (f : M →ₗ[R] N) {S : Submodule R M},
  S.IsPrincipal → (Submodule.map f S).IsPrincipal
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedSup_of_notMem : ∀ {α : Type u_1} [inst : SemilatticeSup α] {s : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : OrderTop α],
  a ∉ lowerClosure ↑s → s.truncatedSup a = ⊤
-- Mathlib.Tactic.Choose
/-- Results of searching for nonempty instances,
to eliminate dependencies on propositions (`choose!`).
`success` means we found at least one instance;
`failure ts` means we didn't find instances for any `t ∈ ts`.
(`failure []` means we didn't look for instances at all.)

Rationale:
`choose!` means we are expected to succeed at least once
in eliminating dependencies on propositions.
 -/
Mathlib.Tactic.Choose.ElimStatus : Type
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.mk.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Semiring R] [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} {E : Type u_11}
  {E₂ : Type u_12} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (toLinearMap toLinearMap_1 : E →ₛₗ[σ₁₂] E₂) (e_toLinearMap : toLinearMap = toLinearMap_1)
  (norm_map' : ∀ (x : E), ‖toLinearMap x‖ = ‖x‖),
  { toLinearMap := toLinearMap, norm_map' := norm_map' } = { toLinearMap := toLinearMap_1, norm_map' := ⋯ }
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- The conjugate of `z` is `trace z - z`.  -/
QuadraticAlgebra.star_eq : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (z : QuadraticAlgebra R a b),
  star z = (algebraMap R (QuadraticAlgebra R a b)) (QuadraticAlgebra.trace z) - z
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- Given a rank function for a proper pairing of a subcomplex of a
simplicial set, this is coproduct of the standard simplices corresponding
to all cells of rank `j`.  -/
SSet.Subcomplex.Pairing.RankFunction.sigmaStdSimplex : {X : SSet} → {A : X.Subcomplex} → {P : A.Pairing} → {ι : Type v} → [inst : LinearOrder ι] → P.RankFunction ι → ι → SSet
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.coe_setOfPred : ∀ {α : Type u_8}, ⇑MeasurableEquiv.setOfPred = Set.ofPred
-- Lean.Compiler.IR.Basic
Lean.IR.instReprCtorInfo : Repr Lean.IR.CtorInfo
-- Init.Data.Option.Monadic
Option.forIn'_yield_eq_pelim : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [inst : Monad m] [LawfulMonad m] (o : Option α)
  (f : (a : α) → a ∈ o → β → m γ) (g : (a : α) → a ∈ o → β → γ → β) (b : β),
  (forIn' o b fun a m_1 b => (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) =
    o.pelim (pure b) fun a h => g a h b <$> f a h b
-- Mathlib.Topology.MetricSpace.HolderNorm
coe_nnHolderNorm_le_eHolderNorm : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y},
  ↑(nnHolderNorm r f) ≤ eHolderNorm r f
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.dropn_ofSeq : ∀ {α : Type u} (s : Stream'.Seq α) (n : ℕ), (↑s).drop n = ↑(s.drop n)
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.instOrdConnectedOrdConnectedComponent : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α}, (s.ordConnectedComponent x).OrdConnected
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_eq_get!_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {a : α}, t[a]! = t[a]?.get!
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.mul'_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] {a b : A}, (LinearMap.mul' R A) (a ⊗ₜ[R] b) = a * b
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.plus_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η γ : J.plusObj P ⟶ Q),
  CategoryTheory.Presheaf.IsSheaf J Q →
    CategoryTheory.CategoryStruct.comp (J.toPlus P) η = CategoryTheory.CategoryStruct.comp (J.toPlus P) γ → η = γ
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.op_φK : ∀ {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₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂), ψ.op.φK = ψ.φQ.op
-- Std.Do.Internal.Ensures.Lemmas
/-- `pure a` is `Ensures`-witnessed at the singleton predicate `(· = a)`.  -/
Std.Do.Internal.Ensures.pure : ∀ {m : Type u → Type u_1} [inst : Monad m] [LawfulMonad m] {α : Type u} (a : α),
  Std.Do.Internal.Ensures (fun x => x = a) (pure a)
-- Mathlib.Algebra.Group.Units.Defs
Units.instDivInvMonoid.eq_1 : ∀ {α : Type u} [inst : Monoid α],
  Units.instDivInvMonoid =
    { toMonoid := Units.instMonoid, toInv := Units.instInv, toDiv := Units.instDiv,
      zpow := fun n a =>
        match n, a with
        | Int.ofNat n, a => a ^ n
        | Int.negSucc n, a => (a ^ n.succ)⁻¹,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯ }
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
CategoryTheory.Limits.ι_comp_sigmaObjIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {α : Type w} [inst_2 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) C]
  (f : α → CategoryTheory.Functor D C) (d : D) (s : α),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Sigma.ι f s).app d)
      (CategoryTheory.Limits.sigmaObjIso f d).hom =
    CategoryTheory.Limits.Sigma.ι (fun s => (f s).obj d) s
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instAdd : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → Add (WithVal v)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.baseChange_nonsingular : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  {f : A →ₐ[S] B},
  Function.Injective ⇑f → ∀ (P : Fin 3 → A), (W'.baseChange B).Nonsingular (⇑f ∘ P) ↔ (W'.baseChange A).Nonsingular P
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.antilipschitz_of_norm_ge : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂) {K : NNReal}, (∀ (x : V₁), ‖x‖ ≤ ↑K * ‖f x‖) → AntilipschitzWith K ⇑f
-- Init.Grind.Ring.CommSolver
/-- A `Poly.combine` optimized for the kernel.  -/
Lean.Grind.CommRing.Poly.combine_k : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.isGround.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis'.subset : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis' I X → I ⊆ X
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.splitAt.go.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → ℕ → List α → Sort u_2) (xs : List α) (x : ℕ) (acc : List α)
  (h_1 : (x : ℕ) → (x_1 : List α) → motive [] x x_1)
  (h_2 : (x : α) → (xs : List α) → (n : ℕ) → (acc : List α) → motive (x :: xs) n.succ acc)
  (h_3 : (xs : List α) → (x : ℕ) → (acc : List α) → motive xs x acc),
  (xs = [] → False) →
    (∀ (x_2 : α) (xs_1 : List α) (n : ℕ), xs = x_2 :: xs_1 → x = n.succ → False) →
      (match xs, x, acc with
        | [], x, x_3 => h_1 x x_3
        | x :: xs, n.succ, acc => h_2 x xs n acc
        | xs, x, acc => h_3 xs x acc) =
        h_3 xs x acc
-- Lean.Meta.Match.Basic
Lean.Meta.Match.withGoalOf : {α : Type} → Lean.Meta.Match.Problem → Lean.MetaM α → Lean.MetaM α
-- Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring : ∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : IsDiscreteValuationRing A]
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K],
  Subring.map (algebraMap A K) ⊤ =
    (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal A)).valuationSubring.toSubring