mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerYield_flatMap : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterator α₂ m γ] {f : β → Std.IterM m γ} {it₁ : Std.IterM m β} {it₂ it₂' : Std.IterM m γ} {b : γ},
  it₂.IsPlausibleStep (Std.IterStep.yield it₂' b) →
    (Std.IterM.flatMapAfter f it₁ (some it₂)).IsPlausibleStep
      (Std.IterStep.yield (Std.IterM.flatMapAfter f it₁ (some it₂')) b)
-- Mathlib.Algebra.Lie.Classical
/-- The special linear Lie algebra: square matrices of trace zero.  -/
LieAlgebra.SpecialLinear.sl : (n : Type u_1) →
  (R : Type u₂) → [inst : CommRing R] → [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → LieSubalgebra R (Matrix n n R)
-- Mathlib.Algebra.Exact.Sequence
/-- This is an unrolled, universe-polymorphic version of
`Module.sum_neg_one_pow_finrank_eq_zero_of_exact`. This special case exists because of the role that
this lemma plays in the proof of `LinearMap.index_comp`.

In theory one could write a `simproc` which conjured up this lemma for a sequence of any length and
then one would not need to have this special-case lemma at all.  -/
Module.sum_neg_one_pow_finrank_eq_zero_of_exact_six : ∀ {k : Type u_1} [inst : DivisionRing k] {V₀ : Type u₀} [inst_1 : AddCommGroup V₀] [inst_2 : Module k V₀]
  [FiniteDimensional k V₀] {V₁ : Type u₁} [inst_4 : AddCommGroup V₁] [inst_5 : Module k V₁] [FiniteDimensional k V₁]
  {V₂ : Type u₂} [inst_7 : AddCommGroup V₂] [inst_8 : Module k V₂] [FiniteDimensional k V₂] {V₃ : Type u₃}
  [inst_10 : AddCommGroup V₃] [inst_11 : Module k V₃] [FiniteDimensional k V₃] {V₄ : Type u₄}
  [inst_13 : AddCommGroup V₄] [inst_14 : Module k V₄] [FiniteDimensional k V₄] {V₅ : Type u₅}
  [inst_16 : AddCommGroup V₅] [inst_17 : Module k V₅] [FiniteDimensional k V₅] (f₀ : V₀ →ₗ[k] V₁) (f₁ : V₁ →ₗ[k] V₂)
  (f₂ : V₂ →ₗ[k] V₃) (f₃ : V₃ →ₗ[k] V₄) (f₄ : V₄ →ₗ[k] V₅),
  Function.Injective ⇑f₀ →
    Function.Exact ⇑f₀ ⇑f₁ →
      Function.Exact ⇑f₁ ⇑f₂ →
        Function.Exact ⇑f₂ ⇑f₃ →
          Function.Exact ⇑f₃ ⇑f₄ →
            Function.Surjective ⇑f₄ →
              ↑(Module.finrank k V₀) - ↑(Module.finrank k V₁) + ↑(Module.finrank k V₂) - ↑(Module.finrank k V₃) +
                    ↑(Module.finrank k V₄) -
                  ↑(Module.finrank k V₅) =
                0
-- Aesop.Forward.State
/-- The hypothesis.  -/
Aesop.RawHyp.fvarId : Lean.FVarId → Aesop.RawHyp
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.mono : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] [inst_1 : NormedAddCommGroup γ] {f : α → β} {g : α → γ},
  MeasureTheory.Integrable g μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖) → MeasureTheory.Integrable f μ
-- Init.Data.Vector.Basic
/-- Remove the last element of a vector.  -/
Vector.pop : {α : Type u_1} → {n : ℕ} → Vector α n → Vector α (n - 1)
-- Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
/-- For `B` a topological space and `F` a `𝕜`-normed space, a map from `U : Set B` to `F ≃L[𝕜] F`
determines an open partial homeomorphism from `B × F` to itself by its action fiberwise.  -/
FiberwiseLinear.openPartialHomeomorph : {𝕜 : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : TopologicalSpace B] →
        [inst_1 : NontriviallyNormedField 𝕜] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace 𝕜 F] →
              {U : Set B} →
                (φ : B → F ≃L[𝕜] F) →
                  IsOpen U →
                    ContinuousOn (fun x => ↑(φ x)) U →
                      ContinuousOn (fun x => ↑(φ x).symm) U → OpenPartialHomeomorph (B × F) (B × F)
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.opNNNorm_comp_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : NontriviallyNormedField 𝕜₃]
  [inst_3 : SeminormedAddCommGroup E] [inst_4 : SeminormedAddCommGroup F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  {σ₁₃ : 𝕜 →+* 𝕜₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomIsometric σ₁₂]
  [inst_11 : RingHomIsometric σ₂₃] [inst_12 : RingHomIsometric σ₁₃] (h : F →SL[σ₂₃] G) (f : E →SL[σ₁₂] F),
  ‖h ∘SL f‖₊ ≤ ‖h‖₊ * ‖f‖₊
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_C : ∀ {R : Type u_1} [inst : Semiring R] {a : R}, a ≠ 0 → (SkewPolynomial.C a).support = {0}
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapCocycles₁_comp_i_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{max u u_1, u, u} k H}
  {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↥(groupCohomology.cocycles₁ A)),
  (ModuleCat.Hom.hom (groupCohomology.shortComplexH1 B).g).ker.subtype
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.mapCocycles₁ f φ)) x) =
    ((Rep.Hom.hom φ).compLeft G)
      ((LinearMap.funLeft k ↑A ⇑f) ((ModuleCat.Hom.hom (groupCohomology.shortComplexH1 A).g).ker.subtype x))
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.deepTerms : Lean.Option Bool
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- When `M` has a `⊥` element, we can define the weighted total degree of a multivariate
polynomial as a function taking values in `M`.  -/
MvPolynomial.weightedTotalDegree : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      {σ : Type u_3} → [AddCommMonoid M] → [inst_2 : SemilatticeSup M] → [OrderBot M] → (σ → M) → MvPolynomial σ R → M
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Functor.mapArrowFunctor_obj : ∀ (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.Functor.mapArrowFunctor C D).obj F = F.mapArrow
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin_fst_le_snd : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (j : ℕ) {a b : α},
  a ≤ b →
    (∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b) →
      ((↑F).PairwiseDisjoint fun z => Set.Icc z.1 z.2) →
        (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- The diagram
```
      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω
```
commutes.
 -/
CategoryTheory.HasSubobjectClassifier.comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasSubobjectClassifier C] {U X : C}
  (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m],
  CategoryTheory.CategoryStruct.comp m (CategoryTheory.HasSubobjectClassifier.χ m) =
    CategoryTheory.CategoryStruct.comp (⋯.some.χ₀ U) (CategoryTheory.HasSubobjectClassifier.truth C)
-- Init.Data.Vector.Basic
Vector.instInhabited : {α : Type u_1} → {n : ℕ} → [Inhabited α] → Inhabited (Vector α n)
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.toList_rii : ∀ {α : Type ąu} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.toList_rii._auto_1)
  {t : Std.TreeMap.Raw α β cmp}, Std.Slice.toList (Std.Rii.Sliceable.mkSlice t *...*) = t.toList
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.top_orthogonal_eq_bot : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ⊤ᗮ = ⊥
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.gMul_def : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {i j : ℕ}
  (a : TensorPower R i M) (b : TensorPower R j M), GradedMonoid.GMul.mul a b = TensorPower.mulEquiv (a ⊗ₜ[R] b)
-- Lean.Elab.Tactic.RCases
/-- This will match a pattern `pat` against a local hypothesis `e`.
* `g`: The initial subgoal
* `fs`: A running variable substitution, the result of `cases` operations upstream.
  The variable `e` must be run through this map before locating it in the context of `g`,
  and the output variable substitutions will be end extensions of this one.
* `clears`: The list of variables to clear in all subgoals generated from this point on.
  We defer clear operations because clearing too early can cause `cases` to fail.
  The actual clearing happens in `RCases.finish`.
* `e`: a local hypothesis, the scrutinee to match against.
* `a`: opaque "user data" which is passed through all the goal calls at the end.
* `pat`: the pattern to match against
* `cont`: A continuation. This is called on every goal generated by the result of the pattern
  match, with updated values for `g` , `fs`, `clears`, and `a`.
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.rcasesCore : {α : Type} →
  Lean.MVarId →
    Lean.Meta.FVarSubst →
      Array Lean.FVarId →
        Lean.Expr →
          α →
            Lean.Elab.Tactic.RCases.RCasesPatt →
              (Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → α → Lean.Elab.TermElabM α) →
                Lean.Elab.TermElabM α
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_hom : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)]
  {j : J} {k : K},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (j, k))
      (CategoryTheory.Limits.colimitIsoColimitCurryCompColim G).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).obj j) k)
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim) j)
-- Mathlib.Analysis.CStarAlgebra.Unitary.Span
/-- If `a : A` is a selfadjoint element in a C⋆-algebra with `‖a‖ ≤ 1`,
then `a + I • CFC.sqrt (1 - a ^ 2)` is unitary.

This is the key tool to show that a C⋆-algebra is spanned by its unitary elements.  -/
IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (a : A),
  IsSelfAdjoint a → ‖a‖ ≤ 1 → a + Complex.I • CFC.sqrt (1 - a ^ 2) ∈ unitary A
-- Mathlib.Order.Filter.IndicatorFunction
Filter.EventuallyEq.mulSupport : ∀ {α : Type u_1} {β : Type u_2} [inst : One β] {f g : α → β} {l : Filter α},
  f =ᶠ[l] g → Function.mulSupport f =ᶠ[l] Function.mulSupport g
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.addEquivBoundedOfCompact_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  [inst_3 : AddMonoid β] [inst_4 : LipschitzAdd β],
  ⇑(ContinuousMap.addEquivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact
-- Init.Data.UInt.Basic
instDivUSize : Div USize
-- Init.Data.Vector.Lemmas
Vector.toList_toArray : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.toArray.toList = xs.toList
-- Lean.Elab.MutualInductive
Lean.Elab.Command.PreElabHeaderResult.view : Lean.Elab.Command.PreElabHeaderResult → Lean.Elab.Command.InductiveView
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoOpPushout_hom_inr : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f.unop g.unop)
      (CategoryTheory.Limits.pullbackIsoOpPushout f g).hom.unop =
    (CategoryTheory.Limits.pullback.snd f g).unop
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- If the domain has dimension one, then Fréchet derivative is equivalent to the classical
definition with a limit. In this version we have to take the limit along the subset `{x}ᶜ`,
because for `y=x` the slope equals zero due to the convention `0⁻¹=0`.  -/
hasDerivAtFilter_iff_tendsto_slope : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter 𝕜},
  HasDerivAtFilter f f' (L ×ˢ pure x) ↔ Filter.Tendsto (slope f x) (L ⊓ Filter.principal {x}ᶜ) (nhds f')
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
TensorAlgebra.toExterior.eq_1 : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  TensorAlgebra.toExterior = (TensorAlgebra.lift R) (ExteriorAlgebra.ι R)
-- Init.Data.Vector.Lex
Vector.lt_toList : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] {xs ys : Vector α n}, xs.toList < ys.toList ↔ xs < ys
-- Mathlib.Algebra.Tropical.Basic
/-- Reinterpret `x : R` as an element of `Tropical R`.
See `Tropical.tropOrderIso` for the order-preserving equivalence.  -/
Tropical.tropEquiv : {R : Type u} → R ≃ Tropical R
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.List.toSlice.eq_1 : ∀ {α : Type u} (as : List α) (start stop : ℕ),
  as.toSlice start stop =
    if start < stop then { internalRepresentation := { list := List.drop start as, stop := some (stop - start) } }
    else { internalRepresentation := { list := [], stop := some 0 } }
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply : ∀ (n : Type u) {X : AlgebraicGeometry.Scheme}
  (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of (MvPolynomial n (ULift.{u, 0} ℤ)))) (i : n),
  (AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n) f i =
    (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f))
      ((CategoryTheory.ConcreteCategory.hom
          (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (ULift.{u, 0} ℤ)))).inv)
        (MvPolynomial.X i))
-- Mathlib.Data.Fin.SuccPred
/-- `predAbove p i` surjects `i : Fin (n+1)` into `Fin n` by subtracting one if `p < i`.  -/
Fin.predAbove : {n : ℕ} → Fin n → Fin (n + 1) → Fin n
-- Init.MetaTypes
Lean.NameGenerator : Type
-- Mathlib.Algebra.Lie.TraceForm
/-- A finite, free (as an `R`-module) Lie algebra `L` carries a bilinear form on `L`.

This is a specialisation of `LieModule.traceForm` to the adjoint representation of `L`.  -/
killingForm : (R : Type u_1) →
  (L : Type u_3) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LinearMap.BilinForm R L
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.integralSum_eq_tsum_div : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] (s : Set (ι → ℝ)) (F : (ι → ℝ) → ℝ) [inst_1 : Fintype ι]
  {B : BoxIntegral.Box ι},
  BoxIntegral.hasIntegralVertices B →
    s ⊆ ↑B →
      BoxIntegral.integralSum (s.indicator F) MeasureTheory.volume.toBoxAdditive.toSMul
          (BoxIntegral.unitPartition.prepartition n B) =
        (∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ Fintype.card ι
-- Mathlib.Algebra.Lie.Weights.Killing
LieSubalgebra.isNonZero_coe_root : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] (α : ↥LieSubalgebra.root),
  (↑α).IsNonZero
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.IsLocallyArtinian.of_isLocallyNoetherian_of_discreteTopology : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] [DiscreteTopology ↥X],
  AlgebraicGeometry.IsLocallyArtinian X
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_sectionsOfPresieve : ∀ {X : AlgebraicGeometry.Scheme} {U : X.AffineZariskiSite} (P : CategoryTheory.Presieve U),
  U.presieveOfSections (AlgebraicGeometry.Scheme.AffineZariskiSite.sectionsOfPresieve P) = P
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.PullbackCone.isIso_snd_of_mono_of_isLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Mono f]
  {t : CategoryTheory.Limits.PullbackCone f f} (ht : CategoryTheory.Limits.IsLimit t), CategoryTheory.IsIso t.snd
-- Mathlib.FieldTheory.SeparableDegree
/-- If a polynomial is separable, then its separable degree is equal to its degree.  -/
Polynomial.natSepDegree_eq_natDegree_of_separable : ∀ {F : Type u} [inst : Field F] (f : Polynomial F), f.Separable → f.natSepDegree = f.natDegree
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.sproj.sizeOf_spec : ∀ (n offset : ℕ) (x : Lean.IR.VarId), sizeOf (Lean.IR.Expr.sproj n offset x) = 1 + sizeOf n + sizeOf offset + sizeOf x
-- Mathlib.Topology.Algebra.Group.Basic
Units.instWeaklyLocallyCompactSpaceOfT1SpaceOfContinuousMul : ∀ {α : Type u} [inst : Monoid α] [inst_1 : TopologicalSpace α] [T1Space α] [ContinuousMul α]
  [WeaklyLocallyCompactSpace α], WeaklyLocallyCompactSpace αˣ
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.prod_coe_rpow : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) (r : ℝ), ∏ i ∈ s, ↑(f i) ^ r = ↑(∏ i ∈ s, f i) ^ r
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_inter_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ((↑(m₁.inter m₂)).isEmpty = true ↔ ∀ (k : α), m₁.contains k = true → m₂.contains k = false)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Iso.sumCongr_toEquiv : ∀ {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W}
  {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ≃g G') (g : H ≃g H'), (f.sumCongr g).toEquiv = f.sumCongr g.toEquiv
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.toFreeRefl_map : ∀ (V : Type u_1) [inst : CategoryTheory.ReflQuiver V] {X Y : V} (f : X ⟶ Y),
  (CategoryTheory.Cat.toFreeRefl V).map f = CategoryTheory.Cat.FreeRefl.homMk f
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
OpenNormalSubgroup.toFiniteIndexNormalSubgroup_injective : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : CompactSpace G] [inst_3 : ContinuousMul G],
  Function.Injective OpenNormalSubgroup.toFiniteIndexNormalSubgroup
-- Lean.Meta.Sym.Arith.Types
/-- `IsCharP` instance for `type` if available.  -/
Lean.Meta.Sym.Arith.Ring.charInst? : Lean.Meta.Sym.Arith.Ring → Option (Lean.Expr × ℕ)
-- Init.Meta.Defs
Lean.isIdBeginEscape : Char → Bool
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecOfCarrierObjModuleCatModulesFunctor : ∀ {R : CommRingCat} (M : ModuleCat ↑R), SheafOfModules.IsQuasicoherent ((AlgebraicGeometry.tilde.functor R).obj M)
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instSingletonSigma : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Singleton ((a : α) × β a) (Std.DTreeMap α β cmp)
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Ordered.mem_inner_iff_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (sz : ℕ) (a : α) (v : β a) (l r : Std.DTreeMap.Internal.Impl α β)
  (k : α), compare k a = Ordering.lt → (k ∈ Std.DTreeMap.Internal.Impl.inner sz a v l r ↔ k ∈ l)
-- Mathlib.Algebra.Ring.ULift
RingHom.ulift_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (x : ULift.{u₁, u_1} R),
  (RingHom.ulift.{u₁, u_3, u_1, u_2} f) x = { down := f x.down }
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.lowerBound?_exists : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBTree.RBSet α cmp} [Std.TransCmp cmp],
  (∃ y, t.lowerBound? x = some y) ↔ ∃ y ∈ t, cmp x y ≠ Ordering.lt
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
CovariantDerivative.of_isCovariantDerivativeOn_of_open_cover_coe : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] {ι : Type u_7} {s : ι → Set M}
  {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} (hcov : ∀ (i : ι), IsCovariantDerivativeOn F cov (s i))
  (hs : ⋃ i, s i = Set.univ), ↑(CovariantDerivative.ofIsCovariantDerivativeOnOfOpenCover hcov hs) = cov
-- Mathlib.Analysis.Complex.ReImTopology
Complex.isOpenMap_im : IsOpenMap Complex.im
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.eq_emptyOn : ∀ {α : Type u_1} [IsEmpty α] (M : Matroid α), M = Matroid.emptyOn α
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.instBEqAtomicFact : BEq Mathlib.Tactic.Order.AtomicFact
-- Mathlib.Order.Partition.Basic
Partition.subset_sUnion_iff_mem : ∀ {α : Type u_1} {S : Set (Set α)} {u t : Set α} {P : Partition u}, t ∈ P → S ⊆ P.parts → (t ⊆ ⋃₀ S ↔ t ∈ S)
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₃ : ∀ {R : Type u} [inst : Ring R] {X₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  (hfg : (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker),
  (CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g hfg).X₃ = X₃
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
/-- For any `RingCon R`, when we view it as an ideal in `Rᵒᵖ`, `subtype` is the injective `Rᵐᵒᵖ`-linear
map `I → Rᵐᵒᵖ`.
 -/
TwoSidedIdeal.subtypeMop : {R : Type u_1} → [inst : Ring R] → (I : TwoSidedIdeal R) → ↥I →ₗ[Rᵐᵒᵖ] Rᵐᵒᵖ
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_eq_iff_eq_mul : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {x : M} {y : ↥S} {z : N}, f.mk' x y = z ↔ f x = z * f ↑y
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.projectiveFamilyFun_union : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {s t : Set ((i : ι) → α i)},
  MeasureTheory.IsProjectiveMeasureFamily P →
    s ∈ MeasureTheory.measurableCylinders α →
      t ∈ MeasureTheory.measurableCylinders α →
        Disjoint s t →
          MeasureTheory.projectiveFamilyFun P (s ∪ t) =
            MeasureTheory.projectiveFamilyFun P s + MeasureTheory.projectiveFamilyFun P t
-- Mathlib.NumberTheory.LucasLehmer
_private.Mathlib.NumberTheory.LucasLehmer.0.LucasLehmer.s.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((i : ℕ) → motive i.succ) → motive x
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.pow_card_le_prod : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulRightMono M] [MulLeftMono M] (l : List M) (n : M),
  (∀ x ∈ l, n ≤ x) → n ^ l.length ≤ l.prod
-- Std.Time.Duration
Std.Time.instReprDuration_1 : Repr Std.Time.Duration
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.revMatchesAt_iff_revMatchesAt_beq : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt c pos ↔ String.Slice.Pattern.Model.RevMatchesAt (fun x => x == c) pos
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The cone hull of a set. The smallest convex cone containing that set.  -/
ConvexCone.hull : (R : Type u_2) →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : SMul R M] → Set M → ConvexCone R M
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.OmissionReason.string.injEq : ∀ (s s_1 : String),
  (Lean.PrettyPrinter.Delaborator.OmissionReason.string s = Lean.PrettyPrinter.Delaborator.OmissionReason.string s_1) =
    (s = s_1)