mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.baseChange_polynomial : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective 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), (W'.baseChange B).polynomial = (MvPolynomial.map ↑f) (W'.baseChange A).polynomial
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.epsilon_zero_le_of_omega0_opow_le : ∀ {o : Ordinal.{u}}, Ordinal.omega0 ^ o ≤ o → Ordinal.epsilon 0 ≤ o
-- Mathlib.Topology.Path
/-- Pointwise inversion of paths in a topological group.  -/
Path.inv : {X : Type u_1} →
  [inst : TopologicalSpace X] → {a b : X} → [inst_1 : Inv X] → [ContinuousInv X] → Path a b → Path a⁻¹ b⁻¹
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- `(iteration W Z κ).obj (Order.succ j)` identifies to the image of
`(iteration W Z κ).obj j` by `succ`.  -/
CategoryTheory.OrthogonalReflection.iterationObjSuccIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (Z : C) →
        [inst_1 : CategoryTheory.Limits.HasPushouts C] →
          [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
            [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
              [inst_4 :
                  ∀ (Z : C),
                    CategoryTheory.Limits.HasMulticoequalizer
                      (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] →
                (κ : Cardinal.{w}) →
                  [inst_5 : OrderBot κ.ord.ToType] →
                    [inst_6 : CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] →
                      [Fact κ.IsRegular] →
                        (j : κ.ord.ToType) →
                          (CategoryTheory.OrthogonalReflection.iteration W Z κ).obj (Order.succ j) ≅
                            CategoryTheory.OrthogonalReflection.succ W
                              ((CategoryTheory.OrthogonalReflection.iteration W Z κ).obj j)
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.instAdd : {R : Type u_1} →
  {E₁ : Type u_2} →
    {E₂ : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E₁] →
          [inst_2 : PartialOrder E₁] →
            [inst_3 : AddCommMonoid E₂] →
              [inst_4 : PartialOrder E₂] →
                [inst_5 : Module R E₁] → [inst_6 : Module R E₂] → [IsOrderedAddMonoid E₂] → Add (E₁ →ₚ[R] E₂)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `eq_condition f f'`, for morphisms `f f' : j ⟶ j'`, is the proof that
`eqHom f f' ≫ f = eqHom f f' ≫ f'`.
 -/
CategoryTheory.IsCofiltered.eq_condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {j j' : C}
  (f f' : j ⟶ j') {Z : C} (h : j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f')
      (CategoryTheory.CategoryStruct.comp f' h)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.flip_separatingLeft : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁]
  [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M}, B.flip.SeparatingLeft ↔ B.SeparatingRight
-- Mathlib.Data.Fin.VecNotation
Matrix.vecAppend_apply_zero : ∀ {m n : ℕ} {α : Type u_1} {o : ℕ} (ho : o + 1 = m + 1 + n) (u : Fin (m + 1) → α) (v : Fin n → α),
  Matrix.vecAppend ho u v 0 = u 0
-- Mathlib.Data.Nat.BitIndices
Nat.bitIndices_bit_false : ∀ (n : ℕ), (Nat.bit false n).bitIndices = List.map (fun x => x + 1) n.bitIndices
-- Mathlib.Data.Vector.Basic
_private.Mathlib.Data.Vector.Basic.0.List.Vector.ofFn.match_1.splitter : {α : Type u_2} →
  (motive : (x : ℕ) → (Fin x → α) → Sort u_1) →
    (x : ℕ) →
      (x_1 : Fin x → α) →
        ((x : Fin 0 → α) → motive 0 x) → ((n : ℕ) → (f : Fin (n + 1) → α) → motive n.succ f) → motive x x_1
-- Init.Data.List.Nat.Range
List.self_mem_range_succ : ∀ {n : ℕ}, n ∈ List.range (n + 1)
-- Init.Data.List.Lemmas
List.contains_filter : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {x : α} {p : α → Bool},
  (List.filter p l).contains x = l.any fun a => x == a && p a
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.writes.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Fintype Γ] (a : Γ → σ → Γ) (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to1.writes (Turing.TM1.Stmt.write a q) =
    Finset.image (fun a => Turing.TM1to1.Λ'.write a q) Finset.univ ∪ Turing.TM1to1.writes q
-- Init.Core
/-- If a type is a subsingleton, then all of its elements are equal.
 -/
Subsingleton.elim : ∀ {α : Sort u} [h : Subsingleton α] (a b : α), a = b
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.exists_code : ∀ {n : ℕ} {f : List.Vector ℕ n →. ℕ}, Nat.Partrec' f → ∃ c, ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> f v
-- Mathlib.Order.SupClosed
/-- **Alias** of the reverse direction of `isSublattice_preimage_toDual`. -/
IsSublattice.of_dual : ∀ {α : Type u_3} [inst : Lattice α] {s : Set αᵒᵈ}, IsSublattice s → IsSublattice (⇑OrderDual.toDual ⁻¹' s)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.liftEquiv.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P],
  Monoid.Coprod.liftEquiv =
    { toFun := fun fg => Monoid.Coprod.lift fg.1 fg.2,
      invFun := fun f => (f.comp Monoid.Coprod.inl, f.comp Monoid.Coprod.inr), left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- The sequence `stirlingSeq` has a positive lower bound.  -/
Stirling.stirlingSeq'_bounded_by_pos_constant : ∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ Stirling.stirlingSeq (n + 1)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.lift_card_closure_le : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {s : Set M},
  Cardinal.lift.{u, w} (Cardinal.mk ↥((FirstOrder.Language.Substructure.closure L).toFun s)) ≤
    max Cardinal.aleph0
      (Cardinal.lift.{u, w} (Cardinal.mk ↑s) + Cardinal.lift.{w, u} (Cardinal.mk ((i : ℕ) × L.Functions i)))
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_comp_δ'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ j) (CategoryTheory.CategoryStruct.comp (X.δ i) h) =
    CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (CategoryTheory.CategoryStruct.comp (X.δ (j.pred ⋯)) h)
-- Mathlib.Probability.Density
MeasureTheory.hasPDF_of_pdf_ne_zero : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {X : Ω → E},
  (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous μ → ¬MeasureTheory.pdf X ℙ μ =ᵐ[μ] 0 → MeasureTheory.HasPDF X ℙ μ
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (α : F ⟶ G) (a : B) {Z : F.obj a ⟶ G.obj a}
  (h : CategoryTheory.CategoryStruct.comp (α.app a) (G.map (CategoryTheory.CategoryStruct.id a)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.naturality (CategoryTheory.CategoryStruct.id a)).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a).hom (α.app a))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (α.app a)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (α.app a)).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (α.app a) (G.mapId a).inv) h)))
-- Init.Data.Float.Model.Unpacked.Sign
/-- Inductive with two constructors `negative` and `positive` for representing sign bits in
floating-point models. This is not a general-purpose sign type like mathlib's `SignType`,
which also includes a `zero` case.
 -/
Float.Model.UnpackedFloat.Sign : Type
-- Mathlib.SetTheory.Cardinal.Basic
/-- **Alias** of `Cardinal.mk_set_eq_zero_iff`. -/
Cardinal.mk_emptyCollection_iff : ∀ {α : Type u} {s : Set α}, Cardinal.mk ↑s = 0 ↔ s = ∅
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.lift_eval_of : ∀ {α : Type u_1} {M : Type u_4} [inst : Monoid M] (f : α → M) (x : α), (FreeMonoid.lift f) (FreeMonoid.of x) = f x
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WSameSide.congr_simp : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  (s s_1 : AffineSubspace R P),
  s = s_1 → ∀ (x x_1 : P), x = x_1 → ∀ (y y_1 : P), y = y_1 → s.WSameSide x y = s_1.WSameSide x_1 y_1
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.fac_lift_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f) {Z : C} (h : F'.I ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.lift F') h) =
    CategoryTheory.CategoryStruct.comp F'.e h
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- **Canonical decomposition:** A meromorphic function `f` on a disk is equal, up to modification over
a discrete set, to a product of canonical factors and a meromorphic function `g` without zeros or
poles in the interior of the disk.
 -/
MeromorphicOn.exists_canonicalDecomp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ} {f : ℂ → E},
  MeromorphicOn f (Metric.closedBall 0 R) →
    (∀ (u : ↑(Metric.closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤) → ∃ g, Complex.CanonicalDecomp f g R
-- Mathlib.Order.Filter.Extr
IsExtrFilter.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder β] (f : α → β) (l : Filter α) (a : α),
  IsExtrFilter f l a = (IsMinFilter f l a ∨ IsMaxFilter f l a)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix_natCast : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (k : ℕ),
  (↑k).charmatrix = Matrix.diagonal fun x => Polynomial.X - ↑k
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.pure_bind : ∀ {α : Type u_1} {β : Type u_2} (a : α) (f : α → PMF β), (PMF.pure a).bind f = f a
-- Mathlib.Order.InitialSeg
/-- Composition of a principal segment embedding with an initial segment embedding, as a principal
segment embedding  -/
PrincipalSeg.transInitial : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {r : α → α → Prop} →
        {s : β → β → Prop} → {t : γ → γ → Prop} → PrincipalSeg r s → InitialSeg s t → PrincipalSeg r t
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
Dynamics.le_coverEntropyInfEntourage_image : ∀ {X : Type u_1} {Y : Type u_2} {V : SetRel Y Y} {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    ∀ (F : Set X) [V.IsSymm],
      Dynamics.coverEntropyInfEntourage S F (Prod.map φ φ ⁻¹' V.comp V) ≤ Dynamics.coverEntropyInfEntourage T (φ '' F) V
-- Mathlib.Data.Finset.Dedup
List.toFinset_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} (n : l.Nodup), { val := ↑l, nodup := n } = l.toFinset
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.isHomogeneous_monomial : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {d : σ →₀ ℕ} (r : R) {n : ℕ},
  Finsupp.degree d = n → ((MvPolynomial.monomial d) r).IsHomogeneous n
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.summable_exp_nat_mul_of_ge : ∀ {c : ℝ}, c < 0 → ∀ {f : ℕ → ℝ}, (∀ (i : ℕ), ↑i ≤ f i) → Summable fun i => Real.exp (c * f i)
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integrable_const : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} (c : E),
  BoxIntegral.Integrable I l (fun x => c) vol
-- Mathlib.Analysis.Normed.Group.Subgroup
Subgroup.normedGroup : {E : Type u_1} → [inst : NormedGroup E] → {s : Subgroup E} → NormedGroup ↥s
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsBasis'.isRkFinite_of_finite : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α}, M.IsBasis' I X → I.Finite → M.IsRkFinite X
-- Mathlib.CategoryTheory.Types.Basic
/-- Any term `x` of a type `X` corresponds to a morphism `PUnit ⟶ X`.  -/
CategoryTheory.homOfElement : {X : Type u} → X → (PUnit.{u + 1} ⟶ X)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
Topology.IsInducing.polynormableSpace : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : NormedField 𝕜₂] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂}
  [RingHomIsometric σ₁₂] [inst_7 : TopologicalSpace F] [PolynormableSpace 𝕜₂ F] [inst_9 : TopologicalSpace E]
  {f : E →ₛₗ[σ₁₂] F}, Topology.IsInducing ⇑f → PolynormableSpace 𝕜 E
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.TreeMap.Raw.getEntryGE? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → Option (α × β)
-- Mathlib.LinearAlgebra.SymplecticGroup
/-- Symplectic matrices have determinant 1.

The proof strategy comes in two steps:
1. Consider a symplectic matrix `M` over a local ring, we can construct a matrix of the
form `fromBlocks 1 X 0 1` s.t. the upper-left block of `(fromBlocks 1 X 0 1) * M` is invertible.
From this we can calculate the determinant.

2. For a symplectic matrix `M` over general commutative ring `R`, we note that by step 1,
`M.det - 1 = 0` in any localization at a maximal ideal in `R`. Therefore `M.det = 1` in `R`.  -/
SymplecticGroup.det_eq_one : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {M : Matrix (l ⊕ l) (l ⊕ l) R}, M ∈ Matrix.symplecticGroup l R → M.det = 1
-- Mathlib.RingTheory.Ideal.Maps
RingEquivClass.toRingEquiv.congr_simp : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : Mul β] [inst_3 : Add β]
  [inst_4 : EquivLike F α β] [inst_5 : RingEquivClass F α β] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Init.MetaTypes
/-- When `true` (default: `true`), performs zeta reduction of `let` and `have` expressions.
That is, `let x := v; e[x]` reduces to `e[v]`.
If `zetaHave` is `false` then `have` expressions are not zeta reduced.
See also `zetaDelta`.
 -/
Lean.Meta.DSimp.Config.zeta : Lean.Meta.DSimp.Config → Bool
-- Init.Data.Order.Opposite
Max.min_oppositeMin : ∀ {α : Type u_1} {max : Max α} {a b : α}, a ⊓ b = a ⊔ b
-- Mathlib.Data.Semiquot
Semiquot.univ_unique : ∀ {α : Type u_1} (I J : Inhabited α), Semiquot.univ = Semiquot.univ
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.resolution.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  HomotopicalAlgebra.CofibrantObject.HoCat.resolution =
    {
      obj := fun X =>
        HomotopicalAlgebra.CofibrantObject.toHoCat.obj
          (HomotopicalAlgebra.CofibrantObject.mk (HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj X)),
      map := fun {X Y} f =>
        HomotopicalAlgebra.CofibrantObject.toHoCat.map
          (HomotopicalAlgebra.CofibrantObject.homMk (HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap f)),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Order.Category.Semilat
SemilatSupCat.instInhabited : Inhabited SemilatSupCat
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
Std.Tactic.BVDecide.BVPred.bitblast_decl_eq : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (input : Std.Tactic.BVDecide.BVExpr.WithCache Std.Tactic.BVDecide.BVPred aig) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (↑(Std.Tactic.BVDecide.BVPred.bitblast aig input).result).aig.decls.size),
  (↑(Std.Tactic.BVDecide.BVPred.bitblast aig input).result).aig.decls[idx] = aig.decls[idx]
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_succ_right_eq_append_map : ∀ {m n : ℕ}, m ≤ n → (m...n + 1).toArray = #[m] ++ Array.map (fun x => x + 1) (m...n).toArray
-- Init.Data.Prod
Prod.map_id' : ∀ {α : Type u_1} {β : Type u_2}, (Prod.map (fun a => a) fun b => b) = fun x => x
-- Mathlib.CategoryTheory.Limits.IsConnected
/-- Prove that a category is connected by supplying an explicit terminal object.  -/
CategoryTheory.isConnected_of_isTerminal : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {x : C} (h : CategoryTheory.Limits.IsTerminal x),
  CategoryTheory.IsConnected C
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonRefInfo : Lean.ToJson Lean.Lsp.RefInfo
-- Mathlib.Algebra.Group.Defs
/-- Typeclass for expressing that a type `M` with addition and a zero satisfies
`0 + a = a` and `a + 0 = a` for all `a : M`.  -/
AddZeroClass : Type u → Type u
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction.congr_simp : ∀ {α : Type u_1} {f f_1 : α → ℚ → ℝ} (e_f : f = f_1) [inst : MeasurableSpace α]
  (hf : ProbabilityTheory.IsMeasurableRatCDF f) (a a_1 : α), a = a_1 → hf.stieltjesFunction a = ⋯.stieltjesFunction a_1
-- Mathlib.Probability.Decision.Risk.Countable
ProbabilityTheory.avgRisk_const_of_fintype : ∀ {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [inst : Fintype 𝓨] [MeasurableSingletonClass 𝓨],
  Measurable ℓ →
    ∀ (μ : MeasureTheory.Measure 𝓧) (κ : ProbabilityTheory.Kernel 𝓧 𝓨) (π : MeasureTheory.Measure Θ),
      ProbabilityTheory.avgRisk ℓ (ProbabilityTheory.Kernel.const Θ μ) κ π = ∑ y, ∫⁻ (θ : Θ), ℓ θ y * (μ.bind ⇑κ) {y} ∂π
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂CompMap₂Iso_inv_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  {C' : Type u₆} [inst_4 : CategoryTheory.Category.{v₆, u₆} C'] {D' : Type u₅}
  [inst_5 : CategoryTheory.Category.{v₅, u₅} D'] {R : CategoryTheory.Functor C' D'} {F' : CategoryTheory.Functor C' C}
  {G' : CategoryTheory.Functor D' D} {X : D'} (α' : F'.comp S ⟶ R.comp G') (β' : G'.obj X ⟶ T)
  (X_1 : CategoryTheory.CostructuredArrow R X),
  ((CategoryTheory.CostructuredArrow.map₂CompMap₂Iso α β α' β').inv.app X_1).left =
    CategoryTheory.CategoryStruct.id (F.obj (F'.obj X_1.left))
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Recursion principle for `MultiseriesExpansion (basis_hd :: basis_tl)`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.recOn : {basis_hd : ℝ → ℝ} →
  {basis_tl : List (ℝ → ℝ)} →
    {motive : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl) → Sort u_1} →
      ((f : ℝ → ℝ) →
          motive
            (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
              Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil f)) →
        ((exp : ℝ) →
            (coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl) →
              (tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl) →
                (f : ℝ → ℝ) →
                  motive
                    (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
                      (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl) f)) →
          (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)) → motive ms
-- Mathlib.Algebra.Group.AddChar
/-- The trivial additive character (sending everything to `1`).  -/
AddChar.instOne : {A : Type u_1} → {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : Monoid M] → One (AddChar A M)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int32.reduceOfNat : Lean.Meta.Simp.DSimproc
-- Mathlib.Combinatorics.Quiver.Subquiver
Quiver.instInhabitedWideSubquiver : {V : Type u_1} → [inst : Quiver V] → Inhabited (WideSubquiver V)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.rel_mk : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {s : Con R}
  {h : ∀ {w x y z : R}, s.toSetoid w x → s.toSetoid y z → s.toSetoid (w + y) (x + z)} {a b : R},
  { toCon := s, add' := h } a b ↔ s a b
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_inverse_obj : ∀ {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.Cone F.leftOp),
  CategoryTheory.Limits.coneLeftOpOfCoconeEquiv.inverse.obj c = Opposite.op (CategoryTheory.Limits.coconeOfConeLeftOp c)
-- Mathlib.Topology.Algebra.UniformField
CompletableTopField.nice : ∀ {K : Type u_1} {inst : Field K} {inst_1 : UniformSpace K} [self : CompletableTopField K] (F : Filter K),
  Cauchy F → nhds 0 ⊓ F = ⊥ → Cauchy (Filter.map (fun x => x⁻¹) F)
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- A finite family is affinely independent if and only if any affine
combinations (with sum of weights 1) that evaluate to the same point are equal.  -/
affineIndependent_iff_eq_of_fintype_affineCombination_eq : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : Fintype ι] (p : ι → P),
  AffineIndependent k p ↔
    ∀ (w1 w2 : ι → k),
      ∑ i, w1 i = 1 →
        ∑ i, w2 i = 1 →
          (Finset.affineCombination k Finset.univ p) w1 = (Finset.affineCombination k Finset.univ p) w2 → w1 = w2
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.yonedaEquiv_symm_app_objEquiv_symm : ∀ {X : SSet} {n : SimplexCategory} (x : X.obj (Opposite.op n)) {m : SimplexCategoryᵒᵖ} (f : Opposite.unop m ⟶ n),
  (CategoryTheory.ConcreteCategory.hom ((SSet.yonedaEquiv.symm x).app m)) (SSet.stdSimplex.objEquiv.symm f) =
    (CategoryTheory.ConcreteCategory.hom (X.map f.op)) x
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instSMulInt : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] → [inst_1 : SeminormedAddCommGroup β] → SMul ℤ (BoundedContinuousFunction α β)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α}, cmp k k' = Ordering.eq → t.getKey? k = t.getKey? k'
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instIsStableUnderShiftISupShiftOfIsClosedUnderIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderIsomorphisms] (G : Type u_4) [inst_2 : AddGroup G] [inst_3 : CategoryTheory.HasShift C G],
  (⨆ a, P.shift a).IsStableUnderShift G
-- Mathlib.Data.Set.Basic
Set.decidableCompl : {α : Type u} → (s : Set α) → (a : α) → [Decidable (a ∈ s)] → Decidable (a ∈ sᶜ)