mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Equiv
/-- `Fin.consEquiv` as a continuous linear equivalence.  -/
Fin.consEquivL : {n : ℕ} →
  (R : Type u_4) →
    (M : Fin n.succ → Type u_5) →
      [inst : Semiring R] →
        [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] →
          [inst_2 : (i : Fin n.succ) → Module R (M i)] →
            [inst_3 : (i : Fin n.succ) → TopologicalSpace (M i)] →
              (M 0 × ((i : Fin n) → M i.succ)) ≃L[R] (i : Fin n.succ) → M i
-- Lean.Meta.PPGoal
Lean.Meta.pp.showLetValues : Lean.Option Bool
-- Mathlib.Data.Seq.Basic
Stream'.Seq.terminates_map_iff : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Stream'.Seq α}, (Stream'.Seq.map f s).Terminates ↔ s.Terminates
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.singleton_repr : ∀ {ι : Type u_7} {𝕜 : Type u_8} [inst : Unique ι] [inst_1 : RCLike 𝕜] (x : 𝕜) (i : ι),
  ((OrthonormalBasis.singleton ι 𝕜).repr x).ofLp i = x
-- Mathlib.Data.Rat.Cast.Defs
map_nnratCast : ∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : DivisionSemiring α]
  [inst_2 : DivisionSemiring β] [RingHomClass F α β] (f : F) (q : ℚ≥0), f ↑q = ↑q
-- Mathlib.Tactic.GCongr.Core
/-- Return `true` if the priority of `a` is less than or equal to the priority of `b`.  -/
Mathlib.Tactic.GCongr.GCongrLemma.prioLE : Mathlib.Tactic.GCongr.GCongrLemma → Mathlib.Tactic.GCongr.GCongrLemma → Bool
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDerivWithin.eq_1 : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (n : ℕ)
  (f : E → F) (s : Set E),
  iteratedFDerivWithin 𝕜 n f s =
    Nat.recOn (motive := fun x => E → E [×x]→L[𝕜] F) n (fun x => ContinuousMultilinearMap.uncurry0 𝕜 E (f x))
      fun x rec x_1 => (fderivWithin 𝕜 rec s x_1).uncurryLeft
-- Mathlib.LinearAlgebra.StdBasis
Pi.basisFun.congr_simp : ∀ (R : Type u_2) (η : Type u_4) [inst : Semiring R] [inst_1 : Finite η], Pi.basisFun R η = Pi.basisFun R η
-- Mathlib.Order.Northcott
/-- A composition `h' ∘ h` is Northcott when `h'` is Northcott and the fibers of `h` are finite.  -/
Northcott.comp_of_finite_fibers : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α → β) (h' : β → γ) [inst : LE γ] [Northcott h']
  [Filter.TendstoCofinite h], Northcott (h' ∘ h)
-- Mathlib.Algebra.Star.Subalgebra
StarAlgHom.restrictScalars_injective : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  [inst_11 : Star A] [inst_12 : Star B], Function.Injective (StarAlgHom.restrictScalars R)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.sub_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄), (h.sub h').h₁ = h.h₁ - h'.h₁
-- Mathlib.Algebra.Group.Embedding
/-- If left-addition by any element is cancellative, left-addition by `g` is an embedding.  -/
addLeftEmbedding : {G : Type u_1} → [inst : Add G] → [IsLeftCancelAdd G] → G → G ↪ G
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] (g : CompleteLatticeHom β γ) (f : CompleteLatticeHom α β),
  CompleteLatticeHom.dual (g.comp f) = (CompleteLatticeHom.dual g).comp (CompleteLatticeHom.dual f)
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.mapFinIdxM.map.match_1.eq_1 : ∀ {α : Type u_1} (as : Array α) (j : ℕ) (motive : (i : ℕ) → i + j = as.size → Sort u_2) (x : 0 + j = as.size)
  (h_1 : (x : 0 + j = as.size) → motive 0 x) (h_2 : (i : ℕ) → (inv : i + 1 + j = as.size) → motive i.succ inv),
  (match 0, x with
    | 0, x => h_1 x
    | i.succ, inv => h_2 i inv) =
    h_1 x
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallWithContext.ctxt : Lean.Elab.WF.GuessLex.RecCallWithContext → Lean.Elab.WF.GuessLex.SavedLocalContext
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- An initial object is terminal in the opposite category.  -/
CategoryTheory.Limits.terminalOpOfInitial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CategoryTheory.Limits.IsInitial X → CategoryTheory.Limits.IsTerminal (Opposite.op X)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- If a product of a `Finset` of size at most 1 has a given value, so
do the terms in that product.  -/
Finset.eq_of_card_le_one_of_prod_eq : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] {s : Finset ι},
  s.card ≤ 1 → ∀ {f : ι → M} {b : M}, ∏ x ∈ s, f x = b → ∀ x ∈ s, f x = b
-- Mathlib.Order.RelClasses
/-- Set notation form of `le_rfl` -/
subset_rfl : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a : α}, a ⊆ a
-- ProofWidgets.Data.Html
ProofWidgets.instInhabitedHtml.default : ProofWidgets.Html
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_erase_eq_of_not_compare_maxKey!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false →
    ¬compare k t.maxKey! = Ordering.eq → (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.maxKey! = t.maxKey!
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.FunInfoEnvCacheKey : Type
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanFinset_eq_zero : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] {ι : Type u_5} {s : Finset ι} {f : ι → K},
  FractionalIdeal.spanFinset R₁ s f = 0 ↔ ∀ j ∈ s, f j = 0
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrX_mapHomologicalComplexObjXIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] {D : Type u_3} [inst_4 : CategoryTheory.Category.{v_2, u_3} D]
  [inst_5 : CategoryTheory.Preadditive D] (H : CategoryTheory.Functor C D) [inst_6 : H.Additive]
  [inst_7 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)] (i : ι),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX ((H.mapHomologicalComplex c).map φ) i)
      (HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjXIso φ H i).inv =
    H.map (HomologicalComplex.homotopyCofiber.inrX φ i)
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.all.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  s.all pat = (s.skipPrefixWhile pat == s.endPos)
-- Mathlib.Topology.ExtremallyDisconnected
/-- Extremally disconnected spaces are totally separated.  -/
instTotallySeparatedSpaceOfExtremallyDisconnectedOfT2Space : ∀ (X : Type u) [inst : TopologicalSpace X] [ExtremallyDisconnected X] [T2Space X], TotallySeparatedSpace X
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimits F],
  CategoryTheory.Limits.PreservesFiniteLimits F
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Given a limit cone over `X` and `Y`, and another limit cone over `Y` and `X`, we can construct
an isomorphism between the cone points. Relative to some fixed choice of limits cones for every
pair, these isomorphisms constitute a braiding.  -/
CategoryTheory.Limits.BinaryFan.braiding : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {s : CategoryTheory.Limits.BinaryFan X Y} →
        {t : CategoryTheory.Limits.BinaryFan Y X} →
          CategoryTheory.Limits.IsLimit s → CategoryTheory.Limits.IsLimit t → (s.pt ≅ t.pt)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The sum of two weighted homogeneous polynomials of degree `n` is weighted homogeneous of
weighted degree `n`.  -/
MvPolynomial.IsWeightedHomogeneous.add : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  {φ ψ : MvPolynomial σ R} {n : M} {w : σ → M},
  MvPolynomial.IsWeightedHomogeneous w φ n →
    MvPolynomial.IsWeightedHomogeneous w ψ n → MvPolynomial.IsWeightedHomogeneous w (φ + ψ) n
-- Init.Data.UInt.Lemmas
UInt32.lt_iff_toNat_lt : ∀ {a b : UInt32}, a < b ↔ a.toNat < b.toNat
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_div_two : ∀ (x i : ℕ), (x / 2).testBit i = x.testBit (i + 1)
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressOptions.mk : Bool → Lean.Lsp.WorkDoneProgressOptions
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.toGradedObjectFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) {X Y : HomologicalComplex₂ C c₁ c₂}
  (φ : X ⟶ Y) (i : I₁ × I₂),
  (HomologicalComplex₂.toGradedObjectFunctor C c₁ c₂).map φ i = HomologicalComplex₂.toGradedObjectMap φ i
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.opNorm_le_iff : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F}
  {M : ℝ}, 0 ≤ M → (‖f‖ ≤ M ↔ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖)
-- Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
AlgebraicGeometry.Scheme.irreducibleComponentOpen.eq_1 : ∀ (X : AlgebraicGeometry.Scheme) (Z : Set ↥X) [inst : AlgebraicGeometry.IsNoetherian X],
  X.irreducibleComponentOpen Z = { carrier := (⋃₀ (irreducibleComponents ↥X \ {Z}))ᶜ, is_open' := ⋯ }
-- Mathlib.LinearAlgebra.Basis.MulOpposite
MulOpposite.instFiniteDimensional : ∀ {R : Type u_1} {H : Type u_2} [inst : DivisionRing R] [inst_1 : AddCommGroup H] [inst_2 : Module R H]
  [FiniteDimensional R H], FiniteDimensional R Hᵐᵒᵖ
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.algebraPolynomial : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : CommSemiring A] → [Algebra R A] → Algebra (Polynomial R) (PowerSeries A)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
instDecidableEqOrderedFinpartition : {n : ℕ} → DecidableEq (OrderedFinpartition n)
-- Init.Conv
/-- Removes one or more hypotheses from the local context.  -/
Lean.Parser.Tactic.Conv.clear : Lean.ParserDescr
-- Std.Sync.StreamMap
/-- Get a combined selector that returns the stream name and value
 -/
Std.StreamMap.selector : {α β : Type} → Std.StreamMap α β → Std.Async.Async (Std.Async.Selector (α × β))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.map_fst_toArray_eq_keysArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α], Array.map Prod.fst (Std.DHashMap.Const.toArray m) = m.keysArray
-- Mathlib.Algebra.Homology.HomologicalComplexAbelian
HomologicalComplex.shortExact_iff_degreewise_shortExact : ∀ {C : Type u_1} {ι : Type u_2} {c : ComplexShape ι} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (HomologicalComplex C c)),
  S.ShortExact ↔ ∀ (i : ι), (S.map (HomologicalComplex.eval C c i)).ShortExact
-- Lean.Linter.MissingDocs
_private.Lean.Linter.MissingDocs.0.Lean.Linter.MissingDocs.lintDocStatusField : Bool → Lean.Syntax → Lean.Syntax → String → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.addCommutator_upperCentralSeries_top_le : ∀ (G : Type u_1) [inst : AddGroup G] (n : ℕ),
  ⁅AddSubgroup.upperCentralSeries G (n + 1), ⊤⁆ ≤ AddSubgroup.upperCentralSeries G n
-- Mathlib.Topology.ContinuousMap.Basic
/-- The restriction of a continuous function `α → β` to a subset `s` of `α`.  -/
ContinuousMap.restrict : {α : Type u_1} →
  {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → (s : Set α) → C(α, β) → C(↑s, β)
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_mul : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (p q : ℕ) (φ : MvPolynomial σ R),
  (MvPolynomial.expand (p * q)) φ = (MvPolynomial.expand p) ((MvPolynomial.expand q) φ)
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- Two polynomials `p` and `q` such that `p(q(X))=X` and `q(p(X))=X`
induces an automorphism of the polynomial algebra.  -/
Polynomial.algEquivOfCompEqX : {R : Type u} →
  [inst : CommSemiring R] →
    (p q : Polynomial R) → p.comp q = Polynomial.X → q.comp p = Polynomial.X → Polynomial R ≃ₐ[R] Polynomial R
-- Mathlib.Logic.Equiv.Basic
Equiv.swapCore_swapCore : ∀ {α : Sort u_1} [inst : DecidableEq α] (r a b : α), Equiv.swapCore a b (Equiv.swapCore a b r) = r
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- In the characteristic zero case, the weights in the centroid sum
to 1 if the set is nonempty.  -/
Finset.sum_centroidWeights_eq_one_of_nonempty : ∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [CharZero k],
  s.Nonempty → ∑ i ∈ s, Finset.centroidWeights k s i = 1
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- Let `s` be a subset of an additive monoid `M` such that the closure of `s` is
the whole monoid. Then `AddMonoidHom.ofClosureEqTopLeft` defines an additive monoid
homomorphism from `M` asking for a proof of `f (x + y) = f x + f y` only for `x ∈ s`.  -/
AddMonoidHom.ofClosureMEqTopLeft : {M : Type u_4} →
  {N : Type u_5} →
    [inst : AddMonoid M] →
      [inst_1 : AddMonoid N] →
        {s : Set M} →
          (f : M → N) → AddSubmonoid.closure s = ⊤ → f 0 = 0 → (∀ x ∈ s, ∀ (y : M), f (x + y) = f x + f y) → M →+ N
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.reflectsLimitsOfShape_of_initial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄}
  [inst_4 : CategoryTheory.Category.{v₄, u₄} B] (H : CategoryTheory.Functor E B)
  [CategoryTheory.Limits.ReflectsLimitsOfShape C H], CategoryTheory.Limits.ReflectsLimitsOfShape D H
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn.IsCompatible.ι_desc : ∀ {n : ℕ} {X : SSet} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)}
  (hf : SSet.horn.IsCompatible f) (j : Fin (n + 2)) (hj : j ≠ i),
  CategoryTheory.CategoryStruct.comp (SSet.horn.ι i j hj) hf.desc = f j hj
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.mul_toMatrix' : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (B : LinearMap.BilinForm R₁ (n → R₁)) (M : Matrix n n R₁),
  M * LinearMap.BilinForm.toMatrix' B = LinearMap.BilinForm.toMatrix' (B.compLeft (Matrix.toLin' M.transpose))
-- Mathlib.Order.Interval.Set.ProjIcc
Set.coe_projIci : ∀ {α : Type u_1} [inst : LinearOrder α] (a x : α), ↑(Set.projIci a x) = max a x
-- Mathlib.Topology.MetricSpace.Congruence
/-- A congruence between indexed sets of vertices v₁ and v₂.
Use `open scoped Congruent` to access the `v₁ ≅ v₂` notation.  -/
Congruent.«term_≅_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Sites.Adjunction
/-- **Alias** of `CategoryTheory.Sheaf.adjunction_unit_app_hom`. -/
CategoryTheory.Sheaf.adjunction_unit_app_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [inst_3 : CategoryTheory.HasWeakSheafify J D]
  [inst_4 : J.HasSheafCompose F] (adj : G ⊣ F) (X : CategoryTheory.Sheaf J E),
  ((CategoryTheory.Sheaf.adjunction J adj).unit.app X).hom =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.obj)
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J (X.obj.comp G)) F)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {k : α}, ∅.contains k = false
-- Mathlib.Order.Heyting.Hom
CoheytingHom.instCoheytingHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β],
  CoheytingHomClass (CoheytingHom α β) α β
-- Mathlib.Data.Int.GCD
Int.exists_gcd_one' : ∀ {m n : ℤ}, 0 < m.gcd n → ∃ g m' n', 0 < g ∧ m'.gcd n' = 1 ∧ m = m' * ↑g ∧ n = n' * ↑g
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.Decidable.instToBackwardSearcherForallCharPropDefaultBackwardSearcherForallBoolDecide : {p : Char → Prop} →
  [inst : DecidablePred p] →
    String.Slice.Pattern.ToBackwardSearcher p
      (String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher fun x => decide (p x))
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.single_sub : ∀ {ι : Type u} [inst : DecidableEq ι] {β : ι → Type v} [inst_1 : (i : ι) → AddGroup (β i)] (i : ι) (x y : β i),
  (fun₀ | i => x - y) = (fun₀ | i => x) - fun₀ | i => y
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimitsOfShape_of_hasLimitsOfShape_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ Cᵒᵖ], CategoryTheory.Limits.HasColimitsOfShape J C
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM : Type → Type
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.containsThenInsertIfNew : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k} (a : t.WF),
  Std.DTreeMap.Internal.Impl.WF.below a → motive t a → Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.le_liftLinear_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β}
  (hf : ∀ (μ : MeasureTheory.Measure α), mβ ≤ (f μ.toOuterMeasure).caratheodory) (s : Set β),
  (f μ.toOuterMeasure) s ≤ ((MeasureTheory.Measure.liftLinear f hf) μ) s
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction_sub_one_lt : ∀ {pat : ByteArray} {stackPos : ℕ} {hst : stackPos - 1 < pat.size},
  0 < stackPos → String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat (stackPos - 1) hst < stackPos
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.IterM.toArray_flatMap : ∀ {α α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [inst_5 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α m]
  [Std.Iterators.Finite α₂ m] [inst_8 : Std.Iterator α m β] [inst_9 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α m]
  [Std.Iterators.Finite α₂ m] {f : β → Std.IterM m γ} {it₁ : Std.IterM m β},
  (Std.IterM.flatMap f it₁).toArray = Array.flatten <$> (Std.IterM.mapM (fun b => (f b).toArray) it₁).toArray
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.symm : ∀ {p q r : ENNReal} [hpqr : p.HolderTriple q r], q.HolderTriple p r
-- Init.Data.Array.Lemmas
/-- Variant of `filter_reverse` with a hypothesis giving the stop condition.  -/
Array.filter_reverse' : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} {stop : ℕ},
  stop = xs.size → Array.filter p xs.reverse 0 stop = (Array.filter p xs).reverse
-- Init.Data.Range.Polymorphic.Nat
Std.PRange.instUpwardEnumerableNat : Std.PRange.UpwardEnumerable ℕ
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddCommMonoid : {M : Type u_1} →
  [inst : TopologicalSpace M] → [inst_1 : AddCommMonoid M] → [ContinuousAdd M] → AddCommMonoid (SeparationQuotient M)
-- Mathlib.Topology.Algebra.Valued.WithVal
Equiv.setCongr.eq_1 : ∀ {α : Type u_3} {s t : Set α} (h : s = t), Equiv.setCongr h = Equiv.subtypeEquivProp ⋯
-- Mathlib.RingTheory.Derivation.MapCoeffs
Differential.deriv_aeval_eq_implicitDeriv : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A] {R : Type u_2} [inst_2 : CommRing R]
  [inst_3 : Differential R] [inst_4 : Algebra A R] [DifferentialAlgebra A R] (x : R) (v : Polynomial A),
  x′ = (Polynomial.aeval x) v →
    ∀ (p : Polynomial A), ((Polynomial.aeval x) p)′ = (Polynomial.aeval x) ((Differential.implicitDeriv v) p)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem_toList_roc : ∀ {m n : ℤ} {i : ℕ} (_h : i < (m<...=n).toList.length), (m<...=n).toList[i] = m + 1 + ↑i
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_zsmul : ∀ {R : Type u} [inst : Ring R] (a : ℤ) (b : AddMonoidAlgebra R ℕ), { toFinsupp := a • b } = a • { toFinsupp := b }
-- Mathlib.Topology.Algebra.AsymptoticCone
asymptoticCone_submodule : ∀ {k : Type u_1} {V : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : TopologicalSpace V] [inst_5 : TopologicalSpace k] [OrderTopology k]
  [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Submodule k V},
  asymptoticCone k ↑s = closure ↑s
-- Mathlib.Topology.Gluing
TopCat.GlueData.MkCore.mk.injEq : ∀ {J : Type u} (U : J → TopCat) (V : (i : J) → J → TopologicalSpace.Opens ↑(U i))
  (t :
    (i j : J) →
      (TopologicalSpace.Opens.toTopCat (U i)).obj (V i j) ⟶ (TopologicalSpace.Opens.toTopCat (U j)).obj (V j i))
  (V_id : ∀ (i : J), V i i = ⊤) (t_id : ∀ (i : J), ⇑(CategoryTheory.ConcreteCategory.hom (t i i)) = id)
  (t_inter :
    ∀ ⦃i j : J⦄ (k : J) (x : ↥(V i j)), ↑x ∈ V i k → ↑((CategoryTheory.ConcreteCategory.hom (t i j)) x) ∈ V j k)
  (cocycle :
    ∀ (i j k : J) (x : ↥(V i j)) (h : ↑x ∈ V i k),
      ↑((CategoryTheory.ConcreteCategory.hom (t j k)) ⟨↑((CategoryTheory.ConcreteCategory.hom (t i j)) x), ⋯⟩) =
        ↑((CategoryTheory.ConcreteCategory.hom (t i k)) ⟨↑x, h⟩))
  (J_1 : Type u) (U_1 : J_1 → TopCat) (V_1 : (i : J_1) → J_1 → TopologicalSpace.Opens ↑(U_1 i))
  (t_1 :
    (i j : J_1) →
      (TopologicalSpace.Opens.toTopCat (U_1 i)).obj (V_1 i j) ⟶ (TopologicalSpace.Opens.toTopCat (U_1 j)).obj (V_1 j i))
  (V_id_1 : ∀ (i : J_1), V_1 i i = ⊤) (t_id_1 : ∀ (i : J_1), ⇑(CategoryTheory.ConcreteCategory.hom (t_1 i i)) = id)
  (t_inter_1 :
    ∀ ⦃i j : J_1⦄ (k : J_1) (x : ↥(V_1 i j)),
      ↑x ∈ V_1 i k → ↑((CategoryTheory.ConcreteCategory.hom (t_1 i j)) x) ∈ V_1 j k)
  (cocycle_1 :
    ∀ (i j k : J_1) (x : ↥(V_1 i j)) (h : ↑x ∈ V_1 i k),
      ↑((CategoryTheory.ConcreteCategory.hom (t_1 j k)) ⟨↑((CategoryTheory.ConcreteCategory.hom (t_1 i j)) x), ⋯⟩) =
        ↑((CategoryTheory.ConcreteCategory.hom (t_1 i k)) ⟨↑x, h⟩)),
  ({ J := J, U := U, V := V, t := t, V_id := V_id, t_id := t_id, t_inter := t_inter, cocycle := cocycle } =
      { J := J_1, U := U_1, V := V_1, t := t_1, V_id := V_id_1, t_id := t_id_1, t_inter := t_inter_1,
        cocycle := cocycle_1 }) =
    (J = J_1 ∧ U ≍ U_1 ∧ V ≍ V_1 ∧ t ≍ t_1)
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.isOpenMap_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsOpenEmbedding g → (IsOpenMap f ↔ IsOpenMap (g ∘ f))