mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
closure_submonoidClosure_eq_closure_subgroupClosure : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (s : Set G),
  closure ↑(Submonoid.closure s) = closure ↑(Subgroup.closure s)
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_fn_inj : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {φ₁ φ₂ : A →ₐ[R] B}, ⇑φ₁ = ⇑φ₂ ↔ φ₁ = φ₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso_inv_snd : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (eₗ : S.fst ≅ S'.fst) (eᵣ : S.snd ≅ S'.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight eₗ.hom F) S'.iso.hom =
        CategoryTheory.CategoryStruct.comp S.iso.hom (CategoryTheory.Functor.whiskerRight eᵣ.hom G))
      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso._auto_1),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso eₗ eᵣ w).inv.snd = eᵣ.inv
-- Mathlib.Logic.Function.Iterate
Function.Commute.iterate_iterate_self : ∀ {α : Type u} (f : α → α) (m n : ℕ), Function.Commute f^[m] f^[n]
-- Mathlib.Algebra.Order.ToIntervalMod
/-- Reduce `b` to the interval `Ico a (a + p)`.  -/
toIcoMod : {α : Type u_1} →
  [inst : AddCommGroup α] →
    [inst_1 : LinearOrder α] → [IsOrderedAddMonoid α] → [hα : Archimedean α] → {p : α} → 0 < p → α → α → α
-- Mathlib.Analysis.Complex.Trigonometric
Complex.exp_im : ∀ (x : ℂ), (Complex.exp x).im = Real.exp x.re * Real.sin x.im
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- Equivalence of coprime powers of primitive roots. Every `n`-th primitive root is taken to the
`a`-th power given that `n` and `a` are coprime.  -/
IsPrimitiveRoot.primitiveRootsPowEquivOfCoprime : {R : Type u_4} →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] → {a n : ℕ} → a.Coprime n → [NeZero n] → ↥(primitiveRoots n R) ≃ ↥(primitiveRoots n R)
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_norm_mul : ∀ {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype l] [inst_1 : Fintype m]
  [inst_2 : Fintype n] [inst_3 : RCLike α] (A : Matrix l m α) (B : Matrix m n α), ‖A * B‖ ≤ ‖A‖ * ‖B‖
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.pointwise_vadd_bot : ∀ {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (v : V), v +ᵥ ⊥ = ⊥
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.Saturate.brecOn : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Coverage C}
  {motive : (X : C) → (a : CategoryTheory.Sieve X) → K.Saturate X a → Prop} {X : C} {a : CategoryTheory.Sieve X}
  (t : K.Saturate X a),
  (∀ (X : C) (a : CategoryTheory.Sieve X) (t : K.Saturate X a),
      CategoryTheory.Coverage.Saturate.below t → motive X a t) →
    motive X a t
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.mk : {R : Type u} →
  [inst : LE R] →
    [inst_1 : AddCommMonoid R] →
      [inst_2 : One R] →
        {M : Type v} → (weights : M →₀ R) → 0 ≤ weights → (weights.sum fun x r => r) = 1 → Convexity.StdSimplex R M
-- Mathlib.LinearAlgebra.TensorProduct.Basis
TensorProduct.sum_tmul_basis_right_eq_zero : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (𝒞 : Module.Basis κ R N) (b : κ →₀ M),
  (b.sum fun i m => m ⊗ₜ[R] 𝒞 i) = 0 → b = 0
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The position of the selected subexpression.  -/
Mathlib.Tactic.ClickSuggestions.Context.pos : Mathlib.Tactic.ClickSuggestions.Context → Lean.SubExpr.Pos
-- Mathlib.Tactic.Linter.TextBased
/-- Print information about all errors encountered to standard output.
`style` specifies if the error should be formatted for humans to read, github problem matchers
to consume, or for the style exceptions file.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.formatErrors : Array Mathlib.Linter.TextBased.ErrorContext✝ → Mathlib.Linter.TextBased.ErrorFormat → IO Unit
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IterM.Partial.instForInOfIteratorLoop : {m : Type w → Type w'} →
  {n : Type w → Type w''} →
    {α β : Type w} →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m n] → [MonadLiftT m n] → [Monad n] → ForIn n (Std.IterM.Partial m β) β
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mk'_map : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictPseudofunctorCore B C) {X Y : B} (a : X ⟶ Y),
  (CategoryTheory.StrictPseudofunctor.mk' S).map a = S.map a
-- Mathlib.Algebra.Group.Action.Defs
/-- Note that the `IsScalarTower α β β` typeclass argument is usually satisfied by `Algebra α β`.  -/
smul_div_assoc : ∀ {α : Type u_5} {β : Type u_6} [inst : DivInvMonoid β] [inst_1 : SMul α β] [IsScalarTower α β β] (r : α) (x y : β),
  r • x / y = r • (x / y)
-- Mathlib.CategoryTheory.Limits.Cones
/-- The categories of cocones over `F` and `G` are equivalent if `F` and `G` are naturally
isomorphic (possibly after changing the indexing category by an equivalence).
 -/
CategoryTheory.Limits.Cocone.equivalenceOfReindexing : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {G : CategoryTheory.Functor K C} →
                (e : K ≌ J) → (e.functor.comp F ≅ G) → (CategoryTheory.Limits.Cocone F ≌ CategoryTheory.Limits.Cocone G)
-- Mathlib.Dynamics.Minimal
MulAction.dense_orbit : ∀ (M : Type u_1) {α : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [MulAction.IsMinimal M α] (x : α), Dense (MulAction.orbit M x)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Filtered
CategoryTheory.Limits.has_cofiltered_limits_of_has_filtered_colimits_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [CategoryTheory.Limits.HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ],
  CategoryTheory.Limits.HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} C
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.integrable_condExpL1 : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] (f : α → F'),
  MeasureTheory.Integrable (↑↑(MeasureTheory.condExpL1 hm μ f)) μ
-- Mathlib.Analysis.Complex.LocallyUniformLimit
/-- If the terms in the sum `∑' (i : ι), F i` are uniformly bounded on `U` by a
summable function, and each term in the sum is differentiable on `U`, then so is the sum.  -/
Complex.differentiableOn_tsum_of_summable_norm : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {U : Set ℂ} {F : ι → ℂ → E}
  [CompleteSpace E] {u : ι → ℝ},
  Summable u →
    (∀ (i : ι), DifferentiableOn ℂ (F i) U) →
      IsOpen U → (∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i) → DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_map_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Precoherent C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A} (f : X ⟶ Y) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).functor.map f).hom.app X_1 =
    f.hom.app (Opposite.op (e.inverse.obj (Opposite.unop X_1)))
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- **Alias** of the reverse direction of `Bornology.isVonNBounded_insert`. -/
Bornology.IsVonNBounded.insert : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] (x : E) {s : Set E},
  Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜 (insert x s)
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.mk : {A : Type u_1} →
  {B : Type u_2} →
    [inst : NonUnitalNonAssocSemiring A] →
      [inst_1 : Star A] →
        [inst_2 : NonUnitalNonAssocSemiring B] →
          [inst_3 : Star B] →
            (toNonUnitalRingHom : A →ₙ+* B) →
              (∀ (a : A), toNonUnitalRingHom.toFun (star a) = star (toNonUnitalRingHom.toFun a)) → A →⋆ₙ+* B
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.mem_toTrivialization_baseSet : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] {x : X} [inst_3 : Nonempty I] (h : IsEvenlyCovered f x I),
  x ∈ h.toTrivialization.baseSet
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.zero_ne_coe : ∀ {α : Type u} {a : α}, 0 ≠ ↑a
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
UniqueMDiffWithinAt.eq_1 : ∀ {𝕜 : 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] (s : Set M) (x : M),
  UniqueMDiffAt[s] x = UniqueDiffWithinAt 𝕜 (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
_private.Mathlib.Algebra.Homology.Embedding.AreComplementary.0.ComplexShape.Embedding.AreComplementary.fromSum.match_1.eq_2 : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} (motive : ι₁ ⊕ ι₂ → Sort u_3) (i₂ : ι₂) (h_1 : (i₁ : ι₁) → motive (Sum.inl i₁))
  (h_2 : (i₂ : ι₂) → motive (Sum.inr i₂)),
  (match Sum.inr i₂ with
    | Sum.inl i₁ => h_1 i₁
    | Sum.inr i₂ => h_2 i₂) =
    h_2 i₂
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.Prepartition.iUnion_toSubordinate : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  (r : (ι → ℝ) → ↑(Set.Ioi 0)), (π.toSubordinate r).iUnion = π.iUnion
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterMapWithPostcondition.match_1.eq_1 : ∀ {β γ : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (Option γ)} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (h' : (f out).Property none)
  (h_1 : (h' : (f out).Property none) → motive ⟨none, h'⟩)
  (h_2 : (out' : γ) → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩),
  (match ⟨none, h'⟩ with
    | ⟨none, h'⟩ => h_1 h'
    | ⟨some out', h'⟩ => h_2 out' h') =
    h_1 h'
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.Y_eq_negY_of_Y_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  Q 2 ≠ 0 →
    P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
      P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3 → P 1 * Q 2 ^ 3 = W'.negY Q * P 2 ^ 3 → P 1 = W'.negY P
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
/-- Given the data of a basic constructible set `s`, namely a tuple `(f, g₁, ..., gₙ)` such that
`s = V(g₁, ..., gₙ) \ V(f)`, return `s`.  -/
PrimeSpectrum.BasicConstructibleSetData.toSet : {R : Type u_1} → [inst : CommSemiring R] → PrimeSpectrum.BasicConstructibleSetData R → Set (PrimeSpectrum R)
-- Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
CategoryTheory.Monoidal.rightRigidFunctorCategory : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Groupoid C] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          [CategoryTheory.RightRigidCategory D] → CategoryTheory.RightRigidCategory (CategoryTheory.Functor C D)
-- Mathlib.Geometry.Manifold.Submersion
/-- A linear equivalence `E ≃L[𝕜] E'' × F` which belongs to the data of a submersion `f` at `x`:
the particular equivalence is arbitrary, but this choice matches the witnesses given by
`h.domChart` and `h.codChart`.  -/
Manifold.IsSubmersionAtOfComplement.equiv : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {F : Type u_5} →
      {H : Type u_7} →
        {G : Type u_9} →
          {E : Type u} →
            [inst : NontriviallyNormedField 𝕜] →
              [inst_1 : NormedAddCommGroup E] →
                [inst_2 : NormedSpace 𝕜 E] →
                  [inst_3 : NormedAddCommGroup E''] →
                    [inst_4 : NormedSpace 𝕜 E''] →
                      [inst_5 : NormedAddCommGroup F] →
                        [inst_6 : NormedSpace 𝕜 F] →
                          [inst_7 : TopologicalSpace H] →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    {N : Type u_13} →
                                      [inst_9 : TopologicalSpace M] →
                                        [inst_10 : ChartedSpace H M] →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} →
                                                    Manifold.IsSubmersionAtOfComplement F I J n f x → E ≃L[𝕜] E'' × F
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.Struct : Type
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- The fan on `i ↦ S ⊗[R] P i` given by `S ⊗[R] ∀ i, P i`  -/
CommRingCat.Under.tensorProductFan : {R : CommRingCat} →
  (S : CommRingCat) →
    [inst : Algebra ↑R ↑S] →
      {ι : Type u} →
        (P : ι → CategoryTheory.Under R) →
          CategoryTheory.Limits.Fan fun i => S.mkUnder (TensorProduct ↑R ↑S ↑(P i).right)
-- Mathlib.Algebra.Category.Ring.Basic
/-- This prevents `CommRingCat.of R` being printed as `{ carrier := R, commRing := ... }` by
`delabStructureInstance`.  -/
CommRingCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab
-- Init.Data.BitVec.Lemmas
BitVec.fill_false : ∀ {w : ℕ}, BitVec.fill w false = 0#w
-- Batteries.Lean.Except
Except.pmap_id : ∀ {ε : Type u} {α : Type v} (x : Except ε α), (x.pmap fun a x => a) = x
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The explicit fan of a family of topological spaces given by the pi type.  -/
TopCat.piFan : {ι : Type v} → (α : ι → TopCat) → CategoryTheory.Limits.Fan α
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
/-- If `f : ℂ → ℂ` is complex-analytic, then its real part is harmonic.
 -/
AnalyticAt.harmonicAt_re : ∀ {x : ℂ} {f : ℂ → ℂ}, AnalyticAt ℂ f x → InnerProductSpace.HarmonicAt (fun z => (f z).re) x
-- Mathlib.Algebra.Group.Defs
AddGroup.toAddCancelMonoid : {G : Type u_1} → [AddGroup G] → AddCancelMonoid G
-- Mathlib.Logic.Basic
/-- Any type `α` has decidable equality classically.  -/
Classical.decEq : (α : Sort u_2) → DecidableEq α
-- Mathlib.Order.Basic
ne_iff_lt_iff_le : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, (a ≠ b ↔ a < b) ↔ a ≤ b
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.MapTarget : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.toMonoidWithZeroHom : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : MulZeroOneClass α] → [inst_3 : MulZeroOneClass β] → (α →*₀o β) → α →*₀ β
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_univ : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst_1 : OrderBot α], sInf Set.univ = ⊥
-- Mathlib.CategoryTheory.Action.Basic
/-- The identity morphism on an `Action V G`.  -/
Action.Hom.id : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] → {G : Type u_2} → [inst_1 : Monoid G] → (M : Action V G) → M.Hom M
-- Mathlib.Analysis.Convex.Body
/-- A convex body has compact carrier set  -/
ConvexBody.isCompact' : ∀ {V : Type u_2} [inst : TopologicalSpace V] [inst_1 : AddCommMonoid V] [inst_2 : SMul ℝ V] (self : ConvexBody V),
  IsCompact self.carrier
-- Mathlib.Analysis.Calculus.FDeriv.Congr
DifferentiableOn.congr_mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {s t : Set E},
  DifferentiableOn 𝕜 f s → (∀ x ∈ t, f₁ x = f x) → t ⊆ s → DifferentiableOn 𝕜 f₁ t
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.ext : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {M₁ M₂ : CStarMatrix m n A},
  (∀ (i : m) (j : n), M₁ i j = M₂ i j) → M₁ = M₂
-- Mathlib.Data.ENNReal.Basic
ENNReal.natCast_le_ofNNReal : ∀ {r : NNReal} {n : ℕ}, ↑n ≤ ↑r ↔ ↑n ≤ r
-- Mathlib.ModelTheory.Basic
/-- The empty language has no symbols.  -/
FirstOrder.Language.empty : FirstOrder.Language
-- Mathlib.Data.EReal.Basic
EReal.hasCoeENNReal : Coe ENNReal EReal
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Forgetting `Rep` to `ModuleCat` is the same as first map to `Action`
then forget to `ModuleCat`.  -/
Rep.forgetNatIsoActionForget : (k : Type u) →
  (G : Type v) →
    [inst : Ring k] →
      [inst_1 : Monoid G] →
        CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k) ≅
          (Rep.RepToAction k G).comp (Action.forget (ModuleCat k) G)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_sdiff : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  s₁ ⊆ s₂ → ∑ x ∈ s₂ \ s₁, f x + ∑ x ∈ s₁, f x = ∑ x ∈ s₂, f x
-- Lean.Meta.Tactic.Split
_private.Lean.Meta.Tactic.Split.0.Lean.Meta.splitTarget?.go : Lean.MVarId → Bool → Bool → Lean.Expr → Lean.ExprSet → Lean.MetaM (Option (List Lean.MVarId))
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.break : Lean.Syntax → Lean.Elab.Term.Do.Code
-- Std.Http.Data.URI.Basic
/-- User information component containing an encoded username and optional encoded password.

The stored strings use URI userinfo percent-encoding so parsed URIs can be rendered without
losing percent-encoding choices (for example, `%3A` versus `:`).

Note: embedding passwords in URIs is deprecated per RFC 9110 Section 4.2.4. Avoid using the
password field in new code, and never include it in logs or error messages.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2.1
 -/
Std.Http.URI.UserInfo : Type
-- Mathlib.Order.WellFoundedSet
Set.wellFoundedOn_sdiff_singleton : ∀ {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α} {a : α},
  (s \ {a}).WellFoundedOn r ↔ s.WellFoundedOn r
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.fold_filterMapM : ∀ {α β γ δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : Std.IteratorLoop α Id n]
  [Std.LawfulIteratorLoop α Id n] {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Std.Iter β},
  Std.IterM.fold g init (Std.Iter.filterMapM f it) =
    Std.Iter.foldM
      (fun d b => do
        let __x ← f b
        match __x with
          | some c => pure (g d c)
          | x => pure d)
      init it
-- Mathlib.Algebra.Ring.Subring.Basic
/-- `closure` forms a Galois insertion with the coercion to set.  -/
Subring.gi : (R : Type u) → [inst : NonAssocRing R] → GaloisInsertion Subring.closure SetLike.coe
-- Mathlib.Algebra.Group.Prod
MulEquiv.prodProdProdComm.eq_1 : ∀ (M : Type u_3) (N : Type u_4) [inst : MulOneClass M] [inst_1 : MulOneClass N] (M' : Type u_6) (N' : Type u_7)
  [inst_2 : MulOneClass N'] [inst_3 : MulOneClass M'],
  MulEquiv.prodProdProdComm M N M' N' =
    { toFun := fun mnmn => ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2),
      invFun := fun mmnn => ((mmnn.1.1, mmnn.2.1), mmnn.1.2, mmnn.2.2), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Data.Int.Bitwise
/-- Compare with `Int.zero_shiftRight`, which has `n : ℕ`.  -/
Int.zero_shiftRight' : ∀ (n : ℤ), 0 >>> n = 0
-- Mathlib.Algebra.Field.Subfield.Basic
/-- If two ring homomorphisms are equal on a set, then they are equal on its subfield closure.  -/
RingHom.eqOn_field_closure : ∀ {K : Type u} [inst : DivisionRing K] {L : Type v} [inst_1 : Semiring L] {f g : K →+* L} {s : Set K},
  Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Subfield.closure s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.Cone.ofPullbackCone_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
  (t :
    CategoryTheory.Limits.PullbackCone (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl)
      (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr)),
  (CategoryTheory.Limits.Cone.ofPullbackCone t).π =
    CategoryTheory.CategoryStruct.comp t.π (CategoryTheory.Limits.diagramIsoCospan F).inv
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.instDecidablePredMatrixIntIsSimplyLacedOfFintypeOfDecidableEq : {ι : Type u_1} → [Fintype ι] → [DecidableEq ι] → DecidablePred Matrix.IsSimplyLaced
-- Lean.Environment
/-- True while inside `realizeConst`'s `realize`.  -/
Lean.Environment.isRealizing : Lean.Environment → Bool
-- Mathlib.Algebra.Order.Archimedean.Class
/-- An `OrderIso` on `MulArchimedeanClass` induces an `OrderIso` on `FiniteMulArchimedeanClass`.  -/
FiniteMulArchimedeanClass.congrOrderIso : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedMonoid M] →
        {N : Type u_2} →
          [inst_3 : CommGroup N] →
            [inst_4 : LinearOrder N] →
              [inst_5 : IsOrderedMonoid N] →
                MulArchimedeanClass M ≃o MulArchimedeanClass N →
                  FiniteMulArchimedeanClass M ≃o FiniteMulArchimedeanClass N
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.AsSmall.equiv_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.AsSmall.equiv.counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
-- Lean.Parser.Command
Lean.Parser.Command.declModifiersF.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Geometry.Euclidean.Incenter
/-- The distance between the incenter and a face of the simplex.  -/
Affine.Simplex.inradius : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] → [inst_3 : NormedAddTorsor V P] → {n : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → ℝ
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDeriv_vcomp_two : ∀ {𝕜 : 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] {g : E → F} {f : 𝕜 → E} {x : 𝕜},
  ContDiffAt 𝕜 2 g (f x) →
    ContDiffAt 𝕜 2 f x →
      iteratedDeriv 2 (g ∘ f) x =
        ((iteratedFDeriv 𝕜 2 g (f x)) fun x_1 => deriv f x) + (fderiv 𝕜 g (f x)) (iteratedDeriv 2 f x)