mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {l : List (α × β)} {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)).getKey! k' = k
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
CommRingCat.moduleCatExtendScalarsPseudofunctor_map : ∀ {X Y : CategoryTheory.LocallyDiscrete CommRingCat} (f : X ⟶ Y),
  CommRingCat.moduleCatExtendScalarsPseudofunctor.map f = (ModuleCat.extendScalars (CommRingCat.Hom.hom f.as)).toCatHom
-- Init.Data.Sum.Lemmas
Sum.getRight?_swap : ∀ {α : Type u_1} {β : Type u_2} (x : α ⊕ β), x.swap.getRight? = x.getLeft?
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolRing_inj : ∀ {α : Type u_1} {a b : AsBoolRing α}, ofBoolRing a = ofBoolRing b ↔ a = b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_modify_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF → ∀ {k : α} {f : β k → β k}, (m.modify k f).getKey? k = if m.contains k = true then some k else none
-- Mathlib.Algebra.Group.Defs
/-- Dividing by an element is the same as multiplying by its inverse.

This is a duplicate of `DivInvMonoid.div_eq_mul_inv` ensuring that the types unfold better.
 -/
div_eq_mul_inv : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
-- Std.Data.HashMap.Basic
Std.HashMap.instInhabited : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Inhabited (Std.HashMap α β)
-- Init.Data.Nat.Lemmas
Nat.exists_eq_add_one : ∀ {a : ℕ}, (∃ n, a = n + 1) ↔ 0 < a
-- Mathlib.Data.Nat.Find
Nat.findGreatest.eq_def : ∀ (P : ℕ → Prop) [inst : DecidablePred P] (x : ℕ),
  Nat.findGreatest P x =
    match x with
    | 0 => 0
    | n.succ => if P (n + 1) then n + 1 else Nat.findGreatest P n
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.LaxTrans.id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) (a : B),
  (CategoryTheory.CategoryStruct.id F).app a = CategoryTheory.CategoryStruct.id (F.obj a)
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.whiskerIdCancel_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (s : CategoryTheory.Bicategory.LeftLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g))
  {t : CategoryTheory.Bicategory.LeftLift f g} (τ : s ⟶ t.whisker (CategoryTheory.CategoryStruct.id c)),
  (s.whiskerIdCancel τ).right =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.Hom.right τ)
      (CategoryTheory.Bicategory.leftUnitor t.lift).hom
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.Monadic.isPlausibleIndirectOutput_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {it : Std.IterM Id α}
  {out : α},
  it.IsPlausibleIndirectOutput out ↔ ∃ n, (it.internalState.next.bind fun x => Std.PRange.succMany? n x) = some out
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.integral_strongDual_stdGaussian : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (L : StrongDual ℝ E), ∫ (x : E), L x ∂ProbabilityTheory.stdGaussian E = 0
-- Mathlib.CategoryTheory.Category.Cat.Limit
/-- Auxiliary definition: the cone over the limit category.  -/
CategoryTheory.Cat.HasLimits.limitCone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CategoryTheory.Cat) → CategoryTheory.Limits.Cone F
-- Mathlib.Algebra.Group.Basic
div_eq_self : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a / b = a ↔ b = 1
-- Std.Http.Data.Headers.Value
Std.Http.Header.instReprValue.repr : Std.Http.Header.Value → ℕ → Std.Format
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.mem_functorPushforward_iff_of_full : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Full] {X Y : C} (R : CategoryTheory.Sieve X) (f : F.obj Y ⟶ F.obj X),
  CategoryTheory.Presieve.functorPushforward F R.arrows f ↔ ∃ g, F.map g = f ∧ R.arrows g
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.coe_id : ∀ (α : Type u_2) [inst : Preorder α], ⇑(PseudoEpimorphism.id α) = id
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_comp_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (g : P →ₗ[R] Q)
  (f : N →ₗ[R] P) (x : TensorProduct R N M),
  (LinearMap.rTensor M (g ∘ₗ f)) x = (LinearMap.rTensor M g) ((LinearMap.rTensor M f) x)
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.nhdsSet_eq_principal_upperClosure : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpperSet α] (s : Set α),
  nhdsSet s = Filter.principal ↑(upperClosure s)
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Icc_succ : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∑ i ∈ Finset.Icc a.succ b.succ, f i = ∑ i ∈ Finset.Icc a b, f i.succ
-- Init.Data.UInt.Lemmas
UInt64.toUInt64_toUInt8 : ∀ (n : UInt64), n.toUInt8.toUInt64 = n % 256
-- Init.Data.Option.Lemmas
Option.guard_apply : ∀ {α : Type u_1} {p : α → Bool} {x : α}, Option.guard p x = if p x = true then some x else none
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f + g) x = f x + g x` has right
addition if `β` has cancellative addition.  -/
FunLike.isCancelAdd : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β] [IsCancelAdd β]
  [IsAddApply F α β], IsCancelAdd F
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_toUInt64 : ∀ (n : USize) (h : System.Platform.numBits = 64), n.toUInt64.toBitVec = BitVec.setWidth 64 (n.toBitVec64 h)
-- Mathlib.Topology.Neighborhoods
tendsto_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {f : α → X} {l : Filter α},
  Filter.Tendsto f l (nhds x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f ⁻¹' s ∈ l
-- Mathlib.Algebra.Ring.SumsOfSquares
Subsemiring.closure_isSquare : ∀ {T : Type u_2} [inst : CommSemiring T], Subsemiring.closure {x | IsSquare x} = Subsemiring.sumSq T
-- Mathlib.LinearAlgebra.Charpoly.Basic
LinearMap.charpoly_monic : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M), f.charpoly.Monic
-- Mathlib.Tactic.NormNum.Core
/-- Run each registered `norm_num` extension on a typed expression `p : Prop`,
and returning the truth or falsity of `p' : Prop` from an equivalence `p ↔ p'`.  -/
Mathlib.Meta.NormNum.deriveBoolOfIff : (p p' : Q(Prop)) → Q(«$p» ↔ «$p'») → Lean.MetaM ((b : Bool) × Mathlib.Meta.NormNum.BoolResult p' b)
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzWith.sub : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E}, LipschitzWith Kf f → LipschitzWith Kg g → LipschitzWith (Kf + Kg) fun x => f x - g x
-- Lean.Meta.Tactic.Simp.Diagnostics
Lean.Meta.Simp.reportDiag : Lean.Meta.Simp.Diagnostics → Lean.MetaM Unit
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.instEquivLike : {M : Type u_1} →
  {N : Type u_2} →
    [inst : TopologicalSpace M] →
      [inst_1 : TopologicalSpace N] → [inst_2 : Add M] → [inst_3 : Add N] → EquivLike (M ≃ₜ+ N) M N
-- Mathlib.Order.Heyting.Basic
sdiff_bot : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a : α}, a \ ⊥ = a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.differentiable_iteratedDeriv_cos : ∀ (n : ℕ), Differentiable ℝ (iteratedDeriv n Real.cos)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_neg : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.Chebyshev.S R (-n) = -Polynomial.Chebyshev.S R (n - 2)
-- Init.Grind.Norm
Lean.Grind.not_exists : ∀ {α : Sort u_1} (p : α → Prop), (¬∃ x, p x) = ∀ (x : α), ¬p x
-- Mathlib.Analysis.Normed.Group.Continuity
NormedCommGroup.toENormedCommMonoid : {E : Type u_4} → [inst : NormedCommGroup E] → ENormedCommMonoid E
-- Std.Time.Time.Unit.Basic
/-- Converts an `Hour.Offset` to a `Nanosecond.Offset`.
 -/
Std.Time.Hour.Offset.toNanoseconds : Std.Time.Hour.Offset → Std.Time.Nanosecond.Offset
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_univ_eq : ∀ {α : Type u_1} (M : Matroid α), M.eRk Set.univ = M.eRank
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The Ore localization of a monoid and a submonoid fulfilling the Ore condition.  -/
OreLocalization.«term__[_⁻¹_]» : Lean.TrailingParserDescr
-- Mathlib.Order.Filter.CardinalInter
Filter.CardinalGenerateSets.brecOn : ∀ {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {motive : (a : Set α) → Filter.CardinalGenerateSets g a → Prop}
  {a : Set α} (t : Filter.CardinalGenerateSets g a),
  (∀ (a : Set α) (t : Filter.CardinalGenerateSets g a), Filter.CardinalGenerateSets.below t → motive a t) → motive a t
-- Lean.Util.ForEachExprWhere
Lean.ForEachExprWhere.checked : {ω : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] → [MonadLiftT (ST ω) m] → [Monad m] → Lean.Expr → Lean.ForEachExprWhere.ForEachM m Bool
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.SplitIterator.toList_eq_splitFromSteps : ∀ {ρ : Type} {pat : ρ} {σ : String.Slice → Type} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  [inst_1 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id] {s : String.Slice}
  (it : Std.Iter (String.Slice.Pattern.SearchStep s)) (currPos : s.Pos),
  { internalState := String.Slice.SplitIterator.operating currPos it }.toList =
    String.Slice.Pattern.Model.splitFromSteps✝ currPos it.toList
-- Mathlib.RingTheory.FiniteType
Algebra.FiniteType.quotient : ∀ (R : Type u_1) {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (I : Ideal S)
  [h : Algebra.FiniteType R S], Algebra.FiniteType R (S ⧸ I)
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.lintegral_of_real_lt_top : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] (μ : MeasureTheory.Measure X)
  [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X ℝ), ∫⁻ (x : X), ENNReal.ofReal (f x) ∂μ < ⊤
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.Hopf.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] [inst_3 : SizeOf C] (X : C) [hopf : CategoryTheory.HopfObj X],
  sizeOf { X := X, hopf := hopf } = 1 + sizeOf X + sizeOf hopf
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The maximality axiom in 'arrow' form: Any arrow `f` in `S` is covered by `S`.  -/
CategoryTheory.GrothendieckTopology.arrow_max : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C)
  (f : Y ⟶ X) (S : CategoryTheory.Sieve X), S.arrows f → J.Covers S f
-- Mathlib.Analysis.Calculus.ContDiff.Convolution
HasCompactSupport.hasFDerivAt_convolution_left : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'} [inst_3 : RCLike 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F]
  [inst_8 : MeasurableSpace G] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [inst_9 : NormedAddCommGroup G]
  [BorelSpace G] [inst_11 : NormedSpace 𝕜 G] [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant],
  HasCompactSupport f →
    ContDiff 𝕜 1 f →
      MeasureTheory.LocallyIntegrable g μ →
        ∀ (x₀ : G),
          HasFDerivAt (MeasureTheory.convolution f g L μ)
            (MeasureTheory.convolution (fderiv 𝕜 f) g (ContinuousLinearMap.precompL G L) μ x₀) x₀
-- Mathlib.Data.Sym.Sym2
Sym2.ext : ∀ {α : Type u_1} {p q : Sym2 α}, (∀ (x : α), x ∈ p ↔ x ∈ q) → p = q
-- Init.Data.Vector.InsertIdx
Vector.getElem_insertIdx_self : ∀ {α : Type u} {n : ℕ} {xs : Vector α n} {x : α} {i : ℕ} (w : i ≤ n), (xs.insertIdx i x w)[i] = x
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WOppSide.not_sSameSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.WOppSide x y → ¬s.SSameSide x y
-- Mathlib.Topology.EMetricSpace.PairReduction
/-- Given the pair set sequence Kᵢ we define the pair set `K` by `K = ⋃ i, Kᵢ`.  -/
PairReduction.pairSet : {T : Type u_1} → [PseudoEMetricSpace T] → [DecidableEq T] → Finset T → ENNReal → ENNReal → Finset (T × T)
-- Mathlib.Algebra.Group.Equiv.Basic
/-- If `α` has a unique term, then the product of magmas `α → M` is isomorphic to `M`.  -/
AddEquiv.funUnique : (α : Type u_2) → (M : Type u_4) → [inst : Add M] → [Unique α] → (α → M) ≃+ M
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.essSup_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : ConditionallyCompleteLinearOrder γ] [inst_4 : TopologicalSpace γ] [OpensMeasurableSpace γ]
  [OrderClosedTopology γ], ProbabilityTheory.IdentDistrib f g μ ν → essSup f μ = essSup g ν
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.fun_mem : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (self : L.Substructure M) {n : ℕ} (f : L.Functions n),
  FirstOrder.Language.ClosedUnder f ↑self
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
/-- Given `F : C ⥤ V`, this is the functor
`G ↦ c c₁ c₂ ↦ ihom (F c₁) (G.obj (c₂ ⊗ c))`.
The internal hom functor for Day convolution `[F, -]` is naturally isomorphic
to the functor `G ↦ c ↦ end_ (c₁ c₂ ↦ ihom (F c₁) (G.obj (c₂ ⊗ c)))`, hence
this definition.  -/
CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            [CategoryTheory.MonoidalClosed V] →
              CategoryTheory.Functor C V →
                CategoryTheory.Functor (CategoryTheory.Functor C V)
                  (CategoryTheory.Functor C (CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C V)))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α}, k ∉ m₂ → (m₁ \ m₂).get? k = m₁.get? k
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- This is [grinberg_clifford_2016] Theorem 7  -/
CliffordAlgebra.contractLeft_contractLeft : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (d : Module.Dual R M) (x : CliffordAlgebra Q),
  (CliffordAlgebra.contractLeft d) ((CliffordAlgebra.contractLeft d) x) = 0
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- For `1 ≤ r`, the characteristic function of `f + g` at `⊤` is less than or equal to the sum of the
characteristic functions of `f` and `g`, respectively, plus `log 2` (where `2` is the number of
summands).
 -/
ValueDistribution.characteristic_add_top_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f₁ f₂ : ℂ → E} {r : ℝ},
  Meromorphic f₁ →
    Meromorphic f₂ →
      1 ≤ r →
        ValueDistribution.characteristic (f₁ + f₂) ⊤ r ≤
          ValueDistribution.characteristic f₁ ⊤ r + ValueDistribution.characteristic f₂ ⊤ r + Real.log 2
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_inf : ∀ {G : Type u_1} [inst : Group G] {p p' : Subgroup G} {x : G}, x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
-- Mathlib.Topology.Algebra.Group.Basic
toAddUnits_homeomorph.eq_1 : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : ContinuousNeg G],
  toAddUnits_homeomorph = { toEquiv := toAddUnits.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.coe_toOuterMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α), ⇑μ.toOuterMeasure = ⇑μ
-- Mathlib.Topology.Maps.Proper.Basic
/-- A homeomorphism is proper.  -/
Homeomorph.isProperMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y), IsProperMap ⇑e
-- Init.Data.Array.Lemmas
Array.toList_shrink : ∀ {α : Type u_1} {xs : Array α} {i : ℕ}, (xs.shrink i).toList = List.take i xs.toList
-- Aesop.Forward.Substitution
Aesop.Substitution.mk.sizeOf_spec : ∀ (premises : Array (Option Lean.Expr)) (levels : Array (Option Lean.Level)),
  sizeOf { premises := premises, levels := levels } = 1 + sizeOf premises + sizeOf levels
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- Any pushforward of the identity morphism is naturally isomorphic to the identity functor.  -/
CategoryTheory.ExponentiableMorphism.pushforwardId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : C) →
      [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id I)] →
        [inst_2 : CategoryTheory.ExponentiableMorphism (CategoryTheory.CategoryStruct.id I)] →
          CategoryTheory.ExponentiableMorphism.pushforward (CategoryTheory.CategoryStruct.id I) ≅
            CategoryTheory.Functor.id (CategoryTheory.Over I)
-- Std.Time.Format.Modifier
Std.Time.Modifier.v.inj : ∀ {presentation presentation_1 : Std.Time.ZoneName},
  Std.Time.Modifier.v presentation = Std.Time.Modifier.v presentation_1 → presentation = presentation_1
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasSum.prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {L : SummationFilter β} [inst : AddCommMonoid α]
  [inst_1 : TopologicalSpace α] [inst_2 : AddCommMonoid γ] [inst_3 : TopologicalSpace γ] {f : β → α} {g : β → γ} {a : α}
  {b : γ}, HasSum f a L → HasSum g b L → HasSum (fun x => (f x, g x)) (a, b) L
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)}, (Std.DHashMap.Const.insertMany m l).isEmpty = (m.isEmpty && l.isEmpty)
-- Mathlib.Data.List.Iterate
_private.Mathlib.Data.List.Iterate.0.Nat.iterate.match_1.eq_1 : ∀ {α : Sort u_2} (motive : ℕ → α → Sort u_1) (a : α) (h_1 : (a : α) → motive 0 a)
  (h_2 : (k : ℕ) → (a : α) → motive k.succ a),
  (match 0, a with
    | 0, a => h_1 a
    | k.succ, a => h_2 k a) =
    h_1 a
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.openCover_I₀ : ∀ (D : AlgebraicGeometry.Scheme.GlueData), D.openCover.I₀ = D.J
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.instFullKaroubiFunctorKaroubiFunctorCategoryEmbedding : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C], (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C).Full
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_psigma_congrRight_prop : ∀ {ι : Prop} {f g : ι → Type v},
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g i)) → Cardinal.mk ((i : ι) ×' f i) = Cardinal.mk ((i : ι) ×' g i)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.epi_f' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → ∀ (h : S.LeftHomologyData), CategoryTheory.Epi h.f'
-- Mathlib.Topology.MetricSpace.Equicontinuity
/-- Characterization of equicontinuity for families of functions between (pseudo) metric spaces.  -/
Metric.equicontinuousAt_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : PseudoMetricSpace β]
  {F : ι → β → α} {x₀ : β},
  EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x : β), dist x x₀ < δ → ∀ (i : ι), dist (F i x₀) (F i x) < ε
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_eq_sum_mul_log_prime : ∀ (n : ℕ), Chebyshev.psi ↑n = ∑ p ∈ n.primesLE, ↑(Nat.log p n) * Real.log ↑p
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_neg : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), (-a).imJ = -a.imJ
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.preimage_id : ∀ {X : SSet} (A : X.Subcomplex), A.preimage (CategoryTheory.CategoryStruct.id X) = A
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.instOrderTopCarrierCarrierCommRingCatOfIsIntegral : (X : AlgebraicGeometry.Scheme) → [AlgebraicGeometry.IsIntegral X] → OrderTop ↥X
-- Batteries.Tactic.ShowUnused
_private.Batteries.Tactic.ShowUnused.0.Batteries.Tactic.ShowUnused.visit.visitExpr : Lean.Environment → Lean.Expr → StateM Lean.NameSet Unit
-- Mathlib.Algebra.Star.Subalgebra
/-- Restriction of the codomain of a `StarAlgHom` to a star subalgebra containing the range.  -/
StarAlgHom.codRestrict : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R A] →
              [inst_4 : StarRing A] →
                [inst_5 : Semiring B] →
                  [inst_6 : Algebra R B] →
                    [inst_7 : StarRing B] →
                      [inst_8 : StarModule R B] →
                        (f : A →⋆ₐ[R] B) → (S : StarSubalgebra R B) → (∀ (x : A), f x ∈ S) → A →⋆ₐ[R] ↥S
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- If the directions of two nonempty affine subspaces span the whole module, they have nonempty
intersection.  -/
AffineSubspace.inter_nonempty_of_nonempty_of_sup_direction_eq_top : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s₁ s₂ : AffineSubspace k P},
  (↑s₁).Nonempty → (↑s₂).Nonempty → s₁.direction ⊔ s₂.direction = ⊤ → (↑s₁ ∩ ↑s₂).Nonempty
-- Mathlib.CategoryTheory.Abelian.Images
CategoryTheory.Abelian.coimageImageComparison'.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C}
  (f : P ⟶ Q) [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasKernel f]
  [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_5 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)],
  CategoryTheory.Abelian.coimageImageComparison' f =
    CategoryTheory.Limits.kernel.lift (CategoryTheory.Limits.cokernel.π f)
      (CategoryTheory.Limits.cokernel.desc (CategoryTheory.Limits.kernel.ι f) f ⋯) ⋯
-- Mathlib.RingTheory.SimpleRing.Basic
DivisionRing.isSimpleRing : ∀ (A : Type u_2) [inst : DivisionRing A], IsSimpleRing A
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.zsmul_right : ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → ∀ (m : ℤ), AddCommute a (m • b)