mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.DFA
DFA.evalFrom_cons : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) (a : α) (x : List α),
  M.evalFrom s (a :: x) = M.evalFrom (M.step s a) x
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- The closed unit ball of a valued ring is clopen.  -/
Valued.isClopen_integer : ∀ (R : Type u) [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀],
  IsClopen ↑Valued.v.integer
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
DifferentiableWithinAt.clog : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E} {x : E},
  DifferentiableWithinAt ℂ f s x → f x ∈ Complex.slitPlane → DifferentiableWithinAt ℂ (fun t => Complex.log (f t)) s x
-- Mathlib.Order.Nucleus
/-- A nucleus preserves `⊤`.  -/
Nucleus.instTopHomClass : ∀ {X : Type u_1} [inst : SemilatticeInf X] [inst_1 : OrderTop X], TopHomClass (Nucleus X) X X
-- Mathlib.LinearAlgebra.Matrix.Reindex
/-- For square matrices with coefficients in an algebra over a commutative semiring, the natural
map that reindexes a matrix's rows and columns with equivalent types,
`Matrix.reindex`, is an equivalence of algebras.  -/
Matrix.reindexAlgEquiv : {m : Type u_2} →
  {n : Type u_3} →
    (R : Type u_11) →
      (A : Type u_12) →
        [inst : CommSemiring R] →
          [inst_1 : Fintype n] →
            [inst_2 : Fintype m] →
              [inst_3 : DecidableEq m] →
                [inst_4 : DecidableEq n] →
                  [inst_5 : Semiring A] → [inst_6 : Algebra R A] → m ≃ n → Matrix m m A ≃ₐ[R] Matrix n n A
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_alter_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)] {f : Option (β k) → Option (β k)}, (m.alter k f).get! k = (f (m.get? k)).get!
-- Mathlib.CategoryTheory.Limits.Shapes.PiProd
CategoryTheory.Limits.Pi.map_eq_prod_map : ∀ {C : Type u_1} {I : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : I → C} (f : (i : I) → X i ⟶ Y i)
  (P : I → Prop) [inst_1 : CategoryTheory.Limits.HasProduct X] [inst_2 : CategoryTheory.Limits.HasProduct Y]
  [inst_3 : CategoryTheory.Limits.HasProduct fun i => X ↑i] [inst_4 : CategoryTheory.Limits.HasProduct fun i => X ↑i]
  [inst_5 : CategoryTheory.Limits.HasProduct fun i => Y ↑i] [inst_6 : CategoryTheory.Limits.HasProduct fun i => Y ↑i]
  [inst_7 : (i : I) → Decidable (P i)],
  CategoryTheory.Limits.Pi.map f =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit X P).conePointUniqueUpToIso
          (CategoryTheory.Limits.prodIsProd (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.Pi.map fun i => f ↑i)
          (CategoryTheory.Limits.Pi.map fun i => f ↑i))
        ((CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso
            (CategoryTheory.Limits.prodIsProd (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).inv)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_eq_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r : R} {m : M}, AddMonoidAlgebra.single m r = 0 ↔ r = 0
-- Mathlib.CategoryTheory.EssentiallySmall
/-- Implementation of `ShrinkHoms.equivalence`.  -/
CategoryTheory.ShrinkHoms.functor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] → CategoryTheory.Functor C (CategoryTheory.ShrinkHoms.{u} C)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.rid_toLinearEquiv : ∀ (R : Type uR) (S : Type uS) (A : Type uA) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A],
  ↑(Algebra.TensorProduct.rid R S A) = TensorProduct.AlgebraTensorModule.rid R S A
-- Init.Data.Nat.Gcd
_private.Init.Data.Nat.Gcd.0.Nat.gcd.eq_def : ∀ (m n : ℕ), m.gcd n = if m = 0 then n else (n % m).gcd m
-- Mathlib.RingTheory.LocalRing.Module
IsLocalRing.map_mkQ_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsLocalRing R] {N : Submodule R M} [Module.Finite R M],
  Submodule.map (IsLocalRing.maximalIdeal R • ⊤).mkQ N = ⊤ ↔ N = ⊤
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.toProd_apply_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] (x : M),
  AddMonoid.Coprod.toProd (AddMonoid.Coprod.inl x) = (x, 0)
-- Init.Data.Nat.Lemmas
Nat.mul_sub_mod : ∀ {x n p : ℕ}, x < n * p → (n * p - (x + 1)) % n = n - (x % n + 1)
-- Mathlib.GroupTheory.PushoutI
/-- All maps in the diagram are injective  -/
Monoid.PushoutI.NormalWord.Transversal.injective : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} (self : Monoid.PushoutI.NormalWord.Transversal φ) (i : ι), Function.Injective ⇑(φ i)
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.mk.injEq : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (toLieModuleHom : M →ₗ⁅R,L⁆ N) (invFun : N → M)
  (left_inv : Function.LeftInverse invFun (↑toLieModuleHom).toFun)
  (right_inv : Function.RightInverse invFun (↑toLieModuleHom).toFun) (toLieModuleHom_1 : M →ₗ⁅R,L⁆ N) (invFun_1 : N → M)
  (left_inv_1 : Function.LeftInverse invFun_1 (↑toLieModuleHom_1).toFun)
  (right_inv_1 : Function.RightInverse invFun_1 (↑toLieModuleHom_1).toFun),
  ({ toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toLieModuleHom := toLieModuleHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }) =
    (toLieModuleHom = toLieModuleHom_1 ∧ invFun = invFun_1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.all_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} {p : α → β → Bool},
  ((Std.DHashMap.Const.toList m).all fun x => p x.1 x.2) = m.all p
-- Mathlib.RingTheory.LocalProperties.Exactness
exact_of_isLocalized_span : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {L : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid L]
  [inst_6 : Module R L] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Mₚ : ↑s → Type u_5) [inst_7 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_8 : (r : ↑s) → Module R (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [inst_9 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] (Nₚ : ↑s → Type u_6)
      [inst_10 : (r : ↑s) → AddCommMonoid (Nₚ r)] [inst_11 : (r : ↑s) → Module R (Nₚ r)] (g : (r : ↑s) → N →ₗ[R] Nₚ r)
      [inst_12 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)] (Lₚ : ↑s → Type u_7)
      [inst_13 : (r : ↑s) → AddCommMonoid (Lₚ r)] [inst_14 : (r : ↑s) → Module R (Lₚ r)] (h : (r : ↑s) → L →ₗ[R] Lₚ r)
      [inst_15 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (h r)] (F : M →ₗ[R] N) (G : N →ₗ[R] L),
      (∀ (r : ↑s),
          Function.Exact ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
            ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G)) →
        Function.Exact ⇑F ⇑G
-- Mathlib.Geometry.Manifold.Instances.Real
IccLeftChart_extend_interior_pos : ∀ {x y : ℝ} [hxy : Fact (x < y)] {p : ↑(Set.Icc x y)},
  x < ↑p ∧ ↑p < y → 0 < (↑((IccLeftChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) p).ofLp 0
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.IsLeftQuasiInverse.eq_1 : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] (u : V →ₗ[K] V₂) (v : V₂ →ₗ[K] V),
  u.IsLeftQuasiInverse v = (u ∘ₗ v ≈ LinearMap.id)
-- Init.Data.Fin.Lemmas
/-- The cast of the successor is the successor of the cast. See `Fin.succ_cast_eq` for rewriting in
the reverse direction.  -/
Fin.cast_succ_eq : ∀ {n n' : ℕ} (i : Fin n) (h : n.succ = n'.succ), Fin.cast h i.succ = (Fin.cast ⋯ i).succ
-- Mathlib.Analysis.Normed.MulAction
IsBoundedSMul.of_nnnorm_smul_le : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedRing α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : Module α β],
  (∀ (r : α) (x : β), ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊) → IsBoundedSMul α β
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.summable_symmetricIco_of_summable_symmetricIcc : ∀ {α : Type u_1} {f : ℤ → α} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [ContinuousAdd α],
  Summable f (SummationFilter.symmetricIcc ℤ) →
    Filter.Tendsto (fun N => -f ↑N) Filter.atTop (nhds 0) → Summable f (SummationFilter.symmetricIco ℤ)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isClosed_subsets_of_isClosed : ∀ {α : Type u_1} [inst : TopologicalSpace α] {F : Set α}, IsClosed F → IsClosed {K | ↑K ⊆ F}
-- Mathlib.Data.Int.Init
Int.le_div_iff_of_dvd_of_pos : ∀ {a b c : ℤ}, 0 < c → c ∣ b → (a ≤ b / c ↔ c * a ≤ b)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.withCurrentStackSize : (ℕ → Lean.Parser.ParserFn) → Lean.Parser.ParserFn
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.instSliceableRocSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.instSliceableRocSlice._auto_1) →
      Std.Roc.Sliceable (Std.TreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.Const.RocSlice α β)
-- Mathlib.Tactic.Simps.Basic
/-- `instantiateLambdasOrApps es e` instantiates lambdas in `e` by expressions from `es`.
If the length of `es` is larger than the number of lambdas in `e`,
then the term is applied to the remaining terms.
Also reduces head let-expressions in `e`, including those after instantiating all lambdas.

This is very similar to `expr.substs`, but this also reduces head let-expressions.  -/
Lean.Expr.instantiateLambdasOrApps : Array Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.apply_mem_iff : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {x : α},
  e.IsImage s t → x ∈ e.source → (↑e x ∈ t ↔ x ∈ s)
-- Mathlib.Data.Finset.Defs
Finset.mk_coe : ∀ {α : Type u_1} {s : Finset α} (x : ↑↑s) {h : ↑x ∈ ↑s}, ⟨↑x, h⟩ = x
-- Mathlib.Topology.NhdsSet
nhdsSet_singleton : ∀ {X : Type u_2} [inst : TopologicalSpace X] {x : X}, nhdsSet {x} = nhds x
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono'_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.LeftHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono' φ h).φH =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h).H
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.one_apply : ∀ {n : Type u_2} {A : Type u_5} [inst : DecidableEq n] [inst_1 : Zero A] [inst_2 : One A] {i j : n},
  1 i j = if i = j then 1 else 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.logDeriv_exp : logDeriv Real.exp = 1
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.map_eq_zero_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β}, AEMeasurable f μ → (MeasureTheory.Measure.map f μ = 0 ↔ μ = 0)
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- **Alias** of `Stirling.log_stirlingSeq_sdiff_hasSum`.

---

The sequence `log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2))` has the series expansion
`∑ 1 / (2 * (k + 1) + 1) * (1 / 2 * (m + 1) + 1)^(2 * (k + 1))`.  -/
Stirling.log_stirlingSeq_diff_hasSum : ∀ (m : ℕ),
  HasSum (fun k => 1 / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ (k + 1))
    (Real.log (Stirling.stirlingSeq (m + 1)) - Real.log (Stirling.stirlingSeq (m + 2)))
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.intermediateFieldEquivSubgroup_symm_apply_toDual : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : FiniteDimensional F E] [inst_4 : IsGalois F E] (H : Subgroup Gal(E/F)),
  IsGalois.intermediateFieldEquivSubgroup.symm (OrderDual.toDual H) = IntermediateField.fixedField H
-- Init.Data.BitVec.Lemmas
BitVec.toNat_sshiftRight_of_msb_true : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, x.msb = true → (x.sshiftRight n).toNat = 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n
-- Init.Grind.Propagator
/-- Auxiliary attribute for builtin `grind` propagators.  -/
Lean.Parser.grindPropagatorBuiltinAttr : Lean.ParserDescr
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.map_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {f : α → γ} {g : β → γ}
  {μ : autoParam (MeasureTheory.Measure α) ProbabilityTheory.IdentDistrib._auto_1}
  {ν : autoParam (MeasureTheory.Measure β) ProbabilityTheory.IdentDistrib._auto_3},
  ProbabilityTheory.IdentDistrib f g μ ν → MeasureTheory.Measure.map f μ = MeasureTheory.Measure.map g ν
-- Mathlib.Algebra.Group.Submonoid.Support
AddSubmonoid.IsPointed.mk : ∀ {G : Type u_1} [inst : AddGroup G] {M : AddSubmonoid G}, (∀ x ∈ M, -x ∈ M → x = 0) → M.IsPointed
-- Mathlib.Data.Finset.NAry
Finset.image₂_inter_singleton : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {b : β} [inst_1 : DecidableEq α]
  (s₁ s₂ : Finset α),
  (Function.Injective fun a => f a b) → Finset.image₂ f (s₁ ∩ s₂) {b} = Finset.image₂ f s₁ {b} ∩ Finset.image₂ f s₂ {b}
-- Lean.Linter.UnusedVariables
Lean.Linter.UnusedVariables.FVarDefinition.mk.sizeOf_spec : ∀ (userName : Lean.Name) (stx : Lean.Syntax) (opts : Lean.Options) (aliases : Array Lean.FVarId),
  sizeOf { userName := userName, stx := stx, opts := opts, aliases := aliases } =
    1 + sizeOf userName + sizeOf stx + sizeOf opts + sizeOf aliases
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.length_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Logic.Equiv.Option
/-- Equivalences between `Option α` and `β` that send `none` to `x` are equivalent to
equivalences between `α` and `{y : β // y ≠ x}`.  -/
Equiv.optionSubtype : {α : Type u_1} → {β : Type u_2} → [DecidableEq β] → (x : β) → { e // e none = x } ≃ (α ≃ { y // y ≠ x })
-- Lean.Elab.Match
/-- Main method for `withDepElimPatterns`.
- `PatternVarDecls`: are the explicit pattern variables provided by the user.
- `ps`: are the patterns provided by the user.
- `matchType`: the expected typ for this branch. It depends on the explicit pattern variables and the implicit ones that are still represented as metavariables,
   and are found by this function.
- `k` is the continuation that is executed in an updated local context with the all pattern variables (explicit and implicit). Note that, `patternVarDecls` are all
   replaced since they may depend on implicit pattern variables (i.e., metavariables) that are converted into new free variables by this method.
 -/
Lean.Elab.Term.ToDepElimPattern.main : {α : Type} →
  Array Lean.Elab.Term.PatternVarDecl →
    Array Lean.Expr →
      Lean.Expr →
        (Array Lean.LocalDecl → Array Lean.Meta.Match.Pattern → Lean.Expr → Lean.Elab.TermElabM α) →
          Lean.Elab.TermElabM α
-- Mathlib.FieldTheory.Normal.Defs
Normal.mk : ∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  [toIsAlgebraic : Algebra.IsAlgebraic F K],
  (∀ (x : K), (Polynomial.map (algebraMap F K) (minpoly F x)).Splits) → Normal F K
-- Mathlib.Algebra.Homology.HomotopyFiber
/-- The path object of a homological complex is defined here by dualizing
the cylinder object of `K.op`.  -/
HomologicalComplex.pathObject : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {α : Type u_2} →
        {c : ComplexShape α} →
          (K : HomologicalComplex C c) →
            [DecidableRel c.Rel] →
              [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [K.HasPathObject] → HomologicalComplex C c.symm.symm
-- Mathlib.CategoryTheory.Action.Basic
Action.mk.sizeOf_spec : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] [inst_2 : SizeOf V]
  [inst_3 : SizeOf G] (V_1 : V) (ρ : G →* CategoryTheory.End V_1),
  sizeOf { V := V_1, ρ := ρ } = 1 + sizeOf V_1 + sizeOf ρ
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.mapRange.linearEquiv_trans : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {R : Type u_5} {R₂ : Type u_6} {R₃ : Type u_7}
  [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : AddCommMonoid N] [inst_6 : Module R₂ N] [inst_7 : AddCommMonoid P] [inst_8 : Module R₃ P] {σ₁₂ : R →+* R₂}
  {σ₂₁ : R₂ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R}
  [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [inst_11 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_12 : RingHomInvPair σ₂₁ σ₁₂] [inst_13 : RingHomInvPair σ₂₃ σ₃₂] [inst_14 : RingHomInvPair σ₃₂ σ₂₃]
  [inst_15 : RingHomInvPair σ₁₃ σ₃₁] [inst_16 : RingHomInvPair σ₃₁ σ₁₃] (f : M ≃ₛₗ[σ₁₂] N) (f₂ : N ≃ₛₗ[σ₂₃] P),
  Finsupp.mapRange.linearEquiv (f.trans f₂) = (Finsupp.mapRange.linearEquiv f).trans (Finsupp.mapRange.linearEquiv f₂)
-- Mathlib.Data.Set.Image
Set.exists_image_iff : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : Set α) (P : β → Prop), (∃ a, P ↑a) ↔ ∃ a, P (f ↑a)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₁.X₃ = Y
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_eq_union_iff_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t
-- Mathlib.GroupTheory.Divisible
divisibleByOfSMulRightSurj.eq_1 : ∀ (A : Type u_1) (α : Type u_2) [inst : AddMonoid A] [inst_1 : SMul α A] [inst_2 : Zero α]
  (H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a => n • a),
  divisibleByOfSMulRightSurj A α H =
    { div := fun a n => if x : n = 0 then 0 else ⋯.choose, div_zero := ⋯, div_cancel := ⋯ }
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_comp_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (n : σ →₀ ℕ),
  MvPowerSeries.coeff n ∘ₗ MvPowerSeries.monomial n = LinearMap.id
-- Mathlib.RingTheory.Congruence.Hom
RingCon.comapQuotientEquivRangeS_symm_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] (c : RingCon M) (f : N →+* M)
  {d : RingCon N} (hcd : d = c.comap f) (x : N), (c.comapQuotientEquivRangeS f hcd).symm ⟨↑(f x), ⋯⟩ = ↑x
-- Init.Data.String.Basic
String.Pos.Raw.IsValid.isValidUTF8_extract_utf8ByteSize : ∀ {s : String} {p : String.Pos.Raw},
  String.Pos.Raw.IsValid s p → (s.toByteArray.extract p.byteIdx s.utf8ByteSize).IsValidUTF8
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wf_filterMap₀ : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} [inst : BEq α] [inst_1 : Hashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  (↑m).WF → ∀ {f : (a : α) → β a → Option (δ a)}, (↑(Std.DHashMap.Internal.Raw₀.filterMap f m)).WF
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- `Localization.mk` as a monoid hom.  -/
AddLocalization.mkHom : {M : Type u_1} → [inst : AddCommMonoid M] → {S : AddSubmonoid M} → M × ↥S →+ AddLocalization S
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.instHasEqualizers : CategoryTheory.Limits.HasEqualizers ωCPO
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- `PreservesLimitsOfSize.{v u} F` means that `F` sends all limit cones over any
diagram `J ⥤ C` to limit cones, where `J : Type u` with `[Category.{v} J]`.  -/
CategoryTheory.Limits.PreservesLimitsOfSize : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.ne_endPos_of_singleton : ∀ {t₁ : String} {c : Char} {t₂ s : String} {p : s.Pos}, p.Splits t₁ (String.singleton c ++ t₂) → p ≠ s.endPos
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.needsNoEscapeAscii : (s : String) → s.utf8ByteSize > 0 → Bool
-- Mathlib.Analysis.LocallyConvex.Polar
StrongDual.polar_zero : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E], StrongDual.polar 𝕜 {0} = Set.univ
-- Mathlib.Data.Finset.Empty
Finset.nonempty_iff_ne_empty : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty ↔ s ≠ ∅
-- Mathlib.Topology.Continuous
tendsto_lift'_closure_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → ∀ (x : X), Filter.Tendsto f ((nhds x).lift' closure) ((nhds (f x)).lift' closure)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minEntry?.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
      h_3 size k v l size_1 k_1 v_1 l_1 r h r_1) =
    h_1 ()
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsTree.dist_ne_of_adj : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsTree → ∀ (u : V) {v w : V}, G.Adj v w → G.dist u v ≠ G.dist u w
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.castLE_castLE : ∀ {L : FirstOrder.Language} {α : Type u'} {k m n : ℕ} (km : k ≤ m) (mn : m ≤ n) (φ : L.BoundedFormula α k),
  FirstOrder.Language.BoundedFormula.castLE mn (FirstOrder.Language.BoundedFormula.castLE km φ) =
    FirstOrder.Language.BoundedFormula.castLE ⋯ φ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₂.d₂₃_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (x : ↥(groupCohomology.cocycles₂ A)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.d₂₃ A)) ⇑x = 0