mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.minEntry?_insertEntry.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (w : (a : α) × β a)
  (h_1 : Unit → motive none) (h_2 : (w : (a : α) × β a) → motive (some w)),
  (match some w with
    | none => h_1 ()
    | some w => h_2 w) =
    h_2 w
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.Measure.IsAddRightInvariant.toVAddInvariantMeasure_op : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : Add G] [μ.IsAddRightInvariant],
  MeasureTheory.VAddInvariantMeasure Gᵃᵒᵖ G μ
-- Mathlib.GroupTheory.FreeAbelianGroup
/-- `FreeAbelianGroup.lift` as an equivalence of groups.  -/
FreeAbelianGroup.liftAddEquiv : {α : Type u} → {G : Type u_1} → [inst : AddCommGroup G] → (α → G) ≃+ (FreeAbelianGroup α →+ G)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix.congr_simp : ∀ (α : Type u_1) {V : Type u_2} (G G_1 : SimpleGraph V),
  G = G_1 →
    ∀ {inst : DecidableRel G.Adj} [inst_1 : DecidableRel G_1.Adj] [inst_2 : Zero α] [inst_3 : One α] (a a_1 : V),
      a = a_1 → ∀ (a_2 a_3 : V), a_2 = a_3 → SimpleGraph.adjMatrix α G a a_2 = SimpleGraph.adjMatrix α G_1 a_1 a_3
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_univ_eight : ∀ {M : Type u_2} [inst : CommMonoid M] (f : Fin 8 → M), ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
HasFDerivAt.cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : E → ℂ} {f' : E →L[𝕜] ℂ} {x : E},
  HasFDerivAt f f' x → HasFDerivAt (fun x => Complex.exp (f x)) (Complex.exp (f x) • f') x
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `DifferentiableAt.smul` -/
DifferentiableAt.fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
  DifferentiableAt 𝕜 c x → DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (fun i => c i • f i) x
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.mul_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (x : α)
  [inst_2 : MulZeroClass β] [inst_3 : ContinuousMul β] (f g : CompactlySupportedContinuousMap α β),
  (f * g) x = f x * g x
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- A side of a right-angled triangle divided by the sine of the opposite angle equals the
hypotenuse.  -/
InnerProductGeometry.norm_div_sin_angle_add_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x = 0 ∨ y ≠ 0 → ‖y‖ / Real.sin (InnerProductGeometry.angle x (x + y)) = ‖x + y‖
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.hcomp_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D}
  {H I : CategoryTheory.Functor D E} (α : F ⟶ G) (β : H ⟶ I) (X : C),
  (α ◫ β).app X = CategoryTheory.CategoryStruct.comp (β.app (F.obj X)) (I.map (α.app X))
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.foldl : {σ : Type w} →
  {α : Type u_1} →
    {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → (σ → α → β → σ) → σ → σ
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofZeros_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0),
  (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg).H = S.X₂
-- Mathlib.LinearAlgebra.FreeModule.Basic
RingHomInvPair.toRingEquiv.congr_simp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] (σ σ_1 : R₁ →+* R₂) (e_σ : σ = σ_1)
  (σ' σ'_1 : R₂ →+* R₁) (e_σ' : σ' = σ'_1) [inst_2 : RingHomInvPair σ σ'],
  RingHomInvPair.toRingEquiv σ σ' = RingHomInvPair.toRingEquiv σ_1 σ'_1
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whisker_assoc_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Y' : C}
  (f : Y ⟶ Y') (Z : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) Z)
        (CategoryTheory.MonoidalCategoryStruct.associator X Y' Z).hom)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.σ_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  (i : Fin (n + 1)), X.σ i = X.map (SimplexCategory.σ i).op
-- Mathlib.Data.Int.Init
Int.div_lt_div_iff_of_dvd_of_pos_of_neg : ∀ {a b c d : ℤ}, 0 < b → d < 0 → b ∣ a → d ∣ c → (a / b < c / d ↔ c * b < d * a)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- Isomorphic graphs are acyclic together.  -/
SimpleGraph.Iso.isAcyclic_iff : ∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ≃g G'), G.IsAcyclic ↔ G'.IsAcyclic
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_abs : ∀ (x : ℝ), ↑|x| = |↑x|
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- The proposition that a sesquilinear form is symmetric  -/
LinearMap.IsSymm : {R : Type u_1} →
  {M : Type u_5} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → {I : R →+* R} → (M →ₛₗ[I] M →ₗ[R] R) → Prop
-- Mathlib.Algebra.BigOperators.Group.Finset.Indicator
/-- Consider a product of `g i (f i)` over a finset.  Suppose `g` is a function such as
`n ↦ (· ^ n)`, which maps a second argument of `1` to `1`. Then if `f` is replaced by the
corresponding multiplicative indicator function, the finset may be replaced by a possibly larger
finset without changing the value of the product.  -/
Finset.prod_mulIndicator_subset_of_eq_one : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] [inst_1 : One α] (f : ι → α) (g : ι → α → β)
  {s t : Finset ι}, s ⊆ t → (∀ (a : ι), g a 1 = 1) → ∏ i ∈ t, g i ((↑s).mulIndicator f i) = ∏ i ∈ s, g i (f i)
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.MatchResult.uncovered.sizeOf_spec : sizeOf Lean.Elab.Term.Quotation.MatchResult.uncovered = 1
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
/-- If `U` is an open of `X` containing `x`, we have a canonical ring map from the sections
over `U` to the residue field of `x`.

If we interpret sections over `U` as functions of `X` defined on `U`, then this ring map
corresponds to evaluation at `x`.
 -/
AlgebraicGeometry.LocallyRingedSpace.evaluation : (X : AlgebraicGeometry.LocallyRingedSpace) →
  {U : TopologicalSpace.Opens ↑X.toTopCat} → (x : ↥U) → X.presheaf.obj (Opposite.op U) ⟶ X.residueField ↑x
-- Mathlib.Data.Seq.Basic
/-- Coinductive principle for proving `b.length' ≤ a.length'` for two sequences `a` and `b`.  -/
Stream'.Seq.at_least_as_long_as_coind : ∀ {α : Type u} {β : Type v} {a : Stream'.Seq α} {b : Stream'.Seq β} (motive : Stream'.Seq α → Stream'.Seq β → Prop),
  motive a b →
    (∀ (a : Stream'.Seq α) (b : Stream'.Seq β),
        motive a b →
          ∀ (b_hd : β) (b_tl : Stream'.Seq β),
            b = Stream'.Seq.cons b_hd b_tl → ∃ a_hd a_tl, a = Stream'.Seq.cons a_hd a_tl ∧ motive a_tl b_tl) →
      b.length' ≤ a.length'
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The word of length `M i i'` that alternates between `i` and `i'`, ending with `i'`.  -/
CoxeterSystem.braidWord : {B : Type u_1} → CoxeterMatrix B → B → B → List B
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.ext : ∀ {α : Type u₁} {x y : CategoryTheory.Discrete α}, x.as = y.as → x = y
-- Init.Data.Range.Polymorphic.IntLemmas
Int.length_toList_roc : ∀ {a b : ℤ}, (a<...=b).toList.length = (b - a).toNat
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.hom_ext'_iff : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {f g : X ⊞ Y ⟶ Z},
  f = g ↔
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl f =
        CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl g ∧
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr f =
        CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr g
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.isGaussian_multivariateGaussian : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ},
  ProbabilityTheory.IsGaussian (ProbabilityTheory.multivariateGaussian μ S)
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasStrictFDerivAt_exp_smul_const_of_mem_ball : ∀ (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [inst : NontriviallyNormedField 𝕂] [CharZero 𝕂]
  [inst_2 : NormedCommRing 𝕊] [inst_3 : NormedRing 𝔸] [inst_4 : NormedSpace 𝕂 𝕊] [inst_5 : NormedAlgebra 𝕂 𝔸]
  [inst_6 : Algebra 𝕊 𝔸] [inst_7 : ContinuousSMul 𝕊 𝔸] [inst_8 : IsScalarTower 𝕂 𝕊 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕊),
  t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius →
    HasStrictFDerivAt (fun u => NormedSpace.exp (u • x)) (NormedSpace.exp (t • x) • ContinuousLinearMap.smulRight 1 x) t
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsHaarMeasure.toIsMulLeftInvariant : ∀ {G : Type u_3} {inst : Group G} {inst_1 : TopologicalSpace G} {inst_2 : MeasurableSpace G}
  {μ : MeasureTheory.Measure G} [self : μ.IsHaarMeasure], μ.IsMulLeftInvariant
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.coeff_mul_order_add_order : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] (x y : HahnSeries Γ R),
  (x * y).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Hom.of.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {as as_1 : CategoryTheory.Oplax.StrongTrans.Modification η θ},
  { as := as } = { as := as_1 } → as = as_1
-- Mathlib.RingTheory.Valuation.Basic
Valuation.one_lt_val_iff : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation K Γ₀) {x : K}, x ≠ 0 → (1 < v x ↔ v x⁻¹ < 1)
-- Mathlib.Data.Int.Lemmas
Int.le_natCast_sub : ∀ (m n : ℕ), ↑m - ↑n ≤ ↑(m - n)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.ConvolutionExistsAt.add_distrib : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : Monoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F] [T2Space F]
  [ContinuousAdd F] {f f' : M → E} {g : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F),
  DiscreteConvolution.ConvolutionExistsAt L f g x →
    DiscreteConvolution.ConvolutionExistsAt L f' g x →
      DiscreteConvolution.convolution L (f + f') g x =
        DiscreteConvolution.convolution L f g x + DiscreteConvolution.convolution L f' g x
-- Mathlib.Order.RelSeries
RelSeries.singleton_toFun : ∀ {α : Type u_1} (r : SetRel α α) (a : α) (x : Fin (0 + 1)), (RelSeries.singleton r a).toFun x = a
-- Init.Data.Array.Erase
Array.erase_replicate_ne : ∀ {α : Type u_1} [inst : BEq α] {n : ℕ} [LawfulBEq α] {a b : α},
  (!b == a) = true → (Array.replicate n a).erase b = Array.replicate n a
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.sum_eq_one : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} [inst_2 : Fintype X]
  (s : ↑(stdSimplex S X)), ∑ x, s x = 1
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.mk.sizeOf_spec : ∀ (coe : ℂ) (coe_im_pos : 0 < coe.im),
  sizeOf { coe := coe, coe_im_pos := coe_im_pos } = 1 + sizeOf coe + sizeOf coe_im_pos
-- Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
rankCondition_iff_le_of_comp_eq_one : ∀ {R : Type u_1} [inst : Semiring R],
  RankCondition R ↔ ∀ (n m : ℕ) (f : (Fin n → R) →ₗ[R] Fin m → R) (g : (Fin m → R) →ₗ[R] Fin n → R), f ∘ₗ g = 1 → m ≤ n
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoOps.mk.injEq : ∀ (mkPureApp : Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr)
  (mkBindApp : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr)
  (isPureApp? : Lean.Expr → Option Lean.Expr)
  (splitMonadApp? : Lean.Expr → Lean.Elab.TermElabM (Option (Lean.Elab.Do.MonadInfo × Lean.Expr)))
  (mkMonadApp : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr)
  (mkPureApp_1 : Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr)
  (mkBindApp_1 : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr)
  (isPureApp?_1 : Lean.Expr → Option Lean.Expr)
  (splitMonadApp?_1 : Lean.Expr → Lean.Elab.TermElabM (Option (Lean.Elab.Do.MonadInfo × Lean.Expr)))
  (mkMonadApp_1 : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr),
  ({ mkPureApp := mkPureApp, mkBindApp := mkBindApp, isPureApp? := isPureApp?, splitMonadApp? := splitMonadApp?,
        mkMonadApp := mkMonadApp } =
      { mkPureApp := mkPureApp_1, mkBindApp := mkBindApp_1, isPureApp? := isPureApp?_1,
        splitMonadApp? := splitMonadApp?_1, mkMonadApp := mkMonadApp_1 }) =
    (mkPureApp = mkPureApp_1 ∧
      mkBindApp = mkBindApp_1 ∧
        isPureApp? = isPureApp?_1 ∧ splitMonadApp? = splitMonadApp?_1 ∧ mkMonadApp = mkMonadApp_1)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.core.inj : ∀ {e : Lean.Expr} {lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr} {e_1 : Lean.Expr}
  {lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr},
  Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.core e lhs rhs =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.core e_1 lhs_1 rhs_1 →
    e = e_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.span_eq_top_of_span_eq_ker : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {ι : Type u_1} (s : ι → P.Ring) (hs : Ideal.span (Set.range s) = P.ker),
  Submodule.span S (Set.range fun i => Algebra.Extension.Cotangent.mk ⟨s i, ⋯⟩) = ⊤
-- Mathlib.Topology.Order.NhdsSet
Ioc_mem_nhdsSet_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c d : α},
  a < b → c < d → Set.Ioc a d ∈ nhdsSet (Set.Icc b c)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_eq_maxKeyD_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.maxKey! = t.maxKeyD default
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
Float.Model.UnpackedFloat.unpackExponent.eq_1 : ∀ {spec : Float.Model.Format} (b : BitVec spec.numBits),
  Float.Model.UnpackedFloat.unpackExponent b =
    BitVec.cast ⋯
      (BitVec.extractLsb (spec.mantissaBitsWithoutImplicit + spec.exponentBits - 1) spec.mantissaBitsWithoutImplicit b)
-- Mathlib.Probability.Process.Kolmogorov
/-- A stochastic process `X : T → Ω → E` on an index space `T` and a measurable space `Ω`
with measure `P` is said to satisfy the Kolmogorov condition with exponents `p, q` and constant `M`
if for all `s, t : T`, the pair `(X s, X t)` is measurable for the Borel sigma-algebra on `E × E`
and the following condition holds: `∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P ≤ M * edist s t ^ q`.  -/
ProbabilityTheory.IsKolmogorovProcess : {T : Type u_1} →
  {Ω : Type u_2} →
    {E : Type u_3} →
      [PseudoEMetricSpace T] →
        {mΩ : MeasurableSpace Ω} →
          [PseudoEMetricSpace E] → (T → Ω → E) → MeasureTheory.Measure Ω → ℝ → ℝ → NNReal → Prop
-- Init.Grind.Ring.Field
Lean.Grind.Field.div_mul_cancel : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {x y : α}, y ≠ 0 → x / y * y = x
-- Lean.Meta.Basic
Lean.Meta.SynthInstanceCacheKey.mk : Lean.LocalInstances → Lean.Expr → ℕ → Lean.Meta.SynthInstanceCacheKey
-- Mathlib.Topology.Separation.Hausdorff
/-- Two continuous maps into a Hausdorff space disagree at a point iff they disagree in a
neighborhood.  -/
ContinuousAt.ne_iff_eventually_ne : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y] {x : X}
  {f g : X → Y}, ContinuousAt f x → ContinuousAt g x → (f x ≠ g x ↔ ∀ᶠ (x : X) in nhds x, f x ≠ g x)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsFiniteKernel.mk : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β},
  (∃ C < ⊤, ∀ (a : α), (κ a) Set.univ ≤ C) → ProbabilityTheory.IsFiniteKernel κ
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.cancel_right_div_gcd' : ∀ {m a b c d : ℕ}, 0 < m → c ≡ d [MOD m] → a * c ≡ b * d [MOD m] → a ≡ b [MOD m / m.gcd c]
-- Mathlib.Data.Nat.Nth
Nat.le_nth_count' : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ}, (∃ k, p k ∧ n ≤ k) → n ≤ Nat.nth p (Nat.count p n)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right] (x : CategoryTheory.Limits.WalkingParallelPair),
  I.parallelPairDiagram.obj x = CategoryTheory.Limits.parallelPair.parallelPairObj (∏ᶜ I.left) (∏ᶜ I.right) x
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftAlgHom_apply : ∀ {K : Type u} [inst : Field K] {L : Type u_1} {S : Type u_2} [inst_1 : Field L] [inst_2 : CommSemiring S]
  [inst_3 : Algebra S (Polynomial K)] [inst_4 : Algebra S L] (φ : Polynomial K →ₐ[S] L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (f : RatFunc K),
  (RatFunc.liftAlgHom φ hφ) f = φ f.num / φ f.denom
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The span of two different points that lie in a line through two points equals that line.  -/
affineSpan_pair_eq_of_mem_of_mem_of_ne : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ p₄ : P},
  p₁ ∈ line[k, p₃, p₄] → p₂ ∈ line[k, p₃, p₄] → p₁ ≠ p₂ → line[k, p₁, p₂] = line[k, p₃, p₄]
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.posGE_offset : ∀ {s : String.Slice} {p : s.Pos}, s.posGE p.offset ⋯ = p
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.diff_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {t₃ : Std.TreeMap.Raw α β cmp}, t₁.WF → t₂.WF → t₃.WF → t₁.Equiv t₂ → (t₁ \ t₃).Equiv (t₂ \ t₃)
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonAssocSemiring α] [inst_1 : Preorder α]
  [inst_2 : NonAssocSemiring β] [inst_3 : Preorder β] [inst_4 : NonAssocSemiring γ] [inst_5 : Preorder γ]
  {f₁ f₂ : β →+*o γ} {g : α →+*o β}, Function.Surjective ⇑g → (f₁.comp g = f₂.comp g ↔ f₁ = f₂)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ico : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => x * a) ⁻¹' Set.Ico b c = Set.Ico (b / a) (c / a)
-- Mathlib.Data.Finset.Sups
Finset.subset_sups_self : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s : Finset α}, s ⊆ s ⊻ s
-- Mathlib.RepresentationTheory.Intertwining
/-- The tensor product of intertwining maps induced from tensor product of linear maps.  -/
Representation.IntertwiningMap.tensor : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        {U : Type u_5} →
          [inst : CommSemiring A] →
            [inst_1 : Monoid G] →
              [inst_2 : AddCommMonoid V] →
                [inst_3 : AddCommMonoid W] →
                  [inst_4 : AddCommMonoid U] →
                    [inst_5 : Module A V] →
                      [inst_6 : Module A W] →
                        [inst_7 : Module A U] →
                          {ρ : Representation A G V} →
                            {σ : Representation A G W} →
                              {τ : Representation A G U} →
                                {P : Type u_6} →
                                  [inst_8 : AddCommMonoid P] →
                                    [inst_9 : Module A P] →
                                      {π : Representation A G P} →
                                        ρ.IntertwiningMap σ →
                                          τ.IntertwiningMap π → (ρ.tprod τ).IntertwiningMap (σ.tprod π)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β}, a ∈ m.insertIfNew k v ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.mk : {𝕜 : 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] →
                            {n : WithTop ℕ∞} →
                              {V : M → Type u_6} →
                                [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                  [inst_9 : (x : M) → TopologicalSpace (V x)] →
                                    [inst_10 : FiberBundle F V] →
                                      (toFun : (x : M) → V x) →
                                        (ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, toFun x⟩) →
                                          ContMDiffSection I F n V
-- Mathlib.Algebra.Exact.Basic
/-- When we have a commutative diagram from a sequence of two maps to another,
such that the left vertical map is surjective, the middle vertical map is bijective and the right
vertical map is injective, then the upper row is exact iff the lower row is.
See `ShortComplex.exact_iff_of_epi_of_isIso_of_mono` in the file
`Mathlib/Algebra/Homology/ShortComplex/Exact.lean` for the categorical version of this result.  -/
MonoidHom.mulExact_iff_of_surjective_of_bijective_of_injective : ∀ {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} {N₃ : Type u_13}
  [inst : CommMonoid M₁] [inst_1 : CommMonoid M₂] [inst_2 : CommMonoid M₃] [inst_3 : CommMonoid N₁]
  [inst_4 : CommMonoid N₂] [inst_5 : CommMonoid N₃] (f : M₁ →* M₂) (g : M₂ →* M₃) (f' : N₁ →* N₂) (g' : N₂ →* N₃)
  (τ₁ : M₁ →* N₁) (τ₂ : M₂ →* N₂) (τ₃ : M₃ →* N₃),
  f'.comp τ₁ = τ₂.comp f →
    g'.comp τ₂ = τ₃.comp g →
      Function.Surjective ⇑τ₁ →
        Function.Bijective ⇑τ₂ → Function.Injective ⇑τ₃ → (Function.MulExact ⇑f ⇑g ↔ Function.MulExact ⇑f' ⇑g')
-- Lean.Server.CodeActions.Attr
/-- The list of command code actions to apply when a particular command kind is highlighted.  -/
Lean.CodeAction.CommandCodeActions.onCmd : Lean.CodeAction.CommandCodeActions → Lean.NameMap (Array Lean.CodeAction.CommandCodeAction)