mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.mem_pointwise_smul_iff_inv_smul_mem₀ : ∀ {M : Type u_1} {R : Type u_2} [inst : GroupWithZero M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M},
  a ≠ 0 → ∀ (S : Subsemiring R) (x : R), x ∈ a • S ↔ a⁻¹ • x ∈ S
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.iSupLift.congr_simp : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : IsScalarTower R A A]
  [inst_6 : SMulCommClass R A A] {ι : Sort u_1} [inst_7 : Nonempty ι] (K : ι → NonUnitalSubalgebra R A)
  (dir : Directed (fun x1 x2 => x1 ≤ x2) K) (f f_1 : (i : ι) → ↥(K i) →ₙₐ[R] B) (e_f : f = f_1)
  (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)) (T : NonUnitalSubalgebra R A)
  (hT : T = iSup K), NonUnitalSubalgebra.iSupLift K dir f hf T hT = NonUnitalSubalgebra.iSupLift K dir f_1 ⋯ T hT
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_insertEntry_of_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {k : α} {v : β k} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = true → Std.Internal.List.minKey! (Std.Internal.List.insertEntry k v l) = k
-- Init.Tactics
/-- `with_reducible_and_instances tacs` executes `tacs` using the `.instances` transparency setting.
In this setting only definitions tagged as `[reducible]` or type class instances are unfolded.
 -/
Lean.Parser.Tactic.withReducibleAndInstances : Lean.ParserDescr
-- Mathlib.Algebra.Category.Ring.Limits
/-- The forgetful functor from semirings to monoids preserves all limits.
 -/
SemiRingCat.forget₂Mon_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ SemiRingCat MonCat)
-- Mathlib.Topology.Separation.Hausdorff
Pi.isCompact_iff : ∀ {ι : Type u_4} {X : ι → Type u_5} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T2Space (X i)]
  {s : Set ((i : ι) → X i)}, IsCompact s ↔ IsClosed s ∧ ∀ (i : ι), IsCompact (Function.eval i '' s)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_eq_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s : Set α},
  MeasurableSet s → Set.EqOn f 0 s → ∫⁻ (x : α) in s, f x ∂μ = 0
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_map_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {S : Subsemigroup N} {f : M →ₙ* N},
  Subsemigroup.comap f (Subsemigroup.map f (Subsemigroup.comap f S)) = Subsemigroup.comap f S
-- Mathlib.RingTheory.IsTensorProduct
/-- The base change of `M` along `R → S` is linearly equivalent to `S ⊗[R] M`.  -/
IsBaseChange.equiv : {R : Type u_1} →
  {M : Type v₁} →
    {N : Type v₂} →
      {S : Type v₃} →
        [inst : AddCommMonoid M] →
          [inst_1 : AddCommMonoid N] →
            [inst_2 : CommSemiring R] →
              [inst_3 : CommSemiring S] →
                [inst_4 : Algebra R S] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      [inst_7 : Module S N] →
                        [inst_8 : IsScalarTower R S N] →
                          {f : M →ₗ[R] N} → IsBaseChange S f → TensorProduct R S M ≃ₗ[S] N
-- Mathlib.Algebra.Category.CommBialgCat
commBialgCatEquivComonCommAlgCat_unitIso_inv_app : ∀ (R : Type u) [inst : CommRing R] (X : CommBialgCat R),
  (commBialgCatEquivComonCommAlgCat R).unitIso.inv.app X = CategoryTheory.CategoryStruct.id (CommBialgCat.of R ↑X)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteGrp.toLimit.eq_1 : ∀ (P : ProfiniteGrp.{u}),
  P.toLimit =
    ProfiniteGrp.ofHom
      (let __src := P.toLimitFun;
      { toMonoidHom := __src, continuous_toFun := ⋯ })
-- Lean.Meta.IndPredBelow
/-- Names of brecOn declarations (corresponding to the motives)  -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.Context.brecOnNames : Lean.Meta.IndPredBelow.Context✝ → Array Lean.Name
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearMap.canLiftContinuousLinearMap : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [inst_5 : AddCommGroup F]
  [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜]
  [T2Space E] [FiniteDimensional 𝕜 E], CanLift (E →ₗ[𝕜] F) (E →L[𝕜] F) ContinuousLinearMap.toLinearMap fun x => True
-- ProofWidgets.Component.Basic
ProofWidgets.MarkdownDisplay.Props.contents : ProofWidgets.MarkdownDisplay.Props → String
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.strictMono_comap_prod_map : ∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal],
  StrictMono fun H => (Subgroup.comap N.subtype H, Subgroup.map (QuotientGroup.mk' N) H)
-- Lean.Meta.AppBuilder
/-- Returns `Inhabited.default α`  -/
Lean.Meta.mkDefault : Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Level
_private.Lean.Level.0.Lean.Level.normLtAux.eq_def : ∀ (x : Lean.Level) (x_1 : ℕ) (x_2 : Lean.Level) (x_3 : ℕ),
  x.normLtAux x_1 x_2 x_3 =
    match x, x_1, x_2, x_3 with
    | l₁.succ, k₁, l₂, k₂ => l₁.normLtAux (k₁ + 1) l₂ k₂
    | l₁, k₁, l₂.succ, k₂ => l₁.normLtAux k₁ l₂ (k₂ + 1)
    | l₁@h:(l₁₁.max l₁₂), k₁, l₂@h_1:(l₂₁.max l₂₂), k₂ =>
      if (l₁ == l₂) = true then decide (k₁ < k₂)
      else if (l₁₁ != l₂₁) = true then l₁₁.normLtAux 0 l₂₁ 0 else l₁₂.normLtAux 0 l₂₂ 0
    | l₁@h:(l₁₁.imax l₁₂), k₁, l₂@h_1:(l₂₁.imax l₂₂), k₂ =>
      if (l₁ == l₂) = true then decide (k₁ < k₂)
      else if (l₁₁ != l₂₁) = true then l₁₁.normLtAux 0 l₂₁ 0 else l₁₂.normLtAux 0 l₂₂ 0
    | Lean.Level.param n₁, k₁, Lean.Level.param n₂, k₂ => if (n₁ == n₂) = true then decide (k₁ < k₂) else n₁.lt n₂
    | Lean.Level.mvar n₁, k₁, Lean.Level.mvar n₂, k₂ =>
      if (n₁ == n₂) = true then decide (k₁ < k₂) else n₁.name.lt n₂.name
    | l₁, k₁, l₂, k₂ => if (l₁ == l₂) = true then decide (k₁ < k₂) else decide (l₁.ctorToNat < l₂.ctorToNat)
-- Std.Async.Select
/-- An event source that can be multiplexed using `Selectable.one`, see the documentation of
`Selectable.one` for how the protocol of communicating with a `Selector` works.
 -/
Std.Async.Selector : Type → Type
-- Mathlib.Algebra.Polynomial.GroupRingAction
Polynomial.smul_eval : ∀ (S : Type u_3) [inst : CommSemiring S] (G : Type u_4) [inst_1 : Group G] [inst_2 : MulSemiringAction G S] (g : G)
  (f : Polynomial S) (x : S), Polynomial.eval x (g • f) = g • Polynomial.eval (g⁻¹ • x) f
-- Mathlib.Topology.Category.Profinite.Extend
/-- `S.asLimitCone'` is a limit cone.  -/
Profinite.asLimit' : (S : Profinite) → CategoryTheory.Limits.IsLimit S.asLimitCone'
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.liftPropWithinAt_self_source : ∀ {H : Type u_1} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H']
  [inst_2 : TopologicalSpace M'] [inst_3 : ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : H → M'}
  {s : Set H} {x : H},
  ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (↑(chartAt H' (f x)) ∘ f) s x
-- Init.Data.Array.Lemmas
Array.any_flatMap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {p : β → Bool},
  (Array.flatMap f xs).any p = xs.any fun a => (f a).any p
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `sub_apply`. -/
MeasureTheory.VectorMeasure.sub_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Sub β}
  {inst_2 : Sub F} [self : IsSubApply F α β] (f g : F) (x : α), (f - g) x = f x - g x
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_single_X : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (s s' : σ) (n : ℕ),
  MvPolynomial.coeff (fun₀ | s' => n) (MvPolynomial.X s) = if n = 1 ∧ s = s' then 1 else 0
-- Mathlib.Order.Filter.Lift
Filter.comap_lift'_eq2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : β → α} {g : Set β → Set γ},
  Monotone g → (Filter.comap m f).lift' g = f.lift' (g ∘ Set.preimage m)
-- Mathlib.Order.RelSeries
RelSeries.head.eq_1 : ∀ {α : Type u_1} {r : SetRel α α} (x : RelSeries r), x.head = x.toFun 0
-- Mathlib.RingTheory.PowerSeries.Binomial
PowerSeries.binomialSeries_constantCoeff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : BinomialRing R] [inst_2 : Ring A] [inst_3 : Algebra R A]
  (r : R), PowerSeries.constantCoeff (PowerSeries.binomialSeries A r) = 1
-- Mathlib.Topology.TietzeExtension
/-- **Tietze extension theorem** for `TietzeExtension` spaces, a version for a closed set. Let
`s` be a closed set in a normal topological space `X`. Let `f` be a continuous function
on `s` with values in a `TietzeExtension` space `Y`. Then there exists a continuous function
`g : C(X, Y)` such that `g.restrict s = f`.  -/
ContinuousMap.exists_restrict_eq : ∀ {X : Type u} [inst : TopologicalSpace X] [NormalSpace X] {s : Set X} {Y : Type v} [inst_2 : TopologicalSpace Y]
  [TietzeExtension Y], IsClosed s → ∀ (f : C(↑s, Y)), ∃ g, ContinuousMap.restrict s g = f
-- Mathlib.Analysis.Convex.Measure
/-- Haar measure of the frontier of a convex set is zero.  -/
Convex.addHaar_frontier : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {s : Set E},
  Convex ℝ s → μ (frontier s) = 0
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.fst_comp_toProd : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  (AddMonoidHom.fst M N).comp AddMonoid.Coprod.toProd = AddMonoid.Coprod.fst
-- Mathlib.CategoryTheory.Localization.Construction
/-- The localized category obtained by formally inverting the morphisms
in `W : MorphismProperty C`  -/
CategoryTheory.MorphismProperty.Localization : {C : Type uC} → [inst : CategoryTheory.Category.{uC', uC} C] → CategoryTheory.MorphismProperty C → Type uC
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.derivWeierstrassPExcept.eq_1 : ∀ (L : PeriodPair) (l₀ z : ℂ),
  L.derivWeierstrassPExcept l₀ z = ∑' (l : ↥L.lattice), if ↑l = l₀ then 0 else -2 / (z - ↑l) ^ 3
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instDivisionAddCommMonoid : {α : Type u_1} → [SubtractionCommMonoid α] → SubtractionCommMonoid αᵒᵈ
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- Constructor for homotopies between morphisms from a mapping cone.  -/
CochainComplex.mappingCone.descHomotopy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ : F ⟶ G) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {K : CochainComplex C ℤ} →
              (f₁ f₂ : CochainComplex.mappingCone φ ⟶ K) →
                (γ₁ : CochainComplex.HomComplex.Cochain F K (-2)) →
                  (γ₂ : CochainComplex.HomComplex.Cochain G K (-1)) →
                    (CochainComplex.mappingCone.inl φ).comp (CochainComplex.HomComplex.Cochain.ofHom f₁) ⋯ =
                        CochainComplex.HomComplex.δ (-2) (-1) γ₁ +
                            (CochainComplex.HomComplex.Cochain.ofHom φ).comp γ₂ ⋯ +
                          (CochainComplex.mappingCone.inl φ).comp (CochainComplex.HomComplex.Cochain.ofHom f₂) ⋯ →
                      CochainComplex.HomComplex.Cochain.ofHom
                            (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ) f₁) =
                          CochainComplex.HomComplex.δ (-1) 0 γ₂ +
                            CochainComplex.HomComplex.Cochain.ofHom
                              (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ) f₂) →
                        Homotopy f₁ f₂
-- Std.Sat.AIG.RefVec
_private.Std.Sat.AIG.RefVec.0.Std.Sat.AIG.RefVec.countKnown.go.match_1.eq_2 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (x : Std.Sat.AIG.Decl α)
  (h_1 : Unit → motive Std.Sat.AIG.Decl.false) (h_2 : (x : Std.Sat.AIG.Decl α) → motive x),
  (x = Std.Sat.AIG.Decl.false → False) →
    (match x with
      | Std.Sat.AIG.Decl.false => h_1 ()
      | x => h_2 x) =
      h_2 x
-- Mathlib.Topology.Sets.BaseChangeNhds
TopologicalSpace.Opens.baseChangeOpenNhds_id : ∀ {α : Type u_1} [inst : TopologicalSpace α] {U : TopologicalSpace.Opens α} (K : ↑U.compactsInside),
  TopologicalSpace.Opens.baseChangeCompactsInside (CategoryTheory.CategoryStruct.id U) K = K
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.denote_mkAndCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α}
  {input : aig.BinaryInput},
  ⟦assign, aig.mkAndCached input⟧ =
    (⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.inclusion_injective : ∀ {M : Type u_1} [inst : MulOneClass M] {S T : Submonoid M} (h : S ≤ T), Function.Injective ⇑(Submonoid.inclusion h)
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_comp_val_Iio_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsCodirectedOrder α] [NoMinOrder α] {a : α} {f : α → β}
  {l : Filter β}, Filter.Tendsto (fun x => f ↑x) Filter.atBot l ↔ Filter.Tendsto f Filter.atBot l
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.closedBall_eq_image : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] (x : E)
  (r : ℝ), Euclidean.closedBall x r = ⇑toEuclidean.symm '' Metric.closedBall (toEuclidean x) r
-- Std.Data.HashMap.Lemmas
/-- Simpler variant of `getElem_filterMap` when `LawfulBEq` is available.  -/
Std.HashMap.getElem_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : LawfulBEq α]
  {f : α → β → Option γ} {k : α} {h : k ∈ Std.HashMap.filterMap f m}, (Std.HashMap.filterMap f m)[k] = (f k m[k]).get ⋯
-- Lean.Meta.Tactic.Replace
/-- Given a hypothesis `fvarId` named `h`, asserts a new hypothesis `h : type`
as soon after `fvarId` as possible, then tries to clear `h`. This is useful to avoid
reordering hypotheses.

The new hypothesis is asserted after any local variables that `type` depends on, and it may contain
metavariables. The value `val : type` can depend on any variables in the local context.

See also `Lean.MVarId.assertAfter'`, which asserts hypotheses without clearing.
 -/
Lean.MVarId.replace : Lean.MVarId →
  Lean.FVarId →
    Lean.Expr →
      optParam (Option Lean.Expr) none → optParam (Option Lean.Name) none → Lean.MetaM Lean.Meta.AssertAfterResult
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instIsBoundedSMul : ∀ {α : Type u} {β : Type v} {𝕜 : Type u_2} [inst : PseudoMetricSpace 𝕜] [inst_1 : TopologicalSpace α]
  [inst_2 : PseudoMetricSpace β] [inst_3 : Zero 𝕜] [inst_4 : Zero β] [inst_5 : SMul 𝕜 β] [inst_6 : IsBoundedSMul 𝕜 β],
  IsBoundedSMul 𝕜 (BoundedContinuousFunction α β)
-- Mathlib.Analysis.Calculus.MeanValue
/-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C` on
`s`, then the function is `C`-Lipschitz on `s`. Version with `fderiv` and `LipschitzOnWith`.  -/
Convex.lipschitzOnWith_of_nnnorm_fderiv_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {s : Set E} {C : NNReal},
  (∀ x ∈ s, DifferentiableAt 𝕜 f x) → (∀ x ∈ s, ‖fderiv 𝕜 f x‖₊ ≤ C) → Convex ℝ s → LipschitzOnWith C f s
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.congr : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f g : α → β} {a : α},
  IsLocalMax f a → f =ᶠ[nhds a] g → IsLocalMax g a
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.homMk_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (u : f.left ⟶ g.left)
  (v : f.right ⟶ g.right)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp u g.hom = CategoryTheory.CategoryStruct.comp f.hom v)
      CategoryTheory.Arrow.homMk._auto_1),
  (CategoryTheory.Arrow.homMk u v w).left = u
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalRotateRight : Lean.Elab.Tactic.Tactic
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicInterior_empty : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P], intrinsicInterior 𝕜 ∅ = ∅
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α}, (m.erase k).getKey? a = if (k == a) = true then none else m.getKey? a
-- Lean.Elab.Deriving.Basic
/-- Result for `mkInst`  -/
_private.Lean.Elab.Deriving.Basic.0.Lean.Elab.Term.MkInstResult : Type
-- Mathlib.Order.Fin.Tuple
liftFun_vecCons : ∀ {α : Type u_1} {n : ℕ} (r : α → α → Prop) [IsTrans α r] {f : Fin (n + 1) → α} {a : α},
  Relator.LiftFun (fun x1 x2 => x1 < x2) r (Matrix.vecCons a f) (Matrix.vecCons a f) ↔
    r a (f 0) ∧ Relator.LiftFun (fun x1 x2 => x1 < x2) r f f
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Eta-expanded form of `meromorphicNFAt_comp_sub_const_iff_meromorphicNFAt`

---

`MeromorphicNFAt` is invariant under translation.  -/
meromorphicNFAt_fun_comp_sub_const_iff_meromorphicNFAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x c : 𝕜} {f : 𝕜 → E}, MeromorphicNFAt (fun x => f (x - c)) x ↔ MeromorphicNFAt f (x - c)
-- Lean.Meta.Tactic.Grind.Solve
/-- Try to solve/close the given goal.
Returns `some goal` if this subgoal failed to be closed,
and `none` if all subgoals were closed.
 -/
Lean.Meta.Grind.solve : Lean.Meta.Grind.Goal → Lean.Meta.Grind.GrindM (Option Lean.Meta.Grind.Goal)
-- Lean.Meta.AppBuilder
/-- Returns a proof of `a ≍ a`.  -/
Lean.Meta.mkHEqRefl : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.ArchimedeanStrata.nontrivial_stratum : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] (u : HahnEmbedding.ArchimedeanStrata K M)
  {c : FiniteArchimedeanClass M}, Nontrivial ↥(u.stratum c)
-- Init.Data.ByteArray.Basic
ByteArray.instForInUInt8OfMonad : {m : Type u_1 → Type u_2} → [Monad m] → ForIn m ByteArray UInt8
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCStarAlgebra.toCStarRing : ∀ {A : Type u_1} [self : NonUnitalCStarAlgebra A], CStarRing A
-- Init.Meta.Defs
/-- Creates literal syntax for a number in scientific notation. The caller must ensure that the provided
string is a valid scientific notation literal.

If `info` is provided, then the literal's source information is copied from it.
 -/
Lean.Syntax.mkScientificLit : String → optParam Lean.SourceInfo Lean.SourceInfo.none → Lean.TSyntax Lean.scientificLitKind
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_sub_self_right : ∀ {m n : ℕ}, m ≤ n → (m.Coprime (n - m) ↔ m.Coprime n)
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.map_eq_mapOfHomotopy : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁)
  (φ₂ : K₂ ⟶ L₂) (a : K₁ ⟶ K₂) (b : L₁ ⟶ L₂)
  (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂),
  CochainComplex.mappingCone.map φ₁ φ₂ a b comm = CochainComplex.mappingCone.mapOfHomotopy (Homotopy.ofEq comm)
-- Mathlib.Order.Partition.Basic
/-- The natural equivalence between the subtype of parts and the subtype of parts of a copy.  -/
Partition.partscopyEquiv : {α : Type u_1} → {s t : α} → [inst : CompleteLattice α] → (P : Partition s) → (hst : s = t) → ↥(P.copy hst) ≃ ↥P
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.ae_cond_of_forall_mem : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω},
  MeasurableSet s → ∀ {p : Ω → Prop}, (∀ x ∈ s, p x) → ∀ᵐ (x : Ω) ∂μ[|s], p x
-- Mathlib.Order.Heyting.Boundary
Coheyting.hnot_boundary : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), ￢Coheyting.boundary a = ⊤
-- Mathlib.LinearAlgebra.PiTensorProduct.Generators
PiTensorProduct.submodule_span_eq_top : ∀ {R : Type u_1} {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {γ : ι → Type u_5} [inst : CommRing R]
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] {g : ⦃i : ι⦄ → γ i → M i},
  (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) → Submodule.span R (Set.range fun j => ⨂ₜ[R] (i : ι), g (j i)) = ⊤
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.asympBound_pos : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r) (n : ℕ), 0 < n → 0 < AkraBazziRecurrence.asympBound g a b n
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.map_lcm : ∀ {R : Type u_1} [inst : CommGroupWithZero R] {f : ArithmeticFunction R},
  f.IsMultiplicative → ∀ {x y : ℕ}, f (x.gcd y) ≠ 0 → f (x.lcm y) = f x * f y / f (x.gcd y)
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupContent.kind : Lean.Lsp.MarkupContent → Lean.Lsp.MarkupKind
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccLimit_lift : ∀ {o : Ordinal.{v}}, Order.IsSuccLimit (Ordinal.lift.{u, v} o) ↔ Order.IsSuccLimit o
-- Mathlib.Data.Finset.Image
Finset.image_const : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Finset α},
  s.Nonempty → ∀ (b : β), Finset.image (fun x => b) s = {b}
-- Mathlib.Order.PiLex
Pi.instOrderTopLexForallOfWellFoundedLT : {ι : Type u_1} →
  {β : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [WellFoundedLT ι] →
        [inst_2 : (a : ι) → PartialOrder (β a)] → [(a : ι) → OrderTop (β a)] → OrderTop (Lex ((a : ι) → β a))
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.instIsSplitEpiRightRArrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g), CategoryTheory.IsSplitEpi (CategoryTheory.Arrow.Hom.right h.r)
-- Mathlib.RingTheory.Ideal.Cotangent
IsLocalRing.CotangentSpace.map_eq_top_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R]
  {M : Submodule R ↥(IsLocalRing.maximalIdeal R)}, Submodule.map (IsLocalRing.maximalIdeal R).toCotangent M = ⊤ ↔ M = ⊤
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (w : F ≅ G) (j : J) {Z : C} (h : CategoryTheory.Limits.colimit G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfNatIso w).hom h) =
    CategoryTheory.CategoryStruct.comp (w.hom.app j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G j) h)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.isPreconnected_sUnion : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set (Set α)},
  IsPreconnected s → (∃ t ∈ s, IsPreconnected t) → IsPreconnected (⋃₀ s)