mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Function
Set.mapsTo_prodMap_diagonal : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Set.MapsTo (Prod.map f f) (Set.diagonal α) (Set.diagonal β)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.HasLeftKanLift.hasInitial : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  [self : CategoryTheory.Bicategory.HasLeftKanLift f g],
  CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftLift f g)
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.isHomogeneous_one : ∀ (σ : Type u_1) (R : Type u_3) [inst : CommSemiring R], MvPolynomial.IsHomogeneous 1 0
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvexHull_isClosed : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] (s : Set E), (absConvexHull 𝕜).IsClosed s = AbsConvex 𝕜 s
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.valuation_posSubmonoid_ne_zero : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] (x : ↥(ValuativeRel.posSubmonoid R)),
  (ValuativeRel.valuation R) ↑x ≠ 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.equiv_iff_toArray_perm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp},
  t₁.Equiv t₂ ↔ t₁.toArray.Perm t₂.toArray
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_int_mul_pi : ∀ (n : ℤ), Complex.sin (↑n * ↑Real.pi) = 0
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context.ctorVal? : Lean.Elab.Term.CollectPatternVars.Context → Option Lean.ConstructorVal
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
/-- There is a zero map from the trivial module.  -/
LinearMap.BilinForm.Isometry.hasZeroOfSubsingleton : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                {B₁ : LinearMap.BilinForm R M₁} → {B₂ : LinearMap.BilinForm R M₂} → [Subsingleton M₁] → Zero (B₁ →bᵢ B₂)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.MorphismProperty.whiskerLeft_mem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [W.IsMonoidal] (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂),
  W g → W (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g)
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.coe_forgetToTop : ∀ (X : AlexDisc), ↑((CategoryTheory.forget₂ AlexDisc TopCat).obj X) = ↑X.toTopCat
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.inv.aux.eq_1 : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] (a : R) (φ : MvPowerSeries σ R) (x : σ →₀ ℕ),
  MvPowerSeries.inv.aux a φ x =
    if x = 0 then a
    else
      -a *
        ∑ x_1 ∈ Finset.HasAntidiagonal.antidiagonal x,
          if x : x_1.2 < x then (MvPowerSeries.coeff x_1.1) φ * MvPowerSeries.inv.aux a φ x_1.2 else 0
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.Limits.hasLimitsOfShape_of_initiallySmall : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.InitiallySmall J] (C : Type u₁)
  [inst_2 : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v₁, u₁} C],
  CategoryTheory.Limits.HasLimitsOfShape J C
-- Mathlib.Algebra.Order.UpperLower
LowerSet.coe_mul : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α] (s t : LowerSet α),
  ↑(s * t) = ↑s * ↑t
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_map : ∀ {α : Type u_1} {X : Set α} {β : Type u_2} {f : α → β} (M : Matroid α) (hf : Set.InjOn f M.E),
  autoParam (X ⊆ M.E) Matroid.eRk_map._auto_1 → (M.map f hf).eRk (f '' X) = M.eRk X
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → (m.isEmpty = false ↔ ∃ a, a ∈ m)
-- Mathlib.Tactic.Linarith.Frontend
_private.Mathlib.Tactic.Linarith.Frontend.0.Mathlib.Tactic.instEvalExprGlobalBranchingPreprocessor : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor
-- Mathlib.Topology.Order.ScottTopology
/-- The closure of a singleton `{a}` in the Scott topology is the right-closed left-infinite interval
`(-∞,a]`.
 -/
Topology.IsScott.closure_singleton : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] {a : α} [Topology.IsScott α Set.univ],
  closure {a} = Set.Iic a
-- Mathlib.Algebra.DirectSum.Module
DirectSum.IsInternal.ofBijective_coeLinearMap_same : ∀ {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} (h : DirectSum.IsInternal A) {i : ι} (x : ↥(A i)),
  ((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm ↑x) i = x
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A B : CategoryTheory.Endofunctor.Algebra F} {f g : A ⟶ B},
  autoParam (f.f = g.f) CategoryTheory.Endofunctor.Algebra.ext._auto_1 → f = g
-- Mathlib.Data.Finset.Powerset
Finset.powersetCard_one : ∀ {α : Type u_1} (s : Finset α), Finset.powersetCard 1 s = Finset.map { toFun := singleton, inj' := ⋯ } s
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_add_aux : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  Measurable f → Measurable g → ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
/-- This is `piIso.inv` as a cone morphism (in fact, isomorphism)  -/
FundamentalGroupoidFunctor.piTopToPiCone : {I : Type u} →
  (X : I → TopCat) →
    CategoryTheory.Limits.Fan.mk (FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i))))
        (FundamentalGroupoidFunctor.proj X) ⟶
      CategoryTheory.Grpd.piLimitFan fun i => FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i)
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.unpackExponent_def : ∀ {spec : Float.Model.Format} (b : BitVec spec.numBits),
  Float.Model.UnpackedFloat.unpackExponent b = BitVec.extractLsb' spec.mantissaBitsWithoutImplicit spec.exponentBits b
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.fourier_coe : ∀ {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]
  (f : SchwartzMap V E), ⇑(FourierTransform.fourier f) = FourierTransform.fourier ⇑f
-- Mathlib.Topology.Sober
genericPoints.component_ofComponent : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : QuasiSober α] (x : ↑(irreducibleComponents α)),
  genericPoints.component (genericPoints.ofComponent x) = x
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- If the orthogonal projection to `K` is well-defined, then a vector splits as the sum of its
orthogonal projections onto a complete submodule `K` and onto the orthogonal complement of `K`.  -/
Submodule.starProjection_add_starProjection_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (w : E), K.starProjection w + Kᗮ.starProjection w = w
-- Mathlib.Algebra.Group.End
Equiv.Perm.mul_def : ∀ {α : Type u_4} (f g : Equiv.Perm α), f * g = Equiv.trans g f
-- Mathlib.Data.Int.GCD
Int.exists_gcd_one : ∀ {m n : ℤ}, 0 < m.gcd n → ∃ m' n', m'.gcd n' = 1 ∧ m = m' * ↑(m.gcd n) ∧ n = n' * ↑(m.gcd n)
-- Aesop.Rule
Aesop.LocalNormSimpRule.name : Aesop.LocalNormSimpRule → Aesop.RuleName
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.hasColimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J] (F : CategoryTheory.Functor J (Type u)),
  CategoryTheory.Limits.HasColimit F
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_const : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal), ∫⁻ (x : α), c ∂μ = c * μ Set.univ
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.id_mem_of_tgt : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c d : C} {f : c ⟶ d},
  f ∈ S.arrows c d → CategoryTheory.CategoryStruct.id d ∈ S.arrows d d
-- Init.System.IO
IO.FileRight.mk : IO.AccessRight → IO.AccessRight → IO.AccessRight → IO.FileRight
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.expandBitVecValuePattern : Lean.Meta.Match.Problem → Lean.MetaM Lean.Meta.Match.Problem
-- Lean.ParserCompiler
Lean.ParserCompiler.Context.mk.injEq : ∀ {α : Type} (varName : Lean.Name) (categoryAttr : Lean.KeyedDeclsAttribute α)
  (combinatorAttr : Lean.ParserCompiler.CombinatorAttribute) (varName_1 : Lean.Name)
  (categoryAttr_1 : Lean.KeyedDeclsAttribute α) (combinatorAttr_1 : Lean.ParserCompiler.CombinatorAttribute),
  ({ varName := varName, categoryAttr := categoryAttr, combinatorAttr := combinatorAttr } =
      { varName := varName_1, categoryAttr := categoryAttr_1, combinatorAttr := combinatorAttr_1 }) =
    (varName = varName_1 ∧ categoryAttr = categoryAttr_1 ∧ combinatorAttr = combinatorAttr_1)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.instField : Field ℝ*
-- Mathlib.Condensed.Discrete.Module
CompHausLike.LocallyConstantModule.functor_obj_obj_obj_carrier : ∀ {P : TopCat → Prop} (R : Type (max u w)) [inst : Ring R] [inst_1 : CompHausLike.HasExplicitFiniteCoproducts P]
  [inst_2 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  (X : ModuleCat R) (x : (CompHausLike P)ᵒᵖ),
  ↑(((CompHausLike.LocallyConstantModule.functor R hs).obj X).obj.obj x) = LocallyConstant ↑(Opposite.unop x).toTop ↑X
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.coe_toEquiv : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y),
  ⇑e.toEquiv = ⇑e
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.isIso_lift : ∀ {Z₁ Z₂ X : AlgebraicGeometry.Scheme} (i₁ : Z₁ ⟶ X) (i₂ : Z₂ ⟶ X) [inst : AlgebraicGeometry.IsClosedImmersion i₁]
  [AlgebraicGeometry.IsClosedImmersion i₂]
  (h : AlgebraicGeometry.Scheme.Hom.ker i₁ = AlgebraicGeometry.Scheme.Hom.ker i₂),
  CategoryTheory.IsIso (AlgebraicGeometry.IsClosedImmersion.lift i₁ i₂ ⋯)
-- Lean.Elab.Open
Lean.Elab.OpenDecl.resolveId : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [MonadExceptOf Lean.Exception m] →
        [Lean.MonadRef m] →
          [Lean.AddErrorMessageContext m] →
            [Lean.AddMessageContext m] →
              [Lean.MonadLog m] →
                [Lean.MonadOptions m] → [Lean.MonadResolveName m] → Lean.Name → Lean.Syntax → m Lean.Name
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.le_monomorphisms : AlgebraicGeometry.IsOpenImmersion ≤ CategoryTheory.MorphismProperty.monomorphisms AlgebraicGeometry.Scheme
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_target' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H}, (f.extend I).target = ↑I '' f.target
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.coe_prodUnique : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] [inst_5 : Unique M₂], ↑LinearEquiv.prodUnique = Equiv.prodUnique M M₂
-- Mathlib.Order.WithBot
WithTop.map_le_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x y : WithTop α} (f : α → β),
  (∀ {a b : α}, f b ≤ f a ↔ b ≤ a) → (WithTop.map f y ≤ WithTop.map f x ↔ y ≤ x)
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- A (limit) kernel fork of the differential on the `r`th page whose point
identifies to an object `X.E`  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kf : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    (r r' : ℤ) →
                      (hrr' : r + 1 = r') →
                        (hr : r₀ ≤ r) →
                          (pq' pq'' : κ) →
                            (i₀' i₀ i₁ i₂ i₃ : ι) →
                              i₀' = data.i₀ r' pq' ⋯ →
                                i₀ = data.i₀ r pq' ⋯ →
                                  i₁ = data.i₁ pq' →
                                    i₂ = data.i₂ pq' →
                                      i₃ = data.i₃ r pq' ⋯ →
                                        (n₀ n₁ n₂ : ℤ) →
                                          n₁ = data.deg pq' →
                                            autoParam (n₀ + 1 = n₁)
                                                CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kf._auto_1 →
                                              autoParam (n₁ + 1 = n₂)
                                                  CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kf._auto_3 →
                                                CategoryTheory.Limits.KernelFork
                                                  ((CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X data r
                                                        hr).d
                                                    pq' pq'')
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.isEmbedding_toCloseds : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T2Space α], Topology.IsEmbedding TopologicalSpace.Compacts.toCloseds
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → t.get! t.max! = t.max!
-- Batteries.Recycling.RBTree.Lemmas
/-- A stronger version of `upperBoundP?_least` that holds when the cut is strict.  -/
RBTree.RBSet.lt_upperBoundP? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x y : α} {t : RBTree.RBSet α cmp} [Std.TransCmp cmp]
  [RBTree.RBNode.IsStrictCut cmp cut],
  t.upperBoundP? cut = some x → y ∈ t → (cmp y x = Ordering.lt ↔ cut y = Ordering.gt)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
vectorSpan_add_self : ∀ (k : Type u_1) {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] (s : Set V),
  ↑(vectorSpan k s) + s = ↑(affineSpan k s)
-- Init.Data.List.MinMax
List.max.congr_simp : ∀ {α : Type u} [inst : Max α] (l l_1 : List α) (e_l : l = l_1) (h : l ≠ []), l.max h = l_1.max ⋯
-- Lean.Elab.Tactic.Grind.Basic
/-- Adapt a syntax transformation to a regular tactic evaluator.  -/
Lean.Elab.Tactic.Grind.adaptExpander : (Lean.Syntax → Lean.Elab.Tactic.Grind.GrindTacticM Lean.Syntax) → Lean.Elab.Tactic.Grind.GrindTactic
-- Std.Internal.Do.ExceptPost
/-- An `EPost.Cons` value is below another if both components are below.  -/
Std.Internal.Do.EPost.Cons.mk_le_tail : ∀ {e : Type u_1} {e' : Type u_2} [inst : Lean.Order.PartialOrder e] [inst_1 : Lean.Order.PartialOrder e'] (epostt : e')
  (epost : EPost.Cons✝ e e'),
  Lean.Order.PartialOrder.rel epostt epost.tail → Lean.Order.PartialOrder.rel (EPost.Cons.mk✝ epost.head epostt) epost
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_finset_subset_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {t : Finset β} {a : α} {s : Finset α},
  a ∈ s → a +ᵥ t ⊆ s +ᵥ t
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.inv : ∀ {f : ℝ → ℝ}, AkraBazziRecurrence.GrowsPolynomially f → AkraBazziRecurrence.GrowsPolynomially fun x => (f x)⁻¹
-- Init.Data.Bool
Bool.false_ne_true : false ≠ true
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instCofibrationITrivialCofibrationsFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y : C} (f : X ⟶ Y)
  (h : (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f),
  HomotopicalAlgebra.Cofibration h.i
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- If two monoid homomorphisms are equal on a set, then they are equal on its subgroup closure.  -/
MonoidHom.eqOn_closure : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : Monoid M] {f g : G →* M} {s : Set G},
  Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Subgroup.closure s)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
CStarAlgebra.norm_negPart_le : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : NormedSpace ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A]
  [inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A), ‖a⁻‖ ≤ ‖a‖
-- Mathlib.Analysis.Normed.MulAction
/-- Mixin class for scalar-multiplication actions with a strictly multiplicative norm, i.e.
`‖r • x‖ = ‖r‖ * ‖x‖`.  -/
NormSMulClass : (α : Type u_3) → (β : Type u_4) → [Norm α] → [Norm β] → [SMul α β] → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdSndIsoProd.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Z Y] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Z X]
  [inst_3 : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f],
  CategoryTheory.Limits.pullbackProdSndIsoProd f Z =
    {
      hom :=
        CategoryTheory.Limits.prod.lift
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.prod.snd f)
            CategoryTheory.Limits.prod.fst)
          (CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.prod.snd f),
      inv :=
        CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id Z) f)
          CategoryTheory.Limits.prod.snd ⋯,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_strictMono_of_injective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂}, Function.Injective ⇑f → StrictMono (Submodule.map f)
-- Mathlib.Algebra.Group.Submonoid.Units
/-- The equivalence between the greatest subgroup of additive units
contained within `T` and `T` itself.  -/
AddSubgroup.addUnitsEquivSelf : {G : Type u_2} → [inst : AddGroup G] → (H : AddSubgroup G) → ↥H.addUnits ≃+ ↥H
-- Init.Data.SInt.Basic
Int32.ofUInt32.injEq : ∀ (toUInt32 toUInt32_1 : UInt32), ({ toUInt32 := toUInt32 } = { toUInt32 := toUInt32_1 }) = (toUInt32 = toUInt32_1)
-- Mathlib.Tactic.Abel
/-- `abel` solves equations in the language of *additive*, commutative monoids and groups.

`abel` and its variants work as both tactics and conv tactics.

* `abel1` fails if the target is not an equality that is provable by the axioms of
  commutative monoids/groups.
* `abel_nf` rewrites all group expressions into a normal form.
  * `abel_nf at h` rewrites in a hypothesis.
  * `abel_nf (config := cfg)` allows for additional configuration:
    * `red`: the reducibility setting (overridden by `!`).
    * `zetaDelta`: if true, local `let` variables can be unfolded (overridden by `!`).
    * `recursive`: if true, `abel_nf` also recurses into atoms.
* `abel!`, `abel1!`, `abel_nf!` use a more aggressive reducibility setting to identify atoms.

Examples:
```
example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel
```
 -/
Mathlib.Tactic.Abel.tacticAbel! : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Dual.Defs
LinearMap.dualMap_comp_dualMap : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] {M₃ : Type u_4} [inst_5 : AddCommMonoid M₃]
  [inst_6 : Module R M₃] (f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃), f.dualMap ∘ₗ g.dualMap = (g ∘ₗ f).dualMap
-- Mathlib.Tactic.DeriveEncodable
/-- Constructs a function from the inductive type to `S`.  -/
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.mkToSFuns : Lean.Elab.Deriving.Context → Array Lean.Name → Lean.Elab.TermElabM (Lean.TSyntax `command)
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.isVerdierLeftLocalizing_op_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C),
  A.op.IsVerdierLeftLocalizing B.op ↔ A.IsVerdierRightLocalizing B
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
PresheafOfModules.instIsRightAdjointPushforwardIdFunctorOppositeRingCat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {S : CategoryTheory.Functor Cᵒᵖ RingCat},
  (PresheafOfModules.pushforward (CategoryTheory.CategoryStruct.id S)).IsRightAdjoint
-- Mathlib.LinearAlgebra.Charpoly.ToMatrix
Matrix.charpoly_toLin' : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n R),
  (Matrix.toLin' A).charpoly = A.charpoly
-- Init.Data.UInt.Lemmas
USize.toUInt32_ofNatTruncate_of_le : ∀ {n : ℕ},
  USize.size ≤ n →
    (USize.ofNatClamp n).toUInt32 = UInt32.ofNatLT (UInt32.size - 1) UInt64.toUInt32_ofNatClamp_of_le._proof_1
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.isCursorInProperWhitespace : Lean.FileMap → String.Pos.Raw → Bool
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Given a pointwise left Kan extension of `F` along `L` at `c`, exhibits
`(LeftExtension.whiskerRight L F G).obj E` as a pointwise left Kan extension of `F ⋙ G` along
`L` at `c`.  -/
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.postcompose : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (G : CategoryTheory.Functor B D) →
                  {F : CategoryTheory.Functor A B} →
                    {L : CategoryTheory.Functor A C} →
                      {c : C} →
                        [G.PreservesPointwiseLeftKanExtensionAt F L c] →
                          {E : L.LeftExtension F} →
                            E.IsPointwiseLeftKanExtensionAt c →
                              ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj
                                    E).IsPointwiseLeftKanExtensionAt
                                c
-- Mathlib.NumberTheory.Padics.WithVal
Equiv.toUniformEquivOfIsUniformInducing.eq_1 : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (f : α ≃ β) (hf : IsUniformInducing ⇑f),
  f.toUniformEquivOfIsUniformInducing hf = { toEquiv := f, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }