mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Data.URI.Config
Std.Http.URI.Config.mk : ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → Std.Http.URI.Config
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.ext_iff : ∀ {ι : Type u_1} {V : Type u} {inst : CategoryTheory.Category.{v, u} V} {inst_1 : CategoryTheory.Preadditive V}
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} {x y : Homotopy f g}, x = y ↔ x.hom = y.hom
-- Mathlib.CategoryTheory.Bicategory.SingleObj
/-- The unique object in the bicategory obtained by "promoting" a monoidal category.  -/
CategoryTheory.MonoidalSingleObj.star : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.MonoidalSingleObj C
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.whenNotPPOption : (Lean.Options → Bool) → Lean.PrettyPrinter.Delaborator.Delab → Lean.PrettyPrinter.Delaborator.Delab
-- Lean.Elab.InfoTree.Main
Lean.Elab.getInfoHoleIdAssignment? : {m : Type → Type} → [Monad m] → [Lean.Elab.MonadInfoTree m] → Lean.MVarId → m (Option Lean.Elab.InfoTree)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.coweightMap_mul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (x y : P.Hom P),
  (x * y).coweightMap = y.coweightMap ∘ₗ x.coweightMap
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.flattenList.toNatAux.eq_2 : ∀ {n : ℕ} (x_1 : BitVec n), BitVec.flattenList.toNatAux [x_1] = x_1.toNat
-- Std.Data.TreeSet.Raw.Lemmas
/-- This is a restatement of `mem_of_mem_insert` that is written to exactly match the
proof obligation in the statement of `get_insert`.  -/
Std.TreeSet.Raw.mem_of_mem_insert' : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, a ∈ t.insert k → ¬(cmp k a = Ordering.eq ∧ k ∉ t) → a ∈ t
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- shift right by another BitVec expression. For constant shifts there exists a `BVUnop`.
 -/
Std.Tactic.BVDecide.BVExpr.shiftRight : {m n : ℕ} → Std.Tactic.BVDecide.BVExpr m → Std.Tactic.BVDecide.BVExpr n → Std.Tactic.BVDecide.BVExpr m
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.eventually_left_inverse : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X}, x ∈ e.source → ∀ᶠ (y : X) in nhds x, ↑e.symm (↑e y) = y
-- Mathlib.RingTheory.KrullDimension.Regular
Module.supportDim_quotSMulTop_succ_eq_supportDim : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {M : Type u_2} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.Finite R M] [inst_5 : IsLocalRing R] {x : R},
  IsSMulRegular M x → x ∈ IsLocalRing.maximalIdeal R → Module.supportDim R (QuotSMulTop x M) + 1 = Module.supportDim R M
-- Mathlib.Order.Irreducible
IsMin.not_supPrime : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α}, IsMin a → ¬SupPrime a
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_biSup : ∀ {α : Type u_1} (u : α → ℕ → ENNReal) {s : Set α},
  s.Finite → ExpGrowth.expGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, ExpGrowth.expGrowthSup (u x)
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α}, m.getKey? k = some k' → k' ∈ m
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.mk_coe' : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) (f : N → M)
  (h₁ : Function.LeftInverse (⇑e) f) (h₂ : Function.RightInverse (⇑e) f)
  (h₃ :
    ∀ (x y : N),
      { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) =
        { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x +
          { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y),
  { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_add' := h₃ } = e.symm
-- Mathlib.Geometry.Manifold.Instances.Real
instLocallyPathConnectedSpaceEuclideanHalfSpace : ∀ {n : ℕ} [inst : NeZero n], LocallyPathConnectedSpace (EuclideanHalfSpace n)
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_mul_self : ∀ {x : ℝ}, 0 ≤ x → √(x * x) = x
-- Mathlib.RingTheory.FreeRing
/-- If `α` is a type, then `FreeRing α` is the free ring generated by `α`.
This is a ring equipped with a function `FreeRing.of : α → FreeRing α` which has
the following universal property: if `R` is any ring, and `f : α → R` is any function,
then this function is the composite of `FreeRing.of` and a unique ring homomorphism
`FreeRing.lift f : FreeRing α →+* R`.

A typical element of `FreeRing α` is a `ℤ`-linear combination of
formal products of elements of `α`.
For example if `x` and `y` are terms of type `α` then `3 * x * y * x - 2 * y * x + 1` is a
"typical" element of `FreeRing α`. In particular if `α` is empty
then `FreeRing α` is isomorphic to `ℤ`, and if `α` has one term `t`
then `FreeRing α` is isomorphic to the polynomial ring `ℤ[t]`.
If `α` has two or more terms then `FreeRing α` is not commutative.
One can think of `FreeRing α` as the free non-commutative polynomial ring
with coefficients in the integers and variables indexed by `α`.
 -/
FreeRing : Type u → Type u
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- The additive submonoid generated by an element.  -/
AddSubmonoid.multiples : {A : Type u_2} → [inst : AddMonoid A] → A → AddSubmonoid A
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residueFieldCongr_refl : ∀ {X : AlgebraicGeometry.Scheme} {x : ↥X},
  AlgebraicGeometry.Scheme.residueFieldCongr ⋯ = CategoryTheory.Iso.refl (X.residueField x)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D)
  [inst_4 : ∀ (A B : C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F],
  (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso F).hom =
    CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans F
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
AlgebraicGeometry.instGeometricallyReducedFstScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyReduced g],
  AlgebraicGeometry.GeometricallyReduced (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.ModelTheory.Complexity
_private.Mathlib.ModelTheory.Complexity.0.FirstOrder.Language.BoundedFormula.toPrenexImp.match_1.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → L.BoundedFormula α x → Sort u_4)
  (x : ℕ) (φ ψ : L.BoundedFormula α x)
  (h_1 :
    (n : ℕ) →
      (φ : L.BoundedFormula α (n + 1)) →
        (ψ : L.BoundedFormula α n) →
          motive n ((φ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum)
            ψ)
  (h_2 : (n : ℕ) → (φ : L.BoundedFormula α (n + 1)) → (ψ : L.BoundedFormula α n) → motive n φ.all ψ)
  (h_3 : (x : ℕ) → (φ ψ : L.BoundedFormula α x) → motive x φ ψ),
  (∀ (φ_1 : L.BoundedFormula α (x + 1)),
      φ = (φ_1.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum →
        False) →
    (∀ (φ_1 : L.BoundedFormula α (x + 1)), φ = φ_1.all → False) →
      (match x, φ, ψ with
        | n, (φ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum, ψ =>
          h_1 n φ ψ
        | n, φ.all, ψ => h_2 n φ ψ
        | x, φ, ψ => h_3 x φ ψ) =
        h_3 x φ ψ
-- Lean.Meta.Tactic.Grind.Split
/-- Returns case-split candidates. Case-splits that are tagged as `.resolved` or `.notReady` are skipped.
Applies additional `filter` if provided.
If `candidates?` is provided, it is used instead of the candidates stored in the goal.
 -/
Lean.Meta.Grind.getSplitCandidateAnchors : (optParam (Lean.Expr → Lean.Meta.Grind.GoalM Bool) fun x => pure true) →
  optParam (Option (List Lean.Meta.Grind.SplitInfo)) none → Lean.Meta.Grind.GoalM Lean.Meta.Grind.SplitCandidateAnchors
-- Lean.Parser.Term
Lean.Parser.Term.cdot.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Piecewise
ite_inter_closure_eq_of_inter_frontier_eq : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s s' t : Set α},
  s ∩ frontier t = s' ∩ frontier t → t.ite s s' ∩ closure t = s ∩ closure t
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.nnnorm_map : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E), ‖e x‖₊ = ‖x‖₊
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffWithinAt.div_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x : E} {𝕜' : Type u_6} [inst_3 : NormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {f : E → 𝕜'} {n : WithTop ℕ∞}, ContDiffWithinAt 𝕜 n f s x → ∀ (c : 𝕜'), ContDiffWithinAt 𝕜 n (fun x => f x / c) s x
-- Mathlib.Analysis.Distribution.Support
Distribution.TemperedDistribution.dsupport_iteratedLineDerivOp_subset : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedSpace ℂ F] {f : TemperedDistribution E F} {n : ℕ} (m : Fin n → E),
  Distribution.dsupport ⇑(LineDeriv.iteratedLineDerivOp m f) ⊆ Distribution.dsupport ⇑f
-- Mathlib.CategoryTheory.Functor.Const
CategoryTheory.Functor.constComp_inv_app : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D] (X : C) (F : CategoryTheory.Functor C D) (x : J),
  (CategoryTheory.Functor.constComp J X F).inv.app x =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj (F.obj X)).obj x)
-- Init.Prelude
/-- Wraps a value to increase its type's universe level.  -/
PULift.up : {α : Sort s} → α → PULift α
-- Mathlib.Algebra.GroupWithZero.Subgroup
/-- The action on an additive subgroup corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.  -/
AddSubgroup.pointwiseMulAction : {M : Type u_3} →
  {A : Type u_4} → [inst : Monoid M] → [inst_1 : AddGroup A] → [DistribMulAction M A] → MulAction M (AddSubgroup A)
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.pow_dvd_of_squarefree_of_pow_succ_dvd_mul_left : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] {x y p : R} {k : ℕ},
  Squarefree y → Prime p → p ^ (k + 1) ∣ x * y → p ^ k ∣ x
-- Mathlib.Data.Finset.Pi
Finset.pi_singletons : ∀ {α : Type u_1} [inst : DecidableEq α] {β : Type u_2} (s : Finset α) (f : α → β),
  (s.pi fun a => {f a}) = {fun a x => f a}
-- Mathlib.Algebra.Module.Submodule.Ker
LinearEquiv.ker : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂),
  (↑e).ker = ⊥
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.map_sSup' : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f : α → β},
  LeftOrdContinuous f → ∀ {s : Set α}, s.Nonempty → f (sSup s) = sSup (f '' s)
-- Mathlib.Topology.Path
Path.pi_coe : ∀ {ι : Type u_3} {χ : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (χ i)] {as bs : (i : ι) → χ i}
  (γ : (i : ι) → Path (as i) (bs i)), ⇑(Path.pi γ) = fun t i => (γ i) t
-- Lean.Compiler.InitAttr
Lean.isIOUnitInitFnCore : Lean.Environment → Lean.ParametricAttribute Lean.Name → Lean.Name → Bool
-- Mathlib.Order.KrullDimension
Order.krullDim_eq_of_orderIso : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β),
  Order.krullDim α = Order.krullDim β
-- Init.Data.Nat.Lemmas
Nat.add_le_of_le_sub' : ∀ {n k m : ℕ}, m ≤ k → n ≤ k - m → m + n ≤ k
-- Lean.Data.Options
Lean.Option.get? : {α : Type} → [Lean.KVMap.Value α] → Lean.Options → Lean.Option α → Option α
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_sqrt_one_sub_sq : ∫ (x : ℝ) in -1..1, √(1 - x ^ 2) = Real.pi / 2
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.reverse_rules : ∀ {T : Type u_1} (g : ContextFreeGrammar T),
  g.reverse.rules = Finset.map { toFun := ContextFreeRule.reverse, inj' := ⋯ } g.rules
-- Mathlib.Order.Hom.Basic
OrderHom.monotone : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), Monotone ⇑f
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.pre_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.Closed A],
  CategoryTheory.MonoidalClosed.pre (CategoryTheory.CategoryStruct.id A) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ihom A)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgHom.map_adjoin_singleton : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A]
  [inst_2 : StarRing A] [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] [inst_10 : StarRing R]
  [inst_11 : IsScalarTower R A A] [inst_12 : SMulCommClass R A A] [inst_13 : StarModule R A]
  [inst_14 : IsScalarTower R B B] [inst_15 : SMulCommClass R B B] [inst_16 : StarModule R B] (f : F) (x : A),
  NonUnitalStarSubalgebra.map f (NonUnitalStarAlgebra.adjoin R {x}) = NonUnitalStarAlgebra.adjoin R {f x}
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
_private.Mathlib.Combinatorics.Enumerative.Catalan.Basic.0.catalan.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.srangeRestrict_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N), Function.Surjective ⇑f.srangeRestrict
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_add_self : Cardinal.continuum + Cardinal.continuum = Cardinal.continuum
-- Mathlib.Topology.Closure
closure_compl : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, closure sᶜ = (interior s)ᶜ
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- **Alias** of `MeasureTheory.sdiff_cylinder_same`. -/
MeasureTheory.diff_cylinder_same : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (S T : Set ((i : ↥s) → α ↑i)),
  MeasureTheory.cylinder s S \ MeasureTheory.cylinder s T = MeasureTheory.cylinder s (S \ T)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.core.sizeOf_spec : ∀ (a b : Lean.Expr) (ea eb : Lean.Grind.AC.Expr),
  sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.core a b ea eb) = 1 + sizeOf a + sizeOf b + sizeOf ea + sizeOf eb
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castSucc_Icc : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.castSucc (Finset.Icc i j) = Finset.Icc i.castSucc j.castSucc
-- Init.Data.List.Pairwise
List.Pairwise.filterMap : ∀ {β : Type u_1} {α : Type u_2} {R : α → α → Prop} {S : β → β → Prop} (f : α → Option β),
  (∀ (a a' : α), R a a' → ∀ (b : β), f a = some b → ∀ (b' : β), f a' = some b' → S b b') →
    ∀ {l : List α}, List.Pairwise R l → List.Pairwise S (List.filterMap f l)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inter_mul_union_subset_union : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s₁ s₂ t₁ t₂ : Finset α},
  s₁ ∩ s₂ * (t₁ ∪ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- In a Banach algebra `A` over a nontrivially normed field `𝕜`, for any `a : A` the
power series with coefficients `a ^ n` represents the function `(1 - z • a)⁻¹` in a disk of
radius `‖a‖₊⁻¹`.  -/
spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [HasSummableGeomSeries A] (a : A),
  HasFPowerSeriesOnBall (fun z => Ring.inverse (1 - z • a))
    (fun n => ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) 0 (↑‖a‖₊)⁻¹
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
Topology.IsOpenEmbedding.toOpenPartialHomeomorph.congr_simp : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f f_1 : X → Y)
  (e_f : f = f_1) (h : Topology.IsOpenEmbedding f) [inst_2 : Nonempty X],
  Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h = Topology.IsOpenEmbedding.toOpenPartialHomeomorph f_1 ⋯
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.unop_iInf : ∀ {ι : Sort u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : ι → Subalgebra R Aᵐᵒᵖ), (iInf S).unop = ⨅ i, (S i).unop
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.compLinearMap_zero : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] [Nonempty ι] (f : M [⋀^ι]→ₗ[R] N), f.compLinearMap 0 = 0
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.mk.sizeOf_spec : ∀ (carrier : Type u) [str : Group carrier], sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.iInf_div'` for the general case, and `ENNReal.iInf_div_of_ne` for another special
case that assumes `a ≠ ∞` but does not require `Nonempty ι`.  -/
ENNReal.iInf_div : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} [Nonempty ι],
  (a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0) → (⨅ i, f i) / a = ⨅ i, f i / a
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.pushout.condition_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {Q Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Limits.pushout f g) Q ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Q)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inl f g) Q) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Q)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inr f g) Q) h)
-- Mathlib.Order.Category.BoolAlg
BoolAlg.hasForgetToHeytAlg_forget₂_map : ∀ {X Y : BoolAlg} (f : X ⟶ Y),
  CategoryTheory.HasForget₂.forget₂.map f =
    HeytAlg.ofHom { toFun := ⇑(BoolAlg.Hom.hom f), map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
AddLeftReflectLE.mk : ∀ {M : Type u_1} [inst : Add M] [inst_1 : LE M], (∀ {a b₁ b₂ : M}, a + b₁ ≤ a + b₂ → b₁ ≤ b₂) → AddLeftReflectLE M
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_ofNat : ∀ (x : ℝ) (n : ℕ) [inst : n.AtLeastTwo], x ^ OfNat.ofNat n = x ^ OfNat.ofNat n
-- Mathlib.Order.Filter.Map
Filter.comap_inr_map_inl : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α}, Filter.comap Sum.inr (Filter.map Sum.inl f) = ⊥
-- Mathlib.GroupTheory.GroupAction.Primitive
MulAction.IsQuasiPreprimitive.mk : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X]
  [toIsPretransitive : MulAction.IsPretransitive G X],
  (∀ {N : Subgroup G} [N.Normal], MulAction.fixedPoints (↥N) X ≠ Set.univ → MulAction.IsPretransitive (↥N) X) →
    MulAction.IsQuasiPreprimitive G X
-- Mathlib.Algebra.Order.AddGroupWithTop
add_lt_add_iff_left_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommMonoidWithTop α] {a b c : α}, a ≠ ⊤ → (b + a < c + a ↔ b < c)
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- Taking the Cartesian product of two continuous multilinear maps is a bounded linear
operation.  -/
isBoundedLinearMap_prod_multilinear : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : SeminormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {G : Type u_4} [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
  {ι : Type u_5} [inst_5 : Fintype ι] {E : ι → Type u_6} [inst_6 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_7 : (i : ι) → NormedSpace 𝕜 (E i)], IsBoundedLinearMap 𝕜 fun p => p.1.prod p.2
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isLittleO_norm_norm`. -/
Asymptotics.IsLittleO.of_norm_norm : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α}, ((fun x => ‖f' x‖) =o[l] fun x => ‖g' x‖) → f' =o[l] g'
-- Mathlib.Data.ENat.Basic
/-- A version of `ENat.map` for `ZeroHom`s.  -/
ZeroHom.ENatMap : {N : Type u_2} → [inst : Zero N] → ZeroHom ℕ N → ZeroHom ℕ∞ (WithTop N)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_eq_getLast?_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.max? = t.toList.getLast?
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The fourth simplicial identity  -/
SimplexCategory.δ_comp_σ_of_gt_assoc : ∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
  j.castSucc < i →
    ∀ {Z : SimplexCategory} (h : { len := n + 1 } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.succ)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j.castSucc) h) =
        CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) h)
-- Mathlib.AlgebraicGeometry.Fiber
/-- The canonical map from the scheme-theoretic fiber to the residue field.  -/
AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) → (y : ↥Y) → AlgebraicGeometry.Scheme.Hom.fiber f y ⟶ AlgebraicGeometry.Spec (Y.residueField y)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.upperBoundP?_mem : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x : α} [Std.OrientedCmp cmp] {t : RBTree.RBSet α cmp},
  t.upperBoundP? cut = some x → x ∈ t
-- Mathlib.Analysis.Normed.Module.Bases
/-- The basis constant for Schauder bases (supremum over projections) as `enorm`.  -/
SchauderBasis.enormProjBound : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {X : Type u_2} → [inst_1 : NormedAddCommGroup X] → [inst_2 : NormedSpace 𝕜 X] → SchauderBasis 𝕜 X → ENNReal
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
/-- A compact, topological group `G` with a natural action on `F.obj X` for each `X : C`
is a fundamental group of `F`, if `G` acts transitively on the fibers of Galois objects,
the action on `F.obj X` is continuous for all `X : C` and the only trivially acting element of `G`
is the identity.  -/
CategoryTheory.PreGaloisCategory.IsFundamentalGroup : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) →
      [CategoryTheory.GaloisCategory C] →
        (G : Type u_1) →
          [inst_2 : Group G] →
            [(X : C) → MulAction G (F.obj X).obj] →
              [inst : TopologicalSpace G] → [IsTopologicalGroup G] → [CompactSpace G] → Prop
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.toLp_val : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E} (h : MeasureTheory.MemLp f p μ),
  ↑(MeasureTheory.MemLp.toLp f h) = MeasureTheory.AEEqFun.mk f ⋯