mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- Given a homology map data `ψ : HomologyMapData φ h₁ h₂` such that
`h₁.left`, `h₁.right`, `h₂.left` and `h₂.right` are all preserved by a functor `F`, this is
the induced homology map data for the morphism `F.mapShortComplex.map φ`.  -/
CategoryTheory.ShortComplex.HomologyMapData.map : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {S₁ S₂ : CategoryTheory.ShortComplex C} →
              {φ : S₁ ⟶ S₂} →
                {h₁ : S₁.HomologyData} →
                  {h₂ : S₂.HomologyData} →
                    CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂ →
                      (F : CategoryTheory.Functor C D) →
                        [inst_4 : F.PreservesZeroMorphisms] →
                          [inst_5 : h₁.left.IsPreservedBy F] →
                            [inst_6 : h₁.right.IsPreservedBy F] →
                              [inst_7 : h₂.left.IsPreservedBy F] →
                                [inst_8 : h₂.right.IsPreservedBy F] →
                                  CategoryTheory.ShortComplex.HomologyMapData (F.mapShortComplex.map φ) (h₁.map F)
                                    (h₂.map F)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The adjunction between `left` and `right`.  -/
CategoryTheory.Bicategory.RightAdjoint.adj : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {left : a ⟶ b} →
        (self : CategoryTheory.Bicategory.RightAdjoint left) → CategoryTheory.Bicategory.Adjunction left self.right
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.netEntropyInfEntourage_monotone : ∀ {X : Type u_1} (T : X → X) (U : SetRel X X), Monotone fun F => Dynamics.netEntropyInfEntourage T F U
-- Mathlib.Analysis.Complex.Trigonometric
Real.cosh_neg : ∀ (x : ℝ), Real.cosh (-x) = Real.cosh x
-- Mathlib.Data.List.Sort
/-- An alternative definition of `orderedInsert` using `takeWhile` and `dropWhile`.  -/
List.orderedInsert_eq_take_drop : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] (a : α) (l : List α),
  List.orderedInsert r a l = List.takeWhile (fun b => decide ¬r a b) l ++ a :: List.dropWhile (fun b => decide ¬r a b) l
-- Mathlib.Data.Vector3
exists_vector_succ : ∀ {α : Type u_1} {n : ℕ} (f : Vector3 α n.succ → Prop), Exists f ↔ ∃ x v, f (Vector3.cons x v)
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Certify one matrix entry lookup `BirdDet.get n A i j`.  -/
Mathlib.Tactic.Determinant.certEntry : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} → ℕ → ℕ → Mathlib.Tactic.Determinant.CertM rα (Mathlib.Tactic.Determinant.Cert rα)
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.verschiebungPoly.eq_1 : ∀ (n : ℕ), WittVector.verschiebungPoly n = if n = 0 then 0 else MvPolynomial.X (n - 1)
-- Mathlib.Data.Rel
SetRel.image_core_gc : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β}, GaloisConnection R.image R.core
-- Init.Core
false_of_true_eq_false : True = False → False
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.modEq_of_xn_modEq : ∀ {a : ℕ} (a1 : 1 < a) {i j n : ℕ},
  0 < i → i ≤ n → Pell.xn a1 j ≡ Pell.xn a1 i [MOD Pell.xn a1 n] → j ≡ i [MOD 4 * n] ∨ j + i ≡ 0 [MOD 4 * n]
-- Mathlib.Topology.Order.IsLUB
IsGLB.mem_lowerBounds_of_tendsto : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : Preorder γ] [inst_4 : TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ},
  MonotoneOn f s → IsGLB s a → Filter.Tendsto f (nhdsWithin a s) (nhds b) → b ∈ lowerBounds (f '' s)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G) (c : CategoryTheory.Limits.Cone F) (d : CategoryTheory.Limits.Cone G)
  (w : (CategoryTheory.Limits.Cone.postcompose α.hom).obj c ≅ d),
  CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso α c d w =
    (CategoryTheory.Limits.IsLimit.postcomposeHomEquiv α c).symm.trans (CategoryTheory.Limits.IsLimit.equivIsoLimit w)
-- Init.Data.Nat.ToString
Nat.two_eq_digitChar : ∀ {n : ℕ}, '2' = n.digitChar ↔ n = 2
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
lowerHemicontinuousOn_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  LowerHemicontinuousOn (fun x => {f x}) s ↔ ContinuousOn f s
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.homMk'_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T),
  f.homMk' (CategoryTheory.CategoryStruct.id f.right) = CategoryTheory.eqToHom ⋯
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_sub : ∀ (x y : ℝ), Real.cos (x - y) = Real.cos x * Real.cos y + Real.sin x * Real.sin y
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- When `p ∤ a`, then `legendreSym p a = 1` iff `a` is a square mod `p`.  -/
legendreSym.eq_one_iff : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {a : ℤ}, ↑a ≠ 0 → (legendreSym p a = 1 ↔ IsSquare ↑a)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contSupp_comp : ∀ (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.contSupp (Turing.PartrecToTM2.Cont'.comp f k) = Turing.PartrecToTM2.codeSupp f k
-- Std.Http.Protocol.H1.Event
/-- Requests that the connection be closed.
 -/
Std.Http.Protocol.H1.Event.close : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Event dir
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Left map, from `J.L` to `C`  -/
CategoryTheory.Limits.MulticospanIndex.left : {J : CategoryTheory.Limits.MulticospanShape} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Limits.MulticospanIndex J C → J.L → C
-- Mathlib.Order.Heyting.Regular
Heyting.IsRegular.disjoint_compl_left_iff : ∀ {α : Type u_1} [inst : HeytingAlgebra α] {a b : α}, Heyting.IsRegular a → (Disjoint aᶜ b ↔ b ≤ a)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_1 : ∀ {R : Type u_1} [inst : Semiring R], SkewPolynomial.C 1 = 1
-- Mathlib.Analysis.Normed.MulAction
instENormSMulClass : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedRing α] [inst_1 : SeminormedAddGroup β] [inst_2 : SMul α β]
  [NormSMulClass α β], ENormSMulClass α β
-- Mathlib.RingTheory.IdealFilter.Basic
/-- We say that an element `m : M` is `F`-torsion if it is annihilated by some ideal belonging to
the filter `F`.  -/
IdealFilter.IsTorsionElem : {A : Type u_1} → [inst : Ring A] → IdealFilter A → {M : Type u_2} → [inst_1 : AddCommMonoid M] → [Module A M] → M → Prop
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.Hom.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {HP HP' : TopPair.HomologyPretheory C c} →
            (homₚ : (i : ι) → HP.Hₚ i ⟶ HP'.Hₚ i) →
              (hom : (i : ι) → HP.H i ⟶ HP'.H i) →
                autoParam
                    (∀ (i : ι),
                      CategoryTheory.CategoryStruct.comp (HP.iso i).hom (TopPair.incl.whiskerLeft (homₚ i)) =
                        CategoryTheory.CategoryStruct.comp (hom i) (HP'.iso i).hom)
                    TopPair.HomologyPretheory.Hom.iso_comm._autoParam →
                  autoParam
                      (∀ (i j : ι),
                        CategoryTheory.CategoryStruct.comp (HP.δ i j) (TopPair.proj₂.whiskerLeft (hom j)) =
                          CategoryTheory.CategoryStruct.comp (homₚ i) (HP'.δ i j))
                      TopPair.HomologyPretheory.Hom.w._autoParam →
                    HP.Hom HP'
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The canonical Coxeter system on the Coxeter group associated to `M`.  -/
CoxeterMatrix.toCoxeterSystem : {B : Type u_1} → (M : CoxeterMatrix B) → CoxeterSystem M M.Group
-- Mathlib.RingTheory.Algebraic.StronglyTranscendental
IsStronglyTranscendental.of_isLocalization : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] (M : Submonoid S) [IsLocalization M T]
  [IsScalarTower R S T] {x : S}, IsStronglyTranscendental R x → IsStronglyTranscendental R ((algebraMap S T) x)
-- Init.WFExtrinsicFix
WellFounded.partialExtrinsicFix₃_eq_partialExtrinsicFix : ∀ {α : Sort u_2} {β : α → Sort u_4} {γ : (a : α) → β a → Sort u_3} {C₃ : (a : α) → (b : β a) → γ a b → Sort u_1}
  [inst : ∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)]
  {R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
  {F :
    (a : α) →
      (b : β a) →
        (c : γ a b) → ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c}
  {a : α} {b : β a} {c : γ a b},
  Acc R ⟨a, ⟨b, c⟩⟩ →
    WellFounded.partialExtrinsicFix₃ R F a b c =
      WellFounded.partialExtrinsicFix R (fun p r => F p.fst p.snd.fst p.snd.snd fun a' b' c' hR => r ⟨a', ⟨b', c'⟩⟩ hR)
        ⟨a, ⟨b, c⟩⟩
-- Std.Http.Data.Method
Std.Http.Method.lock.sizeOf_spec : sizeOf Std.Http.Method.lock = 1
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.eq_of_add_pow : ∀ {α : Type u_1} {a a' b b' : α} [inst : Ring α] [NoZeroDivisors α] (n : ℕ),
  a = b → (a' - b') ^ n - (a - b) = 0 → a' = b'
-- Init.Prelude
/-- Constructs a synthetic `atom` with no source info.  -/
Lean.mkAtom : String → Lean.Syntax
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_inter_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Iic a ∩ Set.Ioi b = Set.Ioc b a
-- Mathlib.Order.CompleteLattice.Basic
/-- Pullback a `CompleteLattice` along an injection.  -/
Function.Injective.completeLattice : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : SupSet α] →
              [inst_5 : InfSet α] →
                [inst_6 : Top α] →
                  [inst_7 : Bot α] →
                    [inst_8 : CompleteLattice β] →
                      (f : α → β) →
                        Function.Injective f →
                          (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                            (∀ {x y : α}, f x < f y ↔ x < y) →
                              (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
                                (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
                                  (∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) →
                                    (∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) → f ⊤ = ⊤ → f ⊥ = ⊥ → CompleteLattice α
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_filter_of_ne : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M} {p : ι → Prop}
  [inst_1 : DecidablePred p], (∀ x ∈ s, f x ≠ 0 → p x) → ∑ x ∈ s with p x, f x = ∑ x ∈ s, f x
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {J : Type w} →
        [inst_1 : LinearOrder J] →
          [inst_2 : SuccOrder J] →
            [inst_3 : OrderBot J] →
              [inst_4 : WellFoundedLT J] →
                {X Y : C} →
                  {f : X ⟶ Y} → W.TransfiniteCompositionOfShape J f → CategoryTheory.TransfiniteCompositionOfShape J f
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.MemSobolev.congr_simp : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] [inst_7 : CompleteSpace F] (s s_1 : ℝ),
  s = s_1 →
    ∀ (p p_1 : ENNReal) (e_p : p = p_1) [hp : Fact (1 ≤ p)] (f f_1 : TemperedDistribution E F),
      f = f_1 → TemperedDistribution.MemSobolev s p f = TemperedDistribution.MemSobolev s_1 p_1 f_1
-- Mathlib.Topology.Order.Lattice
Filter.Tendsto.inf_nhds' : ∀ {L : Type u_1} [inst : TopologicalSpace L] {α : Type u_3} {l : Filter α} {f g : α → L} {x y : L} [inst_1 : Min L]
  [ContinuousInf L], Filter.Tendsto f l (nhds x) → Filter.Tendsto g l (nhds y) → Filter.Tendsto (f ⊓ g) l (nhds (x ⊓ y))
-- Mathlib.RepresentationTheory.FDRep
/-- All hom spaces are finite dimensional.  -/
FDRep.instFiniteDimensionalHom : ∀ {k : Type u} {G : Type v} [inst : Field k] [inst_1 : Monoid G] (V W : FDRep k G), FiniteDimensional k (V ⟶ W)
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instMax : {α : Type u_1} → [inst : LE α] → Max (LowerSet α)
-- Mathlib.Condensed.Light.Monoidal
LightCondensed.instMonoidalClosedLightCondMod : (R : Type u) → [inst : CommRing R] → CategoryTheory.MonoidalClosed (LightCondMod R)
-- Mathlib.Order.Filter.Cofinite
boundary_le_cofinite : ∀ {α : Type u_2} (f : Filter α), Coheyting.boundary f ≤ Filter.cofinite
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The triangle consisting of the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.BinaryBiconeMorphism.wfst_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B)
  {Z : C} (h : P ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp B.fst h) =
    CategoryTheory.CategoryStruct.comp A.fst h
-- Mathlib.CategoryTheory.Limits.Final.Type
/-- Given `P : D ⥤ Type w` and `F : C ⥤ D`, this is the obvious map
`(F ⋙ P).ColimitType → P.ColimitType`.  -/
CategoryTheory.Functor.colimitTypePrecomp : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (P : CategoryTheory.Functor D (Type w)) → (F.comp P).ColimitType → P.ColimitType
-- Mathlib.Algebra.GCDMonoid.Basic
/-- The GCD is a divisor of the first element.  -/
GCDMonoid.gcd_dvd_left : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : GCDMonoid α] (a b : α), gcd a b ∣ a
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.comm_symm : ∀ (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.comm R M N).symm = TensorProduct.comm R N M
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.monoidalComp_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.monoidalComp f g = CategoryTheory.CategoryStruct.comp f g
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutIsoUnopPullback f g).inv.op
      (CategoryTheory.Limits.pullback.fst f.op g.op) =
    (CategoryTheory.Limits.pushout.inl f g).op
-- Aesop.Rule.Basic
Aesop.Rule.instOrd : {α : Type} → Ord (Aesop.Rule α)
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.Quotient.eq_1 : ∀ (G : Type u_1) (α : Type u_2) [inst : AddGroup G] [inst_1 : AddAction G α],
  AddAction.orbitRel.Quotient G α = Quotient (AddAction.orbitRel G α)
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.iterFromIdx_eq_toIter_iterFromIdxM : ∀ {β : Type w} {array : Array β} {pos : ℕ}, array.iterFromIdx pos = (array.iterFromIdxM Id pos).toIter
-- Lean.Meta.ACLt
_private.Lean.Meta.ACLt.0.Lean.Meta.ACLt.main.ltPair : Lean.Meta.ACLt.ReduceMode → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.AState.mk : Array (Lean.Expr × Lean.Expr) → Lean.ExprMap Lean.Expr → Batteries.Tactic.GeneralizeProofs.AState
-- Mathlib.Order.SetAccumulate
Set.accumulate_subset_iUnion : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : LE α] (x : α), Set.accumulate s x ⊆ ⋃ i, s i
-- Mathlib.Computability.Ackermann
ack.eq_def : ∀ (x x_1 : ℕ),
  ack x x_1 =
    match x, x_1 with
    | 0, n => n + 1
    | m.succ, 0 => ack m 1
    | m.succ, n.succ => ack m (ack (m + 1) n)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_filter_ne_zero : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {f : ι → M} (s : Finset ι)
  [inst_1 : (x : ι) → Decidable (f x ≠ 0)], ∑ x ∈ s with f x ≠ 0, f x = ∑ x ∈ s, f x
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.toL1_smul' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_5} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 β] [inst_3 : IsBoundedSMul 𝕜 β] (f : α → β)
  (hf : MeasureTheory.Integrable f μ) (k : 𝕜),
  MeasureTheory.Integrable.toL1 (k • f) ⋯ = k • MeasureTheory.Integrable.toL1 f hf
-- Std.Http.Data.Method
Std.Http.Method.patch.sizeOf_spec : sizeOf Std.Http.Method.patch = 1
-- Mathlib.InformationTheory.Hamming
hammingNorm_smul : ∀ {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → Zero (β i)] [inst_3 : Zero α] [inst_4 : (i : ι) → SMulWithZero α (β i)] {k : α},
  (∀ (i : ι), IsSMulRegular (β i) k) → ∀ (x : (i : ι) → β i), hammingNorm (k • x) = hammingNorm x
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.DSimpCacheKey.variant : Lean.Elab.Tactic.Grind.DSimpCacheKey → Lean.Name
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_apply_eq_zero' : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : ι → MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ((MeasureTheory.Measure.sum μ) s = 0 ↔ ∀ (i : ι), (μ i) s = 0)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α}, k ∉ t → l.contains k = false → (t.insertManyIfNewUnit l).getKey? k = none
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.leftInverse_symm : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (e : A ≃⋆ₐ[R] B),
  Function.LeftInverse ⇑e.symm ⇑e
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.unpackSign_def : ∀ {spec : Float.Model.Format} (b : BitVec spec.numBits),
  Float.Model.UnpackedFloat.unpackSign b = BitVec.extractLsb' (spec.mantissaBitsWithoutImplicit + spec.exponentBits) 1 b
-- Aesop.Tree.Data
Aesop.instInhabitedRappId : Inhabited Aesop.RappId
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.ofFunctor : {C D : CategoryTheory.Cat} → CategoryTheory.Functor ↑C ↑D → C.Hom D
-- Mathlib.RingTheory.Congruence.Defs
/-- Defining the quotient by a congruence relation of a type with addition and multiplication.  -/
RingCon.Quotient : {R : Type u_1} → [inst : Add R] → [inst_1 : Mul R] → RingCon R → Type u_1
-- Mathlib.Data.ZMod.Defs
ZMod.decidableEq : (n : ℕ) → DecidableEq (ZMod n)
-- Init.Data.Vector.Lemmas
Vector.findFinIdx?_toArray : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n},
  Array.findFinIdx? p xs.toArray = Option.map (Fin.cast ⋯) (Vector.findFinIdx? p xs)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqLitValue.beq : Lean.Compiler.LCNF.LitValue → Lean.Compiler.LCNF.LitValue → Bool
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- An alternative statement of the Stone-Weierstrass theorem.

If `A` is a subalgebra of `C(X, ℝ)` which separates points (and `X` is compact),
every real-valued continuous function on `X` is a uniform limit of elements of `A`.
 -/
ContinuousMap.continuousMap_mem_subalgebra_closure_of_separatesPoints : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)),
  A.SeparatesPoints → ∀ (f : C(X, ℝ)), f ∈ A.topologicalClosure
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` creates colimits, then `F : Cᵒᵖ ⥤ D` creates limits.  -/
CategoryTheory.Limits.createsLimitsOfSizeOfRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ D) →
          [CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp] →
            CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.unitBallBall_target : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {P : Type u_2}
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor E P] (c : P) (r : ℝ) (hr : 0 < r),
  (OpenPartialHomeomorph.unitBallBall c r hr).target = Metric.ball c r
-- Mathlib.CategoryTheory.Sites.Over
/-- Applying `overMapPullback` to the identity map gives the identity functor.  -/
CategoryTheory.GrothendieckTopology.overMapPullbackId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u') →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          (X : C) →
            J.overMapPullback A (CategoryTheory.CategoryStruct.id X) ≅
              CategoryTheory.Functor.id (CategoryTheory.Sheaf (J.over X) A)
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `locallyLipschitzOn_neg_iff`. -/
LocallyLipschitzOn.of_neg : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {f : α → E}
  {s : Set α}, LocallyLipschitzOn s (-f) → LocallyLipschitzOn s f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.le_maxKey_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : t.contains k = true), (cmp k (t.maxKey ⋯)).isLE = true
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.modifyInfo : (Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Lean.Meta.Grind.Arith.Cutsat.ToIntInfo) →
  Lean.Meta.Grind.Arith.Cutsat.ToIntM Unit
-- Init.Data.Array.Attach
Array.foldr_wfParam : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β → β} {x : β},
  Array.foldr f x (wfParam xs) = Array.foldr f x xs.attach.unattach
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Lift an algebra homomorphism that maps polynomials `φ : K[X] →ₐ[S] R[X]`
to a `K⟮X⟯ →ₐ[S] R⟮X⟯`,
on the condition that `φ` maps non-zero-divisors to non-zero-divisors,
by mapping both the numerator and denominator and quotienting them.  -/
RatFunc.mapAlgHom : {K : Type u} →
  [inst : CommRing K] →
    [inst_1 : IsDomain K] →
      {R : Type u_2} →
        {S : Type u_3} →
          [inst_2 : CommRing R] →
            [inst_3 : IsDomain R] →
              [inst_4 : CommSemiring S] →
                [inst_5 : Algebra S (Polynomial K)] →
                  [inst_6 : Algebra S (Polynomial R)] →
                    (φ : Polynomial K →ₐ[S] Polynomial R) →
                      nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R)) →
                        RatFunc K →ₐ[S] RatFunc R