mathlib-initiative/mathlib-types huggingface dataset:
-- Init.MetaTypes
/-- If true (default: false), then when no name is provided for a 'let' expression, the name is used as-is without making it be inaccessible.
The name still might be inaccessible if the binder name was.  -/
Lean.Meta.ExtractLetsConfig.preserveBinderNames : Lean.Meta.ExtractLetsConfig → Bool
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.hom.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} {K L : Set V} (h : K ⊆ L) (C C_1 : G.ComponentCompl L),
  C = C_1 → SimpleGraph.ComponentCompl.hom h C = SimpleGraph.ComponentCompl.hom h C_1
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
/-- `simp`-normal form of `mvPolynomialOptionEquivPolynomialAdjoin_C`  -/
AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C' : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (hx : AlgebraicIndependent R x) (r : R),
  Polynomial.C (hx.aevalEquiv (MvPolynomial.C r)) = Polynomial.C ((algebraMap R ↥(Algebra.adjoin R (Set.range x))) r)
-- Mathlib.RingTheory.Polynomial.UniqueFactorization
MvPolynomial.uniqueFactorizationMonoid : ∀ (σ : Type v) {D : Type u} [inst : CommRing D] [UniqueFactorizationMonoid D],
  UniqueFactorizationMonoid (MvPolynomial σ D)
-- Mathlib.Algebra.Lie.Weights.Cartan
/-- Auxiliary definition for `rootSpaceWeightSpaceProduct`,
which is close to the deterministic timeout limit.
 -/
LieAlgebra.rootSpaceWeightSpaceProductAux : (R : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          (H : LieSubalgebra R L) →
            [inst_3 : LieRing.IsNilpotent ↥H] →
              (M : Type u_3) →
                [inst_4 : AddCommGroup M] →
                  [inst_5 : Module R M] →
                    [inst_6 : LieRingModule L M] →
                      [inst_7 : LieModule R L M] →
                        {χ₁ χ₂ χ₃ : ↥H → R} →
                          χ₁ + χ₂ = χ₃ →
                            ↥(LieAlgebra.rootSpace H χ₁) →ₗ[R]
                              ↥(LieModule.genWeightSpace M χ₂) →ₗ[R] ↥(LieModule.genWeightSpace M χ₃)
-- Mathlib.Topology.UniformSpace.Basic
comp_open_symm_mem_uniformity_sets : ∀ {α : Type ua} [inst : UniformSpace α] {s : SetRel α α},
  s ∈ uniformity α → ∃ t ∈ uniformity α, IsOpen t ∧ SetRel.IsSymm t ∧ SetRel.comp t t ⊆ s
-- Init.Data.Option.Attach
Option.get_attachWith : ∀ {α : Type u_1} {p : α → Prop} {o : Option α} (H : ∀ (a : α), o = some a → p a) (h : (o.attachWith p H).isSome = true),
  (o.attachWith p H).get h = ⟨o.get ⋯, ⋯⟩
-- Mathlib.Order.Hom.Set
OrderIso.range_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), Set.range ⇑e = Set.univ
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.hasProd_iInf_prod : ∀ {α : Type u_1} {f : α → ENNReal}, (∀ (i : α), f i ≤ 1) → HasProd f (⨅ s, ∏ i ∈ s, f i)
-- Mathlib.Algebra.Order.Group.Abs
abs_add_three : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] (a b c : G),
  |a + b + c| ≤ |a| + |b| + |c|
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.eq_neg_swap : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α)
  (a b : α), variationOnFromTo f s a b = -variationOnFromTo f s b a
-- Mathlib.Analysis.MellinTransform
MellinConvergent.cpow_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E} {s a : ℂ},
  MellinConvergent (fun t => ↑t ^ a • f t) s ↔ MellinConvergent f (s + a)
-- Mathlib.Topology.MetricSpace.Cover
Metric.IsCover.image_lipschitz_of_surjective : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {f : X → Y} {s : Set Y}
  {N : Set X} {ε K₂ : NNReal},
  Metric.IsCover ε (f ⁻¹' s) N → LipschitzWith K₂ f → Function.Surjective f → Metric.IsCover (K₂ * ε) s (f '' N)
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.mkMethods : Lean.Meta.Simp.SimprocsArray → Lean.Meta.Simp.Discharge → Bool → Lean.Meta.Simp.Methods
-- Mathlib.Data.Nat.Factorization.PrimePow
Nat.not_isPrimePow_iff_nontrivial_of_two_le : ∀ {n : ℕ}, 2 ≤ n → (¬IsPrimePow n ↔ n.primeFactors.Nontrivial)
-- Mathlib.Analysis.Analytic.Constructions
/-- Finite sums of analytic functions are analytic  -/
Finset.analyticOnNhd_sum : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {f : α → E → F} {s : Set E} (N : Finset α), (∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) → AnalyticOnNhd 𝕜 (∑ n ∈ N, f n) s
-- Init.Data.String.Lemmas.StringOrder
String.le_trans : ∀ {a b c : String}, a ≤ b → b ≤ c → a ≤ c
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_le_size_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α}, t.size ≤ (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).size
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_diff_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ((↑(m₁.diff m₂)).isEmpty = true ↔ ∀ (k : α), m₁.contains k = true → m₂.contains k = true)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_top : LinearGrowth.linearGrowthSup ⊤ = ⊤
-- Std.Data.Iterators.Lemmas.Producers.Repeat
Std.Iter.atIdxSlow?_succ_repeat : ∀ {α : Type w} {f : α → α} {init : α} {k : ℕ},
  Std.Iter.atIdxSlow? (k + 1) (Std.Iter.repeat f init) = Std.Iter.atIdxSlow? k (Std.Iter.repeat f (f init))
-- Mathlib.Algebra.GroupWithZero.Action.Units
Commute.smul_left_iff₀ : ∀ {α : Type u_4} {β : Type u_5} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α} [inst_2 : Mul β]
  [SMulCommClass α β β] [IsScalarTower α β β] {x y : β}, a ≠ 0 → (Commute (a • x) y ↔ Commute x y)
-- Mathlib.RingTheory.PowerSeries.Basic
/-- The constant formal power series.  -/
PowerSeries.C : {R : Type u_1} → [inst : Semiring R] → R →+* PowerSeries R
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.obj_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} (x y : CategoryTheory.StructuredArrow S T) (hr : x.right = y.right),
  CategoryTheory.CategoryStruct.comp x.hom (T.map (CategoryTheory.eqToHom hr)) = y.hom → x = y
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.State.mk.sizeOf_spec : ∀ (steps : ℕ) (infos : Lean.SubExpr.PosMap Lean.Elab.Info)
  (holeIter : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator),
  sizeOf { steps := steps, infos := infos, holeIter := holeIter } = 1 + sizeOf steps + sizeOf infos + sizeOf holeIter
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.isFiniteMeasureOfIsEmpty : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [IsEmpty α], MeasureTheory.IsFiniteMeasure μ
-- Mathlib.Data.List.Basic
List.getLastI_eq_getLast?_getD : ∀ {α : Type u} [inst : Inhabited α] (l : List α), l.getLastI = l.getLast?.getD default
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_iterate_derivative_mem_span_T : ∀ {R : Type u_1} [inst : CommRing R] (n k : ℕ),
  (⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T R ↑n) ∈
    Submodule.span ℕ ((fun m => Polynomial.Chebyshev.T R ↑m) '' Set.Icc 0 (n - k))
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- A version of submodularity applied to the insertion of some `e` into two sets.  -/
Matroid.eRk_insert_inter_add_eRk_insert_union_le : ∀ {α : Type u_1} {e : α} (M : Matroid α) (X Y : Set α),
  M.eRk (insert e (X ∩ Y)) + M.eRk (insert e (X ∪ Y)) ≤ M.eRk (insert e X) + M.eRk (insert e Y)
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.IsMonoidalClosed.prop_ihom : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {P : CategoryTheory.ObjectProperty C} {inst_2 : CategoryTheory.MonoidalClosed C} [self : P.IsMonoidalClosed]
  (X Y : C), P X → P Y → P (X ⟹ Y)
-- Mathlib.Data.Matrix.Basis
Matrix.transpose_single : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α] (i : m)
  (j : n) (a : α), (Matrix.single i j a).transpose = Matrix.single j i a
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.Kernel.measure_eq_zero_or_one_or_top_of_indepSet_self : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μα : MeasureTheory.Measure α} {t : Set Ω},
  ProbabilityTheory.Kernel.IndepSet t t κ μα → ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.instIsInvInvariantCount : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableInv G],
  MeasureTheory.Measure.count.IsInvInvariant
-- Mathlib.Order.Directed
/-- A set stable by infimum is `≥`-directed.  -/
directedOn_of_inf_mem : ∀ {α : Type u_1} [inst : SemilatticeInf α] {S : Set α},
  (∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊓ j ∈ S) → DirectedOn (fun x1 x2 => x1 ≥ x2) S
-- Mathlib.Data.Nat.Nth
Nat.le_nth_count : ∀ {p : ℕ → Prop} [inst : DecidablePred p], (Set.ofPred p).Infinite → ∀ (n : ℕ), n ≤ Nat.nth p (Nat.count p n)
-- Lean.Setup
Lean.instReprImportArtifacts.repr : Lean.ImportArtifacts → ℕ → Std.Format
-- Mathlib.RingTheory.Coprime.Lemmas
IsCoprime.prod_left : ∀ {R : Type u} {I : Type v} [inst : CommSemiring R] {x : R} {s : I → R} {t : Finset I},
  (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.hasOne : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → One (Matrix.SpecialLinearGroup n R)
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalSubalgebra.unitization.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : SetLike S A] [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A] (s : S),
  NonUnitalSubalgebra.unitization s = Unitization.lift (NonUnitalSubalgebraClass.subtype s)
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.instVAdd : {ι : Type u_1} →
  {k : Type u_5} →
    {V : Type u_6} →
      {P : Type u_7} →
        [inst : AddCommGroup V] →
          [inst_1 : AddTorsor V P] → [inst_2 : Ring k] → [inst_3 : Module k V] → VAdd V (AffineBasis ι k P)
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHomLeft : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' : Cᵒᵖ} (f : c ⟶ c') (d : Dᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.unop (Opposite.unop d)).op
-- Mathlib.RingTheory.Ideal.Prime
Ideal.IsPrime.mem_of_pow_mem : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I.IsPrime → ∀ {r : α} (n : ℕ), r ^ n ∈ I → r ∈ I
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.HopfObj.antipode_comul₁ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.HopfObj A],
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.HopfObj.antipode A)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ComonObj.comul A)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.ComonObj.comul))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
                  (CategoryTheory.MonoidalCategoryStruct.associator A A A).inv)
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
                    (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A A).hom A))
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
                      (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom)
                    (CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.MonoidalCategoryStruct.associator A A
                          (CategoryTheory.MonoidalCategoryStruct.tensorObj A A)).inv
                      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul
                        CategoryTheory.MonObj.mul))))))))) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one))
-- Mathlib.Data.Num.Basic
/-- The number of bits of a `PosNum`, as a `PosNum`.  -/
PosNum.size : PosNum → PosNum
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulPosStrictMono.toMulPosReflectLE : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : LinearOrder α] [MulPosStrictMono α], MulPosReflectLE α
-- Mathlib.Algebra.Module.Presentation.Tautological
/-- Any `A`-module admits a tautological presentation by generators and relations.  -/
Module.Presentation.tautologicalSolutionIsPresentationCore : (A : Type u) →
  [inst : Ring A] →
    (M : Type v) →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module A M] → (Module.Presentation.tautologicalSolution A M).IsPresentationCore
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleIso_hom_app_hom₁ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [inst_4 : F₁.CommShift ℤ]
  [inst_5 : F₂.CommShift ℤ] [inst_6 : CategoryTheory.NatTrans.CommShift e.hom ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Functor.mapTriangleIso e).hom.app X).hom₁ = e.hom.app X.obj₁
-- Mathlib.Data.Num.Lemmas
Num.cmp_to_nat : ∀ (m n : Num), Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.idealOrderIsoENat_symm_apply_coe : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (n : ℕ),
  (IsDiscreteValuationRing.idealOrderIsoENat R).symm ↑n = IsLocalRing.maximalIdeal R ^ n
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.map_ite_one_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] {F : Type u_7}
  [inst_2 : FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F) (p : Prop) [inst_4 : Decidable p],
  f (if p then 1 else 0) = if p then 1 else 0
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.unique : ∀ {x : ℝ*} {r s : ℝ}, x.IsSt r → x.IsSt s → r = s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_le_size_insertMany : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w}
  [inst_2 : ForIn Id ρ ((a : α) × β a)] [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {l : ρ}, (↑m).size ≤ (↑↑(m.insertMany l)).size
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_mem_openSegment_compl_self : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal}
  [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.NullMeasurableSet s μ →
    μ s ≠ 0 → μ sᶜ ≠ 0 → ⨍⁻ (x : α), f x ∂μ ∈ openSegment ENNReal (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in sᶜ, f x ∂μ)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- The symmetry between the total complex shape for `c₁`, `c₂` and `c₁₂`,
and its symmetric total complex shape.  -/
TotalComplexShape.symmSymmetry : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) →
          (c₁₂ : ComplexShape I₁₂) → [inst : TotalComplexShape c₁ c₂ c₁₂] → TotalComplexShapeSymmetry c₁ c₂ c₁₂
-- Mathlib.Data.Int.ModEq
Int.ModEq.symm : ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → b ≡ a [ZMOD n]
-- Mathlib.Analysis.Normed.Group.Basic
NormedAddCommGroup.uniformity_basis_dist : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E],
  (uniformity E).HasBasis (fun ε => 0 < ε) fun ε => {p | ‖p.1 - p.2‖ < ε}
-- Mathlib.Data.Finset.Functor
Finset.lawfulApplicative : ∀ [inst : (P : Prop) → Decidable P], LawfulApplicative Finset
-- Mathlib.Analysis.Convex.Star
StarConvex.add_smul_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] {x y : E} {s : Set E}, StarConvex 𝕜 x s → x + y ∈ s → ∀ {t : 𝕜}, 0 ≤ t → t ≤ 1 → x + t • y ∈ s
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Submonoid.LocalizationMap.mk'_zero : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  (f : S.LocalizationMap N) (s : ↥S), f.mk' 0 s = 0
-- Mathlib.Algebra.Category.Grp.Basic
/-- The underlying monoid homomorphism.  -/
CommGrpCat.Hom.hom' : {A B : CommGrpCat} → A.Hom B → ↑A →* ↑B
-- Mathlib.RingTheory.Congruence.Basic
RingCon.instSubsingleton : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] [Subsingleton R], Subsingleton (RingCon R)
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Result.counters : Lean.Meta.Grind.Result → Lean.Meta.Grind.Counters
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.addEmptyConstants_symm_isExpansionOn : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M],
  (FirstOrder.Language.LEquiv.addEmptyConstants L ↑∅).symm.toLHom.IsExpansionOn M
-- Mathlib.Data.W.Constructions
WType.Natα.zero : WType.Natα
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.isUnit_of_sub_one_mem_jacobson_bot : ∀ {R : Type u} [inst : CommRing R] (r : R), r - 1 ∈ ⊥.jacobson → IsUnit r
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_map_left : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) {M₃ : Type u_7}
  [inst_8 : AddCommMonoid M₃] [inst_9 : Module R M₃] (f : M₃ →ₗ[R] M₂) (g : M₁ ≃ₗ[R] M₃),
  (LinearMap.toMatrix (v₁.map g) v₂) f = (LinearMap.toMatrix v₁ v₂) (f ∘ₗ ↑g)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.mergeWith! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ t₃ t₄ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t₁.Equiv t₂ →
    t₃.Equiv t₄ →
      t₁.WF →
        t₂.WF →
          t₃.WF →
            t₄.WF →
              ∀ {f : (a : α) → β a → β a → β a},
                (Std.DTreeMap.Internal.Impl.mergeWith! f t₁ t₃).Equiv (Std.DTreeMap.Internal.Impl.mergeWith! f t₂ t₄)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- If `f` is continuous multilinear, then `f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ)` is the sum of
`f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions `r`. This follows from
multilinearity by expanding successively with respect to each coordinate.  -/
ContinuousMultilinearMap.map_sum : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) {α : ι → Type u_1} [inst_7 : Fintype ι] (g : (i : ι) → α i → M₁ i)
  [inst_8 : DecidableEq ι] [inst_9 : (i : ι) → Fintype (α i)], (f fun i => ∑ j, g i j) = ∑ r, f fun i => g i (r i)
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- The functor `Over.forget X : Over X ⥤ C` has a right adjoint given by `star X`.

Note that the binary products assumption is necessary: the existence of a right adjoint to
`Over.forget X` is equivalent to the existence of each binary product `X ⨯ -`.
 -/
CategoryTheory.Over.forgetAdjStar : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] → CategoryTheory.Over.forget X ⊣ CategoryTheory.Over.star X
-- Mathlib.Order.Closure
GaloisConnection.closureOperator_isClosed : ∀ {α : Type u_1} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (gc : GaloisConnection l u) (x : α), gc.closureOperator.IsClosed x = (u (l x) = x)
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.sound : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {a b : C} {f₁ f₂ : a ⟶ b},
  r f₁ f₂ → (CategoryTheory.Quotient.functor r).map f₁ = (CategoryTheory.Quotient.functor r).map f₂
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- Construct a groupoid of partial homeos for which the map and its inverse have some property,
from a pregroupoid asserting that this property is stable under composition.  -/
Pregroupoid.groupoid : {H : Type u_1} → [inst : TopologicalSpace H] → Pregroupoid H → StructureGroupoid H
-- Mathlib.CategoryTheory.Grothendieck
/-- The Grothendieck construction applied to a functor to `Type`
(thought of as a functor to `Cat` by realising a type as a discrete category)
is the same as the 'category of elements' construction.
 -/
CategoryTheory.Grothendieck.grothendieckTypeToCat : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (G : CategoryTheory.Functor C (Type w)) → CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat) ≌ G.Elements
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- The `incidenceSet` is the set of edges incident to a given vertex.  -/
SimpleGraph.Subgraph.incidenceSet : {V : Type u} → {G : SimpleGraph V} → G.Subgraph → V → Set (Sym2 V)
-- Mathlib.Data.Set.Function
Set.BijOn.mk : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β},
  Set.MapsTo f s t → Set.InjOn f s → Set.SurjOn f s t → Set.BijOn f s t
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousLinearMap.flipAlternating_apply_apply : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (f : F →L[𝕜] E [⋀^ι]→L[𝕜] G) (m : (i : ι) → (fun x => E) i) (x : F), (f.flipAlternating m) x = (f x) m
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_insertMany_empty_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : Std.LawfulEqOrd α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} {fallback : β k'},
  List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).getD k' fallback = cast ⋯ v
-- Mathlib.Analysis.Normed.Order.Lattice
norm_sup_le_add : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (x y : α),
  ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖