mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsNatCastApply.natCast_apply`. -/
natCast_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {inst : FunLike F α α} {inst_1 : NatCast F} {inst_2 : SMul ℕ α}
  [self : IsNatCastApply F α] (n : ℕ) (x : α), ↑n x = n • x
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceL!.match_5.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (ls : ℕ) (lk : α) (lv : β lk)
  (ll lr : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (ls : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)),
  (match Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr => h_2 ls lk lv ll lr) =
    h_2 ls lk lv ll lr
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.componentComplMk_eq_of_adj : ∀ {V : Type u} {K : Set V} (G : SimpleGraph V) {v w : V} (vK : v ∉ K) (wK : w ∉ K),
  G.Adj v w → G.componentComplMk vK = G.componentComplMk wK
-- Lean.Elab.PreDefinition.Main
/-- Elaborates the `TerminationHint` in the clique to `TerminationMeasures`
 -/
Lean.Elab.elabTerminationByHints : Array Lean.Elab.PreDefinition → Lean.Elab.TermElabM (Array (Option Lean.Elab.TerminationMeasure))
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.mk.injEq : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (pt : Type w₁)
  (ι : (j : J) → F.obj j → pt)
  (ι_naturality :
    autoParam (∀ {j j' : J} (f : j ⟶ j'), ι j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) = ι j)
      CategoryTheory.Functor.CoconeTypes.ι_naturality._autoParam)
  (pt_1 : Type w₁) (ι_1 : (j : J) → F.obj j → pt_1)
  (ι_naturality_1 :
    autoParam (∀ {j j' : J} (f : j ⟶ j'), ι_1 j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) = ι_1 j)
      CategoryTheory.Functor.CoconeTypes.ι_naturality._autoParam),
  ({ pt := pt, ι := ι, ι_naturality := ι_naturality } = { pt := pt_1, ι := ι_1, ι_naturality := ι_naturality_1 }) =
    (pt = pt_1 ∧ ι ≍ ι_1)
-- Mathlib.Data.List.Basic
List.cons_head!_tail : ∀ {α : Type u} [inst : Inhabited α] {l : List α}, l ≠ [] → l.head! :: l.tail = l
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.cg' : ∀ {L : FirstOrder.Language} {ι : Type u_1} [Countable ι] [inst : Preorder ι] [inst_1 : IsDirectedOrder ι]
  [inst_2 : Nonempty ι] {G : ι → Type w} [inst_3 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [h : ∀ (i : ι), FirstOrder.Language.Structure.CG L (G i)]
  [inst_4 : DirectedSystem G fun i j h => ⇑(f i j h)],
  FirstOrder.Language.Structure.CG L (FirstOrder.Language.DirectLimit G f)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.dropSliceTR.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → Array α → Sort u_2) →
    (x : List α) →
      (x_1 : ℕ) →
        (x_2 : Array α) →
          ((x : ℕ) → (x_3 : Array α) → motive [] x x_3) →
            ((head : α) → (xs : List α) → (acc : Array α) → motive (head :: xs) 0 acc) →
              ((x : α) → (xs : List α) → (n : ℕ) → (acc : Array α) → motive (x :: xs) n.succ acc) → motive x x_1 x_2
-- Mathlib.Topology.Category.Stonean.Basic
Profinite.lift_lifts : ∀ {X Y : Profinite} {Z : Stonean} (e : Stonean.toProfinite.obj Z ⟶ Y) (f : X ⟶ Y) [inst : CategoryTheory.Epi f],
  CategoryTheory.CategoryStruct.comp (Profinite.lift e f) f = e
-- Mathlib.Algebra.Group.Units.Defs
/-- See `isAddUnit_iff_exists_and_exists` for a similar lemma with two existentials.  -/
isAddUnit_iff_exists : ∀ {M : Type u_1} [inst : AddMonoid M] {x : M}, IsAddUnit x ↔ ∃ b, x + b = 0 ∧ b + x = 0
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_mul_sqrt_lt_succ : ∀ (n : ℕ), n.sqrt * n.sqrt < n + 1
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- The category of `1`-hypercovers with refinement morphisms up to homotopy.  -/
CategoryTheory.GrothendieckTopology.HOneHypercover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C → C → Type (max (max u v) (u_1 + 1))
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.opEquivalence_inverse_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (n : ℕ) (X : CategoryTheory.ComposableArrows Cᵒᵖ n),
  (CategoryTheory.ComposableArrows.opEquivalence C n).inverse.obj X =
    Opposite.op
      ((⋯.functor.comp (CategoryTheory.orderDualEquivalence (Fin (n + 1))).functor).comp
        (CategoryTheory.Functor.leftOp X))
-- Mathlib.Tactic.Translate.Core
_private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.elabRename.addRule : Lean.Name →
  Array Lean.Name →
    Lean.TSyntax `ident → Lean.TSyntax `ident → Lean.NameMap Lean.Name → Lean.MetaM (Lean.NameMap Lean.Name)
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.rid_toAlgEquiv : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Bialgebra S A] [inst_4 : Algebra R A] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R S A],
  (Bialgebra.TensorProduct.rid R S A).toAlgEquiv = Algebra.TensorProduct.rid R S A
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.map_star_inv_eq_transpose : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (U : ↥(Matrix.unitaryGroup n α)), (Matrix.UnitaryGroup.map_star U)⁻¹ = Matrix.UnitaryGroup.transpose U
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
Matrix.invOf_fromBlocks_zero₁₂_eq : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α)
  [inst_5 : Invertible A] [inst_6 : Invertible D] [inst_7 : Invertible (Matrix.fromBlocks A 0 C D)],
  ⅟(Matrix.fromBlocks A 0 C D) = Matrix.fromBlocks (⅟A) 0 (-(⅟D * C * ⅟A)) ⅟D
-- Init.Prelude
/-- The successor of a natural number `n`.

Using `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal
form](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).
 -/
Nat.succ : ℕ → ℕ
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_subset_uIcc_iff_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α},
  Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂ ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Map `WithTerminal` with respect to a functor `F : C ⥤ D`.  -/
CategoryTheory.WithTerminal.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Functor C D →
          CategoryTheory.Functor (CategoryTheory.WithTerminal C) (CategoryTheory.WithTerminal D)
-- Mathlib.Analysis.Convex.Function
StrictConcaveOn.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E}
  {f g : E → β}, StrictConcaveOn 𝕜 s f → Set.EqOn f g s → StrictConcaveOn 𝕜 s g
-- Std.Data.HashMap.Lemmas
Std.HashMap.emptyWithCapacity_equiv_iff_isEmpty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {c : ℕ}, (Std.HashMap.emptyWithCapacity c).Equiv m ↔ m.isEmpty = true
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.smul_hsum : ∀ {Γ : Type u_1} {Γ' : Type u_2} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ']
  [inst_2 : VAdd Γ Γ'] [inst_3 : IsOrderedCancelVAdd Γ Γ'] {R : Type u_7} {V : Type u_8} [inst_4 : Semiring R]
  [inst_5 : AddCommMonoid V] [inst_6 : Module R V] (s : HahnSeries.SummableFamily Γ R α)
  (t : HahnSeries.SummableFamily Γ' V β), (s.smul t).hsum = (HahnModule.of R).symm (s.hsum • (HahnModule.of R) t.hsum)
-- Plausible.Testable
Plausible.TestResult.gaveUp.injEq : ∀ {p : Prop} (a a_1 : ℕ), (Plausible.TestResult.gaveUp a = Plausible.TestResult.gaveUp a_1) = (a = a_1)
-- Mathlib.Algebra.Lie.UniversalEnveloping
UniversalEnvelopingAlgebra.ι_comp_lift : ∀ (R : Type u₁) {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {A : Type u₃}
  [inst_3 : Ring A] [inst_4 : Algebra R A] (f : L →ₗ⁅R⁆ A),
  ⇑((UniversalEnvelopingAlgebra.lift R) f) ∘ ⇑(UniversalEnvelopingAlgebra.ι R) = ⇑f
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.coyonedaEquiv_coyoneda_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.coyonedaEquiv (CategoryTheory.coyoneda.map f.op) = f
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} → {S : J.Cover X} → (Y : C) → (f : Y ⟶ X) → (↑S).arrows f → S.Arrow
-- Mathlib.Geometry.Euclidean.Sphere.Power
InnerProductGeometry.mul_norm_eq_abs_sub_sq_norm : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y z : V},
  (∃ k, x = k • y) → ‖z - y‖ = ‖z + y‖ → ‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2|
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι] {Z : C} (h : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage S hkf hcc fac).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)) h) =
    CategoryTheory.CategoryStruct.comp ι (CategoryTheory.CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).hom h)
-- Mathlib.Topology.Neighborhoods
interior_mem_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, interior s ∈ nhds x ↔ s ∈ nhds x
-- Mathlib.Algebra.Module.Equiv.Basic
addMonoidEndRingEquivInt_apply : ∀ (A : Type u_9) [inst : AddCommGroup A] (a : A →+ A),
  (addMonoidEndRingEquivInt A) a = (↑(addMonoidHomLequivInt ℤ)).toFun a
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.findM?_toList : ∀ {α β : Type} {m : Type → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α Id β] [inst_2 : Std.IteratorLoop α Id m]
  [LawfulMonad m] [Std.Iterators.Finite α Id] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {f : β → m Bool},
  List.findM? f it.toList = it.findM? fun x => ULift.up <$> f x
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.map_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  {T : Submonoid P} {Q : Type u_4} [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q] [inst_7 : IsLocalization T Q]
  (hy : M ≤ Submonoid.comap g T) (x : R), (IsLocalization.map Q g hy) ((algebraMap R S) x) = (algebraMap P Q) (g x)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coe_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (n : σ →₀ ℕ) (a : R),
  ↑((MvPolynomial.monomial n) a) = (MvPowerSeries.monomial n) a
-- Mathlib.Topology.Closure
closure_eq_self_union_frontier : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), closure s = s ∪ frontier s
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.GState.mk.inj : ∀ {propToFVar propToFVar_1 : Lean.ExprMap Lean.Expr},
  { propToFVar := propToFVar } = { propToFVar := propToFVar_1 } → propToFVar = propToFVar_1
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.order_weierstrassP : ∀ (L : PeriodPair), ∀ l₀ ∈ L.lattice, meromorphicOrderAt L.weierstrassP l₀ = -2
-- Init.Data.String.Slice
/-- Returns the first character in `s`. If `s` is empty, returns `none`.

Examples:

* `"abc".toSlice.front? = some 'a'`

* `"".toSlice.front? = none`
 -/
String.Slice.front? : String.Slice → Option Char
-- Init.System.IO
IO.AccessRight.mk.injEq : ∀ (read write execution read_1 write_1 execution_1 : Bool),
  ({ read := read, write := write, execution := execution } =
      { read := read_1, write := write_1, execution := execution_1 }) =
    (read = read_1 ∧ write = write_1 ∧ execution = execution_1)
-- Mathlib.FieldTheory.Fixed
cardinalMk_algHom : ∀ (K : Type u) (V : Type v) (W : Type w) [inst : Field K] [inst_1 : Ring V] [inst_2 : Algebra K V]
  [FiniteDimensional K V] [inst_4 : Field W] [inst_5 : Algebra K W],
  Cardinal.mk (V →ₐ[K] W) ≤ ↑(Module.finrank W (V →ₗ[K] W))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_eq_getD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α} {fallback : β a} {h : a ∈ t}, t.get a h = t.getD a fallback
-- Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
/-- If a function `f` locally integrable on an open subset `U` of a finite-dimensional real
manifold has zero integral when multiplied by any smooth function compactly supported
in `U`, then `f` vanishes almost everywhere in `U`.  -/
IsOpen.ae_eq_zero_of_integral_contMDiff_smul_eq_zero' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] {H : Type u_3}
  [inst_6 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [IsManifold I (↑⊤) M] [inst_10 : MeasurableSpace M] [BorelSpace M] [T2Space M] {f : M → F}
  {μ : MeasureTheory.Measure M} {U : Set M},
  IsOpen U →
    IsSigmaCompact U →
      MeasureTheory.LocallyIntegrableOn f U μ →
        (∀ (g : M → ℝ),
            ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) g →
              HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0) →
          ∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.sinh_lt_self_iff : ∀ {x : ℝ}, Real.sinh x < x ↔ x < 0
-- Mathlib.Topology.UniformSpace.Cauchy
cauchySeq_const : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : SemilatticeSup β] [Nonempty β] (x : α),
  CauchySeq fun x_1 => x
-- Mathlib.Algebra.Homology.HomologySequence
/-- The diagram `K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j` is exact
when `c.Rel i j`.  -/
HomologicalComplex.HomologySequence.composableArrows₃_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι),
  c.Rel i j →
    ∀ [inst_2 : CategoryTheory.CategoryWithHomology C],
      (HomologicalComplex.HomologySequence.composableArrows₃ K i j).Exact
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The set of vectors proportional to those in a convex set forms a convex cone.  -/
Convex.toCone : {𝕜 : Type u_1} →
  {M : Type u_4} →
    [inst : Field 𝕜] →
      [inst_1 : LinearOrder 𝕜] →
        [IsStrictOrderedRing 𝕜] →
          [inst_3 : AddCommGroup M] → [inst_4 : Module 𝕜 M] → (s : Set M) → Convex 𝕜 s → ConvexCone 𝕜 M
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- The sum of two vector measure is a vector measure.  -/
MeasureTheory.VectorMeasure.add : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommMonoid M] →
        [inst_1 : TopologicalSpace M] →
          [ContinuousAdd M] →
            MeasureTheory.VectorMeasure α M → MeasureTheory.VectorMeasure α M → MeasureTheory.VectorMeasure α M
-- Init.Internal.Order.Basic
Lean.Order.instCCPOPProd : {α : Sort u} → {β : Sort v} → [Lean.Order.CCPO α] → [Lean.Order.CCPO β] → Lean.Order.CCPO (α ×' β)
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
/-- The norm of `‖φ x ·‖` attains a minimum on `ℝ × ℝ`.  -/
_private.Mathlib.Analysis.Normed.Algebra.GelfandMazur.0.NormedAlgebra.Real.exists_isMinOn_norm_φ : ∀ {F : Type u_1} [inst : NormedRing F] [inst_1 : NormedAlgebra ℝ F] [NormOneClass F] (x : F),
  ∃ z, IsMinOn (fun x_1 => ‖NormedAlgebra.Real.φ✝ x x_1‖) Set.univ z
-- Mathlib.Algebra.Ring.Pi
RingHom.compLeft_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β] (f : α →+* β) (I : Type u_3)
  (h : I → α) (a : I), (f.compLeft I) h a = (⇑f ∘ h) a
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.comap_id : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] (s : ClosedSubmodule R M), ClosedSubmodule.comap (ContinuousLinearMap.id R M) s = s
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.instGroupoidFreeGroupoid : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Groupoid (CategoryTheory.FreeGroupoid C)
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.ncard_le_ncard_iff_ncard_sdiff_le_ncard_sdiff`. -/
Set.ncard_le_ncard_iff_ncard_diff_le_ncard_diff : ∀ {α : Type u_1} {s t : Set α},
  autoParam s.Finite Set.ncard_le_ncard_iff_ncard_sdiff_le_ncard_sdiff._auto_1 →
    autoParam t.Finite Set.ncard_le_ncard_iff_ncard_sdiff_le_ncard_sdiff._auto_3 →
      (s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard)
-- Batteries.Data.Fin.Lemmas
Fin.exists_iff_exists_maximal : ∀ {n : ℕ} (p : Fin n → Prop) [DecidablePred p], (∃ i, p i) ↔ ∃ i, p i ∧ ∀ (j : Fin n), i < j → ¬p j
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalizer_le_normalizer_closure : ∀ {G : Type u_1} [inst : Group G] (s : Set G), Subgroup.normalizer s ≤ Subgroup.normalizer ↑(Subgroup.closure s)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If a measurable space has a finite measure `μ` and a countable group `G` acts
quasi-measure-preservingly, then to show that a set `s` is a fundamental domain, it is sufficient
to check that its translates `g • s` are (almost) disjoint and that the sum `∑' g, μ (g • s)` is
sufficiently large.  -/
MeasureTheory.IsFundamentalDomain.mk_of_measure_univ_le : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [Countable G],
  MeasureTheory.NullMeasurableSet s μ →
    (∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s) →
      (∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g • x) μ μ) →
        μ Set.univ ≤ ∑' (g : G), μ (g • s) → MeasureTheory.IsFundamentalDomain G s μ
-- Mathlib.Data.Subtype
Subtype.map_involutive : ∀ {α : Sort u_1} {p : α → Prop} {f : α → α} (h : ∀ (a : α), p a → p (f a)),
  Function.Involutive f → Function.Involutive (Subtype.map f h)
-- Lean.Data.PersistentArray
Lean.PersistentArray.foldrM : {α : Type u} → {m : Type v → Type w} → {β : Type v} → [Monad m] → Lean.PersistentArray α → (α → β → m β) → β → m β
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.of_compl : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet sᶜ μ → MeasureTheory.NullMeasurableSet s μ
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.Context.toInductiveVal : Lean.Elab.ComputedFields.Context → Lean.InductiveVal
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- **Alias** of `ciSup_mono_of_forall_exists'`. -/
ciSup_mono' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {ι' : Sort u_5} {f : ι → α} {g : ι' → α},
  BddAbove (Set.range g) → (∀ (i : ι), ∃ i', f i ≤ g i') → ⨆ i, f i ≤ ⨆ i', g i'
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.cond_eq_zero_of_meas_eq_zero : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω}, μ s = 0 → μ[|s] = 0
-- Init.Data.Nat.Basic
Nat.lt_add_one_iff : ∀ {m n : ℕ}, m < n + 1 ↔ m ≤ n
-- Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Finset.zero_div_subset : ∀ {α : Type u_1} [inst : GroupWithZero α] [inst_1 : DecidableEq α] (s : Finset α), 0 / s ⊆ 0
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod.instNullSingletonClass_snd : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.NullSingletonClass ν], MeasureTheory.NullSingletonClass (μ.prod ν)
-- Mathlib.Topology.VectorBundle.Hom
/-- The continuous `σ`-semilinear maps between two vector bundles form a fiber bundle.  -/
Bundle.ContinuousLinearMap.fiberBundle : {𝕜₁ : Type u_1} →
  [inst : NontriviallyNormedField 𝕜₁] →
    {𝕜₂ : Type u_2} →
      [inst_1 : NontriviallyNormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          {B : Type u_3} →
            (F₁ : Type u_4) →
              [inst_2 : NormedAddCommGroup F₁] →
                [inst_3 : NormedSpace 𝕜₁ F₁] →
                  (E₁ : B → Type u_5) →
                    [inst_4 : (x : B) → AddCommGroup (E₁ x)] →
                      [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)] →
                        [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
                          (F₂ : Type u_6) →
                            [inst_7 : NormedAddCommGroup F₂] →
                              [inst_8 : NormedSpace 𝕜₂ F₂] →
                                (E₂ : B → Type u_7) →
                                  [inst_9 : (x : B) → AddCommGroup (E₂ x)] →
                                    [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] →
                                      [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                                        [inst_12 : TopologicalSpace B] →
                                          [inst_13 : (x : B) → TopologicalSpace (E₁ x)] →
                                            [inst_14 : FiberBundle F₁ E₁] →
                                              [inst_15 : VectorBundle 𝕜₁ F₁ E₁] →
                                                [inst_16 : (x : B) → TopologicalSpace (E₂ x)] →
                                                  [inst_17 : FiberBundle F₂ E₂] →
                                                    [inst_18 : VectorBundle 𝕜₂ F₂ E₂] →
                                                      [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] →
                                                        [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] →
                                                          [inst_21 : RingHomIsometric σ] →
                                                            FiberBundle (F₁ →SL[σ] F₂) fun x => E₁ x →SL[σ] E₂ x
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal_apply : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} (hv : v.IsReal) (x : v.Completion),
  (NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal hv) x =
    (NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hv) x
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanIdentifier.mk.injEq : ∀ (module decl : Lean.Name) (isExactMatch : Bool) (module_1 decl_1 : Lean.Name) (isExactMatch_1 : Bool),
  ({ module := module, decl := decl, isExactMatch := isExactMatch } =
      { module := module_1, decl := decl_1, isExactMatch := isExactMatch_1 }) =
    (module = module_1 ∧ decl = decl_1 ∧ isExactMatch = isExactMatch_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termL₂'_1 : Lean.ParserDescr