mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertMany_append : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l₁ l₂ : List (α × β)}, m.insertMany (l₁ ++ l₂) = (m.insertMany l₁).insertMany l₂
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_empty : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal), ∫⁻ (x : α) in ∅, f x ∂μ = 0
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital normed commutative ring is a non-unital commutative ring endowed with a
norm which satisfies the inequality `‖x y‖ ≤ ‖x‖ ‖y‖`.  -/
NonUnitalNormedCommRing : Type u_5 → Type u_5
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulStrictMono.toPosMulReflectLE : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : LinearOrder α] [PosMulStrictMono α], PosMulReflectLE α
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.instOneId : {R : Type u} →
  [inst : Monoid R] →
    {A : Type v} → [inst_1 : NonUnitalNonAssocSemiring A] → [inst_2 : DistribMulAction R A] → One (A →ₙₐ[R] A)
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.zero_right : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.MutuallySingular 0
-- Mathlib.Topology.Algebra.ConstMulAction
ContinuousConstVAdd.mk : ∀ {Γ : Type u_1} {T : Type u_2} [inst : TopologicalSpace T] [inst_1 : VAdd Γ T],
  (∀ (γ : Γ), Continuous fun x => γ +ᵥ x) → ContinuousConstVAdd Γ T
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseAMPM : String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_shift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n : ℤ),
  (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app
      ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X) =
    (CategoryTheory.shiftFunctor Cᵒᵖ n).map
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X)
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.pointwise_smul_toAddSubgroup : ∀ {α : Type u_1} [inst : Monoid α] {R : Type u_4} {M : Type u_5} [inst_1 : Ring R] [inst_2 : AddCommGroup M]
  [inst_3 : DistribMulAction α M] [inst_4 : Module R M] [inst_5 : SMulCommClass α R M] (a : α) (S : Submodule R M),
  (a • S).toAddSubgroup = a • S.toAddSubgroup
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RioSliceData.mk.inj : ∀ {α : Type u} {β : α → Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α β} {range : Std.Rio α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α β} {range_1 : Std.Rio α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Analysis.Normed.Module.Connected
/-- In a real vector space of dimension `> 1`, any sphere of nonnegative radius is
path connected.  -/
isPathConnected_sphere : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  1 < Module.rank ℝ E → ∀ (x : E) {r : ℝ}, 0 ≤ r → IsPathConnected (Metric.sphere x r)
-- Mathlib.Control.Bitraversable.Basic
/-- A bitraversable functor commutes with all applicative functors.  -/
bisequence : {t : Type u_1 → Type u_1 → Type u_1} →
  {m : Type u_1 → Type u_1} → [Bitraversable t] → [Applicative m] → {α β : Type u_1} → t (m α) (m β) → m (t α β)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Any fork on `h ≫ f` and `h ≫ g` lifts to a pullback along `h` of an equalizer of `f` and `g`.
 -/
CategoryTheory.Limits.liftPrecomp : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {Z : C} →
          (h : Z ⟶ X) →
            {s : CategoryTheory.Limits.Fork f g} →
              CategoryTheory.Limits.IsLimit s →
                {c : CategoryTheory.Limits.PullbackCone s.ι h} →
                  CategoryTheory.Limits.IsLimit c →
                    (s' :
                        CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.comp h f)
                          (CategoryTheory.CategoryStruct.comp h g)) →
                      s'.pt ⟶ (CategoryTheory.Limits.precompFork h s c).pt
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_iff_eq_empty_or_singleton : ∀ {α : Type u} {s : Set α}, s.Subsingleton ↔ s = ∅ ∨ ∃ x, s = {x}
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.instSMulCommClassSubtypeMemCenter : ∀ {M : Type u_2} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α], SMulCommClass (↥(Submonoid.center M)) M α
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.toQ : {α : Type u} → [inst : Lean.Grind.NatModule α] → α → Lean.Grind.IntModule.OfNatModule.Q α
-- Mathlib.Data.Finset.Pi
Finset.mem_pi : ∀ {α : Type u_1} {β : α → Type u} [inst : DecidableEq α] {s : Finset α} {t : (a : α) → Finset (β a)}
  {f : (a : α) → a ∈ s → β a}, f ∈ s.pi t ↔ ∀ (a : α) (h : a ∈ s), f a h ∈ t a
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.bindOfArrows : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {ι : Type u_1}
  {X : C} {Z : ι → C} {f : (i : ι) → Z i ⟶ X} {R : (i : ι) → CategoryTheory.Presieve (Z i)},
  CategoryTheory.Sieve.ofArrows Z f ∈ J X →
    (∀ (i : ι), CategoryTheory.Sieve.generate (R i) ∈ J (Z i)) →
      CategoryTheory.Sieve.generate (CategoryTheory.Presieve.bindOfArrows Z f R) ∈ J X
-- Mathlib.Algebra.Order.Group.Basic
zsmul_le_zsmul_iff_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {m n : ℤ} {a : α},
  0 < a → (m • a ≤ n • a ↔ m ≤ n)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `u` is a family of uniform structures on `γ`, then
`𝒰(α, γ, (⨅ i, u i)) = ⨅ i, 𝒰(α, γ, u i)`.  -/
UniformFun.iInf_eq : ∀ {α : Type u_1} {γ : Type u_3} {ι : Type u_4} {u : ι → UniformSpace γ},
  UniformFun.uniformSpace α γ = ⨅ i, UniformFun.uniformSpace α γ
-- Mathlib.Algebra.Order.Floor.Defs
/-- `FloorRing.ceil` is the upper adjoint of the coercion `↑ : ℤ → α`.  -/
FloorRing.gc_coe_floor : ∀ {α : Type u_4} {inst : Ring α} {inst_1 : LinearOrder α} [self : FloorRing α],
  GaloisConnection Int.cast FloorRing.floor
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyGED_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.Equiv t₂ → t₁.getKeyGED k fallback = t₂.getKeyGED k fallback
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.rTensorEquiv_symm_singleAlgEquiv : ∀ {R : Type u_1} {M : Type u_2} {S : Type u_4} {A : Type u_5} {B : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R S]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A]
  [inst_9 : AddCommMonoid M] (m : M) (a : A) (b : B),
  (AddMonoidAlgebra.rTensorEquivAlgEquiv R S A B).symm (AddMonoidAlgebra.single m (a ⊗ₜ[R] b)) =
    a ⊗ₜ[R] AddMonoidAlgebra.single m b
-- Lean.Expr
Lean.Expr.isTrue : Lean.Expr → Bool
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.mk.congr_simp : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (var var_1 : relations.G → M) (e_var : var = var_1)
  (linearCombination_var_relation : ∀ (r : relations.R), (Finsupp.linearCombination A var) (relations.relation r) = 0),
  { var := var, linearCombination_var_relation := linearCombination_var_relation } =
    { var := var_1, linearCombination_var_relation := ⋯ }
-- Batteries.Data.MLList.Basic
/-- Apply a function which returns values in the monad to every element of a `MLList`.  -/
MLList.mapM : {m : Type u_1 → Type u_1} → {α β : Type u_1} → [Monad m] → (α → m β) → MLList m α → MLList m β
-- Init.Data.SInt.IntToBitVec
Int64.toBitVec64_toISize : ∀ (n : Int64) (h : System.Platform.numBits = 64), n.toISize.toBitVec64 h = BitVec.signExtend 64 n.toBitVec
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- the inclusion of cycles in `S.X₂`  -/
CategoryTheory.ShortComplex.LeftHomologyData.i : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → (self : S.LeftHomologyData) → self.K ⟶ S.X₂
-- Init.Internal.Order.MonadTail
/-- Bind is monotone in the second (continuation) argument.  -/
Lean.Order.MonadTail.bind_mono_right : ∀ {m : Type u → Type v} {inst : Bind m} [self : Lean.Order.MonadTail m] {α β : Type u} {a : m α} {f₁ f₂ : α → m β}
  [inst_1 : Nonempty β],
  (∀ (x : α), Lean.Order.PartialOrder.rel (f₁ x) (f₂ x)) → Lean.Order.PartialOrder.rel (a >>= f₁) (a >>= f₂)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getThenInsertIfNew?_fst : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {v : β k}, (t.getThenInsertIfNew? k v ⋯).1 = t.get? k
-- Mathlib.Data.Int.Basic
Int.ofNat_dvd_natCast : ∀ {x y : ℕ}, OfNat.ofNat x ∣ ↑y ↔ OfNat.ofNat x ∣ y
-- Lean.Parser.Term
/-- Defines an inductive predicate using lattice theory, based on the Knaster-Tarski fixpoint theorem.

This feature constructs inductive predicates by leveraging the lattice structure on `Prop`
and ensures correctness through monotonicity.

The inductive predicate is defined as the least fixed point of a monotone function on `Prop`.

By default, monotonicity is verified automatically. However, users can provide custom proofs
of monotonicity if needed.
 -/
Lean.Parser.Termination.inductiveFixpoint : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} (h₁ h₂ : CategoryTheory.ModObj M X),
  CategoryTheory.ModObj.smul = CategoryTheory.ModObj.smul → h₁ = h₂
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
Std.IterM.step_attachWith : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop} [inst : Std.Iterator α m β] [inst_1 : Monad m]
  {it : Std.IterM m β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out},
  (it.attachWith P hP).step =
    (fun s => Std.Shrink.deflate ⟨Std.Iterators.Types.Attach.Monadic.modifyStep (it.attachWith P hP) s.inflate, ⋯⟩) <$>
      it.step
-- Init.Data.Order.Classes
Std.LawfulOrderMax.toLawfulOrderSup : ∀ {α : Type u} {inst : Max α} {inst_1 : LE α} [self : Std.LawfulOrderMax α], Std.LawfulOrderSup α
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `ofReal_norm`. -/
ofReal_norm_eq_enorm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (x : E), ENNReal.ofReal ‖x‖ = ‖x‖ₑ
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.log_mul : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : DecidableEq M] {n : M},
  (Function.Injective fun m => n ^ m) →
    ∀ (x y : ↥(Submonoid.powers n)), Submonoid.log (x * y) = Submonoid.log x + Submonoid.log y
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.mem_normalizer_fintype : ∀ {G : Type u_1} [inst : Group G] {S : Set G} [Finite ↑S] {x : G},
  (∀ n ∈ S, x * n * x⁻¹ ∈ S) → x ∈ Subgroup.normalizer S
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
/-- The power function `x ↦ x^s` is integrable on `(0, t)` iff `-1 < s`.  -/
intervalIntegral.integrableOn_Ioo_rpow_iff : ∀ {s t : ℝ}, 0 < t → (MeasureTheory.IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) MeasureTheory.volume ↔ -1 < s)
-- Lean.Meta.Tactic.Try.Collect
/-- Induction candidates.  -/
Lean.Meta.Try.Collector.Result.indCandidates : Lean.Meta.Try.Collector.Result → Array Lean.Meta.Try.Collector.InductionCandidate
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.stabilizer_coe : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [inst_2 : DecidableEq α] {n : ℕ}
  (s : ↑(Set.powersetCard α n)), MulAction.stabilizer G s = MulAction.stabilizer G ↑s
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).get k h' = t₂.get k ⋯
-- Init.Data.Array.Basic
Array.anyMUnsafe : {α : Type u} →
  {m : Type → Type w} → [Monad m] → (α → m Bool) → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → m Bool
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.turanGraph_adj : ∀ {n r : ℕ} {v w : Fin n}, (SimpleGraph.turanGraph n r).Adj v w ↔ ↑v % r ≠ ↑w % r
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_erase_le_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k km kme : α} (hkme : (t.erase k).maxKey? = some kme), t.maxKey?.get ⋯ = km → (cmp kme km).isLE = true
-- Mathlib.RingTheory.TensorProduct.Maps
/-- The natural linear map $A ⊗ \text{Hom}_R(M, N) → \text{Hom}_A (M_A, N_A)$,
where $M_A$ and $N_A$ are the respective modules over $A$ obtained by extension of scalars.

See `LinearMap.tensorProductEnd` for this map specialized to endomorphisms,
and bundled as `A`-algebra homomorphism.  -/
LinearMap.tensorProduct : (R : Type u_1) →
  (A : Type u_2) →
    (M : Type u_3) →
      (N : Type u_4) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : Module R M] →
                  [inst_5 : AddCommMonoid N] →
                    [inst_6 : Module R N] →
                      TensorProduct R A (M →ₗ[R] N) →ₗ[A] TensorProduct R A M →ₗ[A] TensorProduct R A N
-- Init.Data.BitVec.Lemmas
BitVec.add_def : ∀ {n : ℕ} (x y : BitVec n), x + y = BitVec.ofNat n (x.toNat + y.toNat)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.fromSingleMk_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ}
  (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0),
  ↑(CochainComplex.HomComplex.Cocycle.fromSingleMk f h q' hq' hf) = CochainComplex.HomComplex.Cochain.fromSingleMk f h
-- Mathlib.Data.Finset.Lattice.Fold
/-- A version of `Finset.sup'_map` with LHS and RHS reversed.
Also, this lemma assumes that `s` is nonempty instead of assuming that its image is nonempty.  -/
Finset.sup'_comp_eq_map : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] {s : Finset γ} {f : γ ↪ β} (g : β → α)
  (hs : s.Nonempty), s.sup' hs (g ∘ ⇑f) = (Finset.map f s).sup' ⋯ g
-- Mathlib.Algebra.Ring.IsFormallyReal
IsSumNonzeroSq.sq_add : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] {a s : R},
  a ≠ 0 → IsSumNonzeroSq s → IsSumNonzeroSq (a * a + s)
-- Std.Data.ByteSlice
/-- Folds an operation from right to left over the bytes in a byte slice.

An accumulator of type `β` is constructed by starting with `init` and combining each byte of the
byte slice with the current accumulator value in turn, moving from the end to the start.

Examples:
 * `(ByteArray.mk #[1, 2, 3]).toByteSlice.foldr (·.toNat + ·) 0 = 6`
 * `(ByteArray.mk #[1, 2, 3]).toByteSlice.popFront.foldr (·.toNat + ·) 0 = 5`
 -/
ByteSlice.foldr : {β : Type v} → (UInt8 → β → β) → β → ByteSlice → β
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instNonemptySubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredPropSet : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ),
  Nonempty (Subtype J.PropSet)
-- Mathlib.Probability.ProbabilityMassFunction.Basic
MeasureTheory.Measure.toPMF_toMeasure : ∀ {α : Type u_1} [inst : Countable α] [inst_1 : MeasurableSpace α] [inst_2 : MeasurableSingletonClass α]
  (μ : MeasureTheory.Measure α) [inst_3 : MeasureTheory.IsProbabilityMeasure μ], μ.toPMF.toMeasure = μ
-- Mathlib.Algebra.Torsor.Basic
Prod.instAddTorsor : {G : Type u_1} →
  {G' : Type u_2} →
    {P : Type u_3} →
      {P' : Type u_4} →
        [inst : AddGroup G] → [inst_1 : AddGroup G'] → [AddTorsor G P] → [AddTorsor G' P'] → AddTorsor (G × G') (P × P')
-- Mathlib.Order.Lattice
/-- A type with a pair of commutative and associative binary operations which satisfy two absorption
laws relating the two operations has the structure of a lattice.

The partial order is defined so that `a ≤ b` unfolds to `a ⊔ b = b`; cf. `sup_eq_right`.
 -/
Lattice.mk' : {α : Type u_1} →
  [inst : Max α] →
    [inst_1 : Min α] →
      (∀ (a b : α), a ⊔ b = b ⊔ a) →
        (∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)) →
          (∀ (a b : α), a ⊓ b = b ⊓ a) →
            (∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) →
              (∀ (a b : α), a ⊔ a ⊓ b = a) → (∀ (a b : α), a ⊓ (a ⊔ b) = a) → Lattice α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.c_relation : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 1728 * W.Δ = W.c₄ ^ 3 - W.c₆ ^ 2
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.AEFinStronglyMeasurable.ae_nonneg_of_forall_setIntegral_nonneg : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.AEFinStronglyMeasurable f μ →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ) →
      (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ) → 0 ≤ᵐ[μ] f
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.balanceLErase.congr_simp : ∀ {α : Type u} {β : α → Type v} (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (l l_1 : Std.DTreeMap.Internal.Impl α β) (e_l : l = l_1) (r r_1 : Std.DTreeMap.Internal.Impl α β) (e_r : r = r_1)
      (hlb : l.Balanced) (hrb : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size),
      Std.DTreeMap.Internal.Impl.balanceLErase k v l r hlb hrb hlr =
        Std.DTreeMap.Internal.Impl.balanceLErase k v_1 l_1 r_1 ⋯ ⋯ ⋯
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
LinearMap.dualProd_apply_apply : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (a a_1 : Module.Dual R M × M), ((LinearMap.dualProd R M) a) a_1 = a_1.1 a.2 + a.1 a_1.2
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.sub_pf : ∀ {R : Type u_2} [inst : CommRing R] {a b c d : R}, -b = c → a + c = d → a - b = d
-- Mathlib.Algebra.Free
FreeSemigroup.instTraversable.eq_1 : FreeSemigroup.instTraversable = { toFunctor := FreeSemigroup.instMonad.toFunctor, traverse := @FreeSemigroup.traverse }
-- Mathlib.Data.Nat.Cast.Commute
Nat.cast_commute : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ℕ) (x : α), Commute (↑n) x
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- The reflection in `K` of an element of `Kᗮ` is its negation.  -/
Submodule.reflection_mem_subspace_orthogonalComplement_eq_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] {v : E}, v ∈ Kᗮ → K.reflection v = -v
-- Mathlib.RingTheory.PowerSeries.Log
PowerSeries.HasSubst.log : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A], PowerSeries.HasSubst (PowerSeries.log A)
-- Mathlib.Algebra.Ring.Associator
/-- The multiplication `(x * y) * z` of three elements of a (non-associative)
(semi)-ring is an `AddMonoidHom` in each argument. See also `LinearMap.mulLeftRight` for a
related functions realized as a linear map.  -/
AddMonoidHom.mulLeft₃ : {R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → R →+ R →+ R →+ R
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Consumer.select.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (finished : Std.Async.Waiter (Option α)),
  sizeOf (Std.CloseableChannel.Consumer.select✝ finished) = 1 + sizeOf finished
-- Mathlib.CategoryTheory.Comma.Basic
/-- The left subobject  -/
CategoryTheory.Comma.left : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor A T} → {R : CategoryTheory.Functor B T} → CategoryTheory.Comma L R → A
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_le_of_right_le : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l},
  Lean.Order.PartialOrder.rel Q R → Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) R
-- Mathlib.Data.Set.Image
Set.image_subset_image_iff : ∀ {α : Type u_1} {β : Type u_2} {s t : Set α} {f : α → β}, Function.Injective f → (f '' s ⊆ f '' t ↔ s ⊆ t)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.SavedState.mk.inj : ∀ {term term_1 : Lean.Elab.Term.SavedState}, { term := term } = { term := term_1 } → term = term_1
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_iUnion_of_directed_le : ∀ {α : Type u_3} {ι : Sort u_4} (p : ι → Set (Set α)),
  (∀ (n : ι), IsPiSystem (p n)) → Directed (fun x1 x2 => x1 ⊆ x2) p → IsPiSystem (⋃ n, p n)
-- Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
SimplexCategory.Truncated.morphismProperty_eq_top : ∀ {d : ℕ} (W : CategoryTheory.MorphismProperty (SimplexCategory.Truncated d)) [W.IsMultiplicative],
  (∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (SimplexCategory.Truncated.δ d i ⋯ ⋯)) →
    (∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (SimplexCategory.Truncated.σ d i ⋯ ⋯)) → W = ⊤
-- Qq.ForLean.ReduceEval
Lean.Meta.evalList : {α : Type} → [Lean.Meta.ReduceEval α] → Lean.Expr → Lean.MetaM (List α)
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
/-- A bounded continuous function on a finite-measure space is in `Lp`.  -/
BoundedContinuousFunction.mem_Lp : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction α E),
  ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ MeasureTheory.Lp E p μ
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_eq_one_iff_unique : ∀ {α : Type u_1}, Nat.card α = 1 ↔ Subsingleton α ∧ Nonempty α
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.opOpEquivalence.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.opOpEquivalence C =
    { functor := CategoryTheory.unopUnop C, inverse := CategoryTheory.opOp C,
      unitIso := CategoryTheory.Iso.refl (CategoryTheory.Functor.id Cᵒᵖᵒᵖ),
      counitIso := CategoryTheory.Iso.refl ((CategoryTheory.opOp C).comp (CategoryTheory.unopUnop C)),
      functor_unitIso_comp := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.a_add_one_le_four_pow_parts_card : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {P : Finpartition Finset.univ},
  Fintype.card α / P.parts.card - Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card + 1 ≤
    4 ^ P.parts.card
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this is the projection `end_ F ⟶ (F.obj (op j)).obj j`
for any `j : J`.  -/
CategoryTheory.Limits.end_.π : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) →
          [inst_2 : CategoryTheory.Limits.HasEnd F] →
            (j : J) → CategoryTheory.Limits.end_ F ⟶ (F.obj (Opposite.op j)).obj j