mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_eq_some_getValueCast : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
  (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getValueCast? a l = some (Std.Internal.List.getValueCast a l h)
-- Lean.DefEqAttrib
/-- Validates that `declName` is a definitional equality at `.default`/`.all` transparency
(the legacy permissive check). Throws a diagnostic error if not. This is used both as
the validator for the `@[defeq]` and `@[backward_defeq]` attributes and as a building
block for `inferDefEqAttr`.
 -/
Lean.validateDefEqAttr : Lean.Name → Lean.AttrM Unit
-- Mathlib.Analysis.SumIntegralExpDecay
sum_Iic_pow_mul_two_pow_neg_le : ∀ {k M : ℕ} {c : ℝ}, 0 < c → ∑ i ≤ M, ↑i ^ k * 2 ^ (-(c * ↑i)) ≤ 2 ^ c * ↑k.factorial / (Real.log 2 * c) ^ (k + 1)
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts
/-- Has conical products if all discrete diagrams of bounded size have conical products.  -/
CategoryTheory.Enriched.HasConicalProducts : (V : outParam (Type u')) →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u) → [inst_2 : CategoryTheory.Category.{v, u} C] → [CategoryTheory.EnrichedOrdinaryCategory V C] → Prop
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.toCat_map : ∀ {X Y : SimplexCategory} (f : X ⟶ Y), SimplexCategory.toCat.map f = ⋯.functor.toCatHom
-- Init.Data.List.Lemmas
List.getLast_eq_getLastD : ∀ {α : Type u_1} {a : α} {l : List α} (h : a :: l ≠ []), (a :: l).getLast h = l.getLastD a
-- Mathlib.Analysis.Convex.Side
AffineSubspace.isPreconnected_setOfPred_wOppSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P),
  IsPreconnected {y | s.WOppSide x y}
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The additive group equivalence between `ContinuousLinearMapWOT` and `ContinuousLinearMap`.  -/
ContinuousLinearMapWOT.addEquiv : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_3} →
            {F : Type u_4} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : Module 𝕜₂ F] → [inst_8 : IsTopologicalAddGroup F] → (E →SWOT[σ] F) ≃+ (E →SL[σ] F)
-- Init.Data.Slice.Array.Lemmas
Array.toSubarray_eq_toSubarray_of_min_eq_min : ∀ {α : Type u_1} {xs : Array α} {start stop stop' : ℕ},
  min stop xs.size = min stop' xs.size → xs.toSubarray start stop = xs.toSubarray start stop'
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.tendsto_comp_exp_atTop : ∀ {α : Type u_1} {l : Filter α} {f : ℝ → α},
  Filter.Tendsto (fun x => f (Real.exp x)) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.IterM.step_uLift.match_1.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubseqResult.middle.inj : ∀ {p s p_1 s_1 : Lean.Grind.AC.Seq},
  Lean.Grind.AC.SubseqResult.middle p s = Lean.Grind.AC.SubseqResult.middle p_1 s_1 → p = p_1 ∧ s = s_1
-- Init.Data.Rat.Lemmas
Rat.intCast_mul : ∀ (a b : ℤ), ↑(a * b) = ↑a * ↑b
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendHomologyIso_inv_homologyι : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'],
  CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').inv ((K.extend e).homologyι j') =
    CategoryTheory.CategoryStruct.comp (K.homologyι j) (K.extendOpcyclesIso e hj').inv
-- Mathlib.SetTheory.Cardinal.Defs
/-- A variant of `Cardinal.lift_mk_eq` with specialized universes.
Because Lean often cannot realize it should use this specialization itself,
we provide this statement separately so you don't have to solve the specialization problem either.
 -/
Cardinal.lift_mk_eq' : ∀ {α : Type u} {β : Type v},
  Cardinal.lift.{v, u} (Cardinal.mk α) = Cardinal.lift.{u, v} (Cardinal.mk β) ↔ Nonempty (α ≃ β)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
CovariantDerivative.isCovariantDerivativeOn : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] (cov : CovariantDerivative I F V)
  {s : Set M}, IsCovariantDerivativeOn F (↑cov) s
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.instIsStableUnderBaseChangeAlongL : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] (S₁ : CategoryTheory.Span Wₗ Wᵣ c c'), Wᵣ.IsStableUnderBaseChangeAlong S₁.l
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYonedaEquiv_symm_map_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y)
  {F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} (t : F.obj X) {Z : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))}
  (h : F ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.uliftYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYoneda.{w, v₁, u₁}.map f.unop)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYonedaEquiv.symm t) h)
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.mkMulProof.match_1.eq_1 : ∀ {v : Lean.Level} {M : Q(Type v)} (motive : Mathlib.Tactic.FieldSimp.qNF M → Mathlib.Tactic.FieldSimp.qNF M → Sort u_1)
  (l : Mathlib.Tactic.FieldSimp.qNF M) (h_1 : (l : Mathlib.Tactic.FieldSimp.qNF M) → motive [] l)
  (h_2 : (l : Mathlib.Tactic.FieldSimp.qNF M) → motive l [])
  (h_3 :
    (a₁ : ℤ) →
      (x₁ : Q(«$M»)) →
        (k₁ : ℕ) →
          (t₁ : List ((ℤ × Q(«$M»)) × ℕ)) →
            (a₂ : ℤ) →
              (x₂ : Q(«$M»)) →
                (k₂ : ℕ) → (t₂ : List ((ℤ × Q(«$M»)) × ℕ)) → motive (((a₁, x₁), k₁) :: t₁) (((a₂, x₂), k₂) :: t₂)),
  (match [], l with
    | [], l => h_1 l
    | l, [] => h_2 l
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ => h_3 a₁ x₁ k₁ t₁ a₂ x₂ k₂ t₂) =
    h_1 l
-- Mathlib.Algebra.Group.Defs
mul_nsmul' : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M) (m n : ℕ), (m * n) • a = m • n • a
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.instInhabitedId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → Inhabited (CategoryTheory.Functor.id C ⊣ CategoryTheory.Functor.id C)
-- Mathlib.Order.Defs.Unbundled
not_rel_of_subsingleton : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Irrefl r] [Subsingleton α] (x y : α), ¬r x y
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given a homomorphism `f` from the quotient of an `AddMonoid` by an
additive congruence relation, `f` equals the homomorphism on the quotient induced by `f` composed
with the natural map from the `AddMonoid` to the quotient.  -/
AddCon.lift_apply_mk' : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M} (f : c.Quotient →+ P),
  c.lift (f.comp c.mk') ⋯ = f
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion.0.IsCovariantDerivativeOn.torsionAux_tensorial₂ : ∀ {𝕜 : 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] [inst_6 : IsManifold I 2 M] [CompleteSpace E]
  {cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x},
  IsCovariantDerivativeOn E cov →
    ∀ (x : M) (X : (x : M) → TangentSpace I x),
      TensorialAt I E (fun x_1 => IsCovariantDerivativeOn.torsionAux✝ cov X x_1 x) x
-- Lean.Language.Basic
Lean.Language.SnapshotTree.brecOn_3.eq : ∀ {motive_1 : Lean.Language.SnapshotTree → Sort u}
  {motive_2 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u}
  {motive_3 : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u}
  {motive_4 : Lean.Language.SnapshotTask Lean.Language.SnapshotTree → Sort u}
  {motive_5 : Task Lean.Language.SnapshotTree → Sort u} (t : Lean.Language.SnapshotTask Lean.Language.SnapshotTree)
  (F_1 : (t : Lean.Language.SnapshotTree) → t.below → motive_1 t)
  (F_2 :
    (t : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
      Lean.Language.SnapshotTree.below_1 t → motive_2 t)
  (F_3 :
    (t : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
      Lean.Language.SnapshotTree.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_3 t → motive_4 t)
  (F_5 : (t : Task Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_4 t → motive_5 t),
  Lean.Language.SnapshotTree.brecOn_3 t F_1 F_2 F_3 F_4 F_5 =
    F_4 t (Lean.Language.SnapshotTree.brecOn_3.go t F_1 F_2 F_3 F_4 F_5).2
-- Mathlib.Topology.Algebra.MulAction
OrderDual.instContinuousVAdd_right : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : VAdd M X]
  [ContinuousVAdd M X], ContinuousVAdd M Xᵒᵈ
-- Mathlib.Topology.Bases
/-- A second countable space is mapped by an open quotient map to a second countable space.  -/
Topology.IsQuotientMap.secondCountableTopology : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : TopologicalSpace Y] {π : X → Y}
  [SecondCountableTopology X], Topology.IsQuotientMap π → IsOpenMap π → SecondCountableTopology Y
-- Mathlib.Topology.Sheaves.Presheaf
/-- restriction of a section to open subset  -/
AlgebraicGeometry.«term_|__» : Lean.TrailingParserDescr
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `Topology.IsGeneratedBy.iSup`. -/
DeltaGeneratedSpace.iSup : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type u_1} {κ : Sort u_2}
  {t : κ → TopologicalSpace Y}, (∀ (k : κ), Topology.IsGeneratedBy X Y) → Topology.IsGeneratedBy X Y
-- Init.Data.Repr
instReprOption : {α : Type u_1} → [Repr α] → Repr (Option α)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.IterM.step_takeWhileM.match_1.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : MonadAttach m] {P : β → m (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (MonadAttach.CanReturn (P out)) → Sort u_3) (hP : MonadAttach.CanReturn (P out) { down := true })
  (h_1 : (hP : MonadAttach.CanReturn (P out) { down := true }) → motive ⟨{ down := true }, hP⟩)
  (h_2 : (hP : MonadAttach.CanReturn (P out) { down := false }) → motive ⟨{ down := false }, hP⟩),
  (match ⟨{ down := true }, hP⟩ with
    | ⟨{ down := true }, hP⟩ => h_1 hP
    | ⟨{ down := false }, hP⟩ => h_2 hP) =
    h_1 hP
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- Suppose that `p₁` and `p₂` lie in spheres `s₁` and `s₂`. Then the vector between the centers
of those spheres is orthogonal to that between `p₁` and `p₂`; this is a version of
`inner_vsub_vsub_of_dist_eq_of_dist_eq` for bundled spheres. (In two dimensions, this says that
the diagonals of a kite are orthogonal.)  -/
EuclideanGeometry.inner_vsub_vsub_of_mem_sphere_of_mem_sphere : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ : P} {s₁ s₂ : EuclideanGeometry.Sphere P},
  p₁ ∈ s₁ → p₂ ∈ s₁ → p₁ ∈ s₂ → p₂ ∈ s₂ → inner ℝ (s₂.center -ᵥ s₁.center) (p₂ -ᵥ p₁) = 0
-- Mathlib.FieldTheory.Finiteness
Module.natCard_eq_pow_finrank : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [Module.Finite K V],
  Nat.card V = Nat.card K ^ Module.finrank K V
-- Mathlib.Order.Category.DistLat
DistLat.hom_ext : ∀ {X Y : DistLat} {f g : X ⟶ Y}, DistLat.Hom.hom f = DistLat.Hom.hom g → f = g
-- Std.Data.TreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the smallest key that is
greater than the given key.
 -/
Std.TreeMap.getKeyGT : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.TreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.gt) → α
-- Mathlib.Algebra.FreeMonoid.Symbols
FreeAddMonoid.symbols.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (a : FreeAddMonoid α), a.symbols = List.toFinset a
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.UnifIntegrable.sub : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f g : ι → α → β} {p : ENNReal},
  MeasureTheory.UnifIntegrable f p μ →
    MeasureTheory.UnifIntegrable g p μ →
      1 ≤ p →
        (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) →
          (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (g i) μ) → MeasureTheory.UnifIntegrable (f - g) p μ
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.toZSMul : {α : Type u_3} → [self : LinearOrderedAddCommGroupWithTop α] → ZSMul α
-- Mathlib.Topology.Inseparable
SeparationQuotient.continuousWithinAt_lift₂ : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y → Z}
  {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a c → Inseparable b d → f a b = f c d}
  {s : Set (SeparationQuotient X × SeparationQuotient Y)} {x : X} {y : Y},
  ContinuousWithinAt (Function.uncurry (SeparationQuotient.lift₂ f hf)) s
      (SeparationQuotient.mk x, SeparationQuotient.mk y) ↔
    ContinuousWithinAt (Function.uncurry f) (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s) (x, y)
-- Init.Data.Float.Model.Float32
Float32.Model.instLT : LT Float32.Model
-- Init.Data.SInt.Lemmas
Int32.neg_nonpos_iff : ∀ (n : Int32), -n ≤ 0 ↔ n = Int32.minValue ∨ 0 ≤ n
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.Theory.IsUniversal.isUniversal_of_mem : ∀ {L : FirstOrder.Language} {T : L.Theory} [self : T.IsUniversal] ⦃φ : L.Sentence⦄,
  φ ∈ T → FirstOrder.Language.BoundedFormula.IsUniversal φ
-- Mathlib.Topology.Order.DenselyOrdered
IsMax.of_disjoint_nhds_Ioi : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {x : α}
  {u : Set α}, u ∈ nhds x → Disjoint u (Set.Ioi x) → IsMax x
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsWeaklyRegular.cons' : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {r : R}
  {rs : List R},
  IsSMulRegular M r →
    RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) →
      RingTheory.Sequence.IsWeaklyRegular M (r :: rs)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.refl_toEquiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_5} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_9)
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (n : WithTop ℕ∞),
  (Diffeomorph.refl I M n).toEquiv = Equiv.refl M
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.eval_basis_not_at_node : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι} {x : F},
  i ∈ s →
    x ≠ v i →
      Polynomial.eval x (Lagrange.basis s v i) =
        Polynomial.eval x (Lagrange.nodal s v) * (Lagrange.nodalWeight s v i * (x - v i)⁻¹)
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.prod.diag.match_1.eq_1 : ∀ (motive : (x : ℕ) → (x_1 : TypeVec.{u_1} x) → (x : Fin2 x) → x_1 x → Sort u_2) (n : ℕ) (α : TypeVec.{u_1} n.succ)
  (a : Fin2 n) (x : α a.fs)
  (h_1 : (n : ℕ) → (α : TypeVec.{u_1} n.succ) → (a : Fin2 n) → (x : α a.fs) → motive n.succ α a.fs x)
  (h_2 : (n : ℕ) → (x : TypeVec.{u_1} n.succ) → (x_1 : x Fin2.fz) → motive n.succ x Fin2.fz x_1),
  (match n.succ, α, a.fs, x with
    | n.succ, α, a.fs, x => h_1 n α a x
    | n.succ, x, Fin2.fz, x_1 => h_2 n x x_1) =
    h_1 n α a x
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.PlausibleStep.skip : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  {it' : Std.IterM m β},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it') →
    it.internalState.countdown ≠ 1 →
      Std.Iterators.Types.Take.PlausibleStep it
        (Std.IterStep.skip { internalState := { countdown := it.internalState.countdown, inner := it', finite := ⋯ } })
-- Mathlib.Order.Filter.CountablyGenerated
Filter.isCountablyGenerated_iff_exists_antitone_basis : ∀ {α : Type u_1} {f : Filter α}, f.IsCountablyGenerated ↔ ∃ x, f.HasAntitoneBasis x
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.Term.listEncode.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : L.Term α → Sort u_4) (l : ℕ) (f : L.Functions l)
  (ts : Fin l → L.Term α) (h_1 : (i : α) → motive (FirstOrder.Language.var i))
  (h_2 : (l : ℕ) → (f : L.Functions l) → (ts : Fin l → L.Term α) → motive (FirstOrder.Language.func f ts)),
  (match FirstOrder.Language.func f ts with
    | FirstOrder.Language.var i => h_1 i
    | FirstOrder.Language.func f ts => h_2 l f ts) =
    h_2 l f ts
-- Mathlib.Data.PNat.Prime
PNat.one_coprime : ∀ {n : ℕ+}, PNat.Coprime 1 n
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.add_right : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν → ∀ (ν' : MeasureTheory.Measure α), μ.AbsolutelyContinuous (ν + ν')
-- Mathlib.Analysis.SumIntegralComparisons
_private.Mathlib.Analysis.SumIntegralComparisons.0.AntitoneOn.intervalIntegrable_subset : ∀ {x₀ : ℝ} {a : ℕ} {f : ℝ → ℝ},
  AntitoneOn f (Set.Icc x₀ (x₀ + ↑a)) →
    ∀ (k : ℕ), k + 1 ≤ a → IntervalIntegrable f MeasureTheory.volume (x₀ + ↑k) (x₀ + ↑(k + 1))
-- Mathlib.Algebra.Order.Sub.Defs
AddLECancellable.add_tsub_cancel_left : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b : α},
  AddLECancellable a → a + b - a = b
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- If, for all `x` in a set `s`, one has frequently `q < ρ a / μ a`, then `q * μ s ≤ ρ s`, as
proved in `measure_le_of_frequently_le`. Since `ρ a / μ a` tends almost everywhere to
`v.limRatioMeas hρ x`, the same property holds for sets `s` on which `q < v.limRatioMeas hρ`.  -/
VitaliFamily.mul_measure_le_of_subset_lt_limRatioMeas : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α]
  [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) {q : NNReal} {s : Set α},
  s ⊆ {x | ↑q < v.limRatioMeas hρ x} → ↑q * μ s ≤ ρ s
-- Mathlib.Algebra.Lie.Nilpotent
LieAlgebra.non_trivial_center_of_isNilpotent : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [Nontrivial L]
  [LieRing.IsNilpotent L], Nontrivial ↥(LieAlgebra.center R L)
-- Lean.Attributes
/-- Tag attributes are simple and efficient. They are useful for marking declarations in the modules where
they were defined.

The startup cost for this kind of attribute is very small since `addImportedFn` is a constant function.

They provide the predicate `tagAttr.hasTag env decl` which returns true iff declaration `decl`
is tagged in the environment `env`.  -/
Lean.TagAttribute : Type
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_hom : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U)
  (V : TopCat.Presheaf.SheafCondition.OpensLeCover U),
  ((TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).obj V).obj.hom = CategoryTheory.homOfLE ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_bind_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.minKey?.bind t.getKey? = t.minKey?
-- Mathlib.Data.Finset.Basic
Finset.filter_not : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] [inst_1 : DecidableEq α] (s : Finset α),
  {a ∈ s | ¬p a} = s \ Finset.filter p s
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
/-- The property of preserving coproducts expressed in terms of cofans.  -/
CategoryTheory.Limits.isColimitCofanMkObjOfIsColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            (f : J → C) →
              [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] →
                {P : C} →
                  (g : (j : J) → f j ⟶ P) →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk P g) →
                      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (G.obj P) fun j => G.map (g j))
-- Lean.Server.GoTo
Lean.Server.GoToKind.declaration.sizeOf_spec : sizeOf Lean.Server.GoToKind.declaration = 1
-- Mathlib.CategoryTheory.Equivalence
/-- If `e : C ≌ D` is an equivalence of categories, and `iso : e.functor ≅ G` is
an isomorphism, then there is an equivalence of categories whose functor is `G`.  -/
CategoryTheory.Equivalence.changeFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (e : C ≌ D) → {G : CategoryTheory.Functor C D} → (e.functor ≅ G) → (C ≌ D)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.toRuleFilters : Aesop.Frontend.RuleExpr → Aesop.ElabM (Array (Aesop.RuleSetNameFilter × Aesop.RuleFilter))