mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Order
Lean.Grind.Order.le_of_not_lt : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsLinearPreorder α] {a b : α}, ¬a < b → b ≤ a
-- Mathlib.Data.Finset.Lattice.Fold
Finset.isLUB_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α},
  IsLUB (f '' ↑s) (s.sup f)
-- Mathlib.Algebra.Homology.Embedding.Connect
_private.Mathlib.Algebra.Homology.Embedding.Connect.0.CochainComplex.ConnectData.d.match_1.splitter : (motive : ℤ → ℤ → Sort u_1) →
  (x x_1 : ℤ) →
    ((n m : ℕ) → motive (Int.ofNat n) (Int.ofNat m)) →
      ((n m : ℕ) → motive (Int.negSucc n) (Int.negSucc m)) →
        (Unit → motive (Int.negSucc 0) (Int.ofNat 0)) →
          ((a a_1 : ℕ) → motive (Int.ofNat a) (Int.negSucc a_1)) →
            ((a a_1 : ℕ) → (a = 0 → a_1 = 0 → False) → motive (Int.negSucc a) (Int.ofNat a_1)) → motive x x_1
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.sum_basis : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F},
  Set.InjOn v ↑s → s.Nonempty → ∑ j ∈ s, Lagrange.basis s v j = 1
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.toTopologicalSpace_sInf : ∀ {α : Type u} [inst : AddGroup α] (s : Set (AddGroupTopology α)),
  (sInf s).toTopologicalSpace = sInf (AddGroupTopology.toTopologicalSpace '' s)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.traj.congr_simp : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (κ κ_1 : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))) (e_κ : κ = κ_1)
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ),
  ProbabilityTheory.Kernel.traj κ a = ProbabilityTheory.Kernel.traj κ_1 a
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsExtrOn.lineDeriv_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E},
  IsExtrOn f s a → (∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) → lineDeriv ℝ f a b = 0
-- Mathlib.Logic.Basic
/-- Any relation `p` is decidable classically.  -/
Classical.decRel : {α : Sort u_1} → (p : α → α → Prop) → DecidableRel p
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_Ioc_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (a : α i), Pi.mulSingle i '' Set.Ioc a 1 = Set.Ioc (Pi.mulSingle i a) 1
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.addScopes : Lean.Name →
  Bool →
    optParam Bool false →
      optParam Bool false →
        optParam Bool false →
          optParam (List (Lean.TSyntax `Lean.Parser.Term.attrInstance)) [] → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange_sub' : ∀ {ι : Type u_1} {F : Type u_2} {G : Type u_6} {H : Type u_7} [inst : AddGroup G] [inst_1 : SubtractionMonoid H]
  [inst_2 : FunLike F G H] [inst_3 : AddMonoidHomClass F G H] {f : F} (v₁ v₂ : ι →₀ G),
  Finsupp.mapRange ⇑f ⋯ (v₁ - v₂) = Finsupp.mapRange ⇑f ⋯ v₁ - Finsupp.mapRange ⇑f ⋯ v₂
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev?_startPos : ∀ {s : String.Slice}, s.startPos.prev? = none
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSMulZeroClassForallOfSMul : {M : Type u_1} → {β : Type u_2} → {α : Type u_3} → [SMul M α] → [inst : Zero β] → SMulZeroClass Mᵈᵐᵃ (α → β)
-- Init.Data.Slice.List.Lemmas
List.size_mkSlice_rio : ∀ {α : Type u_1} {xs : List α} {hi : ℕ}, Std.Slice.size (Std.Rio.Sliceable.mkSlice xs *...hi) = min hi xs.length
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.mapEquivMonic_symm_map : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (n : ℕ) (p : Polynomial.MonicDegreeEq S n) (g : S →ₐ[R] T),
  (MvPolynomial.mapEquivMonic R T n).symm (p.map ↑g) = g.comp ((MvPolynomial.mapEquivMonic R S n).symm p)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_left_nil : ∀ {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (hu : m = 0), Fin.append u v = v ∘ Fin.cast ⋯
-- Init.Data.Slice.List.Basic
Std.Slice.Internal.ListSliceData.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (list : List α) (stop : Option ℕ),
  sizeOf { list := list, stop := stop } = 1 + sizeOf list + sizeOf stop
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf hkf_1 : CategoryTheory.Limits.IsLimit kf),
  hkf = hkf_1 →
    ∀ (hcc hcc_1 : CategoryTheory.Limits.IsColimit cc),
      hcc = hcc_1 →
        ∀ {H : C} {π π_1 : kf.pt ⟶ H} (e_π : π = π_1) {ι ι_1 : H ⟶ cc.pt} (e_ι : ι = ι_1)
          (fac :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
              CategoryTheory.CategoryStruct.comp π ι)
          [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
          CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac =
            CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf_1 hcc_1 ⋯
-- Mathlib.Analysis.Analytic.Basic
AnalyticWithinAt.congr_set : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s t : Set E}
  {x : E}, AnalyticWithinAt 𝕜 f s x → s =ᶠ[nhds x] t → AnalyticWithinAt 𝕜 f t x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the reverse direction of `Units.inv_le_one`. -/
Units.inv_le_one_of_le : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ), 1 ≤ ↑u → ↑u⁻¹ ≤ 1
-- Mathlib.Topology.Clopen
isClopen_empty : ∀ {X : Type u} [inst : TopologicalSpace X], IsClopen ∅
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k fallback : α},
  (Std.ExtDTreeMap.map f t).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.CategoryTheory.Limits.Cones
/-- A functor `G : C ⥤ D` sends cocones over `F` to cocones over `F ⋙ G` functorially.  -/
CategoryTheory.Limits.Cocone.functoriality : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (F : CategoryTheory.Functor J C) →
              (G : CategoryTheory.Functor C D) →
                CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone (F.comp G))
-- Std.Data.HashSet.Lemmas
Std.HashSet.fold_eq_foldl_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {δ : Type v} {f : δ → α → δ} {init : δ},
  Std.HashSet.fold (fun d a => f d a) init m = Array.foldl f init m.toArray
-- Mathlib.Order.OrderDual
OrderDual.instSubsingleton : ∀ (α : Type u_2) [h : Subsingleton α], Subsingleton αᵒᵈ
-- Mathlib.RingTheory.Ideal.Operations
Ideal.range_mul : ∀ {R : Type u} [inst : CommSemiring R] (A : Type u_2) [inst_1 : CommSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] (a : A),
  ((LinearMap.mul R A) a).range = Submodule.restrictScalars R (Ideal.span {a})
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.prodMap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [inst : VAdd M α]
  [inst_1 : VAdd M β] [inst_2 : VAdd N γ] [inst_3 : VAdd N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : β →ₑ[σ] δ),
  f.prodMap g = { toFun := Prod.map ⇑f ⇑g, map_vadd' := ⋯ }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)], k ∉ m₂ → (m₁ \ m₂).get! k = m₁.get! k
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The main inductive step in the grid-lines lemma for the Gagliardo-Nirenberg-Sobolev inequality.

The grid-lines operation `GridLines.T` on a nonnegative function on a finitary product type is
less than or equal to the grid-lines operation of its partial integral in one co-ordinate
(the latter intuitively considered as a function on a space "one dimension down").  -/
MeasureTheory.GridLines.T_insert_le_T_lmarginal_singleton : ∀ {ι : Type u_1} {A : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → MeasureTheory.Measure (A i))
  [inst_1 : DecidableEq ι] {p : ℝ} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)],
  0 ≤ p →
    ∀ (s : Finset ι),
      ↑s.card * p ≤ 1 →
        ∀ i ∉ s,
          ∀ {f : ((i : ι) → A i) → ENNReal},
            Measurable f →
              MeasureTheory.GridLines.T μ p f (insert i s) ≤ MeasureTheory.GridLines.T μ p (∫⋯∫⁻_{i}, f ∂μ) s
-- Std.Data.DTreeMap.Raw.Basic
/-- Folds the given function over the mappings in the map in descending order.  -/
Std.DTreeMap.Raw.foldr : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → {δ : Type w} → ((a : α) → β a → δ → δ) → δ → Std.DTreeMap.Raw α β cmp → δ
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinAlgEquiv_self : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (M : Matrix n n R) (i : n),
  ((Matrix.toLinAlgEquiv v₁) M) (v₁ i) = ∑ j, M j i • v₁ j
-- Lean.Parser.Term
Lean.Parser.Term.let_delayed.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Normed.Affine.Isometry
LinearIsometryEquiv.toAffineIsometryEquiv_linearIsometryEquiv : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : SeminormedAddCommGroup V₂] [inst_4 : NormedSpace 𝕜 V₂] (e : V ≃ₗᵢ[𝕜] V₂),
  e.toAffineIsometryEquiv.linearIsometryEquiv = e
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_mul_right_nhdsLT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousMul H] {c a : H},
  Filter.map (fun x => x * c) (nhdsWithin a (Set.Iio a)) = nhdsWithin (a * c) (Set.Iio (a * c))
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.inv_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ≅ Y} {g : Y ⟶ X},
  CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.id X → f.inv = g
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.hasDerivWithinAt_arcsin_Iic : ∀ {x : ℝ}, x ≠ 1 → HasDerivWithinAt Real.arcsin (1 / √(1 - x ^ 2)) (Set.Iic x) x
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.ReflexiveRelation.reflexivity₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.ReflexiveRelation p₁ p₂),
  CategoryTheory.CategoryStruct.comp self.r p₁ = CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.UniformSpace.Cauchy
Cauchy.comap : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] {f : Filter β} {m : α → β},
  Cauchy f →
    Filter.comap (fun p => (m p.1, m p.2)) (uniformity β) ≤ uniformity α →
      ∀ [(Filter.comap m f).NeBot], Cauchy (Filter.comap m f)
-- Mathlib.Algebra.Group.Action.Defs
/-- Typeclass for additive actions on additive structures.

The key axiom here is `vadd_add : g +ᵥ (x + y) = (g +ᵥ x) + (g +ᵥ y)`.
If `G` is an additive group with additive automorphism group `Γ`, then there is a natural instance
of `AddDistribAddAction Γ G`.  -/
AddDistribAddAction : (M : Type u_9) → (N : Type u_10) → [AddMonoid M] → [AddMonoid N] → Type (max u_10 u_9)
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_toUInt64 : ∀ (n : UInt8), n.toUInt64.toUInt32 = n.toUInt32
-- Mathlib.Topology.Algebra.Ring.Basic
Subring.topologicalClosure_mono : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Ring R] [inst_2 : IsSemitopologicalRing R] {s t : Subring R},
  s ≤ t → s.topologicalClosure ≤ t.topologicalClosure
-- Mathlib.Topology.Algebra.ConstMulAction
ProperlyDiscontinuousVAdd.exists_nhds_disjoint_image : ∀ (Γ : Type u_4) {T : Type u_5} [inst : TopologicalSpace T] [inst_1 : VAdd Γ T] [ProperlyDiscontinuousVAdd Γ T]
  [T2Space T] [LocallyCompactSpace T] [ContinuousConstVAdd Γ T] (x : T),
  ∃ U ∈ nhds x, ∀ (γ : Γ), γ +ᵥ x ≠ x → Disjoint ((fun x => γ +ᵥ x) '' U) U
-- Batteries.Data.List.Basic
List.zipWithLeft.eq_3 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : α) (as : List α) (b : β) (bs : List β),
  List.zipWithLeft f (a :: as) (b :: bs) = f a (some b) :: List.zipWithLeft f as bs
-- Mathlib.Algebra.Group.Subgroup.Defs
Set.injOn_iff_map_eq_zero : ∀ {F : Type u_3} {G : Type u_4} {H : Type u_5} {S : Type u_6} [inst : AddGroup G] [inst_1 : AddGroup H]
  [inst_2 : FunLike F G H] [AddMonoidHomClass F G H] (f : F) [inst_4 : SetLike S G] [ZeroMemClass S G] [AddMemClass S G]
  [NegMemClass S G] (s : S), Set.InjOn ⇑f ↑s ↔ ∀ a ∈ s, f a = 0 → a = 0
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsert!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.containsThenInsert! k v t =
    (Std.DTreeMap.Internal.Impl.containsThenInsert!.size t == (Std.DTreeMap.Internal.Impl.insert! k v t).size,
      Std.DTreeMap.Internal.Impl.insert! k v t)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instIsNoetherianSubtypeMem : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] [IsNoetherian R M] (N : LieSubmodule R L M), IsNoetherian R ↥N
-- Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
/-- The family of components of the induced chain homotopy  -/
CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] →
      {X Y : CategoryTheory.SimplicialObject C} →
        {f g : X ⟶ Y} →
          CategoryTheory.SimplicialObject.Homotopy f g →
            (p q : ℕ) → X.obj (Opposite.op { len := p }) ⟶ Y.obj (Opposite.op { len := q })
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.mk'_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : DecidableEq ι] (f : ((i : ι) → M₁ i) → M₂)
  (h₁ :
    autoParam
      (∀ (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
        f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y))
      MultilinearMap.mk'._auto_1)
  (h₂ :
    autoParam
      (∀ (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
        f (Function.update m i (c • x)) = c • f (Function.update m i x))
      MultilinearMap.mk'._auto_3)
  (a : (i : ι) → M₁ i), (MultilinearMap.mk' f h₁ h₂) a = f a
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.constantCoeff_subst : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S},
  PowerSeries.HasSubst a →
    ∀ (f : PowerSeries R),
      MvPowerSeries.constantCoeff (PowerSeries.subst a f) =
        ∑ᶠ (d : ℕ), (PowerSeries.coeff d) f • MvPowerSeries.constantCoeff (a ^ d)
-- Mathlib.Data.Multiset.Replicate
Multiset.nodup_iff_le : ∀ {α : Type u_1} {s : Multiset α}, s.Nodup ↔ ∀ (a : α), ¬a ::ₘ a ::ₘ 0 ≤ s
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.ext_inv : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g}
  (i : s.pt ≅ t.pt)
  (w : autoParam (CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι) CategoryTheory.Limits.Fork.ext._auto_1),
  (CategoryTheory.Limits.Fork.ext i w).inv = CategoryTheory.Limits.Fork.mkHom i.inv ⋯
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RicSliceData.mk.inj : ∀ {α : Type u} {β : Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => β} {range : Std.Ric α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β} {range_1 : Std.Ric α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.coe_toOrderRingHom : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α ≃+*o β), ⇑↑f = ⇑f
-- Lean.Message
Lean.MessageDataContext.lctx : Lean.MessageDataContext → Lean.LocalContext
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_zsmul_eq_pi_iff : ∀ {θ : Real.Angle}, 2 • θ = ↑Real.pi ↔ θ = ↑(Real.pi / 2) ∨ θ = ↑(-Real.pi / 2)
-- Init.Data.UInt.Lemmas
UInt16.size_lt_usizeSize : UInt16.size < USize.size
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.LeanSemanticToken.mk.inj : ∀ {stx : Lean.Syntax} {type : Lean.Lsp.SemanticTokenType} {priority : ℕ} {stx_1 : Lean.Syntax}
  {type_1 : Lean.Lsp.SemanticTokenType} {priority_1 : ℕ},
  { stx := stx, type := type, priority := priority } = { stx := stx_1, type := type_1, priority := priority_1 } →
    stx = stx_1 ∧ type = type_1 ∧ priority = priority_1
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.le_one_iff : ∀ {c : Cardinal.{u_1}}, c ≤ 1 ↔ c = 0 ∨ c = 1
-- Mathlib.Topology.UniformSpace.Basic
inv_entourageProd : ∀ {α : Type ua} {β : Type ub} (u : SetRel α α) (v : SetRel β β), (entourageProd u v).inv = entourageProd u.inv v.inv
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.summable_nnnorm_mul_pow : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal}, ↑r < p.radius → Summable fun n => ‖p n‖₊ * r ^ n
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
/-- A monoidal-stable morphism property also stable under braiding isomorphisms.  -/
CategoryTheory.MorphismProperty.IsStableUnderBraiding : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Analysis.Convex.LinearIsometry
LinearIsometryEquiv.strictConvex_image : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : SeminormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] {s : Set E} (e : E ≃ₗᵢ[𝕜] F), StrictConvex 𝕜 (⇑e '' s) ↔ StrictConvex 𝕜 s
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instSMulOfIsScalarTower.eq_1 : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : Monoid M] {S : Submonoid M} [inst_1 : OreLocalization.OreSet S]
  [inst_2 : MulAction M X] [inst_3 : SMul R X] [inst_4 : SMul R M] [inst_5 : IsScalarTower R M X]
  [inst_6 : IsScalarTower R M M], OreLocalization.instSMulOfIsScalarTower = { smul := OreLocalization.hsmul }
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.mk : {R : Type u} → [inst : CommRing R] → Rˣ → R → R → R → WeierstrassCurve.VariableChange R
-- Mathlib.Data.Matrix.Diagonal
Matrix.submatrix_one_equiv : ∀ {l : Type u_1} {m : Type u_2} {α : Type v} [inst : Zero α] [inst_1 : One α] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq l] (e : l ≃ m), Matrix.submatrix 1 ⇑e ⇑e = 1
-- Lean.Meta.Tactic.Grind.Types
/-- Input goal  -/
Lean.Meta.Grind.SplitSource.input : Lean.Meta.Grind.SplitSource
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.coe_trans : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] {L : Type u_3} [inst_4 : Add L] [inst_5 : TopologicalSpace L] (e₁ : M ≃ₜ+ N) (e₂ : N ≃ₜ+ L),
  ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xn_succ : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.xn a1 (n + 1) = Pell.xn a1 n * a + Pell.d✝ a1 * Pell.yn a1 n
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.inr_mem_Icc_iff_nnnorm_le : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {x : A},
  ↑x ∈ Set.Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖₊ ≤ 1
-- Mathlib.Topology.UniformSpace.UniformEmbedding
isUniformInducing_rangeFactorization_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing (Set.rangeFactorization f) ↔ IsUniformInducing f
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.restrictDvd.congr_simp : ∀ {F : Type u_1} [inst : Field F] {p q : Polynomial F} (hpq : p ∣ q),
  Polynomial.Gal.restrictDvd hpq = Polynomial.Gal.restrictDvd hpq
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelZeroIsoTarget_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C},
  CategoryTheory.Limits.cokernelZeroIsoTarget.hom =
    CategoryTheory.Limits.cokernel.desc 0 (CategoryTheory.CategoryStruct.id Y) ⋯
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.FormatError.mk.injEq : ∀ (srcNat : ℕ) (srcEndPos : String.Pos.Raw) (fmtPos : ℕ) (msg : String) (length : ℕ) (srcStartPos : String.Pos.Raw)
  (srcNat_1 : ℕ) (srcEndPos_1 : String.Pos.Raw) (fmtPos_1 : ℕ) (msg_1 : String) (length_1 : ℕ)
  (srcStartPos_1 : String.Pos.Raw),
  ({ srcNat := srcNat, srcEndPos := srcEndPos, fmtPos := fmtPos, msg := msg, length := length,
        srcStartPos := srcStartPos } =
      { srcNat := srcNat_1, srcEndPos := srcEndPos_1, fmtPos := fmtPos_1, msg := msg_1, length := length_1,
        srcStartPos := srcStartPos_1 }) =
    (srcNat = srcNat_1 ∧
      srcEndPos = srcEndPos_1 ∧ fmtPos = fmtPos_1 ∧ msg = msg_1 ∧ length = length_1 ∧ srcStartPos = srcStartPos_1)
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lid_apply : ∀ (R : Type u) [inst : Semiring R] {M : Type v} {ι : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Unique ι] (x : DirectSum ι fun x => M), (DirectSum.lid R M ι) x = x default
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
/-- The adjoint operator as a partially defined linear operator, denoted as `T†`.  -/
LinearPMap.«term_†» : Lean.TrailingParserDescr
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfold.match_2.eq_2 : ∀ (n : ℕ) {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfold._auto_1 → Type u_2}
  (motive : (x : ℕ) → x ≤ n → α (n - x) ⋯ → Sort u_1) (m : ℕ) (h : m.succ ≤ n) (a : α (n - m.succ) ⋯)
  (h_1 : (h : 0 ≤ n) → (a : α (n - 0) ⋯) → motive 0 h a)
  (h_2 : (m : ℕ) → (h : m.succ ≤ n) → (a : α (n - m.succ) ⋯) → motive m.succ h a),
  (match m.succ, h, a with
    | 0, h, a => h_1 h a
    | m.succ, h, a => h_2 m h a) =
    h_2 m h a
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_le_aleph0 : ∀ (n : ℕ∞), ↑n ≤ Cardinal.aleph0
-- Mathlib.CategoryTheory.Opposites
/-- The equivalence of functor categories induced by `leftOp` and `rightOp`.
 -/
CategoryTheory.Functor.leftOpRightOpEquiv : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ ≌ CategoryTheory.Functor C Dᵒᵖ