mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Filter.IsBoundedUnder.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : Filter β) (u : β → α),
  Filter.IsBoundedUnder r f u = Filter.IsBounded r (Filter.map u f)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_mono : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal},
  Measurable g → (∀ x ∈ s, f x ≤ g x) → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
-- Mathlib.Analysis.Fourier.LpSpace
MeasureTheory.Lp.instFourierTransform : {E : Type u_1} →
  {F : Type u_2} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : MeasurableSpace E] →
        [inst_2 : BorelSpace E] →
          [inst_3 : NormedAddCommGroup F] →
            [InnerProductSpace ℂ F] →
              [CompleteSpace F] →
                [inst_6 : InnerProductSpace ℝ E] →
                  [inst_7 : FiniteDimensional ℝ E] →
                    FourierTransform ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)
                      ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.balLeft.eq_def : ∀ {α : Type u_1} (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  l.balLeft v r =
    match l with
    | RBTree.RBNode.node RBTree.RBColor.red a x b =>
      RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a x b) v r
    | l =>
      match r with
      | RBTree.RBNode.node RBTree.RBColor.black a y b => l.balance2 v (RBTree.RBNode.node RBTree.RBColor.red a y b)
      | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c =>
        RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black l v a) y (b.balance2 z c.setRed)
      | r => RBTree.RBNode.node RBTree.RBColor.red l v r
-- Mathlib.LinearAlgebra.FreeModule.IdealQuotient
/-- We can write the quotient of an ideal over a PID as a product of quotients by principal ideals.
 -/
Ideal.quotientEquivPiSpan : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            [inst_3 : IsDomain R] →
              [inst_4 : IsPrincipalIdealRing R] →
                [inst_5 : IsDomain S] →
                  [inst_6 : Finite ι] →
                    (I : Ideal S) →
                      (b : Module.Basis ι R S) →
                        (hI : I ≠ ⊥) → (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ Ideal.span {Ideal.smithCoeffs b I hI i}
-- Init.Data.List.Basic
/-- Checks whether `a` is an element of `l`, using `==` to compare elements.

`O(|l|)`. `List.contains` is a synonym that takes the list before the element.

The preferred simp normal form is `l.contains a`. When `LawfulBEq α` is available,
`l.contains a = true ↔ a ∈ l` and `l.contains a = false ↔ a ∉ l`.

Example:
* `List.elem 3 [1, 4, 2, 3, 3, 7] = true`
* `List.elem 5 [1, 4, 2, 3, 3, 7] = false`
 -/
List.elem : {α : Type u} → [BEq α] → α → List α → Bool
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.inv_iff : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f : 𝕜 → 𝕜'}, MeromorphicAt f⁻¹ x ↔ MeromorphicAt f x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k : α} {fallback : β k},
      (List.map Sigma.fst l).contains k = false → (↑(m.insertMany l)).getD k fallback = m.getD k fallback
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f * g) x = f x * g x`, `1 x = 1`, and `(f ^ n) x = f x ^ n`
is a cancel commutative monoid if `β` is a cancel commutative monoid.  -/
FunLike.cancelCommMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] →
          [inst_2 : One F] →
            [inst_3 : Pow F ℕ] →
              [inst_4 : CancelCommMonoid β] →
                [IsOneApply F α β] → [IsMulApply F α β] → [IsPowApply ℕ F α β] → CancelCommMonoid F
-- Mathlib.Logic.Relation
Relation.instTransTransGen_mathlib : {α : Type u_1} → {r : α → α → Prop} → Trans (Relation.TransGen r) r (Relation.TransGen r)
-- Mathlib.Algebra.EuclideanDomain.Int
Int.euclideanDomain : EuclideanDomain ℤ
-- Mathlib.Algebra.Group.Ext
AddCancelMonoid.toAddLeftCancelMonoid_injective : ∀ {M : Type u}, Function.Injective (@AddCancelMonoid.toAddLeftCancelMonoid M)
-- Lean.Meta.Match.MatcherApp.Basic
/-- Recognizes if `e` is a matcher application, and destructs it into the `MatcherApp` data structure.

This can optionally also treat `casesOn` recursor applications as a special case
of matcher applications.
 -/
Lean.Meta.matchMatcherApp? : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Expr → optParam Bool false → m (Option Lean.Meta.MatcherApp)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `sub_pos`. -/
lt_of_sub_pos : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, 0 < a - b → b < a
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
FractionalIdeal.semifield : {A : Type u_2} →
  (K : Type u_3) →
    [inst : CommRing A] →
      [inst_1 : Field K] →
        [IsDedekindDomain A] →
          [inst_3 : Algebra A K] → [IsFractionRing A K] → Semifield (FractionalIdeal (nonZeroDivisors A) K)
-- Mathlib.AlgebraicGeometry.Sites.Etale
/-- Big étale site: the étale pretopology on the category of schemes.  -/
AlgebraicGeometry.Scheme.etalePretopology : CategoryTheory.Pretopology AlgebraicGeometry.Scheme
-- Mathlib.Data.Rel
SetRel.mem_dom : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {a : α}, a ∈ R.dom ↔ ∃ b, (a, b) ∈ R
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.distinct_keys_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α], List.Pairwise (fun a b => (a.1 == b.1) = false) (Std.DHashMap.Const.toList m)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.mem_cliqueSet_iff : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α}, s ∈ G.cliqueSet n ↔ G.IsNClique n s
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.union_insert_right_equiv_insert_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {p : (_ : α) × β}, t₁.WF → t₂.WF → (t₁ ∪ t₂.insert p.fst p.snd).Equiv ((t₁ ∪ t₂).insert p.fst p.snd)
-- Mathlib.Algebra.Polynomial.PartialFractions
/-- Let `R` be a commutative ring and `f : R[X]`. Let `s` be a finite index set.
Let `g i` be a collection of monic and pairwise coprime polynomials indexed by `s`.
Then `f` can be written in the form `(∏ i ∈ s, g i) * (q + ∑ i ∈ s, r i / g i)`
in at most one way, where `degree (r i) < degree (g i)` and the denominator cancels formally.
See `eq_quo_mul_prod_add_sum_rem_mul_prod` for the existence of such a representation.  -/
Polynomial.quo_mul_prod_add_sum_rem_mul_prod_unique : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {g : ι → Polynomial R},
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j => IsCoprime (g i) (g j)) →
      ∀ {q₁ q₂ : Polynomial R} {r₁ r₂ : ι → Polynomial R},
        (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
          (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
            q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
                q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
              q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.mapArrowLeft_comp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ f₁' : CategoryTheory.Arrow C₁}
  {f₃ : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom)
  {f₁'' : CategoryTheory.Arrow C₁} (sq₁₃'' : G.PullbackObjObj f₁''.hom f₃.hom) (sq' : f₁'' ⟶ f₁') (sq : f₁' ⟶ f₁),
  CategoryTheory.CategoryStruct.comp (sq₁₃.mapArrowLeft sq₁₃' sq) (sq₁₃'.mapArrowLeft sq₁₃'' sq') =
    sq₁₃.mapArrowLeft sq₁₃'' (CategoryTheory.CategoryStruct.comp sq' sq)
-- Init.Data.Dyadic.Basic
Dyadic.add.eq_2 : ∀ (x : Dyadic), (x = Dyadic.zero → False) → x.add Dyadic.zero = x
-- Mathlib.Probability.Moments.ComplexMGF
/-- `complexMGF X μ` is analytic at any point `z` with `z.re ∈ interior (integrableExpSet X μ)`.  -/
ProbabilityTheory.analyticAt_complexMGF : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ},
  z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ) → AnalyticAt ℂ (ProbabilityTheory.complexMGF X μ) z
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Given `X : T`, to upgrade a functor `F : S ⥤ T` to a functor `S ⥤ Under X`, it suffices to
provide maps `X ⟶ F.obj Y` for all `Y` making the obvious triangles involving all `F.map g`
commute.  -/
CategoryTheory.Functor.toUnder : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {S : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} S] →
        (F : CategoryTheory.Functor S T) →
          (X : T) →
            (f : (Y : S) → X ⟶ F.obj Y) →
              (∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) →
                CategoryTheory.Functor S (CategoryTheory.Under X)
-- Mathlib.RingTheory.Grassmannian
/-- The `B`-linear equivalence `(B ⊗[R] M) ⧸ ker (baseChangeMkQ N) ≃ₗ[B] B ⊗[A] ((A ⊗[R] M) ⧸ N)`
underlying `Module.Grassmannian.map`.  -/
Module.Grassmannian.baseChangeMkQEquiv : {R : Type u} →
  [inst : CommRing R] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {A : Type w} →
            [inst_3 : CommRing A] →
              [inst_4 : Algebra R A] →
                {B : Type w} →
                  [inst_5 : CommRing B] →
                    [inst_6 : Algebra R B] →
                      [inst_7 : Algebra A B] →
                        [inst_8 : IsScalarTower R A B] →
                          (N : Submodule A (TensorProduct R A M)) →
                            (TensorProduct R B M ⧸ (Module.Grassmannian.baseChangeMkQ B N).ker) ≃ₗ[B]
                              TensorProduct A B (TensorProduct R A M ⧸ N)
-- Init.Data.Float.Model.Float32
/-- Converts a `USize` to a `Float32.Model`, returning positive zero on zero.  -/
Float32.Model.ofUSize : USize → Float32.Model
-- Batteries.Data.Vector.Lemmas
Vector.scanr_reverse : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {init : β} {f : α → β → β} {as : Vector α n},
  Vector.scanr f init as.reverse = (Vector.scanl (flip f) init as).reverse
-- Mathlib.Analysis.Complex.Circle
Circle.instHasDistribNeg : HasDistribNeg Circle
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.instVAddCommClassSubtypeMem_1 : ∀ {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [inst : SetLike S α] [inst_1 : VAdd M N] [inst_2 : VAdd M α]
  [inst_3 : AddMonoid N] [inst_4 : AddAction N α] [inst_5 : VAddMemClass S N α] [inst_6 : VAddAssocClass M N α] (s : S)
  [VAddCommClass M N α], VAddCommClass M N ↥s
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C}
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] {R : Type u_2}
  [inst_3 : Semiring R] [inst_4 : CategoryTheory.Linear R C] (o : CategoryTheory.HomOrthogonal s) {α β : Type}
  [inst_5 : Finite α] [inst_6 : Finite β] {f : α → ι} {g : β → ι} (a : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b))
  (i : ι), o.matrixDecompositionLinearEquiv a i = o.matrixDecompositionAddEquiv.toFun a i
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.continuous_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  (∀ (t : ℝ), MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ) → Continuous (ProbabilityTheory.mgf X μ)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- Given a "tulip" of morphisms
```
 j₁    j₂    j₃
 |\   / \   / |
 | \ /   \ /  |
 |  vv    vv  |
 \  k₁    k₂ /
  \         /
   \       /
    \     /
     \   /
      v v
       l
```
in a filtered category, we can construct an object `s` and three morphisms from `k₁`, `k₂` and `l`
to `s`, making the resulting squares commute.
 -/
CategoryTheory.IsFiltered.tulip : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ j₃ k₁ k₂ l : C}
  (f₁ : j₁ ⟶ k₁) (f₂ : j₂ ⟶ k₁) (f₃ : j₂ ⟶ k₂) (f₄ : j₃ ⟶ k₂) (g₁ : j₁ ⟶ l) (g₂ : j₃ ⟶ l),
  ∃ s α β γ,
    CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧
      CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp f₃ γ ∧
        CategoryTheory.CategoryStruct.comp f₄ γ = CategoryTheory.CategoryStruct.comp g₂ β
-- Mathlib.FieldTheory.RatFunc.Degree
RatFunc.intDegree_polynomial : ∀ {K : Type u} [inst : Field K] {p : Polynomial K}, ((algebraMap (Polynomial K) (RatFunc K)) p).intDegree = ↑p.natDegree
-- Mathlib.Data.Set.Card
Set.ncard_insert_eq_ite : ∀ {α : Type u_1} {s : Set α} {a : α} [inst : Decidable (a ∈ s)],
  autoParam s.Finite Set.ncard_insert_eq_ite._auto_1 → (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
ZMod.instMeasurableSpace : (n : ℕ) → MeasurableSpace (ZMod n)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.functorFrom_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {E : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E)
  (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c'))
  (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯)
  (hom_comp :
    ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
      hom (CategoryTheory.CategoryStruct.comp f g) =
        CategoryTheory.CategoryStruct.comp (hom f)
          (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g)) (CategoryTheory.eqToHom ⋯)))
  {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y),
  (CategoryTheory.Grothendieck.functorFrom fib hom hom_id hom_comp).map f =
    CategoryTheory.CategoryStruct.comp ((hom f.base).app X.fiber) ((fib Y.base).map f.fiber)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.xRep_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R}, WeierstrassCurve.Affine.Point.xRep 0 = ![1, 0]
-- Init.Data.Array.Lemmas
Array.replace_append_right : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {xs ys : Array α},
  a ∉ xs → (xs ++ ys).replace a b = xs ++ ys.replace a b
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.cellFrontier_subset_complex`. -/
Topology.CWComplex.cellFrontier_subset_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.cellFrontier n j ⊆ C
-- Mathlib.Topology.MetricSpace.Basic
AddOpposite.instMetricSpace.eq_1 : ∀ {α : Type u_2} [inst : MetricSpace α], AddOpposite.instMetricSpace = MetricSpace.induced AddOpposite.unop ⋯ inst
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.nsmul.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S],
  AddOreLocalization.nsmul = nsmulRec
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.brecOn_1.go : {motive_1 : Aesop.Frontend.RuleExpr → Sort u} →
  {motive_2 : Array Aesop.Frontend.RuleExpr → Sort u} →
    {motive_3 : List Aesop.Frontend.RuleExpr → Sort u} →
      (t : Array Aesop.Frontend.RuleExpr) →
        ((t : Aesop.Frontend.RuleExpr) → t.below → motive_1 t) →
          ((t : Array Aesop.Frontend.RuleExpr) → Aesop.Frontend.RuleExpr.below_1 t → motive_2 t) →
            ((t : List Aesop.Frontend.RuleExpr) → Aesop.Frontend.RuleExpr.below_2 t → motive_3 t) →
              motive_2 t ×' Aesop.Frontend.RuleExpr.below_1 t
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_add_mul_right : ∀ {α : Type u} [inst : CommRing α] (x y z : α), Ideal.span {x + z * y, y} = Ideal.span {x, y}
-- Mathlib.RingTheory.Noetherian.Basic
fg_of_ker_bot : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_5} [inst : Ring R] [inst_1 : Ring S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module S P] [IsNoetherian S P]
  {N : Submodule R M} {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (f : M →ₛₗ[σ] P),
  f.ker = ⊥ → N.FG
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The forgetful functor from additive monoids to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types.  -/
AddMonCat.forget_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddMonCat)
-- Qq.MatchImpl
Qq.Impl.mkLambdaQ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.to_image_id' : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → l.HasBasis (fun t => ∃ i, p i ∧ s i = t) id
-- Mathlib.Data.Finsupp.Antidiagonal
Finsupp.prod_antidiagonal_swap : ∀ {α : Type u} [inst : DecidableEq α] {M : Type u_1} [inst_1 : CommMonoid M] (n : α →₀ ℕ) (f : (α →₀ ℕ) → (α →₀ ℕ) → M),
  ∏ p ∈ Finset.HasAntidiagonal.antidiagonal n, f p.1 p.2 = ∏ p ∈ Finset.HasAntidiagonal.antidiagonal n, f p.2 p.1
-- Mathlib.Topology.Homeomorph.Defs
Equiv.toHomeomorphOfIsInducing_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X ≃ Y)
  (hf : Topology.IsInducing ⇑f), ⇑(f.toHomeomorphOfIsInducing hf).symm = ⇑f.symm
-- Mathlib.Analysis.Convex.GaugeRescale
gaugeRescale.eq_1 : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (s t : Set E) (x : E),
  gaugeRescale s t x = (gauge s x / gauge t x) • x
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.associated_denom_inv : ∀ {K : Type u} [inst : Field K] {x : RatFunc K}, x ≠ 0 → Associated x⁻¹.denom x.num
-- Mathlib.Algebra.Order.Archimedean.Defs
/-- For any two elements `x`, `y` such that `0 < y`, there exists a natural number `n`
such that `x ≤ n • y`.  -/
Archimedean.arch : ∀ {R : Type u_2} {inst : AddCommMonoid R} {inst_1 : PartialOrder R} [self : Archimedean R] (x : R) {y : R},
  0 < y → ∃ n, x ≤ n • y
-- Lean.Data.KVMap
Lean.DataValue.ofBool.sizeOf_spec : ∀ (v : Bool), sizeOf (Lean.DataValue.ofBool v) = 1 + sizeOf v
-- Mathlib.Logic.Equiv.Defs
/-- If `α` is an empty type, then it is equivalent to the `PEmpty` type in any universe.  -/
Equiv.equivPEmpty : (α : Sort v) → [IsEmpty α] → α ≃ PEmpty.{u}
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.IsStackFor.isEquivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {S : C}
  {R : CategoryTheory.Presieve S}, F.IsStackFor R → (F.toDescentData fun f => f.obj.hom).IsEquivalence
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.card_subtype : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) (L : Subgroup ↥K), Nat.card ↥(Subgroup.map K.subtype L) = Nat.card ↥L
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.instFullModulesSpecSheafModuleCatCarrierCarrierCommRingCatModulesSpecToSheaf : ∀ {R : CommRingCat}, AlgebraicGeometry.modulesSpecToSheaf.Full
-- Batteries.Recycling.MonadSatisfying.Basic
MonadSatisfying.mk : {m : Type u → Type v} →
  [inst : Functor m] →
    [inst_1 : LawfulFunctor m] →
      (satisfying : {α : Type u} → {p : α → Prop} → {x : m α} → SatisfiesM p x → m { a // p a }) →
        (∀ {α : Type u} {p : α → Prop} {x : m α} (h : SatisfiesM p x), Subtype.val <$> satisfying h = x) →
          MonadSatisfying m
-- Mathlib.Data.List.MinMax
/-- `argmax f l` returns `some a`, where `f a` is maximal among the elements of `l`, in the sense
that there is no `b ∈ l` with `f a < f b`. If `a`, `b` are such that `f a = f b`, it returns
whichever of `a` or `b` comes first in the list. `argmax f [] = none`.  -/
List.argmax : {α : Type u_1} → {β : Type u_2} → [inst : Preorder β] → [DecidableLT β] → (α → β) → List α → Option α
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.bind_apply_le : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {m : MeasureTheory.Measure α}
  (f : α → MeasureTheory.Measure β) {s : Set β}, MeasurableSet s → (m.bind f) s ≤ ∫⁻ (a : α), (f a) s ∂m
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.mk.injEq : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (toEquiv : M ≃ N)
  (map_fun' :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toEquiv.toFun (FirstOrder.Language.Structure.funMap f x) =
          FirstOrder.Language.Structure.funMap f (toEquiv.toFun ∘ x))
      FirstOrder.Language.Equiv.map_fun'._autoParam)
  (map_rel' :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r (toEquiv.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x)
      FirstOrder.Language.Equiv.map_rel'._autoParam)
  (toEquiv_1 : M ≃ N)
  (map_fun'_1 :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toEquiv_1.toFun (FirstOrder.Language.Structure.funMap f x) =
          FirstOrder.Language.Structure.funMap f (toEquiv_1.toFun ∘ x))
      FirstOrder.Language.Equiv.map_fun'._autoParam)
  (map_rel'_1 :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r (toEquiv_1.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x)
      FirstOrder.Language.Equiv.map_rel'._autoParam),
  ({ toEquiv := toEquiv, map_fun' := map_fun', map_rel' := map_rel' } =
      { toEquiv := toEquiv_1, map_fun' := map_fun'_1, map_rel' := map_rel'_1 }) =
    (toEquiv = toEquiv_1)
-- Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate
eventually_apply_eq_iff_implicitFunctionOfBivariate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : IsRCLikeNormedField 𝕜] {E₁ : Type u_2}
  [inst_2 : NormedAddCommGroup E₁] [inst_3 : NormedSpace 𝕜 E₁] [inst_4 : CompleteSpace E₁] {E₂ : Type u_3}
  [inst_5 : NormedAddCommGroup E₂] [inst_6 : NormedSpace 𝕜 E₂] [inst_7 : CompleteSpace E₂] {F : Type u_4}
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ → E₂ → F}
  {f₁ : E₁ → E₂ → E₁ →L[𝕜] F} {f₂ : E₁ → E₂ → E₂ →L[𝕜] F}
  (df₁ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f x v.2) (f₁ v.1 v.2) v.1)
  (df₂ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f v.1 x) (f₂ v.1 v.2) v.2) (cf₁ : ContinuousAt (↿f₁) u)
  (cf₂ : ContinuousAt (↿f₂) u) (if₂u : (f₂ u.1 u.2).IsInvertible),
  ∀ᶠ (v : E₁ × E₂) in nhds u, f v.1 v.2 = f u.1 u.2 ↔ implicitFunctionOfBivariate df₁ df₂ cf₁ cf₂ if₂u v.1 = v.2
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_compl_of_infinite : ∀ {α : Type u_1} [Infinite α] (s : Set α), Cardinal.mk ↑s < Cardinal.mk α → Cardinal.mk ↑sᶜ = Cardinal.mk α
-- Lean.Parser.Types
Lean.Parser.Parser.mk.sizeOf_spec : ∀ (info : Lean.Parser.ParserInfo) (fn : Lean.Parser.ParserFn), sizeOf { info := info, fn := fn } = 1 + sizeOf info
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsStronglyCocartesian.of_isIso : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ]
  [CategoryTheory.IsIso φ], p.IsStronglyCocartesian f φ