mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g)
          (CategoryTheory.Limits.pullback.fst f g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g g) h)
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.symplComp_inf : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] [CompleteSpace H]
  (S T : ClosedSubmodule ℝ H), (S ⊓ T).symplComp = S.symplComp ⊔ T.symplComp
-- Aesop.Nanos
Aesop.instInhabitedNanos : Inhabited Aesop.Nanos
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. A measurable function is smaller than its mean on a set of positive
measure.  -/
MeasureTheory.measure_le_setLAverage_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
  μ s ≠ 0 → μ s ≠ ⊤ → AEMeasurable f (μ.restrict s) → 0 < μ {x | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ}
-- Mathlib.Algebra.Polynomial.Div
Polynomial.sub_modByMonic : ∀ {R : Type u} [inst : CommRing R] (p₁ p₂ q : Polynomial R), (p₁ - p₂) %ₘ q = p₁ %ₘ q - p₂ %ₘ q
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNormal.eq_6 : ∀ (x : Turing.PartrecToTM2.Cont') (f g : Turing.ToPartrec.Code),
  Turing.PartrecToTM2.trNormal (f.case g) x = (Turing.PartrecToTM2.trNormal f x).pred (Turing.PartrecToTM2.trNormal g x)
-- Mathlib.Algebra.Order.Archimedean.Hom
OrderRingIso.apply_eq_self : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] (f : α ≃+*o α)
  (x : α), f x = x
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Stream.next?.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Stream α → Sort u_2) (h_1 : Unit → motive RBTree.RBNode.Stream.nil)
  (h_2 :
    (v : α) → (r : RBTree.RBNode α) → (tail : RBTree.RBNode.Stream α) → motive (RBTree.RBNode.Stream.cons v r tail)),
  (match RBTree.RBNode.Stream.nil with
    | RBTree.RBNode.Stream.nil => h_1 ()
    | RBTree.RBNode.Stream.cons v r tail => h_2 v r tail) =
    h_1 ()
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
/-- The alternating face map complex, on objects  -/
AlgebraicTopology.AlternatingFaceMapComplex.obj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CategoryTheory.SimplicialObject C → ChainComplex C ℕ
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- Reinterpret `G ≃+ Additive H` as `Multiplicative G ≃* H`.  -/
AddEquiv.toMultiplicativeLeft : {G : Type u_2} →
  {H : Type u_3} → [inst : AddZeroClass G] → [inst_1 : MulOneClass H] → G ≃+ Additive H ≃ (Multiplicative G ≃* H)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.darts_map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v),
  (SimpleGraph.Walk.map f p).darts = List.map f.mapDart p.darts
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.acyclic_truncGE_iff_isSupportedOutside : ∀ {ι : 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]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C], (K.truncGE e).Acyclic ↔ K.IsSupportedOutside e
-- Mathlib.Dynamics.Newton
Polynomial.newtonMap_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Polynomial R)
  {x : S}, P.newtonMap x = x - Ring.inverse ((Polynomial.aeval x) (Polynomial.derivative P)) * (Polynomial.aeval x) P
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.piTensorHomMapFun₂_smul : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} {t' : ι → Type u_12} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] [inst_5 : (i : ι) → AddCommMonoid (t' i)] [inst_6 : (i : ι) → Module R (t' i)]
  (r : R) (φ : PiTensorProduct R fun i => s i →ₗ[R] t i →ₗ[R] t' i),
  (r • φ).piTensorHomMapFun₂ = r • φ.piTensorHomMapFun₂
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_or : ∀ (a b : USize) (h : System.Platform.numBits = 32), (a ||| b).toBitVec32 h = a.toBitVec32 h ||| b.toBitVec32 h
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.cm5a : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.trivialCofibrations C).HasFactorization (HomotopicalAlgebra.fibrations C)
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.stepRet.match_1.splitter : (motive : Turing.ToPartrec.Cont → List ℕ → Sort u_1) →
  (x : Turing.ToPartrec.Cont) →
    (x_1 : List ℕ) →
      ((v : List ℕ) → motive Turing.ToPartrec.Cont.halt v) →
        ((fs : Turing.ToPartrec.Code) →
            (as : List ℕ) →
              (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.cons₁ fs as k) v) →
          ((ns : List ℕ) → (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.cons₂ ns k) v) →
            ((f : Turing.ToPartrec.Code) →
                (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.comp f k) v) →
              ((f : Turing.ToPartrec.Code) →
                  (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.fix f k) v) →
                motive x x_1
-- Std.Http.Data.URI.Encoding
/-- Attempts to create an encoded userinfo component from raw bytes.
 -/
Std.Http.URI.EncodedUserInfo.ofByteArray? : ByteArray → Option Std.Http.URI.EncodedUserInfo
-- Mathlib.Order.GaloisConnection.Defs
/-- Make a `GaloisCoinsertion` between `αᵒᵈ` and `βᵒᵈ` from a `GaloisInsertion` between
`α` and `β`.  -/
GaloisConnection.toGaloisCoinsertion : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {u : α → β} → {l : β → α} → GaloisConnection l u → (∀ (b : β), u (l b) ≤ b) → GaloisCoinsertion l u
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.fromBlocks₂₂ : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : CommRing α] [inst_1 : StarRing α] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (A : Matrix m m α) (B : Matrix m n α) {D : Matrix n n α},
  D.IsHermitian → ((Matrix.fromBlocks A B B.conjTranspose D).IsHermitian ↔ (A - B * D⁻¹ * B.conjTranspose).IsHermitian)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom_mapPreimage_assoc : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X₀ W₀ : C₀}
  (a : F.obj W₀ ⟶ F.obj X₀) {i : (data (F.obj X₀)).I₀} (p : F.obj W₀ ⟶ F.obj ((data (F.obj X₀)).X i)),
  CategoryTheory.CategoryStruct.comp p ((data (F.obj X₀)).f i) = a →
    ∀ {Z : A} (h : G₀.obj.obj (Opposite.op W₀) ⟶ Z),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom data G₀ X₀)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ a) h) =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ (F.obj X₀) i)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ p) h)
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Infix notation for `OrderMonoidIso`.  -/
«term_≃*o_» : Lean.TrailingParserDescr
-- Mathlib.Data.Sum.Basic
not_isLeft_and_isRight : ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, ¬(x.isLeft = true ∧ x.isRight = true)
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.comap_comp_apply : ∀ {R : Type u} {S : Type v} {S' : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : CommSemiring S']
  (f : R →+* S) (g : S →+* S') (x : PrimeSpectrum S'),
  PrimeSpectrum.comap (g.comp f) x = PrimeSpectrum.comap f (PrimeSpectrum.comap g x)
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_subset_div_right : ∀ {G : Type u_1} [inst : Group G] {a : G} {s : Set G}, a ∈ s → ↑(MulAction.stabilizer G s) ⊆ s / {a}
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the angle between two vectors is `π / 2`, the vectors are not equal.  -/
Orientation.ne_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → x ≠ y
-- Mathlib.RingTheory.Ideal.Nonunits
mul_mem_nonunits_left : ∀ {α : Type u_2} {a b : α} [inst : CommMonoid α], a ∈ nonunits α → a * b ∈ nonunits α
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.tensorObj_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Mon C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
matPolyEquiv_eq_X_pow_sub_C : ∀ {n : Type v} [inst : DecidableEq n] [inst_1 : Fintype n] {K : Type u_1} (k : ℕ) [inst_2 : CommRing K]
  (M : Matrix n n K),
  matPolyEquiv ((↑(Polynomial.expand K k)).mapMatrix (M ^ k).charmatrix) = Polynomial.X ^ k - Polynomial.C (M ^ k)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.neg_atom : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W → ∀ (a b : ℤ), -IsEllipticNet.atom W a b = IsEllipticNet.atom W b a
-- Init.Data.BitVec.Lemmas
BitVec.getElem_ofBool_zero : ∀ {b : Bool}, (BitVec.ofBool b)[0] = b
-- Mathlib.Data.DFinsupp.Order
DFinsupp.lt_def : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Preorder (α i)]
  {f g : Π₀ (i : ι), α i}, f < g ↔ f ≤ g ∧ ∃ i, f i < g i
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_zero_iff_subsingleton_of_finite : ∀ {α : Type u_1} [inst : MetricSpace α] {s : Set α} [Finite ↑s], s.infsep = 0 ↔ s.Subsingleton
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.emod.match_1.eq_2 : ∀ (motive : ℤ → ℤ → Sort u_1) (m : ℕ) (n : ℤ) (h_1 : (m : ℕ) → (n : ℤ) → motive (Int.ofNat m) n)
  (h_2 : (m : ℕ) → (n : ℤ) → motive (Int.negSucc m) n),
  (match Int.negSucc m, n with
    | Int.ofNat m, n => h_1 m n
    | Int.negSucc m, n => h_2 m n) =
    h_2 m n
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.mem_vonNeumann : ∀ {o : Ordinal.{u}} {x : ZFSet.{u}}, x ∈ ZFSet.vonNeumann o ↔ x.rank < o
-- Mathlib.Order.CompleteLatticeIntervals
Set.Icc.coe_sSup : ∀ {α : Type u_2} [inst : ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) {S : Set ↑(Set.Icc a b)},
  S.Nonempty →
    have this := ⋯;
    ↑(sSup S) = sSup (Subtype.val '' S)
-- Mathlib.SetTheory.ZFC.Basic
/-- The intersection operator, the collection of elements in all of the elements of a ZFC set. We
define `⋂₀ ∅ = ∅`. Uses `⋂₀` notation, scoped under the `ZFSet` namespace.  -/
ZFSet.sInter : ZFSet.{u_1} → ZFSet.{u_1}
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- An additive product monoid algebra is a nested additive monoid algebra.  -/
AddMonoidAlgebra.curryAddEquiv : {R : Type u_1} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : AddMonoid M] →
          [inst_2 : AddMonoid N] → AddMonoidAlgebra R (M × N) ≃+ AddMonoidAlgebra (AddMonoidAlgebra R N) M
-- Mathlib.Topology.Algebra.Module.LocallyConvex
LocallyConvexSpace.ofBasisZero : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] {ι : Type u_3} (b : ι → Set E)
  (p : ι → Prop), (nhds 0).HasBasis p b → (∀ (i : ι), p i → Convex 𝕜 (b i)) → LocallyConvexSpace 𝕜 E
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraQuaternion.Q_apply : ∀ {R : Type u_1} [inst : CommRing R] (c₁ c₂ : R) (v : R × R),
  (CliffordAlgebraQuaternion.Q c₁ c₂) v = c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ι_eq_zero_iff : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : M),
  (ExteriorAlgebra.ι R) x = 0 ↔ x = 0
-- Mathlib.Logic.Equiv.Set
Equiv.subtypeEquiv.congr_simp : ∀ {α : Sort u_1} {β : Sort u_4} {p : α → Prop} {q : β → Prop} (e e_1 : α ≃ β) (e_e : e = e_1)
  (h : ∀ (a : α), p a ↔ q (e a)), e.subtypeEquiv h = e_1.subtypeEquiv ⋯
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  (k : α), m₁.Equiv m₂ → (m₁.erase k).Equiv (m₂.erase k)
-- Init.Data.Ord.SInt
Int8.instOrd : Ord Int8
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup'_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : SemilatticeSup β] (f : α → β), Finset.sup' 0 ⋯ f = f 0
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_pt_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor C (Type w)} {I : Type u₁}
  [inst_1 : CategoryTheory.Category.{v₁, u₁} I] [inst_2 : Small.{w, u₁} I] (F : CategoryTheory.Functor I A.Elements)
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I C] [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape I A],
  (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F).pt.snd =
    CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement F
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.add_lt_add : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommMonoid M] [Lean.Grind.OrderedAdd M]
  [inst_4 : LT M] [Std.LawfulOrderLT M] {a b c d : M}, a < b → c < d → a + c < b + d
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.containsThenInsert_fst : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {k : α} {v : β k},
  (m.containsThenInsert k v).1 = m.contains k
-- Init.Data.Int.Linear
Int.Internal.Linear.not_eq_norm_expr : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.norm_eq_cert lhs rhs p = true →
    ¬Int.Internal.Linear.Expr.denote ctx lhs = Int.Internal.Linear.Expr.denote ctx rhs →
      ¬Int.Internal.Linear.Poly.denote' ctx p = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.forIn_eq_forIn_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ},
  forIn t init f = forIn t.toArray init f
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasSum_subtype_support : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α},
  HasSum (f ∘ Subtype.val) a ↔ HasSum f a
-- Mathlib.Data.ENNReal.Inv
/-- Very general version for distributivity of division over an infimum.

See `ENNReal.iInf_div_of_ne` for the special case assuming `a ≠ 0` and `a ≠ ∞`, and
`ENNReal.iInf_div` for the special case assuming `Nonempty ι`.  -/
ENNReal.iInf_div' : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal},
  (a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0) → (a = ⊤ → Nonempty ι) → (⨅ i, f i) / a = ⨅ i, f i / a
-- Mathlib.Topology.Constructible
Topology.IsConstructible.himp : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X},
  Topology.IsConstructible s → Topology.IsConstructible t → Topology.IsConstructible (s ⇨ t)
-- Mathlib.Topology.MetricSpace.Bilipschitz
/-- If `f : α → β` is bilipschitz, then the pullback of the uniformity on `β` through `f` agrees
with the uniformity on `α`.

This can be used to provide the replacement equality when applying
`PseudoMetricSpace.replaceUniformity`, which can be useful when following the forgetful inheritance
pattern when creating type synonyms.

Important Note: if `α` is some synonym of a type `β` (at default transparency), and `f : α ≃ β` is
some bilipschitz equivalence, then instead of writing:
```
instance : UniformSpace α := inferInstanceAs (UniformSpace β)
```
Users should instead write something like:
```
instance : UniformSpace α := (inferInstance : UniformSpace β).comap f
```
in order to avoid abuse of the definitional equality `α := β`.  -/
uniformity_eq_of_bilipschitz : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K₁ K₂ : NNReal}
  {f : α → β}, AntilipschitzWith K₁ f → LipschitzWith K₂ f → uniformity α = uniformity α
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_zero : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂], ⇑0 = 0
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_eq_sInf : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.edist u v = sInf (Set.range fun w => ↑w.length)
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinearMapRight'_mul : ∀ {R : Type u_1} [inst : Semiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [inst_1 : Fintype m]
  [inst_2 : DecidableEq m] [inst_3 : Fintype l] [inst_4 : DecidableEq l] (M : Matrix l m R) (N : Matrix m n R),
  Matrix.toLinearMapRight' (M * N) = Matrix.toLinearMapRight' N ∘ₗ Matrix.toLinearMapRight' M
-- Mathlib.Order.Bounds.Image
/-- The image under an antitone function of a set which is bounded above is bounded below.  -/
Antitone.map_bddAbove : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → ∀ {s : Set α}, BddAbove s → BddBelow (f '' s)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLE?.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.Const.getEntryLE? k = Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go k none
-- Mathlib.Data.EReal.Operations
EReal.mul_nonpos_iff : ∀ {a b : EReal}, a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
-- Init.Data.SInt.Lemmas
ISize.ne_iff_toBitVec_ne : ∀ {a b : ISize}, a ≠ b ↔ a.toBitVec ≠ b.toBitVec
-- Mathlib.Data.List.Lattice
List.inter_reverse : ∀ {α : Type u_1} [inst : DecidableEq α] {xs ys : List α}, xs ∩ ys.reverse = xs ∩ ys
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The kernel morphism of a zero morphism is an isomorphism  -/
CategoryTheory.Limits.kernel.ι_of_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f],
  f = 0 → CategoryTheory.IsIso (CategoryTheory.Limits.kernel.ι f)
-- Mathlib.Data.Finset.Image
/-- If the only elements outside `s` are those left fixed by `σ`, then mapping by `σ` has no effect.
 -/
Finset.map_perm : ∀ {α : Type u_1} {s : Finset α} {σ : Equiv.Perm α}, {a | σ a ≠ a} ⊆ ↑s → Finset.map (Equiv.toEmbedding σ) s = s
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_eq_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {a : SkewMonoidAlgebra k G}, a.coeff = 0 ↔ a = 0
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tsum_pnat_eq_tsum_succ : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {f : ℕ → M},
  ∑' (n : ℕ+), f ↑n = ∑' (n : ℕ), f (n + 1)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The oriented angle on an oriented real inner product space of dimension 2 can be evaluated in
terms of a complex-number representation of the space.  -/
Orientation.oangle_map_complex : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (f : V ≃ₗᵢ[ℝ] ℂ),
  (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation →
    ∀ (x y : V), o.oangle x y = ↑((starRingEnd ℂ) (f x) * f y).arg
-- Init.Data.Rat.Lemmas
Rat.num_add : ∀ (a b : ℚ),
  (a + b).num = (a.num * ↑b.den + b.num * ↑a.den) / ↑((a.num * ↑b.den + b.num * ↑a.den).natAbs.gcd (a.den * b.den))
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_max : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (max a b).toReal = max a.toReal b.toReal
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.roots_normalize : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : NormalizationMonoid R] {p : Polynomial R},
  (normalize p).roots = p.roots
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.add.eq_1 : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] (x : W.Point),
  WeierstrassCurve.Affine.Point.zero.add x = x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β} {h : k ∈ m.alter k f},
  (m.alter k f)[k] = (f m[k]?).get ⋯
-- Mathlib.RingTheory.Smooth.Kaehler
Algebra.Extension.toInfinitesimal.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S),
  P.toInfinitesimal =
    { toRingHom := Ideal.Quotient.mk (P.ker ^ 2), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
-- Init.Prelude
/-- Re-interprets an `Except ε` action in an exception monad `m`, succeeding if it succeeds and throwing
an exception if it throws an exception.
 -/
MonadExcept.ofExcept : {m : Type u_1 → Type u_2} → {ε : Type u_3} → {α : Type u_1} → [Monad m] → [MonadExcept ε m] → Except ε α → m α
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.ext : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {x y : AdicCompletion I M}, (∀ (n : ℕ), ↑x n = ↑y n) → x = y
-- Mathlib.SetTheory.ZFC.Cardinal
ZFSet.iSup_card_le_card_iUnion : ∀ {α : Type u} [inst : Small.{v, u} α] {f : α → ZFSet.{v}}, ⨆ i, (f i).card ≤ (ZFSet.iUnion fun i => f i).card
-- Init.Data.String.Iterate
String.Slice.RevByteIterator.instIteratorLoopUInt8OfMonad : {m : Type → Type u_1} →
  {n : Type u_2 → Type u_3} → [inst : Monad m] → [Monad n] → Std.IteratorLoop String.Slice.RevByteIterator m n
-- Lean.Server.Requests
Lean.Server.RequestM.mapTaskCheap : {α : Type u_1} →
  {β : Type} →
    Lean.Server.ServerTask α → (α → Lean.Server.RequestM β) → Lean.Server.RequestM (Lean.Server.RequestTask β)
-- Mathlib.MeasureTheory.Measure.PreVariation
/-- If `s` is measurable then `preVariationFun f s` is the supremum over partitions `P` of `s` of
the quantity `∑ p ∈ P.parts, f p`. If `s` is not measurable then it is set to `0`.  -/
MeasureTheory.preVariationFun : {X : Type u_1} → [MeasurableSpace X] → (Set X → ENNReal) → Set X → ENNReal
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeContext : Type