mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
/-- If two locally integrable functions on a finite-dimensional real manifold have the same integral
when multiplied by any smooth compactly supported function, then they coincide almost everywhere.  -/
ae_eq_of_integral_contMDiff_smul_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] {H : Type u_3}
  [inst_6 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [IsManifold I (↑⊤) M] [inst_10 : MeasurableSpace M] [BorelSpace M] [T2Space M]
  {f f' : M → F} {μ : MeasureTheory.Measure M} [SigmaCompactSpace M],
  MeasureTheory.LocallyIntegrable f μ →
    MeasureTheory.LocallyIntegrable f' μ →
      (∀ (g : M → ℝ),
          ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) g →
            HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ) →
        ∀ᵐ (x : M) ∂μ, f x = f' x
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.starIsoInitial_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.WithInitial.starIsoInitial.inv =
    CategoryTheory.Limits.initialIsInitial.to CategoryTheory.WithInitial.star
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.add_nonpos`.  -/
Right.add_nonpos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b : α}, a ≤ 0 → b ≤ 0 → a + b ≤ 0
-- Mathlib.Algebra.Order.Invertible
invOf_nonneg : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} [inst_3 : Invertible a],
  0 ≤ ⅟a ↔ 0 ≤ a
-- Init.Data.Int.Linear
Int.Internal.Linear.sub_fold : ∀ (a b : ℤ), a.sub b = a - b
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpEntry.toUnfold.injEq : ∀ (a a_1 : Lean.Name), (Lean.Meta.SimpEntry.toUnfold a = Lean.Meta.SimpEntry.toUnfold a_1) = (a = a_1)
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_sup : ∀ {R : Type u_2} [inst : NonAssocRing R] (S₁ S₂ : Subring R), (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.findOutermostContextInfo?.go : Lean.Elab.InfoTree → Option Lean.Elab.ContextInfo
-- Mathlib.Algebra.Homology.CochainComplexPlus
CochainComplex.Plus.instHasFiniteColimits : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteColimits C], CategoryTheory.Limits.HasFiniteColimits (CochainComplex.Plus C)
-- Init.Data.Rat.Lemmas
Rat.mkRat_num_den : ∀ {d : ℕ} {n n' : ℤ} {d' : ℕ} {z' : d' ≠ 0} {c : n'.natAbs.Coprime d'},
  d ≠ 0 → mkRat n d = { num := n', den := d', den_nz := z', reduced := c } → ∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_add_neg_iff_add_lt : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b c : α}, c < a + -b ↔ c + b < a
-- Mathlib.NumberTheory.Padics.PadicNumbers
Rat.padicValuation.eq_1 : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)],
  Rat.padicValuation p =
    { toFun := fun x => if x = 0 then 0 else WithZero.exp (-padicValRat p x), map_zero' := ⋯, map_one' := ⋯,
      map_mul' := ⋯, map_add_le_max' := ⋯ }
-- Mathlib.RingTheory.Coalgebra.Hom
/-- Composition of coalgebra homomorphisms.  -/
CoalgHom.comp : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid A] →
            [inst_2 : Module R A] →
              [inst_3 : AddCommMonoid B] →
                [inst_4 : Module R B] →
                  [inst_5 : AddCommMonoid C] →
                    [inst_6 : Module R C] →
                      [inst_7 : CoalgebraStruct R A] →
                        [inst_8 : CoalgebraStruct R B] →
                          [inst_9 : CoalgebraStruct R C] → (B →ₗc[R] C) → (A →ₗc[R] B) → A →ₗc[R] C
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- If `f` is nonnegative and integrable on the unordered interval `Set.uIoc a b`, then its
integral over `a..b` is positive if and only if `a < b` and the measure of
`Function.support f ∩ Set.Ioc a b` is positive.  -/
intervalIntegral.integral_pos_iff_support_of_nonneg_ae' : ∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  0 ≤ᵐ[μ.restrict (Set.uIoc a b)] f →
    IntervalIntegrable f μ a b → (0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (Function.support f ∩ Set.Ioc a b))
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k : α} (mem : k ∈ m) {h₃ : k ∈ m.insertManyIfNewUnit l},
      (m.insertManyIfNewUnit l).getKey k h₃ = m.getKey k mem
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasFDerivAt.csin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E},
  HasFDerivAt f f' x → HasFDerivAt (fun x => Complex.sin (f x)) (Complex.cos (f x) • f') x
-- Init.Data.Nat.Gcd
Nat.gcd_eq_right_iff_dvd : ∀ {n m : ℕ}, n.gcd m = m ↔ m ∣ n
-- Mathlib.Data.Set.Basic
Set.mem_injective : ∀ {α : Type u}, Function.Injective Membership.mem
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLE.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x_3 : Std.DTreeMap.Internal.Impl.leaf.Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isLE = true),
  Std.DTreeMap.Internal.Impl.getKeyLE k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim
-- Mathlib.Algebra.Group.Int.Even
Int.even_iff : ∀ {n : ℤ}, Even n ↔ n % 2 = 0
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.is_left_invariant_addPrehaar : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G},
  (interior U).Nonempty →
    ∀ (g : G) (K : TopologicalSpace.Compacts G),
      MeasureTheory.Measure.haar.addPrehaar (↑K₀) U (TopologicalSpace.Compacts.map (fun x => g + x) ⋯ K) =
        MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K
-- Mathlib.Combinatorics.Enumerative.DyckWord
_private.Mathlib.Combinatorics.Enumerative.DyckWord.0.DyckWord.ofTree.match_1.splitter : (motive : BinaryTree Unit → Sort u_1) →
  (x : BinaryTree Unit) →
    (Unit → motive BinaryTree.nil) →
      ((value : Unit) → (l r : BinaryTree Unit) → motive (BinaryTree.node value l r)) → motive x
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- The empty set is a `C^n` manifold w.r.t. any charted space and model.  -/
IsManifold.empty : ∀ {𝕜 : 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} (n : WithTop ℕ∞)
  {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsEmpty M], IsManifold I n M
-- Mathlib.Algebra.Category.Grp.LeftExactFunctor
AddCommGrpCat.leftExactFunctorForgetEquivalence.instPreservesFiniteLimitsObjLeftExactFunctorTypeFunctorInverseAux : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] (F : C ⥤ₗ Type v),
  CategoryTheory.Limits.PreservesFiniteLimits (AddCommGrpCat.leftExactFunctorForgetEquivalence.inverseAux.obj F)
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.Hom.mk : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : CategoryTheory.Preadditive C] →
              [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                [inst_6 : CategoryTheory.Pretriangulated C] →
                  {X Y : CategoryTheory.Triangulated.SpectralObject C ι} →
                    (hom : X.ω₁ ⟶ Y.ω₁) →
                      autoParam
                          (∀ {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
                            CategoryTheory.CategoryStruct.comp (X.δ f g)
                                ((CategoryTheory.shiftFunctor C 1).map
                                  (hom.app (CategoryTheory.ComposableArrows.mk₁ f))) =
                              CategoryTheory.CategoryStruct.comp (hom.app (CategoryTheory.ComposableArrows.mk₁ g))
                                (Y.δ f g))
                          CategoryTheory.Triangulated.SpectralObject.Hom.comm._autoParam →
                        X.Hom Y
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
adjacent side.  -/
EuclideanGeometry.cos_oangle_right_mul_dist_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → (EuclideanGeometry.oangle p₂ p₃ p₁).cos * dist p₁ p₃ = dist p₃ p₂
-- Init.Ext
PSigma.ext : ∀ {α : Sort u} {β : α → Sort v} {x y : PSigma β}, x.fst = y.fst → x.snd ≍ y.snd → x = y
-- Mathlib.Algebra.Group.Prod
/-- The equivalence between `(M × N) × P` and `M × (N × P)` is additive.  -/
AddEquiv.prodAssoc : {M : Type u_3} →
  {N : Type u_4} →
    {P : Type u_5} →
      [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (M × N) × P ≃+ M × N × P
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- If `s` is a `Finset`, then the measure of its preimage can be found as the sum of measures
of the fibers `f ⁻¹' {y}`.  -/
MeasureTheory.sum_measure_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Finset β) {f : α → β},
  (∀ y ∈ s, MeasurableSet (f ⁻¹' {y})) → ∑ b ∈ s, μ (f ⁻¹' {b}) = μ (f ⁻¹' ↑s)
-- Mathlib.LinearAlgebra.Determinant
LinearMap.detAux_id : ∀ {M : Type u_2} [inst : AddCommGroup M] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {A : Type u_5}
  [inst_3 : CommRing A] [inst_4 : Module A M] (b : Trunc (Module.Basis ι A M)), (LinearMap.detAux b) LinearMap.id = 1
-- Mathlib.Analysis.CStarAlgebra.lpSpace
instCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNRealOfNontrivial : {I : Type u_1} →
  {A : I → Type u_2} →
    [∀ (i : I), Nontrivial (A i)] → [inst : (i : I) → CommCStarAlgebra (A i)] → CommCStarAlgebra ↥(lp A ⊤)
-- Mathlib.LinearAlgebra.Matrix.Module
LinearMap.mapMatrixModule_id_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (v : ι → M), (LinearMap.mapMatrixModule ι LinearMap.id) v = v
-- Lean.Elab.Term.TermElabM
/-- Delay the elaboration of `stx`, and return a fresh metavariable that works a placeholder.
Remark: the caller is responsible for making sure the info tree is properly updated.
This method is used only at `elabUsingElabFnsAux`.
 -/
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.postponeElabTermCore : Lean.Syntax → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∪ t₂)[k]? = t₂[k]?
-- Std.Time.Format.Basic
Std.Time.FormatConfig.mk : Bool → Std.Time.DateFormat → Std.Time.FormatConfig
-- Mathlib.CategoryTheory.Adhesive.Basic
/-- If a van Kampen pushout forms the bottom face of a commutative "half-cube" whose front faces
are pullbacks, then there exist two back faces which are pullbacks and a top face which is a
pushout.  -/
CategoryTheory.IsPushout.IsVanKampen.exists_cube_filling : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  {H : CategoryTheory.IsPushout f g h i},
  H.IsVanKampen →
    ∀ {X' Y' Z' : C} {h' : X' ⟶ Z'} {i' : Y' ⟶ Z'} {αX : X' ⟶ X} {αY : Y' ⟶ Y} {αZ : Z' ⟶ Z}
      [CategoryTheory.Limits.HasPullback αX f],
      CategoryTheory.IsPullback h' αX αZ h →
        CategoryTheory.IsPullback i' αY αZ i →
          ∃ W' f' g' αW,
            CategoryTheory.IsPullback f' αW αX f ∧
              CategoryTheory.IsPullback g' αW αY g ∧ CategoryTheory.IsPushout f' g' h' i'
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.ihom_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] [inst_3 : CategoryTheory.MonoidalClosed C]
  [inst_4 : P.IsMonoidalClosed] (X : P.FullSubcategory) {Y Z : P.FullSubcategory} (f : Y ⟶ Z),
  ((CategoryTheory.ihom X).map f).hom = (CategoryTheory.ihom X.obj).map f.hom
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.preimage_coe_bot : ∀ {α : Type u_1}, WithBot.some ⁻¹' {⊥} = ∅
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The map of a Gaussian distribution by addition of a constant is a Gaussian.  -/
ProbabilityTheory.gaussianReal_map_const_add : ∀ {μ : ℝ} {v : NNReal} (y : ℝ),
  MeasureTheory.Measure.map (fun x => y + x) (ProbabilityTheory.gaussianReal μ v) =
    ProbabilityTheory.gaussianReal (μ + y) v
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_inter_self_eq_sdiff : ∀ {α : Type u_1} {s t : Set α}, s \ (t ∩ s) = s \ t
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesBelow_one : Nat.primesBelow 1 = ∅
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.mk.inj : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {C : Type u₃} {inst_1 : CategoryTheory.Category.{v₃, u₃} C}
  {F : CategoryTheory.Functor J C} {pt : C} {ι : F ⟶ (CategoryTheory.Functor.const J).obj pt} {pt_1 : C}
  {ι_1 : F ⟶ (CategoryTheory.Functor.const J).obj pt_1},
  { pt := pt, ι := ι } = { pt := pt_1, ι := ι_1 } → pt = pt_1 ∧ ι ≍ ι_1
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev?_eq_none_iff : ∀ {s : String} {p : s.Pos}, p.prev? = none ↔ p = s.startPos
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyMap_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
  [inst_4 : S₃.HasHomology] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃),
  CategoryTheory.ShortComplex.homologyMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ₁)
      (CategoryTheory.ShortComplex.homologyMap φ₂)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.im_pnat_div_pos : ∀ (n : ℕ) [NeZero n] (z : UpperHalfPlane), 0 < (-↑n / ↑z).im
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_le : ∀ {a b : UInt16}, a.toUInt32 ≤ b.toUInt32 ↔ a ≤ b
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.exists_isMaximal_dvd_of_dvd_absNorm : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  {p : ℤ},
  Prime p → ∀ (I : Ideal S), p ∣ ↑(Ideal.absNorm I) → ∃ P, P.IsMaximal ∧ Ideal.under ℤ P = Ideal.span {p} ∧ P ∣ I
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalizedModule.map_lTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_2) [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {M' : Type u_4} [inst_5 : AddCommMonoid M'] [inst_6 : Module R M']
  [inst_7 : Module A M'] [inst_8 : IsScalarTower R A M'] (S : Submonoid A) {N : Type u_7} [inst_9 : AddCommMonoid N]
  [inst_10 : Module R N] [inst_11 : Module A M] [inst_12 : IsScalarTower R A M] {P : Type u_8}
  [inst_13 : AddCommMonoid P] [inst_14 : Module R P] (f : N →ₗ[R] P) (g : M →ₗ[A] M') [h : IsLocalizedModule S g],
  (IsLocalizedModule.map S ((TensorProduct.AlgebraTensorModule.rTensor R N) g)
        ((TensorProduct.AlgebraTensorModule.rTensor R P) g))
      ((TensorProduct.AlgebraTensorModule.lTensor A M) f) =
    (TensorProduct.AlgebraTensorModule.lTensor A M') f
-- Mathlib.Algebra.Homology.TotalComplexShift
/-- The shift on bicomplexes obtained by shifting the second indices (and changing the
sign of differentials).  -/
HomologicalComplex₂.shiftFunctor₂ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      ℤ →
        CategoryTheory.Functor (HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ))
          (HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ))
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Continuity from above: the measure of the intersection of a sequence of
measurable sets is the infimum of the measures of the partial intersections.  -/
MeasureTheory.measure_iInter_eq_iInf_measure_iInter_le : ∀ {α : Type u_8} {ι : Type u_9} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] [inst : Preorder ι]
  [IsDirectedOrder ι] {f : ι → Set α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ) →
    (∃ i, μ (f i) ≠ ⊤) → μ (⋂ i, f i) = ⨅ i, μ (⋂ j, ⋂ (_ : j ≤ i), f j)
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.instIsTruncGENatIntEmbeddingUpNat : ComplexShape.embeddingUpNat.IsTruncGE
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- A left Kan lift of `g` along `f` is an initial object in `LeftLift f g`.  -/
CategoryTheory.Bicategory.LeftLift.IsKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : b ⟶ a} → {g : c ⟶ a} → CategoryTheory.Bicategory.LeftLift f g → Type (max (max v w) w)
-- Mathlib.Algebra.MvPolynomial.Equiv
Polynomial.toMvPolynomial.eq_1 : ∀ {R : Type u_1} {σ : Type u_3} [inst : CommSemiring R] (i : σ),
  Polynomial.toMvPolynomial i = Polynomial.aeval (MvPolynomial.X i)
-- Lean.DocString.Extension
Lean.ElabBlock.deferred.sizeOf_spec : ∀ (index : ℕ), sizeOf (Lean.ElabBlock.deferred index) = 1 + sizeOf index
-- Init.Core
ne_comm : ∀ {α : Sort u_1} {a b : α}, a ≠ b ↔ b ≠ a
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.cond_mul_eq_inter' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω},
  MeasurableSet s → μ s ≠ ⊤ → ∀ (t : Set Ω), μ[t | s] * μ s = μ (s ∩ t)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coeFnLinearMap_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] (R : Type u_3) {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : ContinuousAdd M] [inst_5 : Module R M]
  [inst_6 : ContinuousConstSMul R M] (a : C(α, M)) (a_1 : α),
  (ContinuousMap.coeFnLinearMap R) a a_1 = (↑ContinuousMap.coeFnAddMonoidHom).toFun a a_1
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.outerMeasure_exists_compact : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] {U : TopologicalSpace.Opens G},
  μ.outerMeasure ↑U ≠ ⊤ → ∀ {ε : NNReal}, ε ≠ 0 → ∃ K, ↑K ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure ↑K + ↑ε
-- Batteries.Data.PairingHeap
_private.Batteries.Data.PairingHeap.0.Batteries.PairingHeapImp.Heap.foldM.match_1.splitter : {α : Type u_1} →
  (motive : Option (α × Batteries.PairingHeapImp.Heap α) → Sort u_2) →
    (x : Option (α × Batteries.PairingHeapImp.Heap α)) →
      (x = none → motive none) →
        ((hd : α) → (tl : Batteries.PairingHeapImp.Heap α) → x = some (hd, tl) → motive (some (hd, tl))) → motive x
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.forall_mem_sup : ∀ {N : Type u_4} [inst : AddCommMonoid N] {P : N → Prop} {s t : AddSubmonoid N},
  (∀ x ∈ s ⊔ t, P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ + x₂)
-- Mathlib.Algebra.Order.Monoid.Defs
pos_add_self_iff : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a : α}, 0 < a + a ↔ 0 < a
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff_eq_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x : M →₀ R}, AddMonoidAlgebra.ofCoeff x = 0 ↔ x = 0
-- Mathlib.Dynamics.FixedPoints.Basic
/-- Given two maps `f : α → β` and `g : β → α`, `g` is a bijective map between the fixed points
of `f ∘ g` and the fixed points of `g ∘ f`. The inverse map is `f`, see `invOn_fixedPoints_comp`.  -/
Function.bijOn_fixedPoints_comp : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α),
  Set.BijOn g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (g ∘ f))
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonPlainTermGoalParams.toJson : Lean.Lsp.PlainTermGoalParams → Lean.Json
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.le_sin_mul : ∀ {x : ℝ}, 0 ≤ x → x ≤ 1 → x ≤ Real.sin (Real.pi / 2 * x)
-- Mathlib.Algebra.Algebra.Equiv
/-- **Alias** of `AlgEquiv.coe_toAlgHom_injective`. -/
AlgEquiv.coe_algHom_injective : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂], Function.Injective AlgEquiv.toAlgHom
-- Mathlib.Topology.Compactness.SigmaCompact
/-- A choice of compact covering for a `σ`-compact space, chosen to be monotone.  -/
compactCovering : (X : Type u_1) → [inst : TopologicalSpace X] → [SigmaCompactSpace X] → ℕ → Set X
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubsetResult.strict.inj : ∀ {s s_1 : Lean.Grind.AC.Seq}, Lean.Grind.AC.SubsetResult.strict s = Lean.Grind.AC.SubsetResult.strict s_1 → s = s_1
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Ioc_add_one_left_eq_Ioc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] {a b : α}, a < b → insert (a + 1) (Finset.Ioc (a + 1) b) = Finset.Ioc a b
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_neg_sub_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.Chebyshev.S R (-n - 1) = -Polynomial.Chebyshev.S R (n - 1)
-- Mathlib.RingTheory.Invariant.Profinite
instFiniteObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {G : Type u}
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [inst_5 : SMulCommClass G A B] [inst_6 : TopologicalSpace G]
  [CompactSpace G] [IsTopologicalGroup G] (P : Ideal A) (Q : Ideal B) [inst_9 : Q.LiesOver P]
  (σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) (N : OpenNormalSubgroup G),
  Finite ((Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor P Q σ).obj N)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.neg_h₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.neg.h₃ = -h.h₃
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.toAlgEquivAux_eq_liftNormal : ∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (g : ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (x : K)
  (L : FiniteGaloisIntermediateField k K),
  x ∈ L.toIntermediateField → InfiniteGalois.toAlgEquivAux✝ g x = (((InfiniteGalois.proj L) g).liftNormal K) x
-- Init.Control.Lawful.MonadAttach.Instances
instWeaklyLawfulMonadAttachReaderTOfLawfulMonad : ∀ {m : Type u_1 → Type u_2} {ρ : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadAttach m]
  [WeaklyLawfulMonadAttach m], WeaklyLawfulMonadAttach (ReaderT ρ m)
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_sub_const : ∀ {𝕜 : 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} {s : Set E} (c : F), fderivWithin 𝕜 (fun y => f y - c) s x = fderivWithin 𝕜 f s x