mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.leftDistrib.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalLeftDistrib C] (X Y Z : C),
  CategoryTheory.leftDistrib X Y Z = CategoryTheory.leftDistrib X Y Z
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.le_inf_support_list_prod : ∀ {R : Type u_1} {A : Type u_3} {T : Type u_4} [inst : SemilatticeInf T] [inst_1 : OrderTop T] [inst_2 : Semiring R]
  [inst_3 : AddMonoid A] [inst_4 : AddMonoid T] [AddLeftMono T] [AddRightMono T] {degt : A → T},
  0 ≤ degt 0 →
    (∀ (a b : A), degt a + degt b ≤ degt (a + b)) →
      ∀ (l : List (AddMonoidAlgebra R A)),
        (List.map (fun f => f.coeff.support.inf degt) l).sum ≤ l.prod.coeff.support.inf degt
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- The linear map version of `Function.Injective.comp_left`  -/
Function.Injective.injective_linearMapComp_left : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃},
  Function.Injective ⇑f → Function.Injective fun g => f ∘ₛₗ g
-- Mathlib.Algebra.Polynomial.Sequence
/-- Polynomials in a polynomial sequence are linearly independent.  -/
Polynomial.Sequence.linearIndependent : ∀ {R : Type u_1} [inst : Ring R] (S : Polynomial.Sequence R) [IsDomain R], LinearIndependent R ↑S
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.instDecidableEqWalk : {V : Type u_1} → {G : SimpleGraph V} → {a a_1 : V} → [DecidableEq V] → DecidableEq (G.Walk a a_1)
-- Mathlib.AlgebraicGeometry.Sites.Representability
/-- The isomorphism between `yoneda.obj (glueData hf).glued` and `F`.

This implies that `F` is representable.  -/
AlgebraicGeometry.Scheme.LocalRepresentability.yonedaIsoSheaf : {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} →
  {ι : Type u} →
    {X : ι → AlgebraicGeometry.Scheme} →
      {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} →
        (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) →
          [CategoryTheory.Presheaf.IsLocallySurjective AlgebraicGeometry.Scheme.zariskiTopology
                (CategoryTheory.Limits.Sigma.desc f)] →
            AlgebraicGeometry.Scheme.zariskiTopology.yoneda.obj
                (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).glued ≅
              F
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulatedClosed₃] [P.IsClosedUnderIsomorphisms],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₂ → P T.obj₃
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.flip_nondegenerate : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁]
  [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M}, B.flip.Nondegenerate ↔ B.Nondegenerate
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalFactorizationRing.jacobian_resentation : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  (Polynomial.UniversalFactorizationRing.presentation m k hn p).jacobian =
    (-1) ^ n *
      (↑(Polynomial.UniversalFactorizationRing.factor₁ m k hn p)).resultant
        ↑(Polynomial.UniversalFactorizationRing.factor₂ m k hn p)
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.Functor.flip_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (k : D) (j : C), (F.flip.obj k).obj j = (F.obj j).obj k
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} → (aig : Std.Sat.AIG α) → aig.RefVec w → aig.RefVec w → ℕ → aig.RefVec w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.lTensorAlgEquiv.eq_1 : ∀ (R : Type u_1) {M : Type u_2} (A : Type u_5) (B : Type u_6) [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddCommMonoid M],
  AddMonoidAlgebra.lTensorAlgEquiv R A B =
    (Algebra.TensorProduct.comm R (AddMonoidAlgebra A M) B).trans
      ((AddMonoidAlgebra.rTensorEquivAlgEquiv R R B A).trans
        (AddMonoidAlgebra.mapAlgEquiv R M (Algebra.TensorProduct.comm R B A)))
-- Mathlib.Analysis.Convex.Between
/-- A point lies in the closed interior of a 1-simplex if and only if it lies weakly between its
vertices.  -/
Affine.Simplex.mem_closedInterior_iff_wbtw : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {s : Affine.Simplex R P 1} {p : P},
  p ∈ s.closedInterior ↔ Wbtw R (s.points 0) p (s.points 1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.Const.unitOfList l) k = if l.contains k = true then some () else none
-- Mathlib.Geometry.RingedSpace.Basic
/-- High priority: This should fire before `basicOpen_res`.  -/
AlgebraicGeometry.RingedSpace.basicOpen_res_eq : ∀ (X : AlgebraicGeometry.RingedSpace) {U V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ} (i : U ⟶ V)
  [CategoryTheory.IsIso i] (f : ↑(X.presheaf.obj U)),
  X.basicOpen ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map i)) f) = X.basicOpen f
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.map.congr_simp : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (f f_1 : α → β → γ),
  f = f_1 → ∀ (m m_1 : Std.ExtHashMap α β), m = m_1 → Std.ExtHashMap.map f m = Std.ExtHashMap.map f_1 m_1
-- Mathlib.Geometry.Euclidean.Volume.Measure
MeasureTheory.Measure.euclideanHausdorffMeasure_def : ∀ {X : Type u_1} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (d : ℕ),
  MeasureTheory.Measure.euclideanHausdorffMeasure d =
    MeasureTheory.volume.addHaarScalarFactor (MeasureTheory.Measure.hausdorffMeasure ↑d) •
      MeasureTheory.Measure.hausdorffMeasure ↑d
-- Batteries.Data.UInt
UInt32.compare_eq_toNat_compare_toNat : ∀ (x y : UInt32), compare x y = compare x.toNat y.toNat
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.HasSubobjectClassifier`.

---

A category `C` has a subobject classifier if there is at least one subobject classifier.  -/
CategoryTheory.HasClassifier : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.restrict_surjective : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F) (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : Fact (Polynomial.map (algebraMap F E) p).Splits] [Normal F E],
  Function.Surjective ⇑(Polynomial.Gal.restrict p E)
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm is multiplicative.  -/
padicNorm.mul : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q r : ℚ), padicNorm p (q * r) = padicNorm p q * padicNorm p r
-- Mathlib.RingTheory.Valuation.Basic
Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfClassOfIsNontrivial : ∀ {R : Type u_3} [inst : Ring R] {Γ₀ : Type u_7} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  [hv : v.IsNontrivial], Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get?_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∩ t₂).get? k = none
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getGED_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getGED k fallback = t₂.getGED k fallback
-- Mathlib.Order.BoundedOrder.Lattice
sup_eq_bot_iff : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a b : α}, a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥
-- Mathlib.Data.Option.Defs
/-- Inhabited `get` function. Returns `a` if the input is `some a`, otherwise returns `default`.  -/
Option.iget : {α : Type u_1} → [Inhabited α] → Option α → α
-- Init.Grind.Lemmas
Lean.Grind.of_forall_eq_false : ∀ (α : Sort u) (p : α → Prop), (∀ (x : α), p x) = False → ∃ x, ¬p x
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- Given a set `s`, `addConjugatesOfSet s` is the set of all additive conjugates of
the elements of `s`.  -/
AddGroup.addConjugatesOfSet : {G : Type u_1} → [AddGroup G] → Set G → Set G
-- Batteries.Data.String.Matcher
/-- Returns the first substring of `s` that matches `pattern`,
or `none` if there is no such substring.
 -/
String.findSubstr? : String → Substring.Raw → Option Substring.Raw
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced
CategoryTheory.Functor.balanced_of_preserves : ∀ {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] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms]
  [F.PreservesEpimorphisms] [F.PreservesMonomorphisms] [CategoryTheory.Balanced D], CategoryTheory.Balanced C
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- Shorthand for the "backward" arrow corresponding to `f` in `symmetrify V`  -/
Quiver.Hom.toNeg : {V : Type u_2} → [inst : Quiver V] → {X Y : V} → (X ⟶ Y) → (Y ⟶ X)
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.div_eq_of_eq_mul : ∀ {α : Type u} [inst : DivisionMonoid α] {a b c : α}, IsUnit b → a = c * b → a / b = c
-- Init.Data.Array.MinMax
Array.min?_replicate_of_pos : ∀ {α : Type u_1} [inst : Min α] [Std.MinEqOr α] {n : ℕ} {a : α}, 0 < n → (Array.replicate n a).min? = some a
-- Init.Data.Int.DivMod.Lemmas
Int.neg_bmod : ∀ {a : ℤ} {b : ℕ}, (-a).bmod b = if ↑b ∣ 2 * a then a.bmod b else -a.bmod b
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.map_app : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂) (m : M₁),
  Q₂ (f m) = Q₁ m
-- Mathlib.RingTheory.LaurentSeries
PowerSeries.coe_add : ∀ {R : Type u_1} [inst : Semiring R] (f g : PowerSeries R),
  (HahnSeries.ofPowerSeries ℤ R) (f + g) = (HahnSeries.ofPowerSeries ℤ R) f + (HahnSeries.ofPowerSeries ℤ R) g
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsBasis.finite_iff_isRkFinite : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α}, M.IsBasis I X → (I.Finite ↔ M.IsRkFinite X)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
/-- **Alias** of `Left.nsmul_nonneg`. -/
nsmul_nonneg : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] {a : M}, 0 ≤ a → ∀ (n : ℕ), 0 ≤ n • a
-- Lean.DocString.Types
Lean.Doc.instOrdPart.ord : {i : Type u_1} →
  {b : Type u_2} → {p : Type u_3} → [Ord i] → [Ord b] → [Ord p] → Lean.Doc.Part i b p → Lean.Doc.Part i b p → Ordering
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- The identity morphism has a functorial choice of pullbacks.  -/
CategoryTheory.ChosenPullbacksAlong.id : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X : C) → CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id X)
-- Mathlib.RingTheory.Ideal.Operations
/-- See also `Ideal.IsPrime.mul_mem_pow` for prime ideal in Dedekind domain.  -/
Ideal.IsMaximal.mul_mem_pow : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R) [I.IsMaximal] {a b : R} {n : ℕ}, a * b ∈ I ^ n → a ∈ I ∨ b ∈ I ^ n
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The order isomorphism between `Fin n` and `{i, j}ᶜ` when `i < j` are
elements in `Fin (n + 2)`.  -/
SSet.stdSimplex.finOrderIsoPairCompl : {n : ℕ} → (i j : Fin (n + 2)) → i < j → Fin n ≃o ↥{i, j}ᶜ
-- Std.Time.Internal.UnitVal
Std.Time.Internal.UnitVal.ofInt.sizeOf_spec : ∀ {α : ℚ} (val : ℤ), sizeOf { val := val } = 1 + sizeOf val
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.co_support_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : Semiring R] (g : Γ), {a | ¬(0 ^ a).coeff g = 0} ⊆ {0}
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.mk.inj : ∀ {α : Type u} {inst : AddMonoid α} {val neg : α} {val_neg : val + neg = 0} {neg_val : neg + val = 0} {val_1 neg_1 : α}
  {val_neg_1 : val_1 + neg_1 = 0} {neg_val_1 : neg_1 + val_1 = 0},
  { val := val, neg := neg, val_neg := val_neg, neg_val := neg_val } =
      { val := val_1, neg := neg_1, val_neg := val_neg_1, neg_val := neg_val_1 } →
    val = val_1 ∧ neg = neg_1
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftEquiv'_inverse : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (i j : A) (h : i + j = 0),
  (CategoryTheory.shiftEquiv' C i j h).inverse = CategoryTheory.shiftFunctor C j
-- Mathlib.Analysis.Asymptotics.ExpGrowth
Monotone.expGrowthInf_comp : ∀ {u : ℕ → ENNReal} {v : ℕ → ℕ} {a : EReal},
  Monotone u →
    Filter.Tendsto (fun n => ↑(v n) / ↑n) Filter.atTop (nhds a) →
      a ≠ 0 → a ≠ ⊤ → ExpGrowth.expGrowthInf (u ∘ v) = a * ExpGrowth.expGrowthInf u
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.constOfIsEmpty.congr_simp : ∀ (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : IsEmpty ι] (m m_1 : N),
  m = m_1 → ContinuousAlternatingMap.constOfIsEmpty R M ι m = ContinuousAlternatingMap.constOfIsEmpty R M ι m_1
-- Lean.Elab.App
/-- Metavariables for the instance implicit arguments that have already been processed but not yet synthesized..  -/
Lean.Elab.Term.ElabAppArgs.State.instMVars : Lean.Elab.Term.ElabAppArgs.State → Array Lean.MVarId
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.bound : ∀ {N : ℕ}, 4096 ≤ N → ↑N ^ (↑(Behrend.nValue N))⁻¹ / Real.exp 1 < ↑(Behrend.dValue N)
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
/-- The property of objects in the functor category `J ⥤ C`
which preserves the colimit of a functor `F : K ⥤ J`.  -/
CategoryTheory.ObjectProperty.preservesColimit : {J : Type u_1} →
  {C : Type u_3} →
    {K : Type u_5} →
      [inst : CategoryTheory.Category.{v_1, u_5} K] →
        [inst_1 : CategoryTheory.Category.{v_3, u_1} J] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} C] →
            CategoryTheory.Functor K J → CategoryTheory.ObjectProperty (CategoryTheory.Functor J C)
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.nnnorm_def : ∀ {E : Type u_2} [inst : NNNorm E] (x : ULift.{u_5, u_2} E), ‖x‖₊ = ‖x.down‖₊
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.pairwise_toList_lt : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α] [inst_3 : Std.PRange.Least? α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [inst_8 : Std.Rxc.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerableLeast? α], List.Pairwise (fun a b => a < b) r.toList
-- Mathlib.Analysis.Complex.ReImTopology
TendstoUniformlyOn.im : ∀ {α : Type u_1} {ι : Type u_2} {f : ι → α → ℂ} {p : Filter ι} {g : α → ℂ} {K : Set α},
  TendstoUniformlyOn f g p K → TendstoUniformlyOn (fun n x => (f n x).im) (fun y => (g y).im) p K
-- Mathlib.Topology.Algebra.Monoid
isClosed_setOfPred_map_zero : ∀ (M₁ : Type u_6) (M₂ : Type u_7) [inst : TopologicalSpace M₂] [T2Space M₂] [inst_2 : Zero M₁] [inst_3 : Zero M₂],
  IsClosed {f | f 0 = 0}
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- In cartesian monoidal categories, the first product projections `fst` have a functorial choice
of pullbacks.  -/
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (X Y : C) → CategoryTheory.ChosenPullbacksAlong (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.iteratedDerivWithin_sin_Icc : ∀ (n : ℕ) {a b : ℝ},
  a < b → ∀ {x : ℝ}, x ∈ Set.Icc a b → iteratedDerivWithin n Real.sin (Set.Icc a b) x = iteratedDeriv n Real.sin x
-- Std.Time.DateTime.PlainDateTime
/-- Adds a `Millisecond.Offset` to a `PlainDateTime`, adjusting the second, minute, hour, and date if the milliseconds overflow.
 -/
Std.Time.PlainDateTime.addMilliseconds : Std.Time.PlainDateTime → Std.Time.Millisecond.Offset → Std.Time.PlainDateTime
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_injective : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : Zero α] [inst_1 : DecidableEq o],
  Function.Injective Matrix.blockDiagonal
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- `image.preComp f g` is an epimorphism when `f` is an epimorphism
(we need `C` to have equalizers to prove this).
 -/
CategoryTheory.Limits.image.preComp_epi_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [CategoryTheory.Limits.HasEqualizers C] [inst_2 : CategoryTheory.Limits.HasImage g]
  [inst_3 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)] [CategoryTheory.Epi f],
  CategoryTheory.Epi (CategoryTheory.Limits.image.preComp f g)
-- Mathlib.Util.LongNames
/-- Helper function for `#long_names` and `#long_instances`.  -/
printNameHashMap : Std.HashMap Lean.Name (Array Lean.Name) → IO Unit
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.type : Lean.Elab.PreDefinition → Lean.Expr
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- `Spec` is fully faithful on `R`-bialgebras, with inverse `Gamma`.  -/
AlgebraicGeometry.bialgSpec.fullyFaithful : {R : CommRingCat} → (AlgebraicGeometry.bialgSpec R).FullyFaithful
-- Lean.SubExpr
Lean.SubExpr.Pos.instEmptyCollection : EmptyCollection Lean.SubExpr.Pos
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesColimitsOfSize_iff_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h : F ≅ G),
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F ↔
    CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} G
-- Mathlib.CategoryTheory.ComposableArrows.One
CategoryTheory.ComposableArrows.mapFunctorArrows_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (i j i' j' n : ℕ)
  (x : autoParam (i ≤ j) CategoryTheory.ComposableArrows.mapFunctorArrows._auto_1)
  (x_1 : autoParam (i' ≤ j') CategoryTheory.ComposableArrows.mapFunctorArrows._auto_3)
  (x_2 : autoParam (i ≤ i') CategoryTheory.ComposableArrows.mapFunctorArrows._auto_5)
  (x_3 : autoParam (j ≤ j') CategoryTheory.ComposableArrows.mapFunctorArrows._auto_7)
  (x_4 : autoParam (j' ≤ n) CategoryTheory.ComposableArrows.mapFunctorArrows._auto_9)
  (S : CategoryTheory.ComposableArrows C n),
  (CategoryTheory.ComposableArrows.mapFunctorArrows C i j i' j' n x x_1 x_2 x_3 x_4).app S =
    CategoryTheory.ComposableArrows.homMk₁ (S.map' i i' x_2 ⋯) (S.map' j j' x_3 x_4) ⋯
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.mk_zero : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7},
  { toMultilinearMap := 0, map_eq_zero_of_eq' := ⋯ } = 0
-- Mathlib.Topology.Category.LightProfinite.Extend
/-- If the projection maps in the cone are epimorphic and the cone is limiting, then
`LightProfinite.Extend.functorOp` is final.
 -/
LightProfinite.Extend.functorOp_final : ∀ {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite))
  (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)],
  (LightProfinite.Extend.functorOp c).Final
-- Mathlib.Analysis.InnerProductSpace.NormPow
ContDiff.norm_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {F : Type u_2}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {f : F → E},
  ContDiff ℝ 1 f → ∀ {p : ℝ}, 1 < p → ContDiff ℝ 1 fun x => ‖f x‖ ^ p
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k k' : α},
  t.getKey? k = some k' → (Std.ExtTreeMap.filter f t)[k]? = Option.filter (fun x => f k' x) t[k]?
-- Mathlib.RingTheory.RingHom.QuasiFinite
/-- A ring hom `R →+* S` is quasi-finite if `S` is a quasi-finite `R`-algebra.  -/
RingHom.QuasiFinite : {R : Type u_4} → {S : Type u_5} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- Given a local frame `s i` on a neighbourhood `u` of `x`,
if a section `t` has `C^k` coefficients at `x` w.r.t. `s i`, then `t` is `C^n` at `x`.  -/
IsLocalFrameOn.contMDiffAt_of_coeff : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {n : WithTop ℕ∞} {x : M} {t : (x : M) → V x} (hs : IsLocalFrameOn I F n s u) [VectorBundle 𝕜 F V]
  [FiniteDimensional 𝕜 F],
  (∀ (i : ι), ContMDiffAt I (modelWithCornersSelf 𝕜 𝕜) n ((LinearMap.piApply (hs.coeff i)) t) x) →
    u ∈ nhds x → ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t x⟩) x
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
instCoeSortProfiniteGrpType.eq_1 : instCoeSortProfiniteGrpType = { coe := fun G => ↑G.toProfinite.toTop }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] [inst_1 : Inhabited β]
  (t t_1 : Std.ExtDTreeMap α (fun x => β) cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → Std.ExtDTreeMap.Const.get! t a = Std.ExtDTreeMap.Const.get! t_1 a_1
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.pair_iff'ₛ : ∀ {R : Type u_1} [inst : Semiring R] {x y : R},
  CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ y * x = 0 ∧ x + y = 1