mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.getParams : Lean.Compiler.LCNF.Alt Lean.Compiler.LCNF.Purity.pure → Array (Lean.Compiler.LCNF.Param Lean.Compiler.LCNF.Purity.pure)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapHomologyIso'.congr_simp : ∀ {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 : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S.HasHomology]
  [inst_6 : (S.map F).HasHomology] [inst_7 : F.PreservesRightHomologyOf S], S.mapHomologyIso' F = S.mapHomologyIso' F
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion.0.Tactic.ComputeAsymptotics.Seq.FriendlyOperation.coind_comp_friend_left.match_1_1.splitter : {α : Type u_1} →
  (motive : (Stream'.Seq α → Stream'.Seq α) → Prop) →
    (motive_1 : Option (α × Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation × Subtype motive) → Sort u_2) →
      (x : Option (α × Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation × Subtype motive)) →
        (Unit → motive_1 none) →
          ((hd : α) →
              (opf' : Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation) →
                (op' : Subtype motive) → motive_1 (some (hd, opf', op'))) →
            motive_1 x
-- Init.Data.String.PosRaw
String.instHAddCharRaw : HAdd Char String.Pos.Raw String.Pos.Raw
-- Mathlib.Analysis.Complex.JensenFormula
_private.Mathlib.Analysis.Complex.JensenFormula.0.continuousAt_herglotzLogIntegrand : ∀ {w ρ z : ℂ}, z ≠ w → z ≠ ρ → ContinuousAt (herglotzLogIntegrand✝ w ρ) z
-- Mathlib.Analysis.Seminorm
/-- A seminorm is uniformly continuous if `p.ball 0 r ∈ 𝓝 0` for *all* `r > 0`.
Over a `NontriviallyNormedField` it is actually enough to check that this is true
for *some* `r`, see `Seminorm.uniformContinuous`.  -/
Seminorm.uniformContinuous_of_forall : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E]
  [inst_3 : UniformSpace E] [IsUniformAddGroup E] {p : Seminorm 𝕝 E},
  (∀ r > 0, p.ball 0 r ∈ nhds 0) → UniformContinuous ⇑p
-- Init.Data.UInt.Lemmas
UInt8.sub_left_inj : ∀ {a b : UInt8} (c : UInt8), a - c = b - c ↔ a = b
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.intNorm.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)),
  NumberField.mixedEmbedding.fundamentalCone.intNorm a =
    ((Algebra.norm ℤ) ↑(NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet a)).natAbs
-- Mathlib.Data.Part
Part.sdiff_mem_sdiff : ∀ {α : Type u_1} [inst : SDiff α] (a b : Part α) (ma mb : α), ma ∈ a → mb ∈ b → ma \ mb ∈ a \ b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_erase_le_maxKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false →
    ∀ {fallback : α},
      (compare ((Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.maxKeyD fallback) (t.maxKeyD fallback)).isLE = true
-- Mathlib.Analysis.Meromorphic.Basic
/-- Derivatives of meromorphic functions are meromorphic.
 -/
MeromorphicAt.deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜}, MeromorphicAt f x → MeromorphicAt (deriv f) x
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.addHaarScalarFactor_eq_mul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ ν : MeasureTheory.Measure G) [inst_5 : μ.IsAddHaarMeasure]
  [inst_6 : ν.IsAddHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsAddLeftInvariant],
  μ'.addHaarScalarFactor ν = μ'.addHaarScalarFactor μ * μ.addHaarScalarFactor ν
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.instSliceableRccSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.instSliceableRccSlice._auto_1) →
      Std.Rcc.Sliceable (Std.DTreeMap α β cmp) α (Std.DTreeMap.Internal.RccSlice α β)
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on' : ∀ {R : Type u_1} [inst : AddCommGroup R] {f g : ℕ → R} (s : Set ℕ),
  (∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) →
    0 ∉ s →
      ((∀ n ∈ s, ∑ i ∈ n.divisors, f i = g n) ↔
        ∀ n ∈ s, ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 • g x.2 = f n)
-- Mathlib.Order.Filter.Basic
/-- Eta-expanded form of `Filter.EventuallyEq.star` -/
Filter.EventuallyEq.fun_star : ∀ {α : Type u} {R : Type u_2} [inst : Star R] {f g : α → R} {l : Filter α},
  f =ᶠ[l] g → (fun i => star (f i)) =ᶠ[l] fun i => star (g i)
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balance1.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (x_1 : α) →
        (x_2 : RBTree.RBNode α) →
          ((a : RBTree.RBNode α) →
              (x : α) →
                (b : RBTree.RBNode α) →
                  (y : α) →
                    (c : RBTree.RBNode α) →
                      (z : α) →
                        (d : RBTree.RBNode α) →
                          motive
                            (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c) z
                            d) →
            ((a : RBTree.RBNode α) →
                (x : α) →
                  (b : RBTree.RBNode α) →
                    (y : α) →
                      (c : RBTree.RBNode α) →
                        (z : α) →
                          (d : RBTree.RBNode α) →
                            (∀ (a_1 : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
                                a = RBTree.RBNode.node RBTree.RBColor.red a_1 x b → False) →
                              motive
                                (RBTree.RBNode.node RBTree.RBColor.red a x
                                  (RBTree.RBNode.node RBTree.RBColor.red b y c))
                                z d) →
              ((a : RBTree.RBNode α) →
                  (x : α) →
                    (b : RBTree.RBNode α) →
                      (∀ (a_1 : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
                          a =
                              RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a_1 x b) y
                                c →
                            False) →
                        (∀ (a_1 : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
                            a =
                                RBTree.RBNode.node RBTree.RBColor.red a_1 x
                                  (RBTree.RBNode.node RBTree.RBColor.red b y c) →
                              False) →
                          motive a x b) →
                motive x x_1 x_2
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.counit_comp_single : ∀ {R : Type u_1} {n : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : n → Type u_3}
  [inst_3 : (i : n) → AddCommMonoid (A i)] [inst_4 : (i : n) → Module R (A i)]
  [inst_5 : (i : n) → CoalgebraStruct R (A i)] (i : n),
  CoalgebraStruct.counit ∘ₗ LinearMap.single R A i = CoalgebraStruct.counit
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The cone corresponding to a `SieveCompatible` family of elements, dot notation enabled.  -/
CategoryTheory.Presieve.FamilyOfElements.SieveCompatible.cone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {P : CategoryTheory.Functor Cᵒᵖ A} →
          {X : C} →
            {S : CategoryTheory.Sieve X} →
              {E : Aᵒᵖ} →
                {x : CategoryTheory.Presieve.FamilyOfElements (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows} →
                  x.SieveCompatible → CategoryTheory.Limits.Cone (S.arrows.diagram.op.comp P)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.map_mul_right_ae : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G)
  [μ.IsMulRightInvariant] (x : G), Filter.map (fun h => h * x) (MeasureTheory.ae μ) = MeasureTheory.ae μ
-- Mathlib.Algebra.Order.Monoid.ToMulBot
WithZero.toMulBot_coe : ∀ {α : Type u} [inst : Add α] (x : Multiplicative α),
  WithZero.toMulBot ↑x = Multiplicative.ofAdd ↑(Multiplicative.toAdd x)
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signBijAux_mem : ∀ {n : ℕ} {f : Equiv.Perm (Fin n)}, ∀ a ∈ Equiv.Perm.finPairsLT n, f.signBijAux a ∈ Equiv.Perm.finPairsLT n
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.mapComposableArrows₂.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (i : ι),
  HomologicalComplex.HomologySequence.mapComposableArrows₂ φ i =
    CategoryTheory.ComposableArrows.homMk₂ (HomologicalComplex.homologyMap φ.τ₁ i)
      (HomologicalComplex.homologyMap φ.τ₂ i) (HomologicalComplex.homologyMap φ.τ₃ i) ⋯ ⋯
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.u_unique : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u →
    ∀ {l' : α → β} {u' : β → α}, GaloisConnection l' u' → (∀ (a : α), l a = l' a) → ∀ {b : β}, u b = u' b
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsCartesian.fac : ∀ {𝒮 : 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) [inst_2 : p.IsCartesian f φ] {a' : 𝒳}
  (φ' : a' ⟶ b) [inst_3 : p.IsHomLift f φ'],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCartesian.map p f φ φ') φ = φ'
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
ContinuousAlgEquiv.cast.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_5} {A : ι → Type u_6} [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] [inst_3 : (i : ι) → TopologicalSpace (A i)] {i j : ι} (h : i = j),
  ContinuousAlgEquiv.cast h = ContinuousAlgEquiv.cast h
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.instUnique.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Unique M] [inst_1 : Unique N] [inst_2 : Mul M] [inst_3 : Mul N]
  [inst_4 : TopologicalSpace M] [inst_5 : TopologicalSpace N],
  ContinuousMulEquiv.instUnique = { default := ContinuousMulEquiv.ofUnique, uniq := ⋯ }
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise multiplication of
`f` and `g`, which monovary together, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not monovary together. Stated by permuting the entries of `g`.  -/
Monovary.sum_comp_perm_mul_lt_sum_mul_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {σ : Equiv.Perm ι} {f g : ι → α} [inst_4 : Fintype ι],
  Monovary f g → (∑ i, f (σ i) * g i < ∑ i, f i * g i ↔ ¬Monovary (f ∘ ⇑σ) g)
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.instSMulCommClassSubtypeMem : ∀ {M' : Type u_1} {α : Type u_2} {β : Type u_3} {S' : Type u_4} [inst : SetLike S' M'] (s : S') [inst_1 : SMul M' β]
  [inst_2 : SMul α β] [SMulCommClass M' α β], SMulCommClass (↥s) α β
-- Mathlib.Topology.Algebra.Group.Basic
IsOpen.right_addCoset : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {U : Set G},
  IsOpen U → ∀ (x : G), IsOpen (AddOpposite.op x +ᵥ U)
-- Mathlib.Analysis.InnerProductSpace.Basic
ext_iff_inner_right : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, x = y ↔ ∀ (v : E), inner 𝕜 x v = inner 𝕜 y v
-- Mathlib.Analysis.Normed.Lp.Matrix
Matrix.toLpLin_pow : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] (p : ENNReal)
  (A : Matrix n n R) (k : ℕ), (Matrix.toLpLin p p) (A ^ k) = (Matrix.toLpLin p p) A ^ k
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.sec_spec : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  {f : S.LocalizationMap N} (z : N), z + f ↑(f.sec z).2 = f (f.sec z).1
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.integrable : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} [BorelSpace E]
  [FiniteDimensional ℝ E] [MeasureTheory.IsLocallyFiniteMeasure μ], MeasureTheory.Integrable (↑f) μ
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- **Church-Rosser theorem** for word reduction: If `w1 w2 w3` are words such that `w1` reduces
to `w2` and `w3` respectively, then there is a word `w4` such that `w2` and `w3` reduce to `w4`
respectively. This is also known as Newman's diamond lemma.  -/
FreeAddGroup.Red.church_rosser : ∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)},
  FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₁ L₃ → Relation.Join FreeAddGroup.Red L₂ L₃
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
dist_iteratedFDerivWithin_one : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E}
  {x : E} (f g : E → F) {y : E},
  UniqueDiffWithinAt 𝕜 s x →
    UniqueDiffWithinAt 𝕜 t y →
      dist (iteratedFDerivWithin 𝕜 1 f s x) (iteratedFDerivWithin 𝕜 1 g t y) =
        dist (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 g t y)
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Balanced.below.nil : ∀ {α : Type u_1} {motive : (a : RBTree.RBNode α) → (a_1 : RBTree.RBColor) → (a_2 : ℕ) → a.Balanced a_1 a_2 → Prop},
  RBTree.RBNode.Balanced.below ⋯
-- Mathlib.Analysis.Calculus.Deriv.Inv
DifferentiableWithinAt.div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'},
  DifferentiableWithinAt 𝕜 c s x → DifferentiableWithinAt 𝕜 d s x → d x ≠ 0 → DifferentiableWithinAt 𝕜 (c / d) s x
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.IsReduced.of_openCover : ∀ (X : AlgebraicGeometry.Scheme) (𝒰 : X.OpenCover) [∀ (i : 𝒰.I₀), AlgebraicGeometry.IsReduced (𝒰.X i)],
  AlgebraicGeometry.IsReduced X
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α],
  m.WF → ∀ {l : List α} {k : α}, k ∉ m → l.contains k = false → (m.insertMany l).get! k = default
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.lintegral_fn_integral_sub_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} [inst_1 : NormedSpace ℝ E] ⦃f g : γ → E⦄ (F : E → ENNReal),
  MeasureTheory.Integrable f ((η.comp κ) a) →
    MeasureTheory.Integrable g ((η.comp κ) a) →
      ∫⁻ (x : β), F (∫ (y : γ), f y - g y ∂η x) ∂κ a = ∫⁻ (x : β), F (∫ (y : γ), f y ∂η x - ∫ (y : γ), g y ∂η x) ∂κ a
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
TopologicalSpace.Opens.sheafRestrict_obj_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} (U : TopologicalSpace.Opens ↑X)
  (X_1 : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) C) (X_2 : (TopologicalSpace.Opens ↑(TopCat.of ↥U))ᵒᵖ),
  (U.sheafRestrict.obj X_1).obj.obj X_2 = X_1.obj.obj (Opposite.op (⋯.functor.obj (Opposite.unop X_2)))
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.instIsCardinalAccessibleObjConst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular] (A : C),
  ((CategoryTheory.Functor.const C).obj A).IsCardinalAccessible κ
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.IsAffineOpen.isQuasiSeparated : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens}, AlgebraicGeometry.IsAffineOpen U → IsQuasiSeparated ↑U
-- Mathlib.SetTheory.ZFC.Basic
/-- `isFunc x y f` is the assertion that `f` is a subset of `x × y` which relates to each element
of `x` a unique element of `y`, so that we can consider `f` as a ZFC function `x → y`.  -/
ZFSet.IsFunc : ZFSet.{u} → ZFSet.{u} → ZFSet.{u} → Prop
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.orthogonal_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.orthogonal ⊥ = ⊤
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_eq_one : ∀ {r : NNReal}, ↑r = 1 ↔ r = 1
-- Mathlib.Algebra.Group.Action.Sum
Sum.instAddAction.eq_1 : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} {m : AddMonoid M} [inst : AddAction M α] [inst_1 : AddAction M β],
  Sum.instAddAction = { toVAdd := Sum.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.Hom.ext : ∀ {R S : RingCat} {x y : R.Hom S}, x.hom' = y.hom' → x = y
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- To give a morphism in the over category, it suffices to give an arrow fitting in a commutative
triangle.  -/
CategoryTheory.Over.homMk : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} →
      {U V : CategoryTheory.Over X} →
        (f : U.left ⟶ V.left) →
          autoParam (CategoryTheory.CategoryStruct.comp f V.hom = U.hom) CategoryTheory.Over.homMk._auto_1 → (U ⟶ V)
-- Mathlib.Combinatorics.Colex
Finset.Colex.instDecidableLT : {α : Type u_1} → [inst : PartialOrder α] → [DecidableEq α] → [DecidableLE α] → DecidableLT (Colex (Finset α))
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_univ : ∀ {α : Type u_2} [inst : Group α] {s : Set α}, s.Nonempty → s * Set.univ = Set.univ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_le_size_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List α}, t.size ≤ (t.insertManyIfNewUnit l).size
-- Mathlib.Algebra.Group.NatPowAssoc
npow_mul_assoc : ∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [NatPowAssoc M] (k m n : ℕ) (x : M),
  x ^ k * x ^ m * x ^ n = x ^ k * (x ^ m * x ^ n)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The inverse of the right unitor as a term of `normalExpr`.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.rightUnitorInvM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
      [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] →
        Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.NormalExpr
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ \ m₂).get? k = none
-- Mathlib.Tactic.ClickSuggestions.Apply
/-- The total length of the new goals when printed.  -/
Mathlib.Tactic.ClickSuggestions.ApplyKey.replacementSize : Mathlib.Tactic.ClickSuggestions.ApplyKey → ℕ
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.toGeneralLinearGroup_injective : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  Function.Injective ⇑SpecialLinearGroup.toGeneralLinearGroup
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.ext_iff : ∀ {α : Type u_1} [inst : LE α] {s t : UpperSet α}, s = t ↔ ↑s = ↑t
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
subalgebraOfSubsemiring_toSubsemiring : ∀ {R : Type u_1} [inst : Semiring R] (S : Subsemiring R), (subalgebraOfSubsemiring S).toSubsemiring = S
-- Lean.Elab.InfoTree.Types
Lean.Elab.FieldRedeclInfo.mk : Lean.Syntax → Lean.Elab.FieldRedeclInfo
-- Lean.DocString.Markdown
/-- The monad in which docstring Markdown is rendered. This is used when showing Verso docstrings as
plain Markdown, such as in the language server.
 -/
Lean.Doc.MarkdownM : Type → Type
-- Mathlib.Tactic.FunProp.Types
/-- priority  -/
Mathlib.Meta.FunProp.GeneralTheorem.priority : Mathlib.Meta.FunProp.GeneralTheorem → ℕ
-- Mathlib.Condensed.Discrete.Characterization
LightCondMod.isDiscrete_iff_isDiscrete_forget : ∀ (R : Type u) [inst : Ring R] (M : LightCondMod R),
  LightCondensed.IsDiscrete M ↔ LightCondensed.IsDiscrete ((LightCondensed.forget R).obj M)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The `0`-cochain attached to a morphism of cochain complexes.  -/
CochainComplex.HomComplex.Cochain.ofHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} → (F ⟶ G) → CochainComplex.HomComplex.Cochain F G 0
-- Lean.DocString.Extension
Lean.VersoModuleDocs.instReprSnippet : Repr Lean.VersoModuleDocs.Snippet
-- Std.Http.Data.Body.Length
Std.Http.Body.Length.fixed.inj : ∀ {n n_1 : ℕ}, Std.Http.Body.Length.fixed n = Std.Http.Body.Length.fixed n_1 → n = n_1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.w : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] (j : ι),
  CategoryTheory.CategoryStruct.comp (f.t j) (SSet.Subcomplex.homOfLE ⋯) =
    CategoryTheory.CategoryStruct.comp (f.m j) (f.b j)
-- Mathlib.Data.Finset.Option
Finset.mem_insertNone : ∀ {α : Type u_1} {s : Finset α} {o : Option α}, o ∈ Finset.insertNone s ↔ ∀ a ∈ o, a ∈ s
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_rio : ∀ {n i fallback : ℕ}, (*...n).toList.getD i fallback = if i < n then i else fallback
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesOnBall.of_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {m n : ℕ},
  HasFiniteFPowerSeriesOnBall f p x n r → n ≤ m → HasFiniteFPowerSeriesOnBall f p x m r
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {a : α}
  {fallback : β a}, ∅.getD a fallback = fallback
-- Mathlib.Computability.AkraBazzi.AkraBazzi
AkraBazziRecurrence.rpow_p_mul_one_sub_smoothingFn_le : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r),
  ∀ᶠ (n : ℕ) in Filter.atTop,
    ∀ (i : α),
      ↑(r i n) ^ AkraBazziRecurrence.p a b * (1 - AkraBazziRecurrence.smoothingFn ↑(r i n)) ≤
        b i ^ AkraBazziRecurrence.p a b * ↑n ^ AkraBazziRecurrence.p a b * (1 - AkraBazziRecurrence.smoothingFn ↑n)
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mem_orbit : ∀ {γ : Type u_2} {α : Type u_3} [inst : VAdd γ α] (a : α) (m : γ), m +ᵥ a ∈ AddAction.orbit γ a