mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.id_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} {X : CategoryTheory.Comma L R},
  (CategoryTheory.CategoryStruct.id X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_right_strictAnti₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}
  [ZeroLEOneClass G₀], 0 < a → a < 1 → StrictAnti fun n => a ^ n
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.characteristic_iff_comap_eq : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.comap ϕ.toAddMonoidHom H = H
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.comp_mapCommGrp_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] {E : Type u₃}
  [inst_6 : CategoryTheory.Category.{v₃, u₃} E] [inst_7 : CategoryTheory.CartesianMonoidalCategory E]
  [inst_8 : CategoryTheory.BraidedCategory E] {F : CategoryTheory.Functor C D} [inst_9 : F.Braided]
  {G : CategoryTheory.Functor D E} [inst_10 : G.Braided] (A : CategoryTheory.CommGrp C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) A.X A.X)
      ((F.comp G).map CategoryTheory.MonObj.mul)
-- Aesop.RulePattern
_private.Aesop.RulePattern.0.Aesop.RulePattern.elab.fvarsToMVars : Array Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Expr × Array Lean.MVarId)
-- Mathlib.GroupTheory.Torsion
AddCommGroup.freeRank.eq_1 : ∀ (G : Type u_1) [inst : AddCommGroup G] [inst_1 : AddGroup.FG G],
  AddCommGroup.freeRank G = AddGroup.rank (G ⧸ AddCommGroup.torsion G)
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
/-- Given two families of morphisms `f i : X i ⟶ S` and `f' j : X' j ⟶ S`,
this is the sieve on `Over.mk (𝟙 (X i)) : Over (X i)` which corresponds
to the sieve of `X i` that is obtained by pulling back by `f i` the sieve
generated by `f'`.  -/
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type t} →
      {S : C} →
        {X : ι → C} →
          ((i : ι) → X i ⟶ S) →
            {ι' : Type t'} →
              {X' : ι' → C} →
                ((j : ι') → X' j ⟶ S) →
                  (i : ι) → CategoryTheory.Sieve (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (X i)))
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Variant of `mul_le_of_le_one_right` for `a` non-positive instead of non-negative.  -/
le_mul_of_le_one_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b : R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R]
  [AddRightReflectLE R], a ≤ 0 → b ≤ 1 → a ≤ a * b
-- Mathlib.Topology.Algebra.Order.Archimedean
/-- In a nontrivial densely linear ordered archimedean topological multiplicative group,
a subgroup is either dense or is cyclic, but not both.

For a non-exclusive `Or` version with weaker assumptions, see `Subgroup.dense_or_cyclic` above.  -/
Subgroup.dense_xor_cyclic : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] (s : Subgroup G),
  Xor (Dense ↑s) (∃ a, s = Subgroup.zpowers a)
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- `Free R C` is a type synonym for `C`, which, given `[CommRing R]` and `[Category* C]`,
we will equip with a category structure where the morphisms are formal `R`-linear combinations
of the morphisms in `C`.
 -/
CategoryTheory.Free : Type u_1 → Type u → Type u
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- Change of variables for antitone functions.
If `f` is continuous on `[a, b]` and has a nonpositive derivative `f'` in `(a, b)`,
then we can substitute `u = f x` to get `∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`.  -/
intervalIntegral.integral_deriv_smul_comp_of_deriv_nonpos : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), f' x ≤ 0) → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.d.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (n m : ℕ),
  h.d (Int.ofNat n) (Int.ofNat m) = L.d n m
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.lift.congr_simp : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {e : J} (self self_1 : D.IsTerminal e),
  self = self_1 → ∀ {j : J} (hj : D.P j), self.lift hj = self_1.lift hj
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsIso.unop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty Cᵒᵖ) [P.RespectsIso],
  P.unop.RespectsIso
-- Mathlib.Data.List.Iterate
List.take_iterate : ∀ {α : Type u_1} (f : α → α) (a : α) (m n : ℕ), List.take m (List.iterate f a n) = List.iterate f a (min m n)
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_indicator : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] (s t : Set α) (f : α → M),
  s.indicator (t.indicator f) = (s ∩ t).indicator f
-- Init.Data.Range.Polymorphic.PRange
Std.Roc.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (lower upper : α), (sizeOf lower<...=upper) = 1 + sizeOf lower + sizeOf upper
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewRawFact.mk.inj : ∀ {proof prop : Lean.Expr} {generation : ℕ} {splitSource : Lean.Meta.Grind.SplitSource}
  {ematchDiagSource : Lean.Meta.Grind.EMatchDiagSource} {proof_1 prop_1 : Lean.Expr} {generation_1 : ℕ}
  {splitSource_1 : Lean.Meta.Grind.SplitSource} {ematchDiagSource_1 : Lean.Meta.Grind.EMatchDiagSource},
  { proof := proof, prop := prop, generation := generation, splitSource := splitSource,
        ematchDiagSource := ematchDiagSource } =
      { proof := proof_1, prop := prop_1, generation := generation_1, splitSource := splitSource_1,
        ematchDiagSource := ematchDiagSource_1 } →
    proof = proof_1 ∧
      prop = prop_1 ∧ generation = generation_1 ∧ splitSource = splitSource_1 ∧ ematchDiagSource = ematchDiagSource_1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {f : α → Bool} {k : α}, t.WF → (Std.TreeSet.Raw.filter f t).get! k = (Option.filter f (t.get? k)).get!
-- Mathlib.Order.MinMax
le_of_le_min_left : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, c ≤ min a b → c ≤ a
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.ofIsEmpty_onRelation : ∀ (L : FirstOrder.Language) (L' : FirstOrder.Language) [inst : L.IsAlgebraic] [inst_1 : L.IsRelational] {n : ℕ}
  (a : L.Relations n), (FirstOrder.Language.LHom.ofIsEmpty L L').onRelation a = isEmptyElim a
-- Mathlib.Analysis.Convex.Body
/-- The **carrier set** underlying a convex body: the set of points contained in it  -/
ConvexBody.carrier : {V : Type u_2} → [inst : TopologicalSpace V] → [inst_1 : AddCommMonoid V] → [inst_2 : SMul ℝ V] → ConvexBody V → Set V
-- Lean.Compiler.IR.Basic
Lean.IR.Param.mk : Lean.IR.VarId → Bool → Lean.IR.IRType → Lean.IR.Param
-- Init.Data.BitVec.Bitblast
BitVec.cpopLayer.congr_simp : ∀ {len w iterNum : ℕ} (oldLayer oldLayer_1 : BitVec (len * w)),
  oldLayer = oldLayer_1 →
    ∀ (newLayer newLayer_1 : BitVec (iterNum * w)),
      newLayer = newLayer_1 →
        ∀ (hold : 2 * (iterNum - 1) < len), oldLayer.cpopLayer newLayer hold = oldLayer_1.cpopLayer newLayer_1 hold
-- Mathlib.RingTheory.Idempotents
instSemiringCorner : {R : Type u_1} → (e : R) → [inst : NonUnitalSemiring R] → (idem : IsIdempotentElem e) → Semiring idem.Corner
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.pure : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPred} (a : α), ⦃ post a ⦄ pure a ⦃ post; epost ⦄
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Ψ_even : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (m : ℤ),
  W.Ψ (2 * m) * W.ψ₂ = W.Ψ (m - 1) ^ 2 * W.Ψ m * W.Ψ (m + 2) - W.Ψ (m - 2) * W.Ψ m * W.Ψ (m + 1) ^ 2
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_map_eq_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Injective ⇑f → ∀ (S : Subsemigroup M), Subsemigroup.comap f (Subsemigroup.map f S) = S
-- Mathlib.FieldTheory.Relrank
IntermediateField.inf_relrank_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B : IntermediateField F E),
  (A ⊓ B).relrank A = B.relrank A
-- Mathlib.CategoryTheory.Abelian.Transfer
CategoryTheory.ShrinkHoms.hasLimitsOfShape : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.LocallySmall.{w, v_1, u_1} C]
  (J : Type u_2) [inst_2 : CategoryTheory.Category.{v_2, u_2} J] [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.ShrinkHoms.{u_1} C)
-- Mathlib.Data.Set.Operations
/-- The restriction of a function onto the preimage of a set.  -/
Set.restrictPreimage : {α : Type u} → {β : Type v} → (t : Set β) → (f : α → β) → ↑(f ⁻¹' t) → ↑t
-- Mathlib.MeasureTheory.Measure.AEDisjoint
/-- Two sets are said to be `μ`-a.e. disjoint if their intersection has measure zero.  -/
MeasureTheory.AEDisjoint : {α : Type u_2} → {m : MeasurableSpace α} → MeasureTheory.Measure α → Set α → Set α → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.limitBiconeOfUnique_bicone_π : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : Unique J] (f : J → C) (j : J),
  (CategoryTheory.Limits.limitBiconeOfUnique f).bicone.π j = CategoryTheory.eqToHom ⋯
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr.0.Lean.Meta.Grind.Arith.CommRing.denoteExprCore.go : {M : Type → Type} →
  [Monad M] →
    [Lean.MonadError M] →
      [MonadLiftT Lean.MetaM M] →
        [Lean.Meta.Sym.Arith.MonadCanon M] →
          [Lean.Meta.Grind.Arith.CommRing.MonadRing M] →
            (ℕ → Lean.Expr) → Lean.Meta.Grind.Arith.CommRing.RingExpr → M Lean.Expr
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.StrongTrans F G) {a b : B} {f g : a ⟶ b}
  (η : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b))
      (self.naturality g).hom =
    CategoryTheory.CategoryStruct.comp (self.naturality f).hom
      (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_dvd : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) {p q : Polynomial (Polynomial R)},
  p ∣ q → Polynomial.evalEval x y p ∣ Polynomial.evalEval x y q
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.OuterMeasure.toMeasure_eq_zero : ∀ {α : Type u_1} {ms : MeasurableSpace α} {μ : MeasureTheory.OuterMeasure α} (h : ms ≤ μ.caratheodory),
  μ.toMeasure h = 0 ↔ μ = 0
-- Init.Data.String.Lemmas.Slice
String.Pos.get?_toSlice : ∀ {s : String} {p : s.Pos}, p.toSlice.get? = p.get?
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.coeff_mul_right_one_sub_of_lt_order : ∀ {σ : Type u_1} {R : Type u_3} [inst : Ring R] {f g : MvPowerSeries σ R} (d : σ →₀ ℕ),
  ↑(Finsupp.degree d) < g.order → (MvPowerSeries.coeff d) ((1 - g) * f) = (MvPowerSeries.coeff d) f
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.instAdd : {𝕜 : 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} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] → [inst_7 : ContMDiffMul I (↑⊤) G] → Add (LeftInvariantDerivation I G)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.nrComplexPlaces_eq_zero_of_finrank_eq_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  Module.finrank ℚ K = 1 → NumberField.InfinitePlace.nrComplexPlaces K = 0
-- Mathlib.Data.EReal.Basic
instAddCommMonoidEReal : AddCommMonoid EReal
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.mul_adjp_apply_ne : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (A : Matrix n n R)
  (i j : n), i ≠ j → (A * Matrix.adjp 1 A) i j = (A * Matrix.adjp (-1) A) i j
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.toSheaf_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) {X Y : SheafOfModules R} (f : X ⟶ Y),
  ((SheafOfModules.toSheaf R).map f).hom = ((SheafOfModules.forget R).comp (PresheafOfModules.toPresheaf R.obj)).map f
-- Mathlib.RingTheory.FiniteLength
isFiniteLength_iff_isNoetherian_isArtinian : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsFiniteLength R M ↔ IsNoetherian R M ∧ IsArtinian R M
-- Mathlib.Topology.Continuous
continuousAt_id' : ∀ {X : Type u_1} [inst : TopologicalSpace X] (y : X), ContinuousAt (fun x => x) y
-- Mathlib.Analysis.Calculus.ParametricIntegral
/-- Differentiation under integral of `x ↦ ∫ F x a` at a given point `x₀`, assuming
`F x₀` is integrable, `x ↦ F x a` is locally Lipschitz in a neighborhood of `x₀` for ae `a`
(with a neighborhood independent of `a`) with integrable Lipschitz bound, and `F x` is ae-measurable
for `x` in a possibly smaller neighborhood of `x₀`.  -/
hasFDerivAt_integral_of_dominated_loc_of_lip : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [inst_1 : RCLike 𝕜]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace 𝕜 E] {H : Type u_4}
  [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → ℝ} {s : Set H}
  {F' : α → H →L[𝕜] E},
  s ∈ nhds x₀ →
    (∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) →
      MeasureTheory.Integrable (F x₀) μ →
        MeasureTheory.AEStronglyMeasurable F' μ →
          (∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) s) →
            MeasureTheory.Integrable bound μ →
              (∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀) →
                MeasureTheory.Integrable F' μ ∧ HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
-- Lean.Syntax
Lean.Syntax.isQuot : Lean.Syntax → Bool
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.instLTResult : {α : Type} → [Ord α] → LT (Mathlib.Tactic.ClickSuggestions.Result α)
-- Mathlib.LinearAlgebra.Prod
/-- Multiplying by the trivial module from the left does not change the structure.
This is the `LinearEquiv` version of `AddEquiv.uniqueProd`.  -/
LinearEquiv.uniqueProd : {R : Type u} →
  {M : Type v} →
    {M₂ : Type w} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst_4 : Module R M₂] → [Unique M₂] → (M₂ × M) ≃ₗ[R] M
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.instIsGoodTrans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  [inst_2 : HomotopicalAlgebra.IsCofibrant A] (P P' : HomotopicalAlgebra.Cylinder A) [P.IsGood] [inst_4 : P'.IsGood],
  (P.trans P').IsGood
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.mem_map_of_surjective : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {y : L'},
  Function.Surjective ⇑f → y ∈ LieIdeal.map f I → ∃ x, f ↑x = y
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
/-- Turn a measurable function `f : α → ℚ → ℝ` into a measurable function `α → StieltjesFunction ℝ`.
Composition of `toRatCDF` and `IsMeasurableRatCDF.stieltjesFunction`.  -/
ProbabilityTheory.stieltjesOfMeasurableRat : {α : Type u_1} → [inst : MeasurableSpace α] → (f : α → ℚ → ℝ) → Measurable f → α → StieltjesFunction ℝ
-- Std.Internal.Do.WP.Basic
/-- Rewriting the program of a weakest precondition along an equation `x = y` weakens it:
the precondition of `y` entails the precondition of `x`.  -/
Std.Internal.Do.wp_le_wp_of_eq : ∀ {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] {x y : Prog},
  x = y →
    ∀ (post : Value → Pred) (epost : EPred),
      Lean.Order.PartialOrder.rel (Std.Internal.Do.wp y post epost) (Std.Internal.Do.wp x post epost)
-- Mathlib.Data.Complex.Basic
Complex.I_mul_re : ∀ (z : ℂ), (Complex.I * z).re = -z.im
-- Init.Util
withPtrAddr : {α : Type u} → {β : Type v} → α → (k : USize → β) → (∀ (u₁ u₂ : USize), k u₁ = k u₂) → β
-- Mathlib.Order.WellFoundedSet
Set.WellFoundedOn.union : ∀ {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s t : Set α},
  s.WellFoundedOn r → t.WellFoundedOn r → (s ∪ t).WellFoundedOn r
-- Mathlib.GroupTheory.OrderOfElement
orderOf_submonoid : ∀ {G : Type u_1} [inst : Monoid G] {H : Submonoid G} (y : ↥H), orderOf ↑y = orderOf y
-- Aesop.Search.Expansion.Simp
Aesop.SimpResult.simplified.injEq : ∀ (newGoal : Lean.MVarId) (usedTheorems : Lean.Meta.Simp.UsedSimps) (newGoal_1 : Lean.MVarId)
  (usedTheorems_1 : Lean.Meta.Simp.UsedSimps),
  (Aesop.SimpResult.simplified newGoal usedTheorems = Aesop.SimpResult.simplified newGoal_1 usedTheorems_1) =
    (newGoal = newGoal_1 ∧ usedTheorems = usedTheorems_1)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Quotient.instMeasurableSpace : {α : Type u_6} → {s : Setoid α} → [m : MeasurableSpace α] → MeasurableSpace (Quotient s)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_eq_finprod : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {L : SummationFilter β}
  [L.LeAtTop], Function.HasFiniteMulSupport f → ∏'[L] (b : β), f b = ∏ᶠ (b : β), f b
-- Init.Data.Int.DivMod.Lemmas
Int.sub_mul_fdiv_right : ∀ (a b : ℤ) {c : ℤ}, c ≠ 0 → (a - b * c).fdiv c = a.fdiv c - b
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β] {f : α → β → Bool} {k k' : α},
  m.WF → m.getKey? k = some k' → (Std.HashMap.Raw.filter f m)[k]! = (Option.filter (fun x => f k' x) m[k]?).get!
-- Mathlib.Topology.VectorBundle.Basic
/-- Make a `FiberBundle` from a `VectorPrebundle`; auxiliary construction for
`VectorPrebundle.toVectorBundle`.  -/
VectorPrebundle.toFiberBundle : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [inst_2 : (x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace R F] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : (x : B) → TopologicalSpace (E x)] → (a : VectorPrebundle R F E) → FiberBundle F E
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- The cone over a given sheaf whose cone point is the global sections and whose components are
the restriction maps.  -/
CategoryTheory.Sheaf.coneΓ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          [inst_2 : CategoryTheory.HasWeakSheafify J A] →
            [CategoryTheory.HasGlobalSectionsFunctor J A] →
              (F : CategoryTheory.Sheaf J A) → CategoryTheory.Limits.Cone F.obj
-- Mathlib.Algebra.Star.Basic
star_inj : ∀ {R : Type u} [inst : InvolutiveStar R] {x y : R}, star x = star y ↔ x = y
-- Mathlib.NumberTheory.NumberField.Basic
/-- The isomorphism of algebras `(𝓞 K) ≃ₐ[𝓞 k] (𝓞 L)` given by restricting
an isomorphism of algebras `e : K ≃ₐ[k] L` to `𝓞 K`.  -/
NumberField.RingOfIntegers.mapAlgEquiv : {k : Type u_3} →
  {K : Type u_4} →
    {L : Type u_5} →
      {E : Type u_6} →
        [inst : Field k] →
          [inst_1 : Field K] →
            [inst_2 : Field L] →
              [inst_3 : Algebra k K] →
                [inst_4 : Algebra k L] →
                  [inst_5 : EquivLike E K L] →
                    [AlgEquivClass E k K L] →
                      E → NumberField.RingOfIntegers K ≃ₐ[NumberField.RingOfIntegers k] NumberField.RingOfIntegers L
-- Mathlib.Algebra.Order.Archimedean.Class
/-- An open ball defined by `FiniteMulArchimedeanClass.subgroup` of `UpperSet.Ioi c`.  -/
FiniteMulArchimedeanClass.ballSubgroup : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedMonoid M] → FiniteMulArchimedeanClass M → Subgroup M
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
coeff_addMonoidAlgebraAddEquivDirectSum_symm_apply_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f : DirectSum ι fun x => M), ⇑(addMonoidAlgebraAddEquivDirectSum.symm f).coeff = ⇑f
-- Mathlib.RingTheory.Ideal.Quotient.Basic
/-- A ring is made up of a disjoint union of cosets of an ideal.  -/
Ideal.univ_eq_iUnion_image_add : ∀ {R : Type u_3} [inst : Ring R] (I : Ideal R), Set.univ = ⋃ x, Quotient.out x +ᵥ ↑I
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.lintegral_deterministic : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal} {g : α → β} {a : α}
  (hg : Measurable g) [MeasurableSingletonClass β],
  ∫⁻ (x : β), f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = f (g a)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.card_edgeFinset_turanGraph_add : ∀ {n r : ℕ},
  (SimpleGraph.turanGraph (n + r) r).edgeFinset.card =
    (SimpleGraph.turanGraph n r).edgeFinset.card + n * (r - 1) + r.choose 2
-- Mathlib.ModelTheory.Definability
/-- A constant function is a definable function.  -/
FirstOrder.Language.definableFun_const : ∀ {M : Type u_1} (L : FirstOrder.Language) [inst : L.Structure M] {A : Set M} {a : M} (γ : Type u_4),
  a ∈ A → Set.DefinableFun L A fun x => a
-- Mathlib.Order.BooleanSubalgebra
/-- The maximum Boolean subalgebra of a lattice.  -/
BooleanSubalgebra.instTop : {α : Type u_2} → [inst : BooleanAlgebra α] → Top (BooleanSubalgebra α)