mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.instIsRightAdjointAlgebraForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C), T.forget.IsRightAdjoint
-- Mathlib.Topology.Order
TopologicalSpace.GenerateOpen.basic : ∀ {α : Type u} {g : Set (Set α)}, ∀ s ∈ g, TopologicalSpace.GenerateOpen g s
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {f : α → Bool}, m.WF → ((Std.HashSet.Raw.filter f m).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ m), f (m.get k h) = true)
-- Mathlib.Data.Sigma.Basic
Function.Injective.sigma_map : ∀ {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁ → Type u_5} {β₂ : α₂ → Type u_6} {f₁ : α₁ → α₂}
  {f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)},
  Function.Injective f₁ → (∀ (a : α₁), Function.Injective (f₂ a)) → Function.Injective (Sigma.map f₁ f₂)
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy.mem₁ : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {J : CategoryTheory.GrothendieckTopology C} {X : C} {E : J.OneHypercover X} {F : CategoryTheory.Functor C D}
  {K : CategoryTheory.GrothendieckTopology D} [self : E.IsPreservedBy F K] (i₁ i₂ : E.I₀) ⦃W : D⦄
  (p₁ : W ⟶ F.obj (E.X i₁)) (p₂ : W ⟶ F.obj (E.X i₂)),
  CategoryTheory.CategoryStruct.comp p₁ (F.map (E.f i₁)) = CategoryTheory.CategoryStruct.comp p₂ (F.map (E.f i₂)) →
    (E.map F).sieve₁ p₁ p₂ ∈ K W
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBaseNat.atom.sizeOf_spec : ∀ {e : Q(ℕ)} (id : ℕ), sizeOf (Mathlib.Tactic.Ring.Common.ExBaseNat.atom id) = 1 + sizeOf e + sizeOf id
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_tmul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E →L[𝕜] F) (m : E) (n : G),
  (ContinuousLinearMap.rTensor G f) (m ⊗ₜ[𝕜] n) = f m ⊗ₜ[𝕜] n
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_addMonoidHom_of_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {hom : Type u_3}
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [IsUniformAddGroup β] [inst_6 : FunLike hom α β]
  [AddMonoidHomClass hom α β] {f : hom}, Continuous ⇑f → UniformContinuous ⇑f
-- Mathlib.Order.Filter.Pointwise
Filter.frequently_neg : ∀ {α : Type u_2} [inst : Neg α] {f : Filter α} {p : α → Prop}, (∃ᶠ (x : α) in -f, p x) ↔ ∃ᶠ (x : α) in f, p (-x)
-- Mathlib.Data.Set.Finite.Lattice
/-- A finite set is bounded above.  -/
Set.Finite.bddAbove : ∀ {α : Type u} [inst : Preorder α] [IsDirectedOrder α] [Nonempty α] {s : Set α}, s.Finite → BddAbove s
-- Mathlib.LinearAlgebra.Contraction
/-- When `M` and `N` are free `R` modules, the map `homTensorHomMap` is an equivalence. Note that
`homTensorHomEquiv` is not defined directly in terms of `homTensorHomMap`, but the equivalence
between the two is given by `homTensorHomEquiv_toLinearMap` and `homTensorHomEquiv_apply`.
 -/
homTensorHomEquiv : (R : Type u_2) →
  (M : Type u_3) →
    (N : Type u_4) →
      (P : Type u_5) →
        (Q : Type u_6) →
          [inst : CommSemiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid N] →
                [inst_3 : AddCommMonoid P] →
                  [inst_4 : AddCommMonoid Q] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R N] →
                        [inst_7 : Module R P] →
                          [inst_8 : Module R Q] →
                            [Module.Projective R M] →
                              [Module.Finite R M] →
                                [Module.Projective R N] →
                                  [Module.Finite R N] →
                                    TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q) ≃ₗ[R]
                                      TensorProduct R M N →ₗ[R] TensorProduct R P Q
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousSub.measurableSub₂ : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ] [SecondCountableTopology γ]
  [inst_4 : Sub γ] [ContinuousSub γ], MeasurableSub₂ γ
-- Mathlib.RingTheory.AdjoinRoot
/-- If `L` is a field extension of `F` and `f` is a polynomial over `F` then the set
of maps from `F[x]/(f)` into `L` is in bijection with the set of roots of `f` in `L`.  -/
AdjoinRoot.equiv : (L : Type u_6) →
  (F : Type u_7) →
    [inst : Field F] →
      [inst_1 : CommRing L] →
        [inst_2 : IsDomain L] →
          [inst_3 : Algebra F L] → (f : Polynomial F) → f ≠ 0 → (AdjoinRoot f →ₐ[F] L) ≃ { x // x ∈ f.aroots L }
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.comp_eval : ∀ (f g : Turing.ToPartrec.Code), (f.comp g).eval = fun v => g.eval v >>= f.eval
-- Init.Data.BitVec.Lemmas
BitVec.toFin_append : ∀ {m n : ℕ} {x : BitVec m} {y : BitVec n}, (x ++ y).toFin = ⟨x.toNat <<< n ||| y.toNat, ⋯⟩
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_eq_zero_of_ae_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {f : α → ε},
  0 < q → f =ᵐ[μ] 0 → MeasureTheory.eLpNorm' f q μ = 0
-- Mathlib.Analysis.InnerProductSpace.Calculus
/-- Derivative of the inner product.  -/
fderivInnerCLM : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → [inst_3 : NormedSpace ℝ E] → E × E → E × E →L[ℝ] 𝕜
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.map_ne_one : ∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) [Nontrivial B]
  {R : Type u_4} [inst_4 : Semiring R] [Nontrivial R] (f : A →+* R), Polynomial.map f (minpoly A x) ≠ 1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singletonMulHom.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α], Finset.singletonMulHom = { toFun := singleton, map_mul' := ⋯ }
-- Init.Data.Option.Lemmas
Option.mem_some_iff : ∀ {α : Type u_1} {a b : α}, a ∈ some b ↔ b = a
-- Mathlib.Data.Fin.Tuple.Basic
/-- To show two sigma pairs of tuples agree, it to show the second elements are related via
`Fin.cast`.  -/
Fin.sigma_eq_of_eq_comp_cast : ∀ {α : Type u_1} {a b : (ii : ℕ) × (Fin ii → α)} (h : a.fst = b.fst), a.snd = b.snd ∘ Fin.cast h → a = b
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} (i : P ≅ Q),
  CategoryTheory.Projective P → CategoryTheory.Projective Q
-- Mathlib.CategoryTheory.Comma.Arrow
/-- The right part of a morphism in the category of arrows.  -/
CategoryTheory.Arrow.Hom.right : {T : Type u} →
  [inst : CategoryTheory.Category.{v, u} T] → {X Y : CategoryTheory.Arrow T} → (Y ⟶ X) → (Y.right ⟶ X.right)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.LimitCone.mk.sizeOf_spec : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : SizeOf J] [inst_3 : SizeOf C] (cone : CategoryTheory.Limits.Cone F)
  (isLimit : CategoryTheory.Limits.IsLimit cone),
  sizeOf { cone := cone, isLimit := isLimit } = 1 + sizeOf cone + sizeOf isLimit
-- Init.Data.List.Basic
List.decidableBEx : {α : Type u} → (p : α → Prop) → [DecidablePred p] → (l : List α) → Decidable (∃ x ∈ l, p x)
-- Qq.Macro
Qq.Impl.unquoteMVar : Lean.Expr → Qq.Impl.UnquoteM Unit
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max!_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → t.max! ∈ t
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.ediam_image_toSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (s : Set X),
  Metric.ediam (⇑Metric.Snowflaking.toSnowflaking '' s) = Metric.ediam s ^ α
-- Mathlib.Analysis.InnerProductSpace.PiL2
Complex.orthonormalBasisOneI_repr_symm_apply : ∀ (x : EuclideanSpace ℝ (Fin 2)), Complex.orthonormalBasisOneI.repr.symm x = ↑(x.ofLp 0) + ↑(x.ofLp 1) * Complex.I
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- The algebra homomorphism of additive monoid algebras induced by a homomorphism of the base
algebras.  -/
AddMonoidAlgebra.mapAlgHom : {R : Type u_1} →
  {A : Type u_4} →
    {B : Type u_5} →
      (M : Type u_7) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : AddMonoid M] → (A →ₐ[R] B) → AddMonoidAlgebra A M →ₐ[R] AddMonoidAlgebra B M
-- Lean.Elab.Parallel
/-- Runs a list of TermElabM computations in parallel and returns:
* a combined cancellation hook for all tasks, and
* an iterator that yields results in original order.

The iterator runs in TermElabM, and as it yields each result, it updates the TermElabM state
to reflect the state when that particular task completed. This means the state is
threaded through the iteration in the order of the original list.

Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
Lean.Elab.Term.TermElabM.parIterWithCancel : {α : Type} →
  List (Lean.Elab.TermElabM α) →
    Lean.Elab.TermElabM (BaseIO PUnit.{1} × Std.IterM Lean.Elab.TermElabM (Except Lean.Exception α))
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.isOpenEmbedding_coe : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], Topology.IsOpenEmbedding Subtype.val
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsMaximumIndepSet.isMaximalIndepSet : ∀ {α : Type u_3} {G : SimpleGraph α} [inst : Finite α] (s : Finset α), G.IsMaximumIndepSet s → Maximal G.IsIndepSet ↑s
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  (h : Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = true),
  Std.Internal.List.getValueCast a (⟨k, v⟩ :: l) h =
    if h' : (k == a) = true then cast ⋯ v else Std.Internal.List.getValueCast a l ⋯
-- Init.MetaTypes
/-- TODO (currently unimplemented). When `true` (default: `true`), performs eta reduction for `fun` expressions.
That is, `(fun x => f x)` reduces to `f`.
 -/
Lean.Meta.Simp.Config.eta : Lean.Meta.Simp.Config → Bool
-- Mathlib.Data.Multiset.Fold
Multiset.fold_dedup_idem : ∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] [inst : DecidableEq α]
  [hi : Std.IdempotentOp op] (s : Multiset α) (b : α), Multiset.fold op b s.dedup = Multiset.fold op b s
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.iSup_eq_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_9}
  (p : ι → Submodule R M), ⨆ i, p i = Submodule.span R (⋃ i, ↑(p i))
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Iic_add_Iio_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [AddLeftStrictMono α]
  [AddRightStrictMono α] [inst_5 : LocallyFiniteOrderBot α] (a b : α), Finset.Iic a + Finset.Iio b ⊆ Finset.Iio (a + b)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l →
          ∀
            {h :
              (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).contains
                  k' =
                true},
            Std.DHashMap.Internal.Raw₀.Const.get
                (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k' h =
              v
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The canonical map `U ⟶ Spec Γ(X, U)` for an open `U ⊆ X`.  -/
AlgebraicGeometry.Scheme.Opens.toSpecΓ : {X : AlgebraicGeometry.Scheme} → (U : X.Opens) → ↑U ⟶ AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))
-- Init.Data.Iterators.Basic
/-- The output value could plausibly be emitted in a step after the next step.  -/
Std.Iter.IsPlausibleIndirectOutput.indirect : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it it' : Std.Iter β} {out : β},
  it'.IsPlausibleSuccessorOf it → it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.admissible_of_one_lt_sumInv_aux' : ∀ {p q r : ℕ+}, p ≤ q → q ≤ r → 1 < ADEInequality.sumInv {p, q, r} → ADEInequality.Admissible {p, q, r}
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_eq_blsub : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}), Ordinal.lsub (o.familyOfBFamily f) = o.blsub f
-- Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Conv.Path.type.inj : ∀ {next next_1 : Mathlib.Tactic.Conv.Path}, next.type = next_1.type → next = next_1
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The limit cone obtained from a right adjoint of the constant functor.  -/
CategoryTheory.Limits.coneOfAdj : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {L : CategoryTheory.Functor (CategoryTheory.Functor J C) C} →
          (CategoryTheory.Functor.const J ⊣ L) → (F : CategoryTheory.Functor J C) → CategoryTheory.Limits.Cone F
-- Mathlib.MeasureTheory.MeasurableSpace.Invariants
MeasurableSpace.comp_eq_of_measurable_invariants : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β] {f : α → α} {g : α → β}
  [MeasurableSingletonClass β], Measurable g → g ∘ f = g
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false →
      ∀ {km fallback : α}, t.minKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.shortDeclName : Lean.Elab.Command.InductiveView → Lean.Name
-- Mathlib.CategoryTheory.Sites.Precoverage.Generates
/-- If `K` generates `J`, then `J` is equal to the smallest Grothendieck topology containing `K`.
The converse is false, but holds if `K` is a coverage, see `CategoryTheory.Coverage.generates_iff`.
 -/
CategoryTheory.Precoverage.Generates.toGrothendieck_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {J : CategoryTheory.GrothendieckTopology C}, K.Generates J → K.toGrothendieck = J
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfPair.bijective_right : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} {inst : AddCommGroup M} {inst_1 : AddCommGroup N} {inst_2 : CommRing R}
  {inst_3 : Module R M} {inst_4 : Module R N} (p : M →ₗ[R] N →ₗ[R] R) [self : p.IsPerfPair], Function.Bijective ⇑p.flip
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- From a natural transformation `α : F → G` we get a functor from
coalgebras of `F` to coalgebras of `G`.
 -/
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C C} →
      (F ⟶ G) → CategoryTheory.Functor (CategoryTheory.Endofunctor.Coalgebra F) (CategoryTheory.Endofunctor.Coalgebra G)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α}, (t.erase k).get? k = none
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Bornology α] [inst_1 : Bornology β] (toFun : α → β)
  (comap_cobounded_le' : Filter.comap toFun (Bornology.cobounded β) ≤ Bornology.cobounded α) (toFun_1 : α → β)
  (comap_cobounded_le'_1 : Filter.comap toFun_1 (Bornology.cobounded β) ≤ Bornology.cobounded α),
  ({ toFun := toFun, comap_cobounded_le' := comap_cobounded_le' } =
      { toFun := toFun_1, comap_cobounded_le' := comap_cobounded_le'_1 }) =
    (toFun = toFun_1)
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.instPreservesPairwisePullbacksOfPreservesLimitsOfShapeWalkingCospan : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] {X : C}
  (R : CategoryTheory.Presieve X), F.PreservesPairwisePullbacks R
-- Mathlib.Algebra.Group.Action.Defs
IsScalarTower.of_smul_one_mul : ∀ {M : Type u_9} {N : Type u_10} [inst : Monoid N] [inst_1 : SMul M N],
  (∀ (x : M) (y : N), x • 1 * y = x • y) → IsScalarTower M N N
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.IsTrail.map`.

---

**Alias** of the reverse direction of `SimpleGraph.Walk.isTrail_map_iff_of_injective`. -/
SimpleGraph.Walk.map_isTrail_of_injective : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v},
  Function.Injective ⇑f → p.IsTrail → (SimpleGraph.Walk.map f p).IsTrail
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k}, k ∉ m₁ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.LimitBicone.mk.sizeOf_spec : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} [inst_2 : SizeOf J] [inst_3 : SizeOf C]
  (bicone : CategoryTheory.Limits.Bicone F) (isBilimit : bicone.IsBilimit),
  sizeOf { bicone := bicone, isBilimit := isBilimit } = 1 + sizeOf bicone + sizeOf isBilimit
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- Forgetting its algebraic properties, a continuous affine map is a continuous map.  -/
ContinuousAffineMap.toContinuousMap : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        {Q : Type u_5} →
          [inst : Ring R] →
            [inst_1 : AddCommGroup V] →
              [inst_2 : Module R V] →
                [inst_3 : TopologicalSpace P] →
                  [inst_4 : AddTorsor V P] →
                    [inst_5 : AddCommGroup W] →
                      [inst_6 : Module R W] →
                        [inst_7 : TopologicalSpace Q] → [inst_8 : AddTorsor W Q] → (P →ᴬ[R] Q) → C(P, Q)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inter_add_subset : ∀ {α : Type u_2} [inst : Add α] {s₁ s₂ t : Set α}, s₁ ∩ s₂ + t ⊆ (s₁ + t) ∩ (s₂ + t)
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.unop_X₁ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂ᵒᵖ}
  (L : Φ.op.LeftResolution X₂), L.unop.X₁ = Opposite.unop L.X₁
-- Mathlib.Order.Grade
grade_top : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : PartialOrder 𝕆] [inst_1 : Preorder α] [inst_2 : OrderTop 𝕆]
  [inst_3 : OrderTop α] [inst_4 : GradeMaxOrder 𝕆 α], grade 𝕆 ⊤ = ⊤
-- Init.Data.Iterators.Consumers.Monadic.Collect
/-- Traverses the given iterator and stores the emitted values in a list. Because
lists are prepend-only, `toListRev` is usually more efficient that `toList`.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.toList` always terminates after finitely many steps.
 -/
Std.IterM.toList : {α : Type w} → {m : Type w → Type w'} → [Monad m] → {β : Type w} → [Std.Iterator α m β] → Std.IterM m β → m (List β)
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Asymptotics.IsLittleO.sum_range : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] {f : ℕ → α} {g : ℕ → ℝ},
  f =o[Filter.atTop] g →
    0 ≤ g →
      Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, g i) Filter.atTop Filter.atTop →
        (fun n => ∑ i ∈ Finset.range n, f i) =o[Filter.atTop] fun n => ∑ i ∈ Finset.range n, g i
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.denoteN_nil : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α),
  Lean.Grind.Linarith.Poly.denoteN ctx Lean.Grind.Linarith.Poly.nil = 0
-- Init.Data.Option.Lemmas
Option.eq_none_or_eq_some : ∀ {α : Type u_1} (a : Option α), a = none ∨ ∃ x, a = some x
-- Mathlib.Topology.Filter
/-- Neighborhoods of a countably generated filter is a countably generated filter.  -/
Filter.instIsCountablyGeneratedNhds : ∀ {α : Type u_2} {l : Filter α} [l.IsCountablyGenerated], (nhds l).IsCountablyGenerated
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceBackward_forget : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X),
  f.iteratedSliceBackward.comp (CategoryTheory.Over.forget f) = CategoryTheory.Over.map f.hom
-- Mathlib.NumberTheory.NumberField.ClassNumber
Rat.classNumber_eq : NumberField.classNumber ℚ = 1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The natural inclusion `Z₁(G, A) ⟶ C₁(G, A)` is an isomorphism when the representation
on `A` is trivial.  -/
groupHomology.cycles₁IsoOfIsTrivial : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → [A.IsTrivial] → ModuleCat.of k ↥(groupHomology.cycles₁ A) ≅ ModuleCat.of k (G →₀ ↑A)
-- Aesop.Forward.State
Aesop.instInhabitedInstMap.default : Aesop.InstMap
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_const_iff_isFiniteMeasure_enorm : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {c : ε},
  ‖c‖ₑ ≠ 0 → ‖c‖ₑ ≠ ⊤ → (MeasureTheory.Integrable (fun x => c) μ ↔ MeasureTheory.IsFiniteMeasure μ)
-- Mathlib.Topology.Algebra.Group.Basic
/-- Any first countable topological group has an antitone neighborhood basis `u : ℕ → Set G` for
which `(u (n + 1)) ^ 2 ⊆ u n`. The existence of such a neighborhood basis is a key tool for
`QuotientGroup.completeSpace_right`.  -/
IsTopologicalGroup.exists_antitone_basis_nhds_one : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [FirstCountableTopology G],
  ∃ u, (nhds 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
-- Mathlib.Algebra.GCDMonoid.Basic
isGCDMonoid_iff_exists_gcd : ∀ {α : Type u_2} [inst : CommMonoidWithZero α],
  IsGCDMonoid α ↔ IsCancelMulZero α ∧ ∀ (a b : α), ∃ c, ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintKind.parameter : Lean.Lsp.InlayHintKind
-- Mathlib.Data.List.Perm.Basic
List.flatMap_append_perm : ∀ {α : Type u_1} {β : Type u_2} (l : List α) (f g : α → List β),
  (List.flatMap f l ++ List.flatMap g l).Perm (List.flatMap (fun x => f x ++ g x) l)