mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.maxEntry.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β)
  (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l l_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_2 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l_1 = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r →
                      (h :
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r)).isEmpty =
                            false) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r))
                          h),
  (match Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x with
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_1 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l l_1@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r), h_3 =>
      h_2 size k v l l_1 size_1 k_1 v_1 l_2 r h h_3) =
    h_1 size k v l x
-- Mathlib.FieldTheory.Relrank
IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_of_le : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E),
  B ≤ f.fieldRange →
    Cardinal.lift.{v, w} ((IntermediateField.comap f A).relrank (IntermediateField.comap f B)) =
      Cardinal.lift.{w, v} (A.relrank B)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.whiskerLeft_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b) {β β' : b ⟶ c}
  (y : β ⟶ β'),
  (CategoryTheory.Bicategory.Adj.Bicategory.whiskerLeft α y).τr = CategoryTheory.Bicategory.whiskerRight y.τr α.r
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instHashableExpr : Hashable Lean.Grind.CommRing.Expr
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.isCardinalPresentable_monotone : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  {κ' : Cardinal.{w}} [inst_2 : Fact κ'.IsRegular],
  κ ≤ κ' → CategoryTheory.isCardinalPresentable C κ ≤ CategoryTheory.isCardinalPresentable C κ'
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies expressions of the form `a - b` in a ring,
such that `norm_num` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.NormNum.evalSub : Mathlib.Meta.NormNum.NormNumExt
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanPrepareModuleHierarchyParams.mk.inj : ∀ {textDocument textDocument_1 : Lean.Lsp.TextDocumentIdentifier},
  { textDocument := textDocument } = { textDocument := textDocument_1 } → textDocument = textDocument_1
-- Mathlib.Topology.List
/-- Continuity of `insertIdx` in terms of `Tendsto`.  -/
List.tendsto_insertIdx' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {n : ℕ} {l : List α},
  Filter.Tendsto (fun p => p.2.insertIdx n p.1) (nhds a ×ˢ nhds l) (nhds (l.insertIdx n a))
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app : ∀ {R : CommRingCat} (M : (AlgebraicGeometry.Spec (CommRingCat.of ↑R)).Modules)
  (U : (AlgebraicGeometry.Spec (CommRingCat.of ↑R)).Opens),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.tilde.toOpen ((AlgebraicGeometry.modulesSpecToSheaf.obj M).presheaf.obj (Opposite.op ⊤)) U)
      ((AlgebraicGeometry.modulesSpecToSheaf.map M.fromTildeΓ).hom.app (Opposite.op U)) =
    (AlgebraicGeometry.modulesSpecToSheaf.obj M).obj.map (CategoryTheory.homOfLE ⋯).op
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The sine of an angle in a right-angled triangle as a ratio of sides.  -/
Orientation.sin_oangle_add_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle x (x + y)).sin = ‖y‖ / ‖x + y‖
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_ofReal : ∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6} [inst_1 : RCLike 𝕜]
  {f : X → ℝ}, ∫ (x : X), ↑(f x) ∂μ = ↑(∫ (x : X), f x ∂μ)
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.dynEntourage_antitone : ∀ {X : Type u_1} (T : X → X) (U : SetRel X X), Antitone fun n => Dynamics.dynEntourage T U n
-- Mathlib.MeasureTheory.Function.EssSup
le_essInf_of_ae_le : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {f : α → β} (c : β),
  (fun x => c) ≤ᵐ[μ] f →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae μ) f) le_essInf_of_ae_le._auto_1 →
      c ≤ essInf f μ
-- Mathlib.FieldTheory.Finiteness
Module.card_eq_pow_finrank : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [inst_3 : Fintype K]
  [inst_4 : Fintype V], Fintype.card V = Fintype.card K ^ Module.finrank K V
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.range_sin : Set.range Real.sin = Set.Icc (-1) 1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.toList_eq_match : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α],
  r.toList =
    match Std.PRange.succ? r.lower with
    | none => []
    | some next => if next < r.upper then next :: (next<...r.upper).toList else []
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.proj_bot_bijective : ∀ {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : DiscreteTopology X], Function.Bijective ⊥.proj
-- Init.Data.Array.Lemmas
Array.getElem_setIfInBounds_self : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {a : α} (h : i < (xs.setIfInBounds i a).size), (xs.setIfInBounds i a)[i] = a
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- Interpolating between `ContinuousAffineMap`s with `AffineMap.lineMap` commutes with
evaluation.  -/
ContinuousAffineMap.lineMap_apply' : ∀ {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] [inst_9 : TopologicalSpace W]
  [inst_10 : IsTopologicalAddGroup W] [inst_11 : IsTopologicalAddTorsor Q] [inst_12 : ContinuousConstSMul R W]
  [inst_13 : SMulCommClass R R W] (f g : P →ᴬ[R] Q) (c : R) (p : P),
  ((AffineMap.lineMap f g) c) p = (AffineMap.lineMap (f p) (g p)) c
-- Mathlib.Order.Lattice
/-- **Alias** of the reverse direction of `sup_eq_right`. -/
sup_of_le_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≤ b → a ⊔ b = b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α},
  Std.ExtDTreeMap.Const.get? (t₁ ∩ t₂) k = if k ∈ t₂ then Std.ExtDTreeMap.Const.get? t₁ k else none
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.congr' : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P → ∀ {s : Set H} {x : H} {f g : H → H'}, f =ᶠ[nhds x] g → P g s x → P f s x
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mapAlgebra_comp_mapAlgebra : ∀ {R : Type u} [inst : CommSemiring R] {A : Type u_5} {B : Type u_6} [inst_1 : CommSemiring A] [inst_2 : CommSemiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B],
  (CommRing.Pic.mapAlgebra A B).comp (CommRing.Pic.mapAlgebra R A) = CommRing.Pic.mapAlgebra R B
-- Mathlib.Combinatorics.Quiver.SingleObj
/-- The type of arrows from `star α` to itself is equivalent to the original type `α`.  -/
Quiver.SingleObj.toHom : {α : Type u_1} → α ≃ (Quiver.SingleObj.star α ⟶ Quiver.SingleObj.star α)
-- Mathlib.MeasureTheory.MeasurableSpace.Prod
measurableEmbedding_prodMk_left : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [MeasurableSingletonClass α]
  (x : α), MeasurableEmbedding (Prod.mk x)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS.match_1.congr_eq_3 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (x : Lean.Grind.CommRing.Expr) → motive x) (x : Lean.Grind.CommRing.Expr),
  a = x →
    (∀ (n : ℤ), x = Lean.Grind.CommRing.Expr.num n → False) →
      (∀ (x_2 : Lean.Grind.CommRing.Var), x = Lean.Grind.CommRing.Expr.var x_2 → False) →
        (match a with
          | Lean.Grind.CommRing.Expr.num n => h_1 n
          | Lean.Grind.CommRing.Expr.var x => h_2 x
          | x => h_3 x) ≍
          h_3 x
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
mul_inv_lt_of_lt_mul₀ : ∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] {a b c : α}, a < b * c → a * c⁻¹ < b
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.toMeasure_apply : ∀ {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms ≤ m.caratheodory) {s : Set α},
  MeasurableSet s → (m.toMeasure h) s = m s
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.freeHomEquiv_apply : ∀ {R : Type u} [inst : Ring R] {X : Type u} {M : ModuleCat R} (φ : (ModuleCat.free R).obj X ⟶ M),
  ModuleCat.freeHomEquiv φ = TypeCat.ofHom fun x => (CategoryTheory.ConcreteCategory.hom φ) (ModuleCat.freeMk x)
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.RepresentablyFlat.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ (X : D), CategoryTheory.IsCofiltered (CategoryTheory.StructuredArrow X F)) → CategoryTheory.RepresentablyFlat F
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.card_eq_sum_ite : ∀ {ι : Type u_1} {s t : Finset ι} [inst : DecidablePred fun x => x ∈ s],
  s ⊆ t → s.card = ∑ i ∈ t, if i ∈ s then 1 else 0
-- Mathlib.Algebra.Lie.BaseChange
LieAlgebra.ExtendScalars.instLieAlgebra : (R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : Algebra R A] → [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → LieAlgebra A (TensorProduct R A L)
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_insert_abs : ∀ {α : Type u} [inst : Ring α] (x : α) (s : Set α) [inst_1 : LinearOrder α],
  Ideal.span (insert |x| s) = Ideal.span (insert x s)
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
/-- A contravariant functor on `C` satisfies `SingleEqualizerCondition` with respect to a morphism `π`
if it takes its kernel pair to an equalizer diagram.
 -/
CategoryTheory.regularTopology.SingleEqualizerCondition : {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] → CategoryTheory.Functor Cᵒᵖ D → ⦃X B : C⦄ → (X ⟶ B) → Prop
-- Mathlib.Data.Set.Image
Set.range_id' : ∀ {α : Type u_1}, (Set.range fun x => x) = Set.univ
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.instIsLocallyFiniteMeasure : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R], MeasureTheory.IsLocallyFiniteMeasure f.measure
-- Mathlib.Data.Finset.Basic
Finset.disjoint_insert_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α},
  a ∉ t → (Disjoint (s.erase a) (insert a t) ↔ Disjoint s t)
-- Init.Data.Vector.Lemmas
Vector.mk_eq : ∀ {α : Type u_1} {as : Array α} {a : ℕ} {h : as.size = a} {xs : Vector α a}, Vector.mk as h = xs ↔ as = xs.toArray
-- Mathlib.Tactic.GRewrite.Core
/-- Create the `gcongr` goal corresponding to rewriting `e` by relation `rel?`,
so that we can apply `gcongr` lemmas to it.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.makeGCongrGoal : Option Lean.Expr → Lean.Expr → Bool → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.Algebra.Star.Basic
star_zero : ∀ (R : Type u) [inst : AddMonoid R] [inst_1 : StarAddMonoid R], star 0 = 0
-- Init.Data.Iterators.Combinators.ULift
/-- Transforms an iterator with values in `β` into one with values in `ULift β`.

Most other combinators like `map` cannot switch between universe levels. This combinators
makes it possible to transition to a higher universe.

**Marble diagram:**

```
it            ---a    ----b    ---c    --d    ---⊥
it.uLift n    ---.up a----.up b---.up c--.up d---⊥
```

**Termination properties:**

* `Finite`: only if the original iterator is finite
* `Productive`: only if the original iterator is productive
 -/
Std.Iter.uLift : {α β : Type u} → Std.Iter β → Std.Iter (ULift.{v, u} β)
-- Mathlib.Order.Booleanisation
Booleanisation.LE.sep : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α},
  Disjoint a b → (Booleanisation.lift a).LE (Booleanisation.comp b)
-- Mathlib.NumberTheory.ModularForms.SlashActions
_private.Mathlib.NumberTheory.ModularForms.SlashActions.0.ModularForm.privateSlash.eq_1 : ∀ (k : ℤ) (γ : GL (Fin 2) ℝ) (f : UpperHalfPlane → ℂ) (x : UpperHalfPlane),
  ModularForm.privateSlash✝ k γ f x =
    (UpperHalfPlane.σ γ) (f (γ • x)) * ↑|↑(Matrix.GeneralLinearGroup.det γ)| ^ (k - 1) *
      UpperHalfPlane.denom γ ↑x ^ (-k)
-- Mathlib.RingTheory.Polynomial.Quotient
/-- If `I` is an ideal of `R`, then the ring polynomials over the quotient ring `I.quotient` is
isomorphic to the quotient of `R[X]` by the ideal `map C I`,
where `map C I` contains exactly the polynomials whose coefficients all lie in `I`.  -/
Ideal.polynomialQuotientEquivQuotientPolynomial : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → Polynomial (R ⧸ I) ≃+* Polynomial R ⧸ Ideal.map Polynomial.C I
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.piecewise_toPartialHomeomorph : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e e' : OpenPartialHomeomorph X Y) (s : Set X) (t : Set Y) [inst_2 : (x : X) → Decidable (x ∈ s)]
  [inst_3 : (y : Y) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t)
  (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)),
  (e.piecewise e' s t H H' Hs Heq).toPartialHomeomorph =
    { toPartialEquiv := e.piecewise e'.toPartialEquiv s t H H', continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }
-- Mathlib.Order.Heyting.Basic
ofDual_compl : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : αᵒᵈ), OrderDual.ofDual aᶜ = ￢OrderDual.ofDual a
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.instContinuousFourierInv : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V]
  [inst_6 : BorelSpace V], ContinuousFourierInv (SchwartzMap V E) (SchwartzMap V E)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_union_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h₁ : t₁.WF)
  (h₂ : t₂.WF) {k : α} (mem : k ∈ t₂), (t₁ ∪ t₂).get k ⋯ = t₂.get k mem
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Lift a `M → α` function to `MulArchimedeanClass M → α`.  -/
MulArchimedeanClass.lift : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedMonoid M] →
        {α : Type u_2} →
          (f : M → α) →
            (∀ (a b : M), MulArchimedeanClass.mk a = MulArchimedeanClass.mk b → f a = f b) → MulArchimedeanClass M → α
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.cons : {α : Type u} →
  {β : α → Type v} → (key : α) → β key → Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β
-- Mathlib.Data.Int.Cast.Defs
/-- The canonical homomorphism `ℤ → R` agrees with the one from `ℕ → R` on `ℕ`.  -/
AddGroupWithOne.intCast_ofNat : ∀ {R : Type u} [self : AddGroupWithOne R] (n : ℕ), IntCast.intCast ↑n = ↑n
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearMap.mdifferentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E →L[𝕜] E'), MDiff ⇑f
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
/-- The weak topology is the coarsest topology on `E` such that all functionals
`fun x => v x` are continuous.  -/
WeakSpace : (𝕜 : Type u_6) →
  (E : Type u_7) →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [ContinuousAdd 𝕜] →
          [ContinuousConstSMul 𝕜 𝕜] → [inst_4 : AddCommMonoid E] → [Module 𝕜 E] → [TopologicalSpace E] → Type u_7
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.map_π_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) (j : J) {Z : C} (h : g j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map p)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π g j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j)
      (CategoryTheory.CategoryStruct.comp (p j) h)
-- Mathlib.FieldTheory.Galois.Abelian
instIsAbelianGaloisSubtypeMemIntermediateField_1 : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [IsAbelianGalois K L]
  (K' : IntermediateField K L), IsAbelianGalois (↥K') L
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyLE!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} [inst : Inhabited α],
          Std.DTreeMap.Internal.Impl.getKeyLE! k t₁ = Std.DTreeMap.Internal.Impl.getKeyLE! k t₂
-- Init.Data.BitVec.Lemmas
BitVec.of_length_zero : ∀ {x : BitVec 0}, x = 0#0
-- Std.Data.HashMap.RawLemmas
/-- Simpler variant of `getElem_filterMap` when `LawfulBEq` is available.  -/
Std.HashMap.Raw.getElem_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : LawfulBEq α] {f : α → β → Option γ} {k : α} {g : k ∈ Std.HashMap.Raw.filterMap f m} (h : m.WF),
  (Std.HashMap.Raw.filterMap f m)[k] = (f k m[k]).get ⋯
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- Let `{ Dᵢ }` be a cofiltered diagram of compact schemes with affine transition maps.
If `U ⊆ Dⱼ` contains the image of `limᵢ Dᵢ ⟶ Dⱼ`, then it contains the image of some `Dₖ ⟶ Dⱼ`.  -/
AlgebraicGeometry.exists_map_eq_top : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] [∀ (i : I), CompactSpace ↥(D.obj i)] {i : I}
  (U : (D.obj i).Opens),
  (TopologicalSpace.Opens.map (c.π.app i).base).obj U = ⊤ →
    ∃ j fji, (TopologicalSpace.Opens.map (D.map fji).base).obj U = ⊤
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.precomp_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (c : B) (f : a ⟶ b) {X Y : b ⟶ c} (x : X ⟶ Y),
  (CategoryTheory.Bicategory.precomp c f).map x = CategoryTheory.Bicategory.whiskerLeft f x
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : X.Opens)
  (hUV : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (Y.presheaf.obj (Opposite.op U)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp V.toSpecΓ
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appLE f U V hUV))
        h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.resLE f U V hUV)
      (CategoryTheory.CategoryStruct.comp U.toSpecΓ h)
-- Mathlib.CategoryTheory.Types.Basic
/-- **Alias** of `CategoryTheory.Iso.hom_inv_id_app_apply`. -/
CategoryTheory.FunctorToTypes.hom_inv_id_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) {F_1 : D → D → Type uF} {carrier : D → Type w}
  {instFunLike : (X Y : D) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory D F_1]
  (x : carrier (F.obj X)),
  (CategoryTheory.ConcreteCategory.hom (α.inv.app X)) ((CategoryTheory.ConcreteCategory.hom (α.hom.app X)) x) = x
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instCommRingInt64 : Lean.Grind.CommRing Int64
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.δ_leftUnshift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {a n' : ℤ}
  (γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ)
  (hn : n + a = n') (m m' : ℤ) (hm' : m + a = m'),
  CochainComplex.HomComplex.δ n m (γ.leftUnshift n hn) =
    a.negOnePow • (CochainComplex.HomComplex.δ n' m' γ).leftUnshift m hm'
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.rotateR.match_1.eq_1 : ∀ {α : Type u_1} (motive : Ordnode α → α → Ordnode α → Sort u_2) (size : ℕ) (l : Ordnode α) (x : α) (m : Ordnode α)
  (y : α) (r : Ordnode α)
  (h_1 :
    (size : ℕ) →
      (l : Ordnode α) → (x : α) → (m : Ordnode α) → (y : α) → (r : Ordnode α) → motive (Ordnode.node size l x m) y r)
  (h_2 : (y : α) → (r : Ordnode α) → motive Ordnode.nil y r),
  (match Ordnode.node size l x m, y, r with
    | Ordnode.node size l x m, y, r => h_1 size l x m y r
    | Ordnode.nil, y, r => h_2 y r) =
    h_1 size l x m y r
-- Mathlib.Algebra.Order.Invertible
invOf_le_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} [inst_3 : Invertible a],
  1 ≤ a → ⅟a ≤ 1
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.ext : ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : Turing.ListBlank Γ}, (∀ (i_1 : ℕ), L₁.nth i_1 = L₂.nth i_1) → L₁ = L₂
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.α_hom : {C : Type u} → (X Y Z : CategoryTheory.FreeMonoidalCategory C) → ((X.tensor Y).tensor Z).Hom (X.tensor (Y.tensor Z))