mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_5} {ε' : Type u_6}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [inst_2 : TopologicalSpace ε'] [inst_3 : ContinuousENorm ε']
  {f : α → ε} {g : α → ε'} {c : ENNReal},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ) → MeasureTheory.eLpNormEssSup f μ ≤ c • MeasureTheory.eLpNormEssSup g μ
-- Init.Data.Range.Polymorphic.Fin
Fin.instLawfulHasSize_1 : ∀ {n : ℕ}, Std.Rxo.LawfulHasSize (Fin n)
-- Aesop.RulePattern.Cache
/-- Entry of the rule pattern cache.  -/
Aesop.RulePatternCache.Entry : Type
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_union_of_contains_eq_false_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} {fallback : β},
        m₂.contains k = false →
          Std.DHashMap.Internal.Raw₀.Const.getD (m₁.union m₂) k fallback =
            Std.DHashMap.Internal.Raw₀.Const.getD m₁ k fallback
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg_filter_univ : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveNeg α] (p : α → Prop) [inst_2 : Fintype α]
  [inst_3 : DecidablePred p], ↑(-{x | p x}) = {x | p (-x)}
-- Mathlib.Data.Multiset.Functor
Multiset.comp_traverse : ∀ {G H : Type u_1 → Type u_1} [inst : Applicative G] [inst_1 : Applicative H] [inst_2 : CommApplicative G]
  [inst_3 : CommApplicative H] {α β γ : Type u_1} (g : α → G β) (h : β → H γ) (x : Multiset α),
  Multiset.traverse (Functor.Comp.mk ∘ Functor.map h ∘ g) x =
    Functor.Comp.mk (Multiset.traverse h <$> Multiset.traverse g x)
-- Init.PropLemmas
Bool.dite_then_false : ∀ {p : Prop} [inst : Decidable p] {x : ¬p → Bool}, (if h : p then false else x h) = true ↔ ∃ (h : ¬p), x h = true
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.lift₂.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {α : Type u_2}
  (f : M → M → α)
  (h :
    ∀ (a₁ b₁ a₂ b₂ : M),
      MulArchimedeanClass.mk a₁ = MulArchimedeanClass.mk b₁ →
        MulArchimedeanClass.mk a₂ = MulArchimedeanClass.mk b₂ → f a₁ a₂ = f b₁ b₂),
  MulArchimedeanClass.lift₂ f h = Quotient.lift₂ f ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {c : ℕ}, (Std.DHashMap.Raw.emptyWithCapacity c).size = 0
-- Mathlib.Data.Finset.Empty
Finset.empty_subset : ∀ {α : Type u_1} (s : Finset α), ∅ ⊆ s
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_int_eq_addSubgroupClosure : ∀ {M : Type u_9} [inst : AddCommGroup M] (s : Set M), (Submodule.span ℤ s).toAddSubgroup = AddSubgroup.closure s
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.infLELeft_apply : ∀ {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (x : ↥(U ⊓ V)), (U.infLELeft V) x = ⟨↑x, ⋯⟩
-- Mathlib.Analysis.ODE.Transform
isIntegralCurve_comp_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {dt : ℝ},
  IsIntegralCurve (γ ∘ fun x => x - dt) (v ∘ fun x => x - dt) ↔ IsIntegralCurve γ v
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- Composition for polynomial functors  -/
PFunctor.comp : PFunctor.{uA₂, uB₂} → PFunctor.{uA₁, uB₁} → PFunctor.{max uA₁ uA₂ uB₂, max uB₁ uB₂}
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.den_map_intCast : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] (A : Matrix m n ℤ), (A.map Int.cast).den = 1
-- Mathlib.Logic.Hydra
/-- `CutExpand r` is well-founded when `r` is.  -/
WellFounded.cutExpand : ∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r → WellFounded (Relation.CutExpand r)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.id.toOplax : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C),
  CategoryTheory.Oplax.StrongTrans.id F.toOplax =
    CategoryTheory.Pseudofunctor.StrongTrans.toOplax (CategoryTheory.CategoryStruct.id F)
-- Lean.Meta.Basic
/-- `withReducibleAndInstances x` executes `x` using the `.instances` transparency setting. In this setting only definitions tagged as `[reducible]`
or `[instance_reducible]` (e.g. instances) are unfolded. `[implicit_reducible]` is **not** unfolded — use
`withImplicit` for that.
 -/
Lean.Meta.withReducibleAndInstances : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_span_span : ∀ (R : Type u_1) {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] N →ₗ[R] P) (s : Set M) (t : Set N),
  Submodule.map₂ f (Submodule.span R s) (Submodule.span R t) = Submodule.span R (Set.image2 (fun m n => (f m) n) s t)
-- Init.Data.Option.Basic
Option.instDecidableRelLt : {α : Type u_1} → {β : Type u_2} → (r : α → β → Prop) → [s : DecidableRel r] → DecidableRel (Option.lt r)
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (self : X.ExtraDegeneracy) (n : ℕ) (i : Fin (n + 2)) {Z : C} (h : X.left.obj (Opposite.op { len := n + 1 }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.s (n + 1)) (CategoryTheory.CategoryStruct.comp (X.left.δ i.succ) h) =
    CategoryTheory.CategoryStruct.comp (X.left.δ i) (CategoryTheory.CategoryStruct.comp (self.s n) h)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_inverse_map_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) {Y X : CategoryTheory.Comma L R₂} (f : Y ⟶ X),
  ((CategoryTheory.Comma.mapRightIso L i).inverse.map f).left = f.left
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- When all four functors in a square are left adjoints, the mates operation can be iterated:

```
         L₁                  R₁                  R₁
      C --→ D             C ←-- D             C ←-- D
   F₁ ↓  ↗  ↓  F₂      F₁ ↓  ↘  ↓ F₂       U₁ ↑  ↙  ↑ U₂
      E --→ F             E ←-- F             E ←-- F
         L₂                  R₂                  R₂
```

In this case the iterated mate equals the conjugate of the original transformation and is thus an
isomorphism if and only if the original transformation is. This explains why some Beck-Chevalley
natural transformations are natural isomorphisms.
 -/
CategoryTheory.iterated_mateEquiv_conjugateEquiv : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {F₁ : CategoryTheory.Functor A C} {U₁ : CategoryTheory.Functor C A}
  {F₂ : CategoryTheory.Functor B D} {U₂ : CategoryTheory.Functor D B} {L₁ : CategoryTheory.Functor A B}
  {R₁ : CategoryTheory.Functor B A} {L₂ : CategoryTheory.Functor C D} {R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁)
  (adj₂ : L₂ ⊣ R₂) (adj₃ : F₁ ⊣ U₁) (adj₄ : F₂ ⊣ U₂) (α : CategoryTheory.TwoSquare F₁ L₁ L₂ F₂),
  ((CategoryTheory.mateEquiv adj₄ adj₃) ((CategoryTheory.mateEquiv adj₁ adj₂) α)).natTrans =
    (CategoryTheory.conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.mk.injEq : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] (toOpenSubgroup : OpenSubgroup G)
  (isNormal' : autoParam (↑toOpenSubgroup).Normal OpenNormalSubgroup.isNormal'._autoParam)
  (toOpenSubgroup_1 : OpenSubgroup G)
  (isNormal'_1 : autoParam (↑toOpenSubgroup_1).Normal OpenNormalSubgroup.isNormal'._autoParam),
  ({ toOpenSubgroup := toOpenSubgroup, isNormal' := isNormal' } =
      { toOpenSubgroup := toOpenSubgroup_1, isNormal' := isNormal'_1 }) =
    (toOpenSubgroup = toOpenSubgroup_1)
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsShiftClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A], (P.shiftClosure A).IsClosedUnderIsomorphisms
-- Init.Data.BitVec.Lemmas
BitVec.neg_eq_not_add : ∀ {w : ℕ} (x : BitVec w), -x = ~~~x + 1#w
-- Mathlib.RingTheory.Nilpotent.GeometricallyReduced
Algebra.isReduced_of_isGeometricallyReduced : ∀ (k : Type u_1) {A : Type u_2} [inst : Field k] [inst_1 : Ring A] [inst_2 : Algebra k A]
  [Algebra.IsGeometricallyReduced k A], IsReduced A
-- Init.Data.Nat.Dvd
Nat.dvd_mul_right_of_dvd : ∀ {a b : ℕ}, a ∣ b → ∀ (c : ℕ), a ∣ b * c
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ₀Iter_coe_eq_of_lt : ∀ (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : autoParam (n + i = m) SimplexCategory.σ₀Iter_coe_eq_of_lt._auto_1),
  autoParam (↑j < i) SimplexCategory.σ₀Iter_coe_eq_of_lt._auto_3 →
    ↑((CategoryTheory.ConcreteCategory.hom (SimplexCategory.σ₀Iter i hi)) j) = 0
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.Measure.setLIntegral_condKernel : ∀ {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (β × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ]
  {f : β × Ω → ENNReal},
  Measurable f →
    ∀ {s : Set β},
      MeasurableSet s →
        ∀ {t : Set Ω},
          MeasurableSet t →
            ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.toAddSubmonoid_top : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R], ⊤.toAddSubmonoid = ⊤
-- Mathlib.RepresentationTheory.Rep.Iso
Rep.toModuleMonoidAlgebra.eq_1 : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G],
  Rep.toModuleMonoidAlgebra =
    { obj := fun V => ModuleCat.of (MonoidAlgebra k G) V.ρ.asModule,
      map := fun {X Y} f => Rep.toModuleMonoidAlgebraMap f, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.cuspFunction_add : ∀ {h : ℝ} {f g : UpperHalfPlane → ℂ},
  ContinuousAt (UpperHalfPlane.cuspFunction h f) 0 →
    ContinuousAt (UpperHalfPlane.cuspFunction h g) 0 →
      UpperHalfPlane.cuspFunction h (f + g) = UpperHalfPlane.cuspFunction h f + UpperHalfPlane.cuspFunction h g
-- Mathlib.Logic.Equiv.Fin.Basic
/-- Equivalence between `Fin (n + 1)` and `Option (Fin n)`.
This is a version of `Fin.pred` that produces `Option (Fin n)` instead of
requiring a proof that the input is not `0`.  -/
finSuccEquiv : (n : ℕ) → Fin (n + 1) ≃ Option (Fin n)
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.locally_of_iff : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => Q) →
      (∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
          P f ↔
            ∀ (x : ↥X),
              ∃ U V,
                ∃ (_ : x ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U),
                  Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e))) →
        AlgebraicGeometry.HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] =>
          RingHom.Locally fun {R S} [CommRing R] [CommRing S] => Q
-- Lean.Meta.Match.Match
Lean.Meta.Match.State.mk.sizeOf_spec : ∀ (used : Std.HashSet ℕ) (overlaps : Lean.Meta.Match.Overlaps) (counterExamples : Array (List Lean.Meta.Match.Example)),
  sizeOf { used := used, overlaps := overlaps, counterExamples := counterExamples } =
    1 + sizeOf used + sizeOf overlaps + sizeOf counterExamples
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableOn.eq_1 : ∀ {𝕜 : 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),
  MDiff[s] f = ∀ x ∈ s, MDiffAt[s] f x
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.orderHom_injective : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {N : Type u_2}
  [inst_3 : CommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedMonoid N] {f : M →*o N},
  Function.Injective ⇑f → Function.Injective ⇑(MulArchimedeanClass.orderHom f)
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsPreBrownianReal.aemeasurable : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P → ∀ (t : NNReal), AEMeasurable (B t) P
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₂_obj_obj_obj_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [inst_4 : CategoryTheory.Category.{v_7, u_7} E]
  (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂)
  (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) {X_1 Y : C₁} (f : X_1 ⟶ Y) (X_2 : C₂),
  (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).obj F₂).obj X).map f).app X_2 =
    (X.map (F₁.map f)).app (F₂.obj X_2)
-- Lean.Widget.Diff
/-- Add a tag at the given position to the `changesAfter` dict.  -/
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiff.insertAfterChange : Lean.SubExpr.Pos →
  optParam Lean.Widget.ExprDiffTag✝ Lean.Widget.ExprDiffTag.change✝ → Lean.Widget.ExprDiff✝ → Lean.Widget.ExprDiff✝
-- Lean.Elab.Attributes
Lean.Elab.mkAttrKindGlobal : Lean.Syntax
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_inv_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) (i : ℕ),
  (AlgebraicTopology.DoldKan.Γ₀NondegComplexIso K).inv.f i =
    CategoryTheory.CategoryStruct.id ((AlgebraicTopology.DoldKan.Γ₀.splitting K).N i)
-- Mathlib.Order.CompleteLattice.Basic
/-- Transfer `CompleteLattice` across an `Equiv`.  -/
Equiv.completeLattice : {α : Type u_1} → {β : Type u_2} → α ≃ β → [CompleteLattice β] → CompleteLattice α
-- Lean.Meta.Sym.Arith.Poly
/-- Returns the number of monomials in the polynomial.  -/
Lean.Grind.CommRing.Poly.numTerms : Lean.Grind.CommRing.Poly → ℕ
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- Composition of morphisms  -/
RootPairing.Hom.comp : {ι : 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] →
                  {ι₁ : Type u_5} →
                    {M₁ : Type u_6} →
                      {N₁ : Type u_7} →
                        {ι₂ : Type u_8} →
                          {M₂ : Type u_9} →
                            {N₂ : Type u_10} →
                              [inst_5 : AddCommGroup M₁] →
                                [inst_6 : Module R M₁] →
                                  [inst_7 : AddCommGroup N₁] →
                                    [inst_8 : Module R N₁] →
                                      [inst_9 : AddCommGroup M₂] →
                                        [inst_10 : Module R M₂] →
                                          [inst_11 : AddCommGroup N₂] →
                                            [inst_12 : Module R N₂] →
                                              {P : RootPairing ι R M N} →
                                                {P₁ : RootPairing ι₁ R M₁ N₁} →
                                                  {P₂ : RootPairing ι₂ R M₂ N₂} → P₁.Hom P₂ → P.Hom P₁ → P.Hom P₂
-- Mathlib.Algebra.Group.Prod
MonoidHom.snd.eq_1 : ∀ (M : Type u_3) (N : Type u_4) [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.snd M N = { toFun := Prod.snd, map_one' := ⋯, map_mul' := ⋯ }
-- Std.Http.Data.Method
Std.Http.Method.checkin.sizeOf_spec : sizeOf Std.Http.Method.checkin = 1
-- Lean.Meta.Tactic.Grind.Attr
_private.Lean.Meta.Tactic.Grind.Attr.0.Lean.Meta.Grind.Extension.eraseInjectiveAttr : Lean.Meta.Grind.Extension → Lean.Name → Lean.MetaM Unit
-- Mathlib.GroupTheory.GroupAction.Basic
/-- A isomorphism between the stabilizers of two elements in the same orbit.  -/
MulAction.stabilizerEquivStabilizerOfOrbitRel : {G : Type u_1} →
  {α : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G α] →
        {a b : α} → (MulAction.orbitRel G α) a b → ↥(MulAction.stabilizer G a) ≃* ↥(MulAction.stabilizer G b)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inl_add : ∀ {R : Type u_3} (A : Type u_4) [inst : Add R] [inst_1 : AddZeroClass A] (r₁ r₂ : R),
  Unitization.inl (r₁ + r₂) = Unitization.inl r₁ + Unitization.inl r₂
-- Lean.Expr
Lean.instInhabitedMVarIdSet : Inhabited Lean.MVarIdSet
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.union_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₂.Equiv m₃ → (m₁ ∪ m₂).Equiv (m₁ ∪ m₃)
-- Mathlib.Algebra.Order.Group.Finset
Finset.fold_max_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : LinearOrder M] [inst_1 : Add M] [AddRightMono M] (s : Finset ι) (a : WithBot M)
  (f : ι → M), Finset.fold max ⊥ (fun i => ↑(f i) + a) s = Finset.fold max ⊥ (WithBot.some ∘ f) s + a
-- Mathlib.Topology.Homeomorph.Lemmas
/-- A bijection between discrete topological spaces induces a homeomorphism.  -/
Homeomorph.ofDiscrete : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → [DiscreteTopology X] → [DiscreteTopology Y] → X ≃ Y → X ≃ₜ Y
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- Auxiliary lemma used as an argument to `CliffordAlgebra.changeForm`  -/
CliffordAlgebra.changeForm.zero_proof : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, LinearMap.BilinMap.toQuadraticMap 0 = Q - Q
-- Init.Internal.Order.Basic
Lean.Order.lfp_postfixed : ∀ {α : Sort u} [inst : Lean.Order.CompleteLattice α] {f : α → α} {hm : Lean.Order.monotone f},
  Lean.Order.PartialOrder.rel (Lean.Order.lfp f) (f (Lean.Order.lfp f))
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_eq_one_iff_of_le_one' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : PartialOrder N] {f : ι → N} {s : Finset ι}
  [MulLeftMono N], (∀ i ∈ s, f i ≤ 1) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
-- Lean.Message
Lean.TraceResult.failure.sizeOf_spec : sizeOf Lean.TraceResult.failure = 1
-- Aesop.Frontend.Extension
Aesop.Frontend.getDeclaredGlobalRuleSets : Lean.CoreM (Array (Aesop.RuleSetName × Aesop.GlobalRuleSet × Lean.Name × Lean.Name))
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.le_one : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) (i : ι) (x : M), (f i) x ≤ 1
-- Mathlib.RingTheory.Ideal.Maps
Algebra.idealMap_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : Semiring S] [inst_2 : Algebra R S] (I : Ideal R)
  (x y : ↥I), (Algebra.idealMap S I) (x * y) = (Algebra.idealMap S I) x * (Algebra.idealMap S I) y
-- Std.Sat.AIG.Basic
Std.Sat.AIG.RefVecEntry.mk.inj : ∀ {α : Type} {inst : DecidableEq α} {inst_1 : Hashable α} {inst_2 : DecidableEq α} {w : ℕ} {aig : Std.Sat.AIG α}
  {vec : aig.RefVec w} {aig_1 : Std.Sat.AIG α} {vec_1 : aig_1.RefVec w},
  { aig := aig, vec := vec } = { aig := aig_1, vec := vec_1 } → aig = aig_1 ∧ vec ≍ vec_1
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.restrict_univ : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β},
  κ.restrict ⋯ = κ
-- Init.Data.SInt.Lemmas
Int64.ofInt_int16ToInt : ∀ (x : Int16), Int64.ofInt x.toInt = x.toInt64
-- Std.Http.Data.Method
Std.Http.Method.label.sizeOf_spec : sizeOf Std.Http.Method.label = 1
-- Mathlib.Order.Filter.CountablyGenerated
Filter.Nat.inhabitedCountableFilterBasis : Inhabited (Filter.CountableFilterBasis ℕ)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.InitResults.errors : {α : Type} → Lean.Meta.LazyDiscrTree.InitResults α → Array Lean.Meta.LazyDiscrTree.ImportFailure
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.hasCompactSupport : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n), HasCompactSupport ⇑f
-- Mathlib.NumberTheory.ClassNumber.Finite
ClassGroup.mem_finsetApprox : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (bS : Module.Basis ι R S) (adm : abv.IsAdmissible) [inst_6 : Infinite R] [inst_7 : DecidableEq R] {x : R},
  x ∈ ClassGroup.finsetApprox bS adm ↔
    ∃ i j, i ≠ j ∧ (ClassGroup.distinctElems bS adm) i - (ClassGroup.distinctElems bS adm) j = x
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_one : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N], TensorProduct.map 1 1 = 1
-- Mathlib.Data.Rel
SetRel.isTrans_empty : ∀ {α : Type u_1}, ∅.IsTrans
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.Spec_basicOpen : ∀ {R : CommRingCat} (f : ↑R), AlgebraicGeometry.IsAffineOpen (PrimeSpectrum.basicOpen f)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.transport_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (i : F ≅ G) (X Y : C),
  CategoryTheory.Functor.OplaxMonoidal.δ G X Y =
    CategoryTheory.CategoryStruct.comp (i.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (i.hom.app X) (i.hom.app Y)))
-- Mathlib.Algebra.Homology.DerivedCategory.Fractions
DerivedCategory.instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)).HasLeftCalculusOfFractions