mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiconeMorphism.mk.congr_simp : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (hom hom_1 : A.pt ⟶ B.pt) (e_hom : hom = hom_1)
  (wfst : CategoryTheory.CategoryStruct.comp hom B.fst = A.fst)
  (wsnd : CategoryTheory.CategoryStruct.comp hom B.snd = A.snd)
  (winl : CategoryTheory.CategoryStruct.comp A.inl hom = B.inl)
  (winr : CategoryTheory.CategoryStruct.comp A.inr hom = B.inr),
  { hom := hom, wfst := wfst, wsnd := wsnd, winl := winl, winr := winr } =
    { hom := hom_1, wfst := ⋯, wsnd := ⋯, winl := ⋯, winr := ⋯ }
-- Mathlib.Data.Set.Finite.Lattice
Set.Finite.iSup_biInf_of_monotone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Preorder ι'] [Nonempty ι'] [IsDirectedOrder ι']
  [inst_3 : Order.Frame α] {s : Set ι},
  s.Finite → ∀ {f : ι → ι' → α}, (∀ i ∈ s, Monotone (f i)) → ⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j
-- Lean.Parser.Basic
/-- Generate an error at the position saved with the `withPosition` combinator.
If `delta == true`, then it reports at saved position+1.
This useful to make sure a parser consumed at least one character.   -/
Lean.Parser.errorAtSavedPos : String → Bool → Lean.Parser.Parser
-- Std.Data.ExtDHashMap.Lemmas
/-- Variant of `get_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.ExtDHashMap.Const.get_map' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α} {h' : k ∈ Std.ExtDHashMap.map f m},
  Std.ExtDHashMap.Const.get (Std.ExtDHashMap.map f m) k h' = f (m.getKey k ⋯) (Std.ExtDHashMap.Const.get m k ⋯)
-- Mathlib.RingTheory.Multiplicity
emultiplicity_zero_eq_zero_of_ne_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α] (a : α), a ≠ 0 → emultiplicity 0 a = 0
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_sup_distrib_right : ∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α),
  s.inf' hs f ⊔ a = s.inf' hs fun i => f i ⊔ a
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- **Alias** of `AEMeasurable.add`. -/
AEMeasurable.add' : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α} {f g : α → M}
  {μ : MeasureTheory.Measure α} [MeasurableAdd₂ M], AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f + g) μ
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsUniformizer.val_lt_one : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] {v : Valuation A Γ}
  [hv : v.IsRankOneDiscrete] {π : A}, v.IsUniformizer π → v π < 1
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_two_mul_eq_one_sub : ∀ (x : ℝ), Real.cos (2 * x) = 1 - 2 * Real.sin x ^ 2
-- Mathlib.Order.Comparable
/-- Exactly one of the following is true.  -/
lt_or_eq_or_gt_or_incompRel : ∀ {α : Type u_1} [inst : PartialOrder α] (a b : α), a < b ∨ a = b ∨ b < a ∨ IncompRel (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulOneClass α] [inst_4 : MulOneClass β] [inst_5 : MulOneClass γ] (f : β →*o γ) (g : α →*o β) (a : α),
  (f.comp g) a = f (g a)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_eq_singleton_append_iff : ∀ {xs : Array ℕ} {m n a : ℕ}, (m...=n).toArray = #[a] ++ xs ↔ m = a ∧ m ≤ n ∧ ((m + 1)...=n).toArray = xs
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticForm.equivalent_weightedSumSquares : ∀ {K : Type u_3} {V : Type u_8} [inst : Field K] [Invertible 2] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [FiniteDimensional K V] (Q : QuadraticForm K V), ∃ w, QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K w)
-- Lean.Meta.Basic
/-- `backDeps` contains the backwards dependencies. That is, the (0-indexed) position of previous parameters that this one depends on.  -/
Lean.Meta.ParamInfo.backDeps : Lean.Meta.ParamInfo → Array ℕ
-- Mathlib.Order.Types.Defs
OrderType.instNontrivial : Nontrivial OrderType.{u}
-- Mathlib.Geometry.Euclidean.Triangle
/-- The least angle of a possibly degenerate triangle is at most `π / 3`, unless all three vertices
are equal.  -/
EuclideanGeometry.angle_le_pi_div_three_of_le_of_le : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ ≤ EuclideanGeometry.angle p₂ p₃ p₁ →
    EuclideanGeometry.angle p₁ p₂ p₃ ≤ EuclideanGeometry.angle p₃ p₁ p₂ →
      p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃ → EuclideanGeometry.angle p₁ p₂ p₃ ≤ Real.pi / 3
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.comp_toNatTrans : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {F G H : CategoryTheory.BasedFunctor 𝒳 𝒴} (α : CategoryTheory.BasedNatTrans F G)
  (β : CategoryTheory.BasedNatTrans G H), (α.comp β).toNatTrans = α.vcomp β.toNatTrans
-- Init.Data.Array.Lemmas
Option.getD.eq_2 : ∀ {α : Type u_1} (dflt : α), none.getD dflt = dflt
-- Mathlib.LinearAlgebra.Dimension.Free
/-- **Alias** of the reverse direction of `Module.nonempty_linearEquiv_iff_finrank_eq_one`.

---

See also `finrank_eq_one_iff`  -/
Module.nonempty_linearEquiv_of_finrank_eq_one : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [StrongRankCondition R], Module.finrank R M = 1 → Nonempty (R ≃ₗ[R] M)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanSingleton_eq_spanSingleton : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] [IsDomain R] [Module.IsTorsionFree R P] {x y : P},
  FractionalIdeal.spanSingleton S x = FractionalIdeal.spanSingleton S y ↔ ∃ z, z • x = y
-- Mathlib.Order.Filter.Basic
Filter.Eventually.choice : ∀ {α : Type u} {β : Type v} {r : α → β → Prop} {l : Filter α} [l.NeBot],
  (∀ᶠ (x : α) in l, ∃ y, r x y) → ∃ f, ∀ᶠ (x : α) in l, r x (f x)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instAddZeroClass : {M : Type u_2} →
  {N : Type u_3} →
    {X : Type u_4} →
      {Y : Type u_5} →
        {σ : M → N} →
          [inst : SMul M X] → [inst_1 : AddZeroClass Y] → [inst_2 : DistribSMul N Y] → AddZeroClass (X →ₑ[σ] Y)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prodFunctorToFunctorProd_obj : ∀ (A : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (C : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B × CategoryTheory.Functor A C),
  (CategoryTheory.prodFunctorToFunctorProd A B C).obj F = F.1.prod' F.2
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_image_of_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set α), Nat.card ↑(f '' s) = Nat.card ↑s
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.normUnit_content : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p : Polynomial R}, normUnit p.content = 1
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Under.instHasInitialTopOfContainsIdentities : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T)
  [P.ContainsIdentities], CategoryTheory.Limits.HasInitial (P.Under ⊤ X)
-- Mathlib.Order.Interval.Finset.Nat
List.toFinset_range'_1 : ∀ (a b : ℕ), (List.range' a b).toFinset = Finset.Ico a (a + b)
-- Init.Data.SInt.Lemmas
ISize.cast_toNatClampNeg : ∀ (x : ISize), 0 ≤ x → ↑x.toNatClampNeg = x.toInt
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.fibration_unop_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y : Cᵒᵖ} (f : X ⟶ Y), HomotopicalAlgebra.Fibration f.unop ↔ HomotopicalAlgebra.Cofibration f
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- If `m₁ d ≤ m₂ d` for `d < ε` for some `ε > 0` (we use `≤ᶠ[𝓝 0]` to state this), then
`mkMetric m₁ hm₁ ≤ mkMetric m₂ hm₂`.  -/
MeasureTheory.Measure.mkMetric_mono : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
  {m₁ m₂ : ENNReal → ENNReal}, m₁ ≤ᶠ[nhds 0] m₂ → MeasureTheory.Measure.mkMetric m₁ ≤ MeasureTheory.Measure.mkMetric m₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combine.go.eq_1 : ∀ (p₁ p₂ : Lean.Grind.CommRing.Poly), Lean.Grind.CommRing.Poly.combine.go 0 p₁ p₂ = p₁.concat p₂
-- Mathlib.Algebra.Torsor.Defs
/-- The permutation given by `p ↦ v • p`.  -/
Equiv.constSMul : {G : Type u_1} → (P : Type u_2) → [inst : Group G] → [Torsor G P] → G → Equiv.Perm P
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_def : ∀ (n : ℤ), n.negOnePow = (-1) ^ n
-- Lean.Elab.Command
Lean.Elab.Command.Context.currRecDepth : Lean.Elab.Command.Context → ℕ
-- Mathlib.Analysis.Normed.Group.Constructions
/-- The seminorm of an element in a product space is `< r` if and only if the norm of each
component is.  -/
pi_norm_lt_iff' : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (G i)] {x : (i : ι) → G i}
  {r : ℝ}, 0 < r → (‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r)
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductCone_pt : ∀ (X Y : Type u), (CategoryTheory.Limits.Types.binaryProductCone X Y).pt = (X × Y)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map'_comp_π_assoc : ∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct g] (p : β → α)
  (q : (b : β) → f (p b) ⟶ g b) (b : β) {Z : C} (h : g b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (p b)) (CategoryTheory.CategoryStruct.comp (q b) h)
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.div_self : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α}, IsUnit a → a / a = 1
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.opHomeomorph_symm_apply : ∀ {M : Type u_1} [inst : TopologicalSpace M] (a : Mᵐᵒᵖ), MulOpposite.opHomeomorph.symm a = MulOpposite.unop a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHom.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {p p_1 : A → Prop} (e_p : p = p_1) [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A]
  [inst_6 : Ring A] [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A}
  (ha : p a), cfcHom ha = cfcHom ⋯
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramProps.embeds : ProofWidgets.Penrose.DiagramProps → Array (String × ProofWidgets.Html)
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
ArithmeticFunction.carmichael_mul : ∀ {a b : ℕ},
  a.Coprime b →
    ArithmeticFunction.carmichael (a * b) = (ArithmeticFunction.carmichael a).lcm (ArithmeticFunction.carmichael b)
-- Mathlib.Algebra.Order.Field.Basic
/-- A version of `inv_nonpos` which holds with different assumptions. In particular, the type
must be a field, not just a `GroupWithZero`, but the order assumptions replace `LinearOrder` and
`PosMulMono` with `PartialOrder`, `IsStrictOrderedRing` and `PosMulReflectLT`. Thus neither version
is more general than the other. This one applies, for instance, to `ℂ`.  -/
inv_nonpos' : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a : α},
  a⁻¹ ≤ 0 ↔ a ≤ 0
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.CofixA.intro : {F : PFunctor.{uA, uB}} → {n : ℕ} → (a : F.A) → (F.B a → PFunctor.Approx.CofixA F n) → PFunctor.Approx.CofixA F n.succ
-- Init.Data.Dyadic.Instances
Dyadic.instOrderedRing : Lean.Grind.OrderedRing Dyadic
-- Std.Http.Server.Connection
/-- Handles request/response processing for a single connection using an `Async` handler.
The library-level entry point for running a server is `Server.serve`.
This function can be used with a `TCP.Socket` or any other type that implements
`Transport` to build custom server loops.

# Example

```lean
-- Create a TCP socket server instance
let server ← Socket.Server.mk
server.bind addr
server.listen backlog

-- Enter an infinite loop to handle incoming client connections
while true do
  let client ← server.accept
  background (serveConnection client handler config)
```
 -/
Std.Http.Server.serveConnection : {t σ : Type} →
  [Std.Http.Transport t] →
    [Std.Http.Server.Handler σ] →
      t → σ → Std.Http.Config → optParam Std.Http.Extensions Std.Http.Extensions.empty → Std.Async.ContextAsync Unit
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_inf_leOnePart_eq_one : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] (a : α), a⁺ᵐ ⊓ a⁻ᵐ = 1
-- Std.Http.Data.URI.Basic
/-- Sets the port number.
 -/
Std.Http.URI.Builder.setPort : Std.Http.URI.Builder → UInt16 → Std.Http.URI.Builder
-- Mathlib.Analysis.Normed.Group.Quotient
Submodule.Quotient.seminormedAddCommGroup : {M : Type u_1} →
  [inst : SeminormedAddCommGroup M] →
    {R : Type u_3} → [inst_1 : Ring R] → [inst_2 : Module R M] → (S : Submodule R M) → SeminormedAddCommGroup (M ⧸ S)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.iterate_derivative_T_eval_zero_recurrence : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ) (k : ℕ),
  Polynomial.eval 0 ((⇑Polynomial.derivative)^[k + 2] (Polynomial.Chebyshev.T R n)) =
    -(↑n ^ 2 - ↑k ^ 2) * Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T R n))
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_self_ne_zero : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [cd : InnerProductSpace.Core 𝕜 F] {x : F}, inner 𝕜 x x ≠ 0 ↔ x ≠ 0
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.CanonicallyOverClass.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {S : semiOutParam C} → [toOverClass : CategoryTheory.OverClass X S] → CategoryTheory.CanonicallyOverClass X S
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.instIsAddRightInvariantHausdorffMeasureOfIsIsometricVAddAddOpposite : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {d : ℝ}
  [inst_3 : AddGroup X] [IsIsometricVAdd Xᵃᵒᵖ X], (MeasureTheory.Measure.hausdorffMeasure d).IsAddRightInvariant
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.addConst_k_eq_addConst : ∀ (p : Lean.Grind.CommRing.Poly) (k : ℤ), p.addConst_k k = p.addConst k
-- Lean.Meta.Tactic.LibrarySearch
/-- Process-global cache for the imported-declarations discrimination tree. This must *not* live in
an environment extension: the snapshot used by `--incr-load` compacts the whole environment object
(including non-persistent extension state), and a mutable `IO.Ref` baked into the read-only mapped
region is unsound to read or write. A process-global ref is rebuilt per process instead.  -/
_private.Lean.Meta.Tactic.LibrarySearch.0.Lean.Meta.LibrarySearch.ext : IO.Ref (Option (Lean.Meta.LazyDiscrTree (Lean.Name × Lean.Meta.LibrarySearch.DeclMod)))
-- Mathlib.Data.Fintype.Fin
Fin.map_valEmbedding_univ : ∀ {n : ℕ}, Finset.map Fin.valEmbedding Finset.univ = Finset.Iio n
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
MulRingNorm.mulRingNormEquivAbsoluteValue.congr_simp : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : Nontrivial R],
  MulRingNorm.mulRingNormEquivAbsoluteValue = MulRingNorm.mulRingNormEquivAbsoluteValue
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
_private.Mathlib.Tactic.CategoryTheory.Coherence.Normalize.0.Mathlib.Tactic.BicategoryLike.evalComp.match_1.splitter : (motive : Mathlib.Tactic.BicategoryLike.Eval.Result → Sort u_1) →
  (x : Mathlib.Tactic.BicategoryLike.Eval.Result) →
    ((ι : Mathlib.Tactic.BicategoryLike.NormalExpr) → (e_ι : Lean.Expr) → motive { expr := ι, proof := e_ι }) → motive x
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.ensureExtensionsArraySize.loop : ℕ → Array Lean.EnvExtensionState → IO (Array Lean.EnvExtensionState)
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.differentiableAt_mulExpNegMulSq : ∀ {ε : ℝ} (y : ℝ), DifferentiableAt ℝ ε.mulExpNegMulSq y
-- Mathlib.RingTheory.Perfectoid.BDeRham
_private.Mathlib.RingTheory.Perfectoid.BDeRham.0.term𝕎_ : Lean.ParserDescr
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The Coxeter group associated to a Coxeter matrix $M$; that is, the group
$$\langle \{s_i\}_{i \in B} \vert \{(s_i s_{i'})^{M_{i, i'}}\}_{i, i' \in B} \rangle.$$  -/
CoxeterMatrix.Group : {B : Type u_1} → CoxeterMatrix B → Type u_1
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.coe_inv_of_ne_zero : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {J : FractionalIdeal (nonZeroDivisors R₁) K},
  J ≠ 0 → ↑J⁻¹ = IsLocalization.coeSubmodule K ⊤ / ↑J
-- Init.Prelude
HShiftRight.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → HShiftRight α β γ
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.weightEquiv_comp_toLin : ∀ {ι : 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} (x y : P.Equiv P),
  RootPairing.Equiv.weightEquiv P P (x.comp y) =
    RootPairing.Equiv.weightEquiv P P y ≪≫ₗ RootPairing.Equiv.weightEquiv P P x
-- Init.Grind.ToInt
Lean.Grind.IntInterval.nonEmpty_of_mem : ∀ {x : ℤ} {i : Lean.Grind.IntInterval}, x ∈ i → i.nonEmpty = true
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Finset.aestronglyMeasurable_prod : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [inst : CommMonoid M]
  [inst_1 : TopologicalSpace M] [ContinuousMul M] {ι : Type u_6} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) → MeasureTheory.AEStronglyMeasurable (∏ i ∈ s, f i) μ
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorAlgebra.ofDirectSum_comp_toDirectSum : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  TensorAlgebra.ofDirectSum.comp TensorAlgebra.toDirectSum = AlgHom.id R (TensorAlgebra R M)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.sSup_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {c : Set (E →ₛₗ.[σ] F)}
  (hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c) {l : E →ₛₗ.[σ] F} (hl : l ∈ c) (x : ↥l.domain),
  ↑(LinearPMap.sSup c hc) ⟨↑x, ⋯⟩ = ↑l x
-- Mathlib.RepresentationTheory.Action
Representation.linearizeMap.eq_1 : ∀ {k : Type u} {G : Type v} [inst : Monoid G] [inst_1 : Semiring k] {X Y : Action (Type w) G} (f : X ⟶ Y),
  Representation.linearizeMap f =
    { toLinearMap := MonoidAlgebra.mapDomainLinearMap k k ⇑(CategoryTheory.ConcreteCategory.hom f.hom),
      isIntertwining' := ⋯ }
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The canonical projection on the base object.  -/
CategoryTheory.SmallObject.π'FunctorObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S X : C} →
            (πX : X ⟶ S) →
              [inst_1 :
                  CategoryTheory.Limits.HasColimitsOfShape
                    (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
                ∐ CategoryTheory.SmallObject.functorObjTgtFamily f πX ⟶ S
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.NatIso.prod_hom : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {F F' : CategoryTheory.Functor A B} {G G' : CategoryTheory.Functor C D}
  (e₁ : F ≅ F') (e₂ : G ≅ G'), (CategoryTheory.NatIso.prod e₁ e₂).hom = CategoryTheory.NatTrans.prod e₁.hom e₂.hom
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.sum_coord_apply_eq_one : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) [inst_4 : Fintype ι] (q : P), ∑ i, (b.coord i) q = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The proposition that a Jacobian point representative `(x, y, z)` on a Weierstrass curve `W` is
nonsingular.

In other words, either `W_X(x, y, z) ≠ 0`, `W_Y(x, y, z) ≠ 0`, or `W_Z(x, y, z) ≠ 0`.

Note that this definition is only mathematically accurate for fields.  -/
WeierstrassCurve.Jacobian.Nonsingular : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → Prop
-- Qq.Macro
Qq.Impl.ExprBackSubstResult.unquoted.injEq : ∀ (e e_1 : Lean.Expr), (Qq.Impl.ExprBackSubstResult.unquoted e = Qq.Impl.ExprBackSubstResult.unquoted e_1) = (e = e_1)
-- Lean.DocString.Parser
Lean.Doc.Parser.instReprUnorderedListType : Repr Lean.Doc.Parser.UnorderedListType
-- Mathlib.Order.Hom.Basic
OrderIso.coe_toEquiv : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), ⇑e.toEquiv = ⇑e
-- Mathlib.GroupTheory.Goursat
/-- **Goursat's lemma** for an arbitrary subgroup.

If `I` is a subgroup of `G × H`, then there exist subgroups `G' ≤ G`, `H' ≤ H` and normal subgroups
`M ⊴ G'` and `N ⊴ H'` such that `M × N ≤ I` and the image of `I` in `G' ⧸ M × H' ⧸ N` is the graph
of an isomorphism `G' ⧸ M ≃ H' ⧸ N`.  -/
Subgroup.goursat : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {I : Subgroup (G × H)},
  ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          Subgroup.map (G'.subtype.prodMap H'.subtype)
            (Subgroup.comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.toCompositionAsSet_blocks : ∀ {n : ℕ} (c : Composition n), c.toCompositionAsSet.blocks = c.blocks
-- Init.Data.List.Zip
List.map_prod_left_eq_zip : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β}, List.map (fun x => (x, f x)) l = l.zip (List.map f l)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.fold_filterM : ∀ {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [inst_5 : MonadAttach n]
  [WeaklyLawfulMonadAttach n] [inst_7 : Std.Internal.Do.Assertion Pred] [inst_8 : Std.Internal.Do.Assertion EPred]
  [inst_9 : Std.Internal.Do.WPMonad n Pred EPred] [inst_10 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_12 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (ULift.{w, 0} Bool)} {g : δ → β → δ} {init : δ}
  {it : Std.IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.IterM.foldM
        (fun d b => do
          let __do_lift ← f b
          pure (if __do_lift.down = true then g d b else d))
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.IterM.filterM f it) ⦃ Q; eQ ⦄
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `insertMin` which can be used in the absence of balance information but
still assumes the preconditions of `insertMin`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.insertMin! : {α : Type u} → {β : α → Type v} → (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β