mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
/-- The total derivative of a function in two variables is the sum of the partial derivatives.
Note that to state this (without casts) we need to be able to see through the definition of
`TangentSpace`.  -/
mfderiv_prod_eq_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M × M' → M''} {p : M × M'},
  MDiffAt f p → mfderiv% f p = (mfderiv% fun z => f (z.1, p.2)) p + (mfderiv% fun z => f (p.1, z.2)) p
-- Mathlib.Order.SupClosed
upperBounds_supClosure : ∀ {α : Type u_3} [inst : SemilatticeSup α] (s : Set α), upperBounds (supClosure s) = upperBounds s
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.toNonneg_le : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : SemilatticeSup α] {a : α} {b : { x // 0 ≤ x }},
  Nonneg.toNonneg a ≤ b ↔ a ≤ ↑b
-- Init.Data.List.Basic
/-- Returns a list of the numbers with the given length `len`, starting at `start` and increasing by
`step` at each element.

In other words, `List.range'TR start len step` is `[start, start+step, ..., start+(len-1)*step]`.

This is a tail-recursive version of `List.range'`.

Examples:
 * `List.range'TR 0 3 (step := 1) = [0, 1, 2]`
 * `List.range'TR 0 3 (step := 2) = [0, 2, 4]`
 * `List.range'TR 0 4 (step := 2) = [0, 2, 4, 6]`
 * `List.range'TR 3 4 (step := 2) = [3, 5, 7, 9]`
 -/
List.range'TR : ℕ → ℕ → optParam ℕ 1 → List ℕ
-- Mathlib.Topology.Algebra.Group.Basic
isClosedMap_sub_right : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] (a : G),
  IsClosedMap fun x => x - a
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The constructed localized category for a morphism property
that has left calculus of fractions.  -/
CategoryTheory.MorphismProperty.LeftFraction.Localization : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.MorphismProperty C → Type u_1
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable.0.cond.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The Lie algebra corresponding to a Cartan matrix.

Note that it is defined for any matrix of integers. Its value for non-Cartan matrices should be
regarded as junk.  -/
Matrix.ToLieAlgebra : (R : Type u) → {B : Type v} → [CommRing R] → Matrix B B ℤ → [DecidableEq B] → Type (max (max v u) u v)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.adj_comm : ∀ {V : Type u} (G : SimpleGraph V) (u v : V), G.Adj u v ↔ G.Adj v u
-- Mathlib.Data.TwoPointing
/-- The product of two two-pointings.  -/
TwoPointing.prod : {α : Type u_1} → {β : Type u_2} → TwoPointing α → TwoPointing β → TwoPointing (α × β)
-- Mathlib.Order.RelIso.Basic
RelIso.coe_fn_symm_mk : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : α ≃ β)
  (o : ∀ {a b : α}, s (f a) (f b) ↔ r a b), ⇑{ toEquiv := f, map_rel_iff' := o }.symm = ⇑f.symm
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.enum : Lean.Lsp.SemanticTokenType
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.compl_cylinder : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (S : Set ((i : ↥s) → α ↑i)),
  (MeasureTheory.cylinder s S)ᶜ = MeasureTheory.cylinder s Sᶜ
-- Lean.Declaration
Lean.ReducibilityHints.abbrev.sizeOf_spec : sizeOf Lean.ReducibilityHints.abbrev = 1
-- Std.Http.Protocol.H1
/-- Builds canonical framing headers for a chosen transfer mode.
The caller handles status/method exceptions that should skip normalization.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.normalizeFramingHeaders : Std.Http.Headers → Std.Http.Body.Length → Std.Http.Headers
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.algEquivOfTranscendental_symm_gen : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : L)
  (h : Transcendental K f),
  (RatFunc.algEquivOfTranscendental f h).symm (IntermediateField.AdjoinSimple.gen K f) = RatFunc.X
-- Mathlib.Algebra.Free
FreeAddMagma.map.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β), FreeAddMagma.map f = FreeAddMagma.lift (FreeAddMagma.of ∘ f)
-- Mathlib.Order.OrderIsoNat
WellFoundedGT.monotone_chain_condition' : ∀ {α : Type u_1} [inst : Preorder α] [h : WellFoundedGT α] (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.isCofiltered : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (self : J.Point),
  CategoryTheory.IsCofiltered self.fiber.Elements
-- Mathlib.Analysis.Seminorm
Seminorm.ball_sup : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p q : Seminorm 𝕜 E) (e : E) (r : ℝ), (p ⊔ q).ball e r = p.ball e r ∩ q.ball e r
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- The scalar factor between two left-invariant measures is non-zero when both measures are
positive on open sets.  -/
MeasureTheory.Measure.haarScalarFactor_pos_of_isHaarMeasure : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsHaarMeasure]
  [inst_6 : μ'.IsHaarMeasure], 0 < μ'.haarScalarFactor μ
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt) (j : C),
  ((t.eTriangleLTGE.obj i).obj j).mor₁ = (t.eTruncLTι i).app j
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.pred_lt_iff_not_isSuccPrelimit : ∀ {o : Ordinal.{u_4}}, o.pred < o ↔ ¬Order.IsSuccPrelimit o
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M},
  MDiffAt f x → f₁ =ᶠ[nhds x] f → MDiffAt f₁ x
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_add_left_left_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime (y * z + x) y ↔ IsCoprime x y
-- Mathlib.Order.LiminfLimsup
Filter.limsup.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] (u : β → α) (f : Filter β),
  Filter.limsup u f = (Filter.map u f).limsSup
-- Mathlib.Data.Nat.Nth
Nat.nth_lt_nth_of_lt_card : ∀ {p : ℕ → Prop} (hf : (Set.ofPred p).Finite) {m n : ℕ}, m < n → n < hf.toFinset.card → Nat.nth p m < Nat.nth p n
-- Mathlib.Algebra.Star.Subalgebra
StarAlgHom.subtype_comp_codRestrict : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : Semiring B] [inst_6 : Algebra R B] [inst_7 : StarRing B]
  [inst_8 : StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S),
  S.subtype.comp (f.codRestrict S hf) = f
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.isNonloop_iff_delete_of_notMem : ∀ {α : Type u_1} {M : Matroid α} {e : α} {D : Set α}, e ∉ D → (M.IsNonloop e ↔ (M.delete D).IsNonloop e)
-- Mathlib.Algebra.Group.Defs
DivInvMonoid.toDiv : {G : Type u} → [self : DivInvMonoid G] → Div G
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.compLeft.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  {γ : Type u_5} [inst_3 : TopologicalSpace γ] [inst_4 : Zero γ] (g : C(β, γ))
  (f : CompactlySupportedContinuousMap α β),
  CompactlySupportedContinuousMap.compLeft g f =
    { toContinuousMap := if g 0 = 0 then g.comp ↑f else 0, hasCompactSupport' := ⋯ }
-- Mathlib.Topology.Separation.Basic
/-- In an R₁ space, a point belongs to the closure of a compact set `K`
if and only if it is topologically inseparable from some point of `K`.  -/
IsCompact.mem_closure_iff_exists_inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {y : X} {K : Set X},
  IsCompact K → (y ∈ closure K ↔ ∃ x ∈ K, Inseparable x y)
-- Lean.Data.Format
Lean.instToFormatKVMap : Std.ToFormat Lean.KVMap
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.right' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y : C) →
        [CategoryTheory.MonoidalCoherence X Y] →
          CategoryTheory.MonoidalCoherence X
            (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Mathlib.Algebra.Group.Units.Hom
Units.coe_liftRight : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] {f : M →* N} {g : M → Nˣ}
  (h : ∀ (x : M), ↑(g x) = f x) (x : M), ↑((Units.liftRight f g h) x) = f x
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.leadingCoeff_preΨ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {n : ℤ},
  ↑n ≠ 0 → (W.preΨ n).leadingCoeff = ↑(if Even n then n / 2 else n)
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
SimplexCategory.toMk₁_injective : ∀ {n : ℕ}, Function.Injective SimplexCategory.toMk₁
-- Mathlib.RingTheory.Ideal.Prod
Ideal.coe_prod : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (I : Ideal R) (J : Ideal S),
  ↑(I.prod J) = ↑I ×ˢ ↑J
-- Mathlib.Tactic.Widget.Conv
/-- End a `conv` sequence with `depth`-many repetitions of the `conv` tactic `fun`.
For example, `Path.fun 3` corresponds to the `conv` sequence `fun; fun; fun`,
and `Path.fun 0` just terminates a `Path` without any extra `conv` tactics.
 -/
Mathlib.Tactic.Conv.Path.fun : ℕ → Mathlib.Tactic.Conv.Path
-- Init.Notation
/-- Alternative syntax for `<|`. `f $ x` means the same as `f x`,
except that it parses `x` with lower precedence, which means that `f $ g $ x`
is interpreted as `f (g x)` rather than `(f g) x`.
 -/
«term_$__» : Lean.TrailingParserDescr
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_apply_of_containsKey_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α]
  {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : Std.Internal.List.DistinctKeys l)
  (h :
    Std.Internal.List.containsKey k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
      true),
  (f k (Std.Internal.List.getValueCast k l ⋯)).isSome = true
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.instIsFaithfulEnd : ∀ (R : Type u) (M : Type w) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  LieModule.IsFaithful R (Module.End R M) M
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_inter_eq_size_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (∀ a ∈ m₂, a ∈ m₁) → (m₁ ∩ m₂).size = m₂.size
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A *tree* is a connected acyclic graph.  -/
SimpleGraph.IsTree : {V : Type u_1} → SimpleGraph V → Prop
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
/-- Coercion from subgroups of `SL(2, ℤ)` to subgroups of `GL(2, ℝ)` by mapping along the obvious
inclusion homomorphism.  -/
Subgroup.instCoeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupReal : Coe (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (Subgroup (GL (Fin 2) ℝ))
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_map_equiv : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'}
  (X : Ω → ℝ) (Y : Ω' ≃ᵐ Ω),
  ProbabilityTheory.variance X (MeasureTheory.Measure.map (⇑Y) μ) = ProbabilityTheory.variance (X ∘ ⇑Y) μ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.obj.μ_def_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] (X : C) [inst_5 : CategoryTheory.MonObj X] {Z : D}
  (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X X)
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.MonObj.mul) h)
-- Mathlib.Data.Stream.Init
Stream'.dropLast_take : ∀ {α : Type u} {n : ℕ} {xs : Stream' α}, (Stream'.take n xs).dropLast = Stream'.take (n - 1) xs
-- Lean.Data.JsonRpc
Lean.JsonRpc.instBEqRequest.beq : {α : Type u_1} → [BEq α] → Lean.JsonRpc.Request α → Lean.JsonRpc.Request α → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.liftOfStrictSegal_app_1 : ∀ {X Y : SSet.Truncated 2}
  (f₀ :
    X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
      Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }))
  (f₁ :
    X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
      Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }))
  (hδ₁ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hδ₀ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (H :
    ∀ (x : X.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ }))
      (y : Y.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ })),
      f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝ _proof_15✝).op)) x) =
          (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝ _proof_15✝).op)) y →
        f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝ _proof_15✝).op)) x) =
            (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝ _proof_15✝).op)) y →
          f₁
              ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝ _proof_15✝).op))
                x) =
            (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝ _proof_15✝).op)) y)
  (hσ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })),
      f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝ _proof_11✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝ _proof_11✝).op)) (f₀ x))
  (hY : Y.StrictSegal),
  (SSet.Truncated.liftOfStrictSegal f₀ f₁ hδ₁ hδ₀ H hσ hY).app
      (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) =
    TypeCat.ofHom f₁
-- Mathlib.Topology.Category.LightProfinite.Extend
/-- Given a functor `G` from `LightProfinite` and `S : LightProfinite`, we obtain a cone on
`(StructuredArrow.proj S toLightProfinite ⋙ toLightProfinite ⋙ G)` with cone point `G.obj S`.

Whiskering this cone with `LightProfinite.Extend.functor c` gives `G.mapCone c` as we check in the
example below.
 -/
LightProfinite.Extend.cone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (G : CategoryTheory.Functor LightProfinite C) →
      (S : LightProfinite) →
        CategoryTheory.Limits.Cone
          ((CategoryTheory.StructuredArrow.proj S FintypeCat.toLightProfinite).comp
            (FintypeCat.toLightProfinite.comp G))
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.Hom.mk.injEq : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} (hom' hom'_1 : ↑M →ₗ[R] ↑N),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stepAux.eq_def : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (x : Turing.TM2.Stmt Γ Λ σ)
  (x_1 : σ) (x_2 : (k : K) → List (Γ k)),
  Turing.TM2.stepAux x x_1 x_2 =
    match x, x_1, x_2 with
    | Turing.TM2.Stmt.push k f q, v, S => Turing.TM2.stepAux q v (Function.update S k (f v :: S k))
    | Turing.TM2.Stmt.peek k f q, v, S => Turing.TM2.stepAux q (f v (S k).head?) S
    | Turing.TM2.Stmt.pop k f q, v, S => Turing.TM2.stepAux q (f v (S k).head?) (Function.update S k (S k).tail)
    | Turing.TM2.Stmt.load a q, v, S => Turing.TM2.stepAux q (a v) S
    | Turing.TM2.Stmt.branch f q₁ q₂, v, S => bif f v then Turing.TM2.stepAux q₁ v S else Turing.TM2.stepAux q₂ v S
    | Turing.TM2.Stmt.goto f, v, S => { l := some (f v), var := v, stk := S }
    | Turing.TM2.Stmt.halt, v, S => { l := none, var := v, stk := S }
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- (Implementation): The refinement morphism `cylinder f g ⟶ E`.  -/
CategoryTheory.PreOneHypercover.cylinderHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
            (f g : E.Hom F) → (CategoryTheory.PreOneHypercover.cylinder f g).Hom E
-- Lean.Server.References
Lean.Server.ModuleImport.mk : Lean.Name → Lean.Lsp.DocumentUri → Bool → Bool → Lean.Lsp.LeanImportMetaKind → Lean.Server.ModuleImport
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_setWidth' : ∀ {m n : ℕ} (ge : m ≥ n) (x : BitVec n) (i : ℕ), (BitVec.setWidth' ge x).getLsbD i = x.getLsbD i
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.order_neg : ∀ {R : Type u_2} [inst : Ring R] (φ : PowerSeries R), (-φ).order = φ.order
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryProductEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C)
  (z : (F ⨯ G).obj a),
  (CategoryTheory.FunctorToTypes.binaryProductEquiv F G a) z =
    (((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryProductIso F G).hom.app a)) z).1,
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryProductIso F G).hom.app a)) z).2)
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.succ?_eq_none_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  (f : Std.PRange.UpwardEnumerable.Map α β) {a : α}, Std.PRange.succ? a = none ↔ Std.PRange.succ? (f.toFun a) = none
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.symm_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A), P.symm.I = P.I
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `lowerSemicontinuousOn_neg_iff`. -/
UpperSemicontinuousOn.neg : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β], UpperSemicontinuousOn f s → LowerSemicontinuousOn (-f) s
-- Mathlib.RingTheory.TensorProduct.Basic
LinearMap.liftBaseChange_comp : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : Module A N] [inst_8 : IsScalarTower R A N] {P : Type u_1} [inst_9 : AddCommMonoid P]
  [inst_10 : Module A P] [inst_11 : Module R P] [inst_12 : IsScalarTower R A P] (l : M →ₗ[R] N) (l' : N →ₗ[A] P),
  l' ∘ₗ LinearMap.liftBaseChange A l = LinearMap.liftBaseChange A (↑R l' ∘ₗ l)
-- Mathlib.Algebra.Group.TransferInstance
Equiv.addCommMonoid.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : AddCommMonoid β],
  e.addCommMonoid = Function.Injective.addCommMonoid ⇑e ⋯ ⋯ ⋯ ⋯
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.elabHeadersAux.match_1.splitter : (motive : Lean.Expr × ℕ → Sort u_1) →
  (x : Lean.Expr × ℕ) → ((type : Lean.Expr) → (snd : ℕ) → motive (type, snd)) → motive x
-- Init.Data.List.Impl
/-- Auxiliary for `setTR`: `setTR.go l a xs n acc = acc.toList ++ set xs a`,
unless `n ≥ l.length` in which case it returns `l`  -/
_private.Init.Data.List.Impl.0.List.setTR.go : {α : Type u_1} → List α → α → List α → ℕ → Array α → List α
-- Mathlib.Geometry.Manifold.HasGroupoid
TopologicalSpace.Opens.chartAt_subtype_val_symm_eventuallyEq : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (U : TopologicalSpace.Opens M) {x : ↥U},
  ↑(chartAt H ↑x).symm =ᶠ[nhds (↑(chartAt H ↑x) ↑x)] Subtype.val ∘ ↑(chartAt H x).symm
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instT4Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T4Space M], T4Space Mᵈᵐᵃ
-- Mathlib.Algebra.Module.ZLattice.Covolume
/-- A version of `ZLattice.covolume.tendsto_card_div_pow` for the general case;
see the `Naming convention` section in the introduction.  -/
ZLattice.covolume.tendsto_card_div_pow'' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {L : Submodule ℤ E}
  [inst_2 : DiscreteTopology ↥L] [inst_3 : IsZLattice ℝ L] {ι : Type u_2} [inst_4 : Fintype ι] (b : Module.Basis ι ℤ ↥L)
  [inst_5 : FiniteDimensional ℝ E] [inst_6 : MeasurableSpace E] [BorelSpace E] {s : Set E},
  Bornology.IsBounded s →
    MeasurableSet s →
      MeasureTheory.volume (frontier (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0 →
        Filter.Tendsto (fun n => ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ Fintype.card ι) Filter.atTop
          (nhds (MeasureTheory.volume.real (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' s)))
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.instBEqInlayHintTextEdit.beq : Lean.Elab.InlayHintTextEdit → Lean.Elab.InlayHintTextEdit → Bool
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.linearMapAt.eq_1 : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Bundle.Pretrivialization.IsLinear R e] (b : B),
  Bundle.Pretrivialization.linearMapAt R e b =
    if hb : b ∈ e.baseSet then ↑(Bundle.Pretrivialization.linearEquivAt R e b hb) else 0