mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y X : C} →
      {f : Y ⟶ X} →
        (pullback : CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Over Y)) →
          (CategoryTheory.Over.map f ⊣ pullback) → CategoryTheory.ChosenPullbacksAlong f
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.foldlM.loop.match_1.splitter : (motive : ℕ → Sort u_1) → (i : ℕ) → (Unit → motive 0) → ((i' : ℕ) → motive i'.succ) → motive i
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.algebra_section_stalk : {X : TopCat} →
  (F : TopCat.Presheaf CommRingCat X) →
    {U : TopologicalSpace.Opens ↑X} → (x : ↥U) → Algebra ↑(F.obj (Opposite.op U)) ↑(F.stalk ↑x)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instAddCommMonoid : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → AddCommMonoid (ρ.IntertwiningMap σ)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- A terminal object is initial in the opposite category.  -/
CategoryTheory.Limits.IsTerminal.op : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CategoryTheory.Limits.IsTerminal X → CategoryTheory.Limits.IsInitial (Opposite.op X)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_map_right_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) {X Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G}
  (g : X ⟶ Y),
  ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).map g).right.left =
    CategoryTheory.Under.Hom.right g.left
-- Mathlib.Data.Nat.Factorization.Basic
/-- Two positive naturals are equal if their prime padic valuations are equal  -/
Nat.eq_iff_prime_padicValNat_eq : ∀ (a b : ℕ), a ≠ 0 → b ≠ 0 → (a = b ↔ ∀ (p : ℕ), Nat.Prime p → padicValNat p a = padicValNat p b)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.quasiFiniteAt : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {x : ↥X},
  AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x →
    ∀ {V : X.Opens} (hV : AlgebraicGeometry.IsAffineOpen V) {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (hxV : x ∈ V.carrier),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V hVU)).QuasiFiniteAt
            (hV.primeIdealOf ⟨x, hxV⟩).asIdeal
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
lintegral_comp_polarCoord_symm : ∀ (f : ℝ × ℝ → ENNReal),
  ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑polarCoord.symm p) = ∫⁻ (p : ℝ × ℝ), f p
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A continuous function is strongly measurable when either the source space or the target space
is second-countable.  -/
Continuous.stronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [h : SecondCountableTopologyEither α β]
  {f : α → β}, Continuous f → MeasureTheory.StronglyMeasurable f
-- Mathlib.SetTheory.Cardinal.Arithmetic
/-- If `α` is an infinite type, then `α × α` and `α` have the same cardinality.  -/
Cardinal.mul_eq_self : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → c * c = c
-- Init.Data.Int.Gcd
/-- Computes the greatest common divisor of two integers as a natural number. The GCD of two integers is
the largest natural number that evenly divides both. However, the GCD of a number and `0` is the
number's absolute value.

This implementation uses `Nat.gcd`, which is overridden in both the kernel and the compiler to
efficiently evaluate using arbitrary-precision arithmetic.

Examples:
* `Int.gcd 10 15 = 5`
* `Int.gcd 10 (-15) = 5`
* `Int.gcd (-6) (-9) = 3`
* `Int.gcd 0 5 = 5`
* `Int.gcd (-7) 0 = 7`
 -/
Int.gcd : ℤ → ℤ → ℕ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α}, k ∈ Std.ExtDHashMap.filter f m ↔ ∃ (h : k ∈ m), f k (m.get k h) = true
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.surjOn_iff_le_map : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {f : M →+ N} {H : AddSubmonoid M}
  {K : AddSubmonoid N}, Set.SurjOn ⇑f ↑H ↑K ↔ K ≤ AddSubmonoid.map f H
-- Mathlib.Topology.Instances.EReal.Lemmas
continuous_coe_ennreal_ereal : Continuous ENNReal.toEReal
-- Mathlib.Algebra.Lie.Abelian
isMulCommutative_iff_isLieAbelian : ∀ {A : Type v} [inst : Ring A], IsMulCommutative A ↔ IsLieAbelian A
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.IterM.toList_flatMapM : ∀ {α α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [inst_5 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α m]
  [Std.Iterators.Finite α₂ m] {f : β → m (Std.IterM m γ)} {it₁ : Std.IterM m β},
  (Std.IterM.flatMapM f it₁).toList =
    List.flatten <$>
      (Std.IterM.mapM
          (fun b => do
            let __do_lift ← f b
            __do_lift.toList)
          it₁).toList
-- Init.Data.Rat.Lemmas
Rat.mul_def : ∀ (a b : ℚ), a * b = Rat.normalize (a.num * b.num) (a.den * b.den) ⋯
-- Mathlib.Order.BoundedOrder.Basic
Subtype.orderBot.eq_1 : ∀ {α : Type u} {p : α → Prop} [inst : LE α] [inst_1 : OrderBot α] (hbot : p ⊥),
  Subtype.orderBot hbot = { bot := ⟨⊥, hbot⟩, bot_le := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.instIsGEObjιHeartOfNatInt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (H : Type u') [inst_6 : CategoryTheory.Category.{v', u'} H]
  [inst_7 : CategoryTheory.Preadditive H] [inst_8 : t.Heart H] (X : H), t.IsGE (t.ιHeart.obj X) 0
-- Mathlib.LinearAlgebra.TensorProduct.Basis
TensorProduct.equivFinsuppOfBasisLeft_symm : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq ι]
  (ℬ : Module.Basis ι R M),
  ↑(TensorProduct.equivFinsuppOfBasisLeft ℬ).symm = (Finsupp.lsum R) fun i => (TensorProduct.mk R M N) (ℬ i)
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.liftP_iff : ∀ {n : ℕ} {P : MvPFunctor.{u} n} {α : TypeVec.{u} n} (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : ↑P α),
  MvFunctor.LiftP p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
/-- Similar to `IntInterval`, but with symbolic bounds.  -/
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval : Type
-- Mathlib.Order.Filter.Pointwise
Filter.isAddUnit_iff : ∀ {α : Type u_2} [inst : SubtractionMonoid α] {f : Filter α}, IsAddUnit f ↔ ∃ a, f = pure a ∧ IsAddUnit a
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.AlternatingFaceMapComplex.d_squared : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.AlternatingFaceMapComplex.objD X (n + 1))
      (AlgebraicTopology.AlternatingFaceMapComplex.objD X n) =
    0
-- Mathlib.Tactic.Widget.Conv
/-- Traverse an application from argument to function, accumulating arguments and consuming `pos`
(incrementing `i`) as we approach the head. If `pos[i]` tells us to enter the argument of `.app`
instead of the function at some point, we stop consuming `pos` and start counting arguments
(`some n`) until we hit the head. This gives us enough information to determine the value for
`Path.arg` once we reach the head, and then enter the argument we encountered earlier.

Note: if we instead run out of `pos` before reaching the head, the `Path` is a chain of `fun`s.

Note: `conv` does not see through `.mdata` surrounding an `.app`, so we do not here either.  -/
_private.Mathlib.Tactic.Widget.Conv.0.Mathlib.Tactic.Conv.Path.ofSubExprPosArray.appT : (pos : Array ℕ) →
  Lean.Expr →
    Fin (pos.size + 1) → (acc : List Lean.Expr) → Option (Fin acc.length) → Lean.MetaM Mathlib.Tactic.Conv.Path
-- Mathlib.RingTheory.Spectrum.Prime.Homeomorph
/-- If `L` is a purely inseparable extension of `K` over `R` and `S` is an `R`-algebra,
the induced map `Spec (L ⊗[R] S) ⟶ Spec (K ⊗[R] S)` is a homeomorphism.  -/
PrimeSpectrum.isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable : ∀ (K : Type u_2) (R : Type u_3) (S : Type u_4) [inst : Field K] [inst_1 : CommRing R] [inst_2 : CommRing S]
  [inst_3 : Algebra R K] [inst_4 : Algebra R S] (L : Type u_5) [inst_5 : Field L] [inst_6 : Algebra R L]
  [inst_7 : Algebra K L] [inst_8 : IsScalarTower R K L] [IsPurelyInseparable K L],
  IsHomeomorph (PrimeSpectrum.comap (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S)).toRingHom)
-- Plausible.Random
/-- Given a random generator for `α`, we can convert it to a random generator for `ULift α`.  -/
Plausible.Rand.up : {α : Type u} → {g : Type} → [RandomGen g] → Plausible.RandG g α → Plausible.RandG g (ULift.{v, u} α)
-- Std.Internal.Do.Triple.Basic
/-- Construct a triple from a weakest precondition entailment.  -/
Std.Internal.Do.Triple.intro : ∀ {Pred EPred : Type u} {Prog : Type v} {Value : Type u} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] {x : Prog} [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] {pre : Pred}
  {post : Value → Pred} {epost : EPred},
  Lean.Order.PartialOrder.rel pre (Std.Internal.Do.wp x post epost) → ⦃ pre ⦄ x ⦃ post; epost ⦄
-- Init.Data.Nat.Lemmas
Nat.mod_two_ne_zero : ∀ {n : ℕ}, n % 2 ≠ 0 ↔ n % 2 = 1
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- A point-free means of proving membership in the center, for a non-associative ring.

This can be helpful when working with types that have ext lemmas for `R →+ R`.  -/
Set.mem_center_iff_addMonoidHom : ∀ (R : Type u) [inst : NonUnitalNonAssocSemiring R] (a : R),
  a ∈ Set.center R ↔
    AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧
      AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) ∧
        AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- If the set where you want `f` to be smooth lies entirely in a single chart, and `f` maps it
into a single chart, the smoothness of `f` on that set can be expressed by purely looking in
these charts.
Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
that this set lies in `(extChartAt I x).target`.  -/
mdifferentiableOn_iff_of_subset_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  [IsManifold I 1 M] [IsManifold I' 1 M'] {x : M} {y : M'},
  s ⊆ (chartAt H x).source →
    Set.MapsTo f s (chartAt H' y).source →
      (MDiff[s] f ↔
        ContinuousOn f s ∧
          DifferentiableOn 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) '' s))
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.coe_pow : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (A : Matrix.SpecialLinearGroup n R) (m : ℕ), ↑(A ^ m) = ↑A ^ m
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- Component of the integer multiplied by `√d`  -/
Zsqrtd.im : {d : ℤ} → ℤ√d → ℤ
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.reachable_iff_reflTransGen : ∀ {V : Type u} {G : SimpleGraph V} (u v : V), G.Reachable u v ↔ Relation.ReflTransGen G.Adj u v
-- Init.Data.SInt.Lemmas
Int16.ofInt_eq_ofNat : ∀ {n : ℕ}, Int16.ofInt ↑n = Int16.ofNat n
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.homMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x y : F.Elements)
  (f f_1 : x.fst ⟶ y.fst) (e_f : f = f_1) (hf : (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd = y.snd),
  CategoryTheory.CategoryOfElements.homMk x y f hf = CategoryTheory.CategoryOfElements.homMk x y f_1 ⋯
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.isRoot_iterate_derivative_of_lt_rootMultiplicity : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R} {n : ℕ},
  n < Polynomial.rootMultiplicity t p → ((⇑Polynomial.derivative)^[n] p).IsRoot t
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.bestLabelForDecl?.visitNamespaces : (Lean.Name → StateT (Option Lean.Name) Lean.Server.Completion.M✝ Unit) →
  Lean.Name → StateT (Option Lean.Name) Lean.Server.Completion.M✝ Unit
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.ofSet_symm : ∀ {α : Type u_1} (s : Set α), (PartialEquiv.ofSet s).symm = PartialEquiv.ofSet s
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- If `F` has a limit, then it is a retract of any weak limit of `F`.
 -/
CategoryTheory.Limits.IsWeakLimit.retractOfIsLimit : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        {F : CategoryTheory.Functor J C} →
          {t t' : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsLimit t → CategoryTheory.Limits.IsWeakLimit t' → CategoryTheory.Retract t.pt t'.pt
-- Mathlib.Algebra.Group.Hom.Defs
/-- `AddHom` is a type of addition-preserving homomorphisms  -/
AddHom.addHomClass : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N], AddHomClass (M →ₙ+ N) M N
-- Mathlib.Analysis.Convex.Hull
Convex.convex_remove_iff_notMem_convexHull_remove : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (x : E), Convex 𝕜 (s \ {x}) ↔ x ∉ (convexHull 𝕜) (s \ {x})
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instInhabited : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Inhabited (SlashInvariantForm Γ k)
-- Mathlib.SetTheory.Cardinal.Aleph
/-- `ω₁` is the first uncountable ordinal. 

Conventions for notations in identifiers:

 * The recommended spelling of `ω₁` in identifiers is `omega_one`. -/
Ordinal.termω₁ : Lean.ParserDescr
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.fromLeftInv.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) (x : ↥S.leftInv), S.fromLeftInv x = Exists.choose ⋯
-- Mathlib.Tactic.TacticAnalysis
_private.Mathlib.Tactic.TacticAnalysis.0.Mathlib.TacticAnalysis.Entry.import.unsafe_impl_2 : Mathlib.TacticAnalysis.Entry → Lean.Environment → Lean.Options → ExceptT String Id Mathlib.TacticAnalysis.Config
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreUnitCounit.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (unit : CategoryTheory.Functor.id C ⟶ F.comp G) →
              (counit : G.comp F ⟶ CategoryTheory.Functor.id D) →
                autoParam
                    (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight unit F)
                        (CategoryTheory.CategoryStruct.comp (F.associator G F).hom (F.whiskerLeft counit)) =
                      CategoryTheory.NatTrans.id ((CategoryTheory.Functor.id C).comp F))
                    CategoryTheory.Adjunction.CoreUnitCounit.left_triangle._autoParam →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp (G.whiskerLeft unit)
                          (CategoryTheory.CategoryStruct.comp (G.associator F G).inv
                            (CategoryTheory.Functor.whiskerRight counit G)) =
                        CategoryTheory.NatTrans.id (G.comp (CategoryTheory.Functor.id C)))
                      CategoryTheory.Adjunction.CoreUnitCounit.right_triangle._autoParam →
                    CategoryTheory.Adjunction.CoreUnitCounit F G
-- Mathlib.MeasureTheory.Integral.IntegrableOn
Continuous.stronglyMeasurableAtFilter : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace α] [OpensMeasurableSpace α]
  [inst_2 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [SecondCountableTopologyEither α β]
  {f : α → β}, Continuous f → ∀ (μ : MeasureTheory.Measure α) (l : Filter α), StronglyMeasurableAtFilter f l μ
-- Mathlib.Data.Int.Bitwise
_private.Mathlib.Data.Int.Bitwise.0.Int.bitwise.match_1.eq_4 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.negSucc n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_4 m n
-- Mathlib.Topology.Order.LiminfLimsup
liminf_eq_top : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [FirstCountableTopology α]
  [OrderTopology α] {f : Filter β} [CountableInterFilter f] {u : β → α}, Filter.liminf u f = ⊤ ↔ u =ᶠ[f] ⊤
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
_private.Mathlib.LinearAlgebra.CliffordAlgebra.Contraction.0.CliffordAlgebra.«term_⌋__1» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_add : ∀ {R : Type u} [inst : LinearOrder R] (x y : Tropical R),
  Tropical.untrop (x + y) = min (Tropical.untrop x) (Tropical.untrop y)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Endowing the space `WithLp p (α × β)` with the `L^p` norm. We register this instance
separate from `WithLp.instProdSeminormedAddCommGroup` since the latter requires the type class
hypothesis `[Fact (1 ≤ p)]` in order to prove the triangle inequality.

Registering this separately allows for a future norm-like structure on `WithLp p (α × β)` for
`p < 1` satisfying a relaxed triangle inequality. These are called *quasi-norms*.  -/
WithLp.instProdNorm : (p : ENNReal) → (α : Type u_2) → (β : Type u_3) → [Norm α] → [Norm β] → Norm (WithLp p (α × β))
-- Mathlib.Algebra.FiveLemma
/-- A special case of one four lemma such that the left-most term is zero in terms
of additive groups. For a diagram explaining the variables, see the module docstring.  -/
AddMonoidHom.surjective_of_surjective_of_injective_of_left_exact : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8} [inst : AddGroup M₁]
  [inst_1 : AddGroup M₂] [inst_2 : AddGroup M₃] [inst_3 : AddGroup N₁] [inst_4 : AddGroup N₂] [inst_5 : AddGroup N₃]
  (f₁ : M₁ →+ M₂) (f₂ : M₂ →+ M₃) (g₁ : N₁ →+ N₂) (g₂ : N₂ →+ N₃) (i₁ : M₁ →+ N₁) (i₂ : M₂ →+ N₂) (i₃ : M₃ →+ N₃),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      Function.Exact ⇑f₁ ⇑f₂ →
        Function.Exact ⇑g₁ ⇑g₂ →
          Function.Surjective ⇑i₂ → Function.Injective ⇑i₃ → Function.Injective ⇑g₁ → Function.Surjective ⇑i₁
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_alter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  [Inhabited α] (h : t.WF) {k k' : α} {f : Option β → Option β}
  {hc : k' ∈ Std.DTreeMap.Internal.Impl.Const.alter! k f t},
  (Std.DTreeMap.Internal.Impl.Const.alter! k f t).getKey k' hc =
    if heq : compare k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.mk.inj : ∀ {α : Type u} {β : Type v} {inst : TopologicalSpace α} {inst_1 : PseudoMetricSpace β} {toContinuousMap : C(α, β)}
  {map_bounded' : ∃ C, ∀ (x y : α), dist (toContinuousMap.toFun x) (toContinuousMap.toFun y) ≤ C}
  {toContinuousMap_1 : C(α, β)}
  {map_bounded'_1 : ∃ C, ∀ (x y : α), dist (toContinuousMap_1.toFun x) (toContinuousMap_1.toFun y) ≤ C},
  { toContinuousMap := toContinuousMap, map_bounded' := map_bounded' } =
      { toContinuousMap := toContinuousMap_1, map_bounded' := map_bounded'_1 } →
    toContinuousMap = toContinuousMap_1
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.instSetLike : {α : Type u_2} → [inst : TopologicalSpace α] → {x : α} → SetLike (TopologicalSpace.OpenNhdsOf x) α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.erase_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {k : α} {c : ℕ},
  (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c).erase k = Std.DHashMap.Internal.Raw₀.emptyWithCapacity c
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
/-- The regular sheaf condition can be checked after precomposing with the equivalence.
 -/
CategoryTheory.Equivalence.preregular_isSheaf_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preregular C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D) (F : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology C) F ↔
    CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology D) (e.inverse.op.comp F)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.congr_left : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {g : α → F} {l : Filter α}
  {f₁ f₂ : α → E}, Asymptotics.IsBigOWith c l f₁ g → (∀ (x : α), f₁ x = f₂ x) → Asymptotics.IsBigOWith c l f₂ g
-- Mathlib.Topology.Separation.CompletelyRegular
T35Space.toT0Space : ∀ {X : Type u} {inst : TopologicalSpace X} [self : T35Space X], T0Space X
-- Mathlib.Topology.Sober
genericPoints.isGenericPoint : ∀ {α : Type u_1} [inst : TopologicalSpace α] (x : ↑(genericPoints α)), IsGenericPoint ↑x ↑(genericPoints.component x)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `DistribMulActionHomClass F M A B` states that `F` is a type of morphisms preserving
the additive monoid structure and equivariant with respect to the action of `M`.
It is an abbreviation to `DistribMulActionHomClass F (MonoidHom.id M) A B`
You should extend this class when you extend `DistribMulActionHom`.  -/
DistribMulActionHomClass : (F : Type u_10) →
  (M : outParam (Type u_11)) →
    (A : outParam (Type u_12)) →
      (B : outParam (Type u_13)) →
        [inst : Monoid M] →
          [inst_1 : AddMonoid A] →
            [inst_2 : AddMonoid B] → [DistribMulAction M A] → [DistribMulAction M B] → [FunLike F A B] → Prop
-- Mathlib.Logic.Function.Basic
Function.RightInverse.eq : ∀ {α : Sort u_1} {β : Sort u_2} {g : β → α} {f : α → β}, Function.RightInverse g f → ∀ (x : β), f (g x) = x
-- Mathlib.Algebra.Group.Basic
inv_inv_div_inv : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α), (a⁻¹ / b⁻¹)⁻¹ = a / b