mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Meta.Defs
/-- Uses the separator `sep` (usually `"."`) to combine the components of the `Name` into a string.
See the documentation for `Name.toStringWithToken` for an explanation of `escape` and `isToken`.
 -/
_private.Init.Meta.Defs.0.Lean.Name.Internal.Meta.toStringWithSep : String → Bool → Lean.Name → (optParam (String → Bool) fun x => false) → String
-- Mathlib.Algebra.Group.TypeTags.Hom
/-- Reinterpret `α →* β` as `Additive α →+ Additive β`.  -/
MonoidHom.toAdditive : {α : Type u_3} →
  {β : Type u_4} → [inst : MulOneClass α] → [inst_1 : MulOneClass β] → (α →* β) ≃ (Additive α →+ Additive β)
-- Mathlib.MeasureTheory.OuterMeasure.Induced
/-- To test whether `s` is Carathéodory-measurable we only need to check the sets `t` for which
`P t` holds. See `ofFunction_caratheodory` for another way to show the Carathéodory-measurability
of `s`.
 -/
MeasureTheory.inducedOuterMeasure_caratheodory : ∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0}
  (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
  (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) →
    (∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) →
      ∀ (s : Set α),
        MeasurableSet s ↔
          ∀ (t : Set α),
            P t →
              (MeasureTheory.inducedOuterMeasure m P0 m0) (t ∩ s) +
                  (MeasureTheory.inducedOuterMeasure m P0 m0) (t \ s) ≤
                (MeasureTheory.inducedOuterMeasure m P0 m0) t
-- Std.Async.UDP
/-- Sets the time-to-live (TTL) for multicast packets.
 -/
Std.Async.UDP.Socket.setMulticastTTL : Std.Async.UDP.Socket → UInt32 → IO Unit
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.measurableSet_sigmaFiniteSetGE : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure ν]
  (n : ℕ), MeasurableSet (μ.sigmaFiniteSetGE ν n)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.post_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} (F : CategoryTheory.Functor T D) (Y : CategoryTheory.Over X),
  (CategoryTheory.Over.post F).obj Y = CategoryTheory.Over.mk (F.map Y.hom)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.one_le_m_coe : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {P : Finpartition Finset.univ} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α → 1 ≤ ↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card)
-- Lean.Environment
Lean.Kernel.Diagnostics.mk.injEq : ∀ (unfoldCounter : Lean.PHashMap Lean.Name ℕ) (enabled : Bool) (unfoldCounter_1 : Lean.PHashMap Lean.Name ℕ)
  (enabled_1 : Bool),
  ({ unfoldCounter := unfoldCounter, enabled := enabled } =
      { unfoldCounter := unfoldCounter_1, enabled := enabled_1 }) =
    (unfoldCounter = unfoldCounter_1 ∧ enabled = enabled_1)
-- Mathlib.Algebra.Lie.OfAssociative
LieAlgebra.ad_lie : ∀ (R : Type u) {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x y z : L),
  ((LieAlgebra.ad R L) x) ⁅y, z⁆ = ⁅((LieAlgebra.ad R L) x) y, z⁆ + ⁅y, ((LieAlgebra.ad R L) x) z⁆
-- Mathlib.Data.Fin.SuccPred
Fin.castpred_succ_le_iff : ∀ {n : ℕ} {a b : Fin (n + 1)} (ha : a.succ ≠ Fin.last (n + 1)), a.succ.castPred ha ≤ b ↔ a < b
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {I₁ I₂ : S.Arrow} {x y : I₁.Relation I₂}, x = y ↔ x.Z = y.Z ∧ x.g₁ ≍ y.g₁ ∧ x.g₂ ≍ y.g₂
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.instList : {α : Type} → [Lean.Elab.ConfigEval.EvalTerm α] → Lean.Elab.ConfigEval.EvalTerm (List α)
-- Mathlib.Geometry.Convex.Cone.TensorProduct
/-- The minimal tensor product is commutative.  -/
PointedCone.minTensorProduct_comm : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {G : Type u_2}
  [inst_3 : AddCommGroup G] [inst_4 : Module R G] {H : Type u_3} [inst_5 : AddCommGroup H] [inst_6 : Module R H]
  {C₁ : PointedCone R G} {C₂ : PointedCone R H},
  PointedCone.map (↑(TensorProduct.comm R G H)) (C₁.minTensorProduct C₂) = C₂.minTensorProduct C₁
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.instInhabitedResult : Inhabited Lean.Meta.Sym.DSimp.Result
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.rightUnshift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ γ_1 : CochainComplex.HomComplex.Cocycle K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'),
  γ = γ_1 → ∀ (n : ℤ) (hn : n' + a = n), γ.rightUnshift n hn = γ_1.rightUnshift n hn
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst_1 : Inhabited (β k)], k ∉ t₁ → (t₁ \ t₂).get! k = default
-- Mathlib.Order.Category.Lat
Lat.id_apply : ∀ (X : Lat) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverMincard.eq_1 : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X) (n : ℕ),
  Dynamics.coverMincard T F U n = ⨅ s, ⨅ (_ : Dynamics.IsDynCoverOf T F U n ↑s), ↑s.card
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_maxValue : ∀ (h : System.Platform.numBits = 32), ISize.maxValue.toBitVec32 h = BitVec.intMax 32
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.u₃ : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} →
      {hζ : IsPrimitiveRoot ζ 3} →
        FermatLastTheoremForThreeGen.Solution✝ hζ →
          [inst_1 : NumberField K] → [IsCyclotomicExtension {3} ℚ K] → (NumberField.RingOfIntegers K)ˣ
-- Mathlib.Combinatorics.Additive.CovBySMul
CovBySMul.trans : ∀ {M : Type u_1} {N : Type u_2} {X : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : MulAction M X]
  [inst_3 : MulAction N X] {K L : ℝ} {A B C : Set X} [inst_4 : SMul M N] [IsScalarTower M N X],
  CovBySMul M K A B → CovBySMul N L B C → CovBySMul N (K * L) A C
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.ι_totalShift₂Iso_inv_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (a b n : ℤ) (h : a + b = n) (b' n' : ℤ) (hb' : a + b' = n') (hn' : n' = n + y),
  CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a b' n' hb')
      (CategoryTheory.CategoryStruct.comp
        (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) y n n' hn').inv
        ((K.totalShift₂Iso y).inv.f n)) =
    (a * y).negOnePow •
      CategoryTheory.CategoryStruct.comp (K.shiftFunctor₂XXIso a b y b' ⋯).inv
        (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).ιTotal (ComplexShape.up ℤ) a b n h)
-- Init.Data.List.Find
/-- `xs.findIdx p = i` iff `p xs[i]` and `¬ p xs [j]` for all `j < i`.  -/
List.findIdx_eq : ∀ {α : Type u_1} {p : α → Bool} {xs : List α} {i : ℕ} (h : i < xs.length),
  List.findIdx p xs = i ↔ p xs[i] = true ∧ ∀ (j : ℕ) (hji : j < i), p xs[j] = false
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.sConvexComb_mem : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {w : Convexity.StdSimplex R X} {s : Set X},
  Convexity.IsConvexSet R s → ↑w.weights.support ⊆ s → Convexity.sConvexComb w ∈ s
-- Mathlib.Control.Monad.Writer
WriterT.mk : {M : Type u → Type v} → {α ω : Type u} → M (α × ω) → WriterT ω M α
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOpEquiv_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.Cocone F.op),
  CategoryTheory.Limits.coneOpEquiv.inverse.obj c = Opposite.op c.unop
-- Mathlib.Data.List.Sym
List.sym.eq_2 : ∀ {α : Type u_1} (x : ℕ), (x = 0 → False) → List.sym x [] = []
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instSMul : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] →
            {abv : β → α} →
              [IsAbsoluteValue abv] →
                {G : Type u_3} → [inst_5 : SMul G β] → [IsScalarTower G β β] → SMul G (CauSeq β abv)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoImage_preimage_hom_homOfLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.isoImage f ((TopologicalSpace.Opens.map f.base).obj U)).hom (Y.homOfLE ⋯) =
    f ∣_ U
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.toEquiv_inj : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S}
  {σ' : S →+* R} [inst_4 : RingHomInvPair σ σ'] [inst_5 : RingHomInvPair σ' σ] {e₁ e₂ : M ≃ₛₗ[σ] M₂},
  e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat),
  (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).counitIso =
    CategoryTheory.Iso.refl
      ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).comp
        (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F))
-- Mathlib.MeasureTheory.OuterMeasure.AE
/-- If two sets are equal modulo a set of measure zero, then `μ s = μ t`.  -/
MeasureTheory.measure_congr : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, s =ᵐ[μ] t → μ s = μ t
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.trans : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ θ : L.BoundedFormula α n},
  T.Iff φ ψ → T.Iff ψ θ → T.Iff φ θ
-- Init.MetaTypes
/-- When `true` (default: `true`), `simp` tries to realize constant `f.congr_simp`
when constructing an auxiliary congruence proof for `f`.
This option exists because the termination prover uses `simp` and `withoutModifyingEnv`
while constructing the termination proof. Thus, any constant realized by `simp`
is deleted.
 -/
Lean.Meta.Simp.Config.congrConsts : Lean.Meta.Simp.Config → Bool
-- Lean.DocString.Extension
/-- A custom block element. The type of the value in the `Dynamic` determines how it is interpreted
and rendered.
 -/
Lean.ElabBlock.custom : Dynamic → Lean.ElabBlock
-- Init.Data.SInt.Bitwise
UInt8.toInt8_not : ∀ (a : UInt8), (~~~a).toInt8 = ~~~a.toInt8
-- Init.Data.BitVec.Lemmas
BitVec.and_comm : ∀ {w : ℕ} (x y : BitVec w), x &&& y = y &&& x
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_subtype : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] {p : ι → Prop} {F : Fintype (Subtype p)} (s : Finset ι),
  (∀ (x : ι), x ∈ s ↔ p x) → ∀ (f : ι → M), ∏ a ∈ s, f a = ∏ a, f ↑a
-- Mathlib.Tactic.NormNum.NatLog
Mathlib.Meta.NormNum.nat_log_helper0 : ∀ (b n : ℕ), n.blt b = true → Nat.log b n = 0
-- Mathlib.Algebra.Star.Unitary
/-- The star monoid isomorphism between unitary subgroups induced by a star monoid isomorphism of
the underlying star monoids.  -/
Unitary.mapEquiv : {R : Type u_2} →
  {S : Type u_3} →
    [inst : Monoid R] →
      [inst_1 : StarMul R] → [inst_2 : Monoid S] → [inst_3 : StarMul S] → (R ≃⋆* S) → ↥(unitary R) ≃⋆* ↥(unitary S)
-- Init.Data.SInt.Lemmas
USize.toBitVec_toISize : ∀ (x : USize), x.toISize.toBitVec = x.toBitVec
-- Mathlib.Util.Export
Lean.Export.Alloc.mk : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashMap α ℕ → ℕ → Lean.Export.Alloc α
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
/-- The canonical projection `𝟭 C ⥤ Φ.quotient` where `Φ.quotient` is the cokernel of
`Φ.ι : Φ.r ⟶ 𝟭 C`.  -/
CategoryTheory.Abelian.Preradical.π : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (Φ : CategoryTheory.Abelian.Preradical C) → CategoryTheory.Functor.id C ⟶ Φ.quotient
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_and : ∀ {w i : ℕ} {x y : BitVec w}, (x &&& y).getMsbD i = (x.getMsbD i && y.getMsbD i)
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.coe_listSum : ∀ {ι : Type u_1} {S : Type u_2} [inst : AddMonoid S] [inst_1 : Mul S] (t : RingCon S) (l : List ι) (f : ι → S),
  ↑(List.map f l).sum = (List.map (fun i => ↑(f i)) l).sum
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Alt.replaceFVarId : Lean.FVarId → Lean.Expr → Lean.Meta.Match.Alt → Lean.Meta.Match.Alt
-- Mathlib.Topology.Algebra.Valued.ValuativeRel
/-- Assuming `ContinuousConstVAdd R R`, we only need to check the neighbourhood of `0` in order to
prove `IsValuativeTopology R`.  -/
IsValuativeTopology.of_zero : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : TopologicalSpace R] [ContinuousConstVAdd R R],
  (∀ (s : Set R), s ∈ nhds 0 ↔ ∃ γ, {z | (ValuativeRel.valuation R) z < ↑γ} ⊆ s) → IsValuativeTopology R
-- Init.Data.Int.Linear
Int.Internal.Linear.not_le_of_le_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.SupportsStmt.eq_5 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (S : Finset Λ) (l : Γ → σ → Λ),
  Turing.TM1.SupportsStmt S (Turing.TM1.Stmt.goto l) = ∀ (a : Γ) (v : σ), l a v ∈ S
-- Mathlib.Topology.EMetricSpace.PairReduction
/-- The log-size radius of `t` in `V` is the smallest natural number n greater than zero such that
`|{x ∈ V | d(t, x) ≤ nc}| ≤ aⁿ`.  -/
PairReduction.logSizeRadius : {T : Type u_1} → [PseudoEMetricSpace T] → T → Finset T → ENNReal → ENNReal → ℕ
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.inclusion.toFun_eq_coe : ∀ {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst_1 : AddAction M α] (s : SubAddAction M α),
  s.inclusion.toFun = Subtype.val
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
UnitAddCircle.measure_univ : MeasureTheory.volume Set.univ = 1
-- Init.Data.List.FinRange
List.finRange_succ : ∀ {n : ℕ}, List.finRange (n + 1) = 0 :: List.map Fin.succ (List.finRange n)
-- Mathlib.Data.List.Induction
List.reverseRec_concat : ∀ {α : Type u_1} {motive : List α → Sort u_2} (x : α) (xs : List α) (nil : motive [])
  (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])),
  List.reverseRec nil append_singleton (xs ++ [x]) = append_singleton xs x (List.reverseRec nil append_singleton xs)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_ofList_le : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  (Std.HashMap.ofList l).size ≤ l.length
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.bilinLeftCLM_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7}
  [inst_3 : NormedAlgebra ℝ 𝕜] [inst_4 : NormedAddCommGroup F₁] [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁]
  [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂] [inst_9 : NormedSpace ℝ F₂]
  [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] [inst_12 : NormedSpace ℝ F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃)
  {g : E → F₂} (hg : ContDiff ℝ (↑n) g) (φ : ContDiffMapSupportedIn E F₁ n K),
  ⇑((ContDiffMapSupportedIn.bilinLeftCLM B hg) φ) = fun x => (B (φ x)) (g x)
-- Mathlib.FieldTheory.Perfect
powMulEquiv_mul : ∀ (M : Type u_1) (p q : ℕ) [inst : CommMonoid M] [inst_1 : PerfectRing M p] [inst_2 : PerfectRing M q],
  powMulEquiv M (p * q) = (powMulEquiv M p).trans (powMulEquiv M q)
-- Mathlib.CategoryTheory.Subobject.Limits
/-- A factorisation of `f : X ⟶ Y` through `imageSubobject f`.  -/
CategoryTheory.Limits.factorThruImageSubobject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.Limits.HasImage f] →
          X ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f)
-- Init.Data.List.Lemmas
List.singleton_eq_append_iff : ∀ {α : Type u_1} {x : α} {a b : List α}, [x] = a ++ b ↔ a = [] ∧ b = [x] ∨ a = [x] ∧ b = []
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instMul.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  LowerSet.instMul = { mul := fun s t => { carrier := Set.image2 (fun x1 x2 => x1 * x2) ↑s ↑t, lower' := ⋯ } }
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.bind_dirac_eq_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (m : MeasureTheory.Measure α)
  {f : α → β}, Measurable f → (m.bind fun x => MeasureTheory.Measure.dirac (f x)) = MeasureTheory.Measure.map f m
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- In `Δ[n + 1]`, the face corresponding to the complement of `{i}`
for `i : Fin (n + 2)` is isomorphic to `Δ[n]`.  -/
SSet.stdSimplex.faceSingletonComplIso : {n : ℕ} → (i : Fin (n + 2)) → SSet.stdSimplex.obj { len := n } ≅ (SSet.stdSimplex.face {i}ᶜ).toSSet
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Given the original parameter names from `originalVarNames`, find
good variable names to be used when talking about termination measures:
Use user-given parameter names if present; use x1...xn otherwise.

The names ought to accessible (no macro scopes) and fresh wrt to the current environment,
so that with `showInferredTerminationBy` we can print them to the user reliably.
We do that by appending `'` as needed.

It is possible (but unlikely without malice) that some of the user-given names
shadow each other, and the guessed relation refers to the wrong one. In that
case, the user gets to keep both pieces (and may have to rename variables).
 -/
Lean.Elab.WF.GuessLex.naryVarNames : Array Lean.Name → Lean.MetaM (Array Lean.Name)
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.span_repr_eq_single : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : ι → M} (hli : LinearIndependent R v) (i : ι) (hi : optParam (v i ∈ Submodule.span R (Set.range v)) ⋯),
  (Module.Basis.span hli).repr ⟨v i, hi⟩ = fun₀ | i => 1
-- Mathlib.Logic.Relation
Relation.reflTransGen_idem : ∀ {α : Type u_1} {r : α → α → Prop}, Relation.ReflTransGen (Relation.ReflTransGen r) = Relation.ReflTransGen r
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.id_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (x : E.I₀),
  (CategoryTheory.CategoryStruct.id E).h₀ x = CategoryTheory.CategoryStruct.id (E.X x)
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesOnBall.sum : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ},
  HasFiniteFPowerSeriesOnBall f p x n r → ∀ {y : E}, y ∈ Metric.eball 0 r → f (x + y) = p.sum y
-- Init.System.Uri
System.Uri.UriEscape.zero : UInt8
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_3.eq_1 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1) (h_1 : Unit → motive none)
  (h_2 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some c)),
  (match none with
    | none => h_1 ()
    | some c => h_2 c) =
    h_1 ()
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_neg : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), (-p).degree = p.degree
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.image_exp_Ioc_eq_sphere : (fun θ => Complex.exp (↑θ * Complex.I)) '' Set.Ioc (-Real.pi) Real.pi = Metric.sphere 0 1
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.IsFiltered.instHasColimitOfIsEventuallyConstant : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J C)
  [hF : CategoryTheory.IsFiltered.IsEventuallyConstant F] [CategoryTheory.IsFiltered J],
  CategoryTheory.Limits.HasColimit F
-- Mathlib.Analysis.Calculus.Gradient.Basic
gradientWithin.eq_1 : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (f : F → 𝕜) (s : Set F) (x : F),
  gradientWithin f s x = (InnerProductSpace.toDual 𝕜 F).symm (fderivWithin 𝕜 f s x)
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.toList_inj : ∀ {V : Type u} [inst : Quiver V] {a b : V} [∀ (a b : V), Subsingleton (a ⟶ b)] {p q : Quiver.Path a b},
  p.toList = q.toList ↔ p = q
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- Let `s : Set ℝ≥0` be a compact set and consider pairs `(f, a) : (ℝ≥0 → ℝ≥0) × A` where `f` is
continuous on `s` and `spectrum ℝ≥0 a ⊆ s` and `0 ≤ a`.

Then `cfc` is jointly continuous in both variables (i.e., continuous in its uncurried form) on this
set of pairs when the function space is equipped with the topology of uniform convergence on `s`.  -/
continuousOn_cfc_nnreal_setProd : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  {s : Set NNReal},
  IsCompact s →
    ContinuousOn (fun fa => cfc ((UniformOnFun.toFun {s}) fa.1) fa.2)
      ({f | ContinuousOn ((UniformOnFun.toFun {s}) f) s} ×ˢ {a | 0 ≤ a ∧ spectrum NNReal a ⊆ s})
-- Mathlib.Topology.Order.OrderClosed
isOpen_Ioi : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a : α}, IsOpen (Set.Ioi a)
-- Mathlib.Algebra.Group.Action.Opposite
/-- With `open scoped RightActions`, a shorthand for right actions, `op r • m`.

In lemma names this is still called `op_smul`.  -/
RightActions.«term_<•_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidalFunctorMonoidal.eq_1 : ∀ {M : Type u} [inst : AddMonoid M] {N : Type u'} [inst_1 : AddMonoid N] (F : M →+ N),
  CategoryTheory.Discrete.addMonoidalFunctorMonoidal F =
    { εIso := CategoryTheory.Discrete.eqToIso ⋯, μIso := fun m₁ m₂ => CategoryTheory.Discrete.eqToIso ⋯,
        μIso_hom_natural_left := ⋯, μIso_hom_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯,
        right_unitality := ⋯ }.toMonoidal
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.hasColimit_of_comp_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C)
  (E : CategoryTheory.Functor C D) [E.IsEquivalence] [CategoryTheory.Limits.HasColimit (K.comp E)],
  CategoryTheory.Limits.HasColimit K
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_idempotent : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s ∪ s = s
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.longestPrefix.eq_1 : ∀ {E : ℕ → Type u_2} (x : (n : ℕ) → E n) (s : Set ((n : ℕ) → E n)),
  PiNat.longestPrefix x s = PiNat.shortestPrefixDiff x s - 1