mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- The function `f ↦ cfc f a` is Lipschitz with constant 1 with respect to
supremum metric (on `R →ᵤ[{spectrum R a}] R`) on those functions which are continuous on
the spectrum.  -/
lipschitzOnWith_cfc_fun : ∀ (R : Type u_2) {A : Type u_3} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : MetricSpace A] [inst_8 : Algebra R A] [inst_9 : IsometricContinuousFunctionalCalculus R A p] (a : A),
  LipschitzOnWith 1 (fun f => cfc ((UniformOnFun.toFun {spectrum R a}) f) a)
    {f | ContinuousOn ((UniformOnFun.toFun {spectrum R a}) f) (spectrum R a)}
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_minKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {he : l.isEmpty = false},
  Std.Internal.List.getKey (Std.Internal.List.minKey l he) l ⋯ = Std.Internal.List.minKey l he
-- Mathlib.Data.Real.Basic
Real.instMax : Max ℝ
-- Mathlib.Algebra.Exact.Basic
Function.Exact.apply_apply_eq_zero : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [inst : Zero P],
  Function.Exact f g → ∀ (x : M), g (f x) = 0
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
/-- An (additive) Klein four-group is an (additive) group of cardinality four and exponent two.  -/
IsAddKleinFour : (G : Type u_1) → [AddGroup G] → Prop
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.eq_two_or_odd' : ∀ {p : ℕ}, Nat.Prime p → p = 2 ∨ Odd p
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.preconnected_bot : ∀ {V : Type u} [Subsingleton V], ⊥.Preconnected
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- Construct a `Zero C` for a category with a zero object.
This cannot be a global instance as it will trigger for every `Zero C` typeclass search.
 -/
CategoryTheory.Limits.HasZeroObject.zero' : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasZeroObject C] → Zero C
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_pow : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommSemiring M] [inst_1 : Module ℚ≥0 M] [IsScalarTower ℚ≥0 M M]
  [SMulCommClass ℚ≥0 M M] (s : Finset ι) (f : ι → M) (n : ℕ),
  (s.expect fun i => f i) ^ n = (Fintype.piFinset fun x => s).expect fun p => ∏ i, f (p i)
-- Mathlib.CategoryTheory.Limits.Preorder
Preorder.coconeOfUpperBound_ι_app : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C) {x : C} (h : x ∈ upperBounds (Set.range F.obj)) (i : J),
  (Preorder.coconeOfUpperBound F h).ι.app i = CategoryTheory.homOfLE ⋯
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.instVAddSubtypeAEEqFunMemAddAddSubgroupLp : {M : Type u_1} →
  {α : Type u_3} →
    {E : Type u_4} →
      [inst : MeasurableSpace α] →
        [inst_1 : NormedAddCommGroup E] →
          {μ : MeasureTheory.Measure α} →
            {p : ENNReal} →
              [inst_2 : VAdd M α] →
                [MeasureTheory.VAddInvariantMeasure M α μ] →
                  [MeasurableConstVAdd M α] → VAdd Mᵈᵃᵃ ↥(MeasureTheory.Lp E p μ)
-- Init.Sym.Lemmas
Lean.Sym.dite_false_congr : ∀ {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬c → α) (c' : Prop) (h : c = c') {ht : ¬c'},
  dite c a b = b ⋯
-- Mathlib.Analysis.Complex.Harmonic.Poisson
_private.Mathlib.Analysis.Complex.Harmonic.Poisson.0.InnerProductSpace.continuousOn_herglotz_riesz : ∀ {c w : ℂ} {R : ℝ},
  w ∈ Metric.ball c R →
    ContinuousOn (fun x => ((x - c + (w - c)) / (x - c - (w - c))).re) {z | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
_private.Mathlib.Analysis.InnerProductSpace.ExteriorPower.0.exteriorPower.flip_innerProductForm : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E],
  exteriorPower.innerProductForm✝.flip = exteriorPower.innerProductForm✝
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Cell.alter.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α] {k : α}
  (f f_1 : Option (β k) → Option (β k)),
  f = f_1 →
    ∀ (c c_1 : Std.DTreeMap.Internal.Cell α β (compare k)),
      c = c_1 → Std.DTreeMap.Internal.Cell.alter f c = Std.DTreeMap.Internal.Cell.alter f_1 c_1
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IntermediateField.algHomEquivAlgHomOfSplits_apply_apply : ∀ {F : Type u_1} {K : Type u_2} (A : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field A]
  [inst_3 : Algebra F K] [inst_4 : Algebra F A] [inst_5 : Algebra.IsAlgebraic F K] (L : IntermediateField F A)
  (hL : ∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits) (f : K →ₐ[F] ↥L) (x : K),
  ((IntermediateField.algHomEquivAlgHomOfSplits A L hL) f) x = (algebraMap (↥L) A) (f x)
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.continuous : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  IsCoveringMap f → Continuous f
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.Products.max_eq_o_cons_tail' : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2) [inst_2 : Inhabited I] (l : Profinite.NobelingProof.Products I),
  ↑l ≠ [] →
    (↑l).head! = Profinite.NobelingProof.term I ho →
      ∀ (hlc : List.IsChain (fun x1 x2 => x1 > x2) (Profinite.NobelingProof.term I ho :: ↑l.Tail)),
        l = ⟨Profinite.NobelingProof.term I ho :: ↑l.Tail, hlc⟩
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The morphism in `CochainComplex C ℤ` associated to a `0`-cocycle.  -/
CochainComplex.HomComplex.Cocycle.homOf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} → CochainComplex.HomComplex.Cocycle F G 0 → (F ⟶ G)
-- Mathlib.Data.Set.Function
Set.BijOn.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α) (t : Set β),
  Set.BijOn f s t = (Set.MapsTo f s t ∧ Set.InjOn f s ∧ Set.SurjOn f s t)
-- Mathlib.NumberTheory.Multiplicity
padicValNat.pow_two_sub_one_ge : ∀ {n x : ℕ}, 1 < x → ¬2 ∣ x → n ≠ 0 → Even n → padicValNat 2 n + 2 ≤ padicValNat 2 (x ^ n - 1)
-- Mathlib.Logic.Function.Basic
Function.Surjective.exists₂ : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β},
  Function.Surjective f → ∀ {p : β → β → Prop}, (∃ y₁ y₂, p y₁ y₂) ↔ ∃ x₁ x₂, p (f x₁) (f x₂)
-- Mathlib.CategoryTheory.Sites.Limits
CategoryTheory.Sheaf.hasLimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] [CategoryTheory.Limits.HasLimitsOfSize.{u₁, u₂, w', w} D],
  CategoryTheory.Limits.HasLimitsOfSize.{u₁, u₂, max u w', max (max (max w u) w') v} (CategoryTheory.Sheaf J D)
-- Mathlib.RingTheory.MatrixAlgebra
kroneckerTMulLinearEquiv_tmul : ∀ (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9)
  (N : Type u_10) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module S M] [inst_7 : Module R N]
  [inst_8 : IsScalarTower R S M] [inst_9 : Fintype l] [inst_10 : Fintype m] [inst_11 : Fintype n] [inst_12 : Fintype p]
  [inst_13 : DecidableEq l] [inst_14 : DecidableEq m] [inst_15 : DecidableEq n] [inst_16 : DecidableEq p]
  (a : Matrix l m M) (b : Matrix n p N),
  (kroneckerTMulLinearEquiv l m n p R S M N) (a ⊗ₜ[R] b) = Matrix.kroneckerMap (TensorProduct.tmul R) a b
-- Mathlib.Order.Filter.IsBounded
Filter.isCoboundedUnder_le_of_eventually_le : ∀ {α : Type u_1} {ι : Type u_4} [inst : Preorder α] (l : Filter ι) [l.NeBot] {f : ι → α} {x : α},
  (∀ᶠ (i : ι) in l, x ≤ f i) → Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) l f
-- Mathlib.Topology.UniformSpace.Cauchy
/-- **Alias** of `isComplete_univ`. -/
complete_univ : ∀ {α : Type u} [inst : UniformSpace α] [CompleteSpace α], IsComplete Set.univ
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableAt_iff_of_mem_source : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} [IsManifold I 1 M]
  [IsManifold I' 1 M'] {x' : M} {y : M'},
  x' ∈ (chartAt H x).source →
    f x' ∈ (chartAt H' y).source →
      (MDiffAt f x' ↔
        ContinuousAt f x' ∧
          DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (Set.range ↑I)
            (↑(extChartAt I x) x'))
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_X_pow : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (n : ℕ), (Polynomial.X ^ n).roots = n • {0}
-- Mathlib.Topology.Separation.CompletelyRegular
instT35SpaceSubtype : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop} [T35Space X], T35Space (Subtype p)
-- Mathlib.Geometry.Euclidean.Congruence
/-- **Angle–Side–Angle (ASA) congruence**
If two triangles have two equal angles and the included side equal, then the triangles are
congruent. We require that one of the triangles is non-degenerate, the non-collinearity of the
other is then implied by the given equalities.
 -/
EuclideanGeometry.angle_side_angle : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [inst : NormedAddCommGroup V₁]
  [inst_1 : NormedAddCommGroup V₂] [inst_2 : InnerProductSpace ℝ V₁] [inst_3 : InnerProductSpace ℝ V₂]
  [inst_4 : MetricSpace P₁] [inst_5 : MetricSpace P₂] [inst_6 : NormedAddTorsor V₁ P₁] [inst_7 : NormedAddTorsor V₂ P₂]
  {a b c : P₁} {a' b' c' : P₂},
  ¬Collinear ℝ {a, b, c} →
    EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c' →
      dist b c = dist b' c' →
        EuclideanGeometry.angle b c a = EuclideanGeometry.angle b' c' a' → Congruent ![a, b, c] ![a', b', c']
-- Mathlib.Data.Complex.Basic
Complex.instRatCast : RatCast ℂ
-- Init.Data.Ord.Basic
Ordering.instIdempotentOpThen : Std.IdempotentOp Ordering.then
-- Mathlib.GroupTheory.Exponent
/-- If two commuting elements `x` and `y` of a monoid have order `n` and `m`, then there is an
element of order `lcm n m` that lies in the subgroup generated by `x` and `y`.  -/
Commute.exists_orderOf_eq_lcm : ∀ (G : Type u) [inst : Monoid G] {x y : G},
  Commute x y → ∃ z ∈ Submonoid.closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.refl_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} (f : u ⟶ v), (CategoryTheory.Arrow.LeftHomotopy.refl f).hom = 0
-- Mathlib.Analysis.Calculus.Gradient.Basic
gradient_eq_deriv : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {g : 𝕜 → 𝕜} {u : 𝕜}, gradient g u = (starRingEnd 𝕜) (deriv g u)
-- Lean.Elab.Tactic.Simp
Lean.Meta.Simp.ConfigWithOptions.mk : Lean.Meta.Simp.Config → Lean.Options → Lean.Meta.Simp.ConfigWithOptions
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.constantCoeff_Xzero : ∀ {R : Type u_1} [inst : CommRing R] (F : FormalGroup R), PowerSeries.constantCoeff F.Xzero = 0
-- Mathlib.Data.TypeVec
/-- arrow in the category of `TypeVec`  -/
TypeVec.Arrow : {n : ℕ} → TypeVec.{u} n → TypeVec.{v} n → Type (max u v)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_inv_app_right_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  (X_1 : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)),
  ((CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso α β X).inv.app X_1).right.right =
    CategoryTheory.CategoryStruct.id X_1.right.right
-- Mathlib.Data.Fintype.Sigma
PSigma.instFintype : {ι : Type u_1} → {κ : ι → Type u_3} → [(i : ι) → Fintype (κ i)] → [Fintype ι] → Fintype ((i : ι) ×' κ i)
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.Balanced.right : ∀ {α : Type u} {β : α → Type v} {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k v l r).Balanced → r.Balanced
-- Mathlib.Data.Set.Countable
/-- The set of finite sets in a countable type is countable.  -/
Set.Countable.ofPred_finite : ∀ {α : Type u} [Countable α], {s | s.Finite}.Countable
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- A nonzero ring seminorm on a field `K` is a ring norm.  -/
RingSeminorm.toRingNorm : {K : Type u_2} → [inst : Field K] → (f : RingSeminorm K) → f ≠ 0 → RingNorm K
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.quasiIsoAt_extendMap_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c')
  {j : ι} {j' : ι'},
  e.f j = j' →
    ∀ [inst_3 : K.HasHomology j] [inst_4 : L.HasHomology j] [inst_5 : (K.extend e).HasHomology j']
      [inst_6 : (L.extend e).HasHomology j'], QuasiIsoAt (HomologicalComplex.extendMap φ e) j' ↔ QuasiIsoAt φ j
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.alter.match_3.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) →
    (x = Ordering.lt → motive Ordering.lt) →
      (x = Ordering.gt → motive Ordering.gt) → (x = Ordering.eq → motive Ordering.eq) → motive x
-- Init.Data.String.Lemmas.Order
String.Pos.Raw.offsetBy.eq_1 : ∀ (p offset : String.Pos.Raw), p.offsetBy offset = { byteIdx := offset.byteIdx + p.byteIdx }
-- Init.Data.Array.Find
Array.findRev?_push_of_neg : ∀ {α : Type} {p : α → Bool} {a : α} {xs : Array α}, ¬p a = true → Array.findRev? p (xs.push a) = Array.findRev? p xs
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_of_contains_insertIfNew : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF → ∀ {k a : α} {v : β k}, (m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.parseLowerHex?.match_1.congr_eq_1 : ∀ (motive : Option ℕ → Sort u_1) (x : Option ℕ) (h_1 : (d : ℕ) → motive (some d)) (h_2 : Unit → motive none) (d : ℕ),
  x = some d →
    (match x with
      | some d => h_1 d
      | none => h_2 ()) ≍
      h_1 d
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.fst_comp_quotientInfEquivQuotientProd : ∀ {R : Type u_2} [inst : CommRing R] (I J : Ideal R) (coprime : IsCoprime I J),
  (RingHom.fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime) = Ideal.Quotient.factor ⋯
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseRequestTarget.origin : Std.Http.URI.Config → Std.Internal.Parsec.ByteArray.Parser Std.Http.RequestTarget
-- Mathlib.RingTheory.Ideal.Defs
Ideal.add_mem_iff_left : ∀ {α : Type u} [inst : Ring α] (I : Ideal α) {a b : α}, b ∈ I → (a + b ∈ I ↔ a ∈ I)
-- Lean.Meta.Sym.Pattern
/-- The next declaration index at the entry point of `isDefEqS`.
This information is used to decide whether an application is a Miller pattern or not.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.DefEqM.Context.lctxInitialNextIndex : Lean.Meta.Sym.DefEqM.Context✝ → ℕ
-- Init.Data.List.Scan.Lemmas
List.getElem_scanr : ∀ {α : Type u_1} {β : Type u_2} {i : ℕ} {b : β} {l : List α} {f : α → β → β} (h : i < (List.scanr f b l).length),
  (List.scanr f b l)[i] = List.foldr f b (List.drop i l)
-- Mathlib.Algebra.Module.Equiv.Basic
DistribMulAction.toLinearEquiv_apply : ∀ (R : Type u_1) {S : Type u_4} (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Group S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M] (s : S) (a : M),
  (DistribMulAction.toLinearEquiv R M s) a = s • a
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.Context.mk.injEq : ∀ (cfg : Mathlib.Tactic.DepRewrite.Config) (p x h : Lean.Expr) (Δ : Array (Lean.FVarId × Lean.Expr))
  (δ : Std.HashSet Lean.FVarId) (pHeadIdx : Lean.HeadIndex) (pNumArgs : ℕ) (cfg_1 : Mathlib.Tactic.DepRewrite.Config)
  (p_1 x_1 h_1 : Lean.Expr) (Δ_1 : Array (Lean.FVarId × Lean.Expr)) (δ_1 : Std.HashSet Lean.FVarId)
  (pHeadIdx_1 : Lean.HeadIndex) (pNumArgs_1 : ℕ),
  ({ cfg := cfg, p := p, x := x, h := h, Δ := Δ, δ := δ, pHeadIdx := pHeadIdx, pNumArgs := pNumArgs } =
      { cfg := cfg_1, p := p_1, x := x_1, h := h_1, Δ := Δ_1, δ := δ_1, pHeadIdx := pHeadIdx_1,
        pNumArgs := pNumArgs_1 }) =
    (cfg = cfg_1 ∧ p = p_1 ∧ x = x_1 ∧ h = h_1 ∧ Δ = Δ_1 ∧ δ = δ_1 ∧ pHeadIdx = pHeadIdx_1 ∧ pNumArgs = pNumArgs_1)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.cmp_veblenWith : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a b : Ordinal.{u}},
  Order.IsNormal f →
    cmp (Ordinal.veblenWith f o₁ a) (Ordinal.veblenWith f o₂ b) =
      match cmp o₁ o₂ with
      | Ordering.eq => cmp a b
      | Ordering.lt => cmp a (Ordinal.veblenWith f o₂ b)
      | Ordering.gt => cmp (Ordinal.veblenWith f o₁ a) b
-- Mathlib.CategoryTheory.ComposableArrows.Three
/-- Variant of `threeδ₂Toδ₁` for preorders.  -/
CategoryTheory.ComposableArrows.threeδ₂Toδ₁' : {ι : Type u_1} →
  [inst : Preorder ι] →
    (i₀ i₁ i₂ i₃ : ι) →
      (hi₀₁ : i₀ ≤ i₁) →
        (hi₁₂ : i₁ ≤ i₂) →
          (hi₂₃ : i₂ ≤ i₃) →
            CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE ⋯) ⟶
              CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE hi₂₃)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.foldrM_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} {δ : Type w} {m : Type w → Type w'}
  [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.TreeSet.Raw.foldrM f init t₁ = Std.TreeSet.Raw.foldrM f init t₂
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.comap_sup : ∀ {α : Type u_1} {β : Type u_2} {m₁ m₂ : MeasurableSpace α} {g : β → α},
  MeasurableSpace.comap g (m₁ ⊔ m₂) = MeasurableSpace.comap g m₁ ⊔ MeasurableSpace.comap g m₂
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_neg_mul_zpow_self : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R] (n : ℤ)
  {A : Matrix n' n' R}, IsUnit A.det → A ^ (-n) * A ^ n = 1
-- Init.Prelude
instDecidableEqRaw : DecidableEq String.Pos.Raw
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are flat algebras over `R`, such that `A ⊗[R] B` is a domain, and such that
the algebra maps are injective, then there exists an `R`-algebra `K` that is a field that `A`
and `B` inject into with linearly disjoint images. Note: `K` can chosen to be the
fraction field of `A ⊗[R] B`, but here we hide this fact.  -/
Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective : ∀ (R : Type u) [inst : CommRing R] (A : Type v) [inst_1 : CommRing A] (B : Type w) [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [Module.Flat R A] [Module.Flat R B] [IsDomain (TensorProduct R A B)],
  Function.Injective ⇑(algebraMap R A) →
    Function.Injective ⇑(algebraMap R B) →
      ∃ K x x_1 fa fb, Function.Injective ⇑fa ∧ Function.Injective ⇑fb ∧ fa.range.LinearDisjoint fb.range
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- *Lebesgue differentiation theorem*: for almost every point `x`, the
average of `f` on `a` tends to `f x` as `a` shrinks to `x` along a Vitali family.  -/
VitaliFamily.ae_tendsto_average : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) {E : Type u_2} [inst_1 : NormedAddCommGroup E] [SecondCountableTopology α] [BorelSpace α]
  [MeasureTheory.IsLocallyFiniteMeasure μ] [inst_5 : NormedSpace ℝ E] [CompleteSpace E] {f : α → E},
  MeasureTheory.LocallyIntegrable f μ →
    ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ⨍ (y : α) in a, f y ∂μ) (v.filterAt x) (nhds (f x))
-- Mathlib.Data.Nat.Cast.SetInterval
Nat.image_cast_int_Icc : ∀ (a b : ℕ), Nat.cast '' Set.Icc a b = Set.Icc ↑a ↑b
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
instPolynormableSpaceProd : ∀ {𝕜 : Type u_2} [inst : NormedField 𝕜] {E₁ : Type u_11} {E₂ : Type u_12} [inst_1 : AddCommGroup E₁]
  [inst_2 : AddCommGroup E₂] [inst_3 : Module 𝕜 E₁] [inst_4 : Module 𝕜 E₂] [inst_5 : TopologicalSpace E₁]
  [inst_6 : TopologicalSpace E₂] [PolynormableSpace 𝕜 E₁] [PolynormableSpace 𝕜 E₂], PolynormableSpace 𝕜 (E₁ × E₂)
-- Mathlib.Data.Setoid.Partition
/-- The indices of `Quotient.out` and `IndexedPartition.out` are equal.  -/
IndexedPartition.index_out : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : hs.Quotient),
  hs.index (Quotient.out x) = hs.index (hs.out x)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.induction_on_addUnits : ∀ {M : Type u_1} [inst : AddMonoid M] {c : AddCon M} {p : AddUnits c.Quotient → Prop} (u : AddUnits c.Quotient),
  (∀ (x y : M) (hxy : c (x + y) 0) (hyx : c (y + x) 0), p { val := ↑x, neg := ↑y, val_neg := ⋯, neg_val := ⋯ }) → p u
-- Mathlib.Algebra.Order.AddGroupWithTop
/-- In a `LinearOrderedAddCommMonoidWithTop`, the `⊤` element is invariant under addition.  -/
LinearOrderedAddCommGroupWithTop.top_add' : ∀ {α : Type u_3} [self : LinearOrderedAddCommGroupWithTop α] (x : α), ⊤ + x = ⊤
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
OrderEmbedding.toOrderHom.eq_1 : ∀ {X : Type u_6} {Y : Type u_7} [inst : Preorder X] [inst_1 : Preorder Y] (f : X ↪o Y),
  f.toOrderHom = { toFun := ⇑f, monotone' := ⋯ }
-- Lean.Meta.Structure
/-- If `struct` is an application of the form `S ..` with `S` a constant for a structure,
returns the name of the structure, otherwise throws an error.
 -/
Lean.Meta.getStructureName : Lean.Expr → Lean.MetaM Lean.Name
-- Lean.DocString.Types
/-- How to render mathematical content.
 -/
Lean.Doc.MathMode : Type
-- Lean.Data.KVMap
Lean.KVMap.mk.injEq : ∀ (entries entries_1 : List (Lean.Name × Lean.DataValue)),
  ({ entries := entries } = { entries := entries_1 }) = (entries = entries_1)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_inv : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Inv β] (f : MeasureTheory.SimpleFunc α β),
  ⇑f⁻¹ = (⇑f)⁻¹
-- Mathlib.Topology.MetricSpace.ShrinkingLemma
/-- Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover
of a closed subset of a proper metric space by nonempty open balls can be shrunk to a new cover by
nonempty open balls so that each of the new balls has strictly smaller radius than the old one.  -/
exists_subset_iUnion_ball_radius_pos_lt : ∀ {α : Type u} {ι : Type v} [inst : MetricSpace α] [ProperSpace α] {c : ι → α} {s : Set α} {r : ι → ℝ},
  (∀ (i : ι), 0 < r i) →
    IsClosed s →
      (∀ x ∈ s, {i | x ∈ Metric.ball (c i) (r i)}.Finite) →
        s ⊆ ⋃ i, Metric.ball (c i) (r i) → ∃ r', s ⊆ ⋃ i, Metric.ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Set.Ioo 0 (r i)