mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommFold.congr_simp : ∀ {α : Type u_3} (op op_1 : α → α → α) (e_op : op = op_1) [assoc : Std.Associative op] (s s_1 : Multiset α)
  (e_s : s = s_1) (comm : {x | x ∈ s}.Pairwise fun x y => op x y = op y x) (a a_1 : α),
  a = a_1 → Multiset.noncommFold op s comm a = Multiset.noncommFold op_1 s_1 ⋯ a_1
-- Mathlib.Algebra.Group.Action.Defs
IsCancelVAdd.toIsLeftCancelVAdd : ∀ {G : Type u_9} {P : Type u_10} {inst : VAdd G P} [self : IsCancelVAdd G P], IsLeftCancelVAdd G P
-- Mathlib.Dynamics.PeriodicPts.Defs
AddAction.nsmul_add_period_vadd : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] (n : ℕ) (m : M) (a : α),
  (n + AddAction.period m a) • m +ᵥ a = n • m +ᵥ a
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.π'_f_zero_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.ProjectiveResolution X) {Z : C}
  (h : ((CochainComplex.singleFunctor C 0).obj X).X 0 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (R.π'.f 0) h =
    CategoryTheory.CategoryStruct.comp
      (R.cochainComplexXIso 0 0 CategoryTheory.ProjectiveResolution.π'_f_zero._proof_2).hom
      (CategoryTheory.CategoryStruct.comp (R.π.f 0)
        (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv h))
-- Mathlib.ModelTheory.Order
_private.Mathlib.ModelTheory.Order.0.FirstOrder.Language.orderLHom.match_1.splitter : (motive : (x : ℕ) → FirstOrder.Language.order.Relations x → Sort u_1) →
  (x : ℕ) →
    (x_1 : FirstOrder.Language.order.Relations x) → (Unit → motive 2 FirstOrder.Language.orderRel.le) → motive x x_1
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise multiplication of `f` and `g`,
which monovary together, is unchanged by a permutation if and only if `f` and `g ∘ σ` monovary
together. Stated by permuting the entries of `g`.  -/
Monovary.sum_mul_comp_perm_eq_sum_mul_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {σ : Equiv.Perm ι} {f g : ι → α} [inst_4 : Fintype ι],
  Monovary f g → (∑ i, f i * g (σ i) = ∑ i, f i * g i ↔ Monovary f (g ∘ ⇑σ))
-- Mathlib.Algebra.Group.Basic
add_sub_add_comm : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c d : α), a + b - (c + d) = a - c + (b - d)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
MulOpposite.isometry_opLinearEquiv : ∀ {R : Type u_11} {H : Type u_12} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup H] [inst_2 : Module R H],
  Isometry ⇑(MulOpposite.opLinearEquiv R)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.id.eq_1 : ∀ (A : Type u_2) [inst : AddMonoid A] [inst_1 : TopologicalSpace A],
  ContinuousAddMonoidHom.id A = { toAddMonoidHom := AddMonoidHom.id A, continuous_toFun := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toShortNFOfCharThree.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : CharP R 3],
  W.toShortNFOfCharThree = W.toCharNeTwoNF
-- Init.Internal.Order.Basic
Lean.Order.instPartialOrderExceptT : {m : Type u_1 → Type u_2} →
  {ε α : Type u_1} → [inst : (α : Type u_1) → Lean.Order.PartialOrder (m α)] → Lean.Order.PartialOrder (ExceptT ε m α)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.maximalAtlas_subset_of_le : ∀ {𝕜 : 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] {m n : WithTop ℕ∞},
  m ≤ n → IsManifold.maximalAtlas I n M ⊆ IsManifold.maximalAtlas I m M
-- Mathlib.GroupTheory.Archimedean
/-- Every subgroup of `ℤ` is cyclic.  -/
Int.subgroup_cyclic : ∀ (H : AddSubgroup ℤ), ∃ a, H = AddSubgroup.closure {a}
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceGE : Lean.Meta.Simp.Simproc
-- Lean.Elab.Term.TermElabM
/-- Tasks for subsequent, potentially parallel, tactic steps.  -/
Lean.Elab.Tactic.TacticParsedSnapshot.next : Lean.Elab.Tactic.TacticParsedSnapshot → Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)
-- Mathlib.Order.Interval.Finset.Defs
/-- **Alias** of `Set.finite_uIcc`. -/
Set.finite_interval : ∀ {α : Type u_1} [inst : Lattice α] [LocallyFiniteOrder α] (a b : α), (Set.uIcc a b).Finite
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.one_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (f : M ⟶ N)
  [CategoryTheory.IsMonHom f], CategoryTheory.CategoryStruct.comp 1 f = 1
-- Mathlib.Algebra.MvPolynomial.NoZeroDivisors
MvPolynomial.degreeOf_pow_eq : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R] (i : σ) (p : MvPolynomial σ R) (n : ℕ),
  p ≠ 0 → MvPolynomial.degreeOf i (p ^ n) = n * MvPolynomial.degreeOf i p
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.isNormal_preOmega : Order.IsNormal ⇑Ordinal.preOmega
-- Mathlib.Order.Filter.Map
Filter.comap_snd_neBot : ∀ {α : Type u_1} {β : Type u_2} [Nonempty α] {f : Filter β} [f.NeBot], (Filter.comap Prod.snd f).NeBot
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)],
  ((HomologicalComplex₂.shiftFunctor₂ C y).obj K).HasTotal (ComplexShape.up ℤ)
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteLimits F],
  CategoryTheory.CategoryStruct.comp F.rightDerivedZeroIsoSelf.hom F.toRightDerivedZero =
    CategoryTheory.CategoryStruct.id (F.rightDerived 0)
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.id : Nat.Primrec id
-- Mathlib.Algebra.DirectSum.Module
/-- The canonical linear map from `⨁ i, A i` to `M` where `A` is a collection of `Submodule R M`
indexed by `ι`. This is `DirectSum.coeAddMonoidHom` as a `LinearMap`.  -/
DirectSum.coeLinearMap : {R : Type u} →
  [inst : Semiring R] →
    {ι : Type v} →
      [dec_ι : DecidableEq ι] →
        {M : Type u_1} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] → (A : ι → Submodule R M) → (DirectSum ι fun i => ↥(A i)) →ₗ[R] M
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the oriented angle between two vectors is `π / 2`, the inner product of those vectors
is zero.  -/
Orientation.inner_eq_zero_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → inner ℝ x y = 0
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.isPell_star : ∀ {d : ℤ} {b : ℤ√d}, Pell.IsPell b ↔ Pell.IsPell (star b)
-- Mathlib.Algebra.NeZero
NeZero.of_pos : ∀ {M : Type u_2} {x : M} [inst : Preorder M] [inst_1 : Zero M], 0 < x → NeZero x
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projectionOnto_apply_of_mem_right`.

---

**Alias** of the reverse direction of `Submodule.projectionOnto_apply_eq_zero_iff`. -/
Submodule.linearProjOfIsCompl_apply_of_mem_right : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) {x : E}, x ∈ q → (p.projectionOnto q h) x = 0
-- Init.Data.BitVec.Lemmas
BitVec.add_right_inj : ∀ {w : ℕ} {x y : BitVec w} (z : BitVec w), z + x = z + y ↔ x = y
-- Std.Time.Date.Unit.Month
/-- `Offset` represents an offset in months. It is defined as an `Int`.
 -/
Std.Time.Month.Offset : Type
-- Mathlib.Analysis.RCLike.Inner
RCLike.inner_eq_wInner_one : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : Fintype ι] [inst_1 : RCLike 𝕜] (f g : PiLp 2 fun _i => 𝕜),
  inner 𝕜 f g = ⟪f.ofLp, g.ofLp⟫_[𝕜]
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.eq_interpolate : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {f : Polynomial F},
  Set.InjOn v ↑s → f.degree < ↑s.card → f = (Lagrange.interpolate s v) fun i => Polynomial.eval (v i) f
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.opcyclesFunctor_linear : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C]
  [inst_4 : CategoryTheory.Limits.HasKernels C] [inst_5 : CategoryTheory.Limits.HasCokernels C],
  CategoryTheory.Functor.Linear R (CategoryTheory.ShortComplex.opcyclesFunctor C)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
Homeomorph.toOpenPartialHomeomorphOfImageEq_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X)
  (hs : IsOpen s) (t : Set Y) (h : ⇑e '' s = t), ↑(e.toOpenPartialHomeomorphOfImageEq s hs t h).symm = ⇑e.symm
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι},
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iIndep s μ →
      (∀ (t : Set ι), p t → tᶜ ∈ f) →
        Directed (fun x1 x2 => x1 ⊆ x2) ns →
          (∀ (a : β), p (ns a)) → (∀ (n : ι), ∃ a, n ∈ ns a) → ∀ {t : Set Ω}, MeasurableSet t → μ t = 0 ∨ μ t = 1
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.zmultiples_eq_closure : ∀ {G : Type u_1} [inst : AddGroup G] (g : G), AddSubgroup.zmultiples g = AddSubgroup.closure {g}
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Functor.reflectsColimits_of_isEquivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : CategoryTheory.Functor D C) [E.IsEquivalence],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E
-- Mathlib.Data.Finset.Insert
Finset.mem_insert_self : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), a ∈ insert a s
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.minimalPrimes.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (I : Ideal R), I.minimalPrimes = {p | I.IsMinimalPrime p}
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.closedUnit_app : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] [inst_2 : (i : I) → CategoryTheory.MonoidalClosed (C i)]
  (X Y : (i : I) → C i) (i : I), (CategoryTheory.Pi.closedUnit X).app Y i = (CategoryTheory.ihom.coev (X i)).app (Y i)
-- Mathlib.Analysis.SpecialFunctions.Arsinh
DifferentiableWithinAt.arsinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a : E},
  DifferentiableWithinAt ℝ f s a → DifferentiableWithinAt ℝ (fun x => Real.arsinh (f x)) s a
-- Mathlib.Order.WithBot
WithTop.noMinOrder : ∀ {α : Type u_1} [inst : LT α] [NoMinOrder α] [Nonempty α], NoMinOrder (WithTop α)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited γ] {f : α → β → Option γ} {k : α},
  Std.DHashMap.Const.get! (Std.DHashMap.filterMap f m) k =
    ((Std.DHashMap.Const.get? m k).pbind fun x_2 h' => f (m.getKey k ⋯) x_2).get!
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The object of `MonoidalOpposite C` that represents `x : C`.  -/
CategoryTheory.MonoidalOpposite.mop : {C : Type u₁} → C → Cᴹᵒᵖ
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {R₁ R₂ : CategoryTheory.CommRingObjCat C} {x y : R₁.Hom R₂},
  x = y ↔ x.hom = y.hom
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
/-- The map of a cofork is a colimit iff the cofork consisting of the mapped morphisms is a colimit.
This essentially lets us commute `Cofork.ofπ` with `Functor.mapCocone`.
 -/
CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {X Y Z : C} →
            {f g : X ⟶ Y} →
              {h : Y ⟶ Z} →
                (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) →
                  CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.Cofork.ofπ h w)) ≃
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (G.map h) ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.lift_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (hP : CategoryTheory.IsPullback fst snd f g) {W : C} (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) {Z_1 : C} (h_1 : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (hP.lift h k w) (CategoryTheory.CategoryStruct.comp fst h_1) =
    CategoryTheory.CategoryStruct.comp h h_1
-- Init.Omega.Int
Lean.Omega.Int.pos_pow_of_pos : ∀ (a : ℤ) (b : ℕ), 0 < a → 0 < a ^ b
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.SeparatingLeft.toBilin : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] {ι : Type u_6}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {M : Matrix ι ι R₂},
  M.SeparatingLeft → ∀ (b : Module.Basis ι R₂ M₂), LinearMap.SeparatingLeft ((Matrix.toBilin b) M)
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.addRecAux.eq_1 : ∀ {l w : ℕ} (x : BitVec (l * w)) (acc : BitVec w), BitVec.addRecAux✝ x 0 acc = acc
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.infix_support_iff_mem_edges : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v},
  [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support ↔ s(u', v') ∈ p.edges
-- Mathlib.NumberTheory.Rayleigh
beattySeq'_symmDiff_beattySeq_pos : ∀ {r s : ℝ},
  r.HolderConjugate s → symmDiff {x | ∃ k > 0, beattySeq' r k = x} {x | ∃ k > 0, beattySeq s k = x} = {n | 0 < n}
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_neg_le_tight_cert.eq_1 : ∀ (d : ℤ) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.dvd_neg_le_tight_cert d p₁ p₂ p₃ =
    (Int.blt' 0 d).and'
      ((p₂.beq' (((p₁.addConst_k (-p₁.getConst)).mul_k (-1)).addConst_k p₂.getConst)).and'
        (p₃.beq'
          (((p₁.addConst_k (-p₁.getConst)).mul_k (-1)).addConst_k
            (-p₁.getConst - d * ((-p₁.getConst - p₂.getConst) / d)))))
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁),
  (F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv
      (CategoryTheory.Bicategory.whiskerRight (F.mapId b₀).inv (F.map f))
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.ι_gluedTo_assoc : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.glueData.ι U) (CategoryTheory.CategoryStruct.comp I.gluedTo h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (↑U).ι) h
-- Mathlib.GroupTheory.Solvable
not_isSolvable_of_mem_derivedSeries : ∀ {G : Type u_1} [inst : Group G] {g : G}, g ≠ 1 → (∀ (n : ℕ), g ∈ derivedSeries G n) → ¬Group.IsSolvable G
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instVAdd.eq_1 : ∀ {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [inst : (i : ι) → VAdd α (M i)],
  Pi.instVAdd = { vadd := fun a f i => a +ᵥ f i }
-- Mathlib.Topology.Order.IsLUB
lowerClosure_eq_Iic_csSup : ∀ {α : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {s : Set α}, s.Nonempty → BddAbove s → IsClosed s → ↑(lowerClosure s) = Set.Iic (sSup s)
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.invOfUnit_mul : ∀ {R : Type u_1} [inst : Ring R] (φ : PowerSeries R) (u : Rˣ), PowerSeries.constantCoeff φ = ↑u → φ.invOfUnit u * φ = 1
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.Hom.rel_id : ∀ (X : CategoryTheory.RelCat), (CategoryTheory.CategoryStruct.id X).rel = SetRel.id
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.uniqueHomToTrivial.eq_1 : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D]
  (A : CategoryTheory.Mon D),
  A.uniqueHomToTrivial =
    { default := { hom := CategoryTheory.SemiCartesianMonoidalCategory.toUnit A.X, isMonHom_hom := ⋯ }, uniq := ⋯ }
-- Mathlib.Topology.Algebra.Ring.Basic
NonUnitalSubsemiring.topologicalClosure_minimal : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalSemiring R] [inst_2 : IsSemitopologicalSemiring R]
  (s : NonUnitalSubsemiring R) {t : NonUnitalSubsemiring R}, s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Lean.Elab.DeprecatedSyntax
/-- Optional deprecation message.  -/
Lean.Elab.SyntaxDeprecationEntry.text? : Lean.Elab.SyntaxDeprecationEntry → Option String
-- Mathlib.Order.Sublocale
Sublocale.mk.sizeOf_spec : ∀ {X : Type u_2} [inst : Order.Frame X] [inst_1 : SizeOf X] (carrier : Set X)
  (sInf_mem' : ∀ s ⊆ carrier, sInf s ∈ carrier) (himp_mem' : ∀ (a b : X), b ∈ carrier → a ⇨ b ∈ carrier),
  sizeOf { carrier := carrier, sInf_mem' := sInf_mem', himp_mem' := himp_mem' } = 1
-- Mathlib.MeasureTheory.Measure.Content
/-- A content is an additive function on compact sets taking values in `ℝ≥0`. It is a device
from which one can define a measure.  -/
MeasureTheory.Content : (G : Type w) → [TopologicalSpace G] → Type w
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.finsetSup'_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SemilatticeSup β] [inst_2 : Zero β]
  [inst_3 : TopologicalSpace β] [inst_4 : ContinuousSup β] {ι : Type u_5} {s : Finset ι} (H : s.Nonempty)
  (f : ι → CompactlySupportedContinuousMap α β) (a : α), (s.sup' H f) a = s.sup' H fun i => (f i) a
-- Mathlib.Analysis.Normed.Module.Alternating.Curry
ContinuousAlternatingMap.curryLeft_compContinuousLinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ} (g : F [⋀^Fin (n + 1)]→L[𝕜] G) (f : E →L[𝕜] F)
  (x : E), (g.compContinuousLinearMap f).curryLeft x = (g.curryLeft (f x)).compContinuousLinearMap f
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.arrowCongr.eq_1 : ∀ {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [inst : Add P] [inst_1 : Add Q] (f : M ≃ N)
  (g : P ≃+ Q),
  AddEquiv.arrowCongr f g =
    { toFun := fun h n => g (h (f.symm n)), invFun := fun k m => g.symm (k (f m)), left_inv := ⋯, right_inv := ⋯,
      map_add' := ⋯ }
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNNNorm_mulVec : ∀ {l : Type u_2} {m : Type u_3} {α : Type u_5} [inst : Fintype l] [inst_1 : Fintype m]
  [inst_2 : NonUnitalSeminormedRing α] (A : Matrix l m α) (v : m → α), ‖A.mulVec v‖₊ ≤ ‖A‖₊ * ‖v‖₊
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Subfield.extendScalars_sup : ∀ {L : Type u_2} [inst : Field L] {F E E' : Subfield L} (h : F ≤ E) (h' : F ≤ E'),
  Subfield.extendScalars h ⊔ Subfield.extendScalars h' = Subfield.extendScalars ⋯
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.Indep.of_contract : ∀ {α : Type u_1} {M : Matroid α} {I C : Set α}, (M.contract C).Indep I → M.Indep I
-- Lean.Environment
Lean.Environment.ofKernelEnv : Lean.Kernel.Environment → Lean.Environment
-- Mathlib.RingTheory.Frobenius
AlgHom.IsArithFrobAt.restrict_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ : S →ₐ[R] S}
  {Q : Ideal S} (H : φ.IsArithFrobAt Q) (x : S ⧸ Q), H.restrict x = x ^ Nat.card (R ⧸ Ideal.under R Q)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.liftAlgHom_mk : ∀ {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 S R] [inst_4 : Algebra S T] (p : Polynomial R) (i : R →ₐ[S] T) (x : T)
  (h : Polynomial.eval₂ (↑i) x p = 0) (f : Polynomial R),
  (AdjoinRoot.liftAlgHom p i x h) ((AdjoinRoot.mk p) f) = Polynomial.eval₂ (↑i) x f
-- Mathlib.Topology.Convenient.Localization
TopCat.instIsLocalizationContinuousGeneratedByCatToContinuousGeneratedByCatMorphismPropertyWithGeneratedByTopologyEquiv : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)],
  (TopCat.toContinuousGeneratedByCat X).IsLocalization (TopCat.morphismPropertyWithGeneratedByTopologyEquiv X)
-- Mathlib.Topology.Algebra.InfiniteSum.Real
dist_le_tsum_of_dist_le_of_tendsto : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {f : ℕ → α} (d : ℕ → ℝ),
  (∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n) →
    Summable d → ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), dist (f n) a ≤ ∑' (m : ℕ), d (n + m)
-- Mathlib.Data.List.Sublists
List.map_pure_sublist_sublists : ∀ {α : Type u} (l : List α), (List.map pure l).Sublist l.sublists
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.eventually_hasFTaylorSeriesUpToOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {f : E → F} {s : Set E} {a : E},
  ContDiffWithinAt 𝕜 n f s a →
    UniqueDiffOn 𝕜 s →
      a ∈ s →
        ∀ {m : ℕ},
          ↑m ≤ n →
            ∀ᶠ (t : Set E) in (nhdsWithin a s).smallSets, HasFTaylorSeriesUpToOn (↑m) f (ftaylorSeriesWithin 𝕜 f s) t
-- Mathlib.RingTheory.Multiplicity
le_emultiplicity_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Monoid β] {F : Type u_3} [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (f : F) {a b : α}, emultiplicity a b ≤ emultiplicity (f a) (f b)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.reverse_NT : ∀ {T : Type u_1} (g : ContextFreeGrammar T), g.reverse.NT = g.NT
-- Mathlib.Data.TwoPointing
TwoPointing.instInhabitedBool : Inhabited (TwoPointing Bool)
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.instNonemptyOfNontrivial : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] [Nontrivial M],
  Nonempty (FiniteMulArchimedeanClass M)
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasSheafify J A],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.presheafToSheaf J A)