mathlib-initiative/mathlib-types huggingface dataset:
-- Init.MetaTypes
/-- If `instances` is `true`, `dsimp` will visit instance arguments.
If option `backward.dsimp.instances` is `true`, it overrides this field.
 -/
Lean.Meta.DSimp.Config.instances : Lean.Meta.DSimp.Config → Bool
-- Lean.Expr
Lean.Expr.appFn!' : Lean.Expr → Lean.Expr
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.mul_iff_right : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : CommGroup β] [IsTopologicalGroup β],
  MeasureTheory.AEStronglyMeasurable f μ →
    (MeasureTheory.AEStronglyMeasurable (f * g) μ ↔ MeasureTheory.AEStronglyMeasurable g μ)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.revlexWF.match_1.eq_3 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (p : Lean.Grind.CommRing.Power)
  (m : Lean.Grind.CommRing.Mon) (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit)
  (h_2 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m))
  (h_3 :
    (p : Lean.Grind.CommRing.Power) →
      (m : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit)
  (h_4 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)),
  (match Lean.Grind.CommRing.Mon.mult p m, Lean.Grind.CommRing.Mon.unit with
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => h_1 ()
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.mult p m => h_2 p m
    | Lean.Grind.CommRing.Mon.mult p m, Lean.Grind.CommRing.Mon.unit => h_3 p m
    | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_4 pw₁ m₁ pw₂ m₂) =
    h_3 p m
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {km fallback : α},
  t.max? = some km → t.getD km fallback = km
-- Mathlib.Algebra.Torsor.Basic
/-- A product of `Torsor`s is a `Torsor`.  -/
Pi.instTorsor : {I : Type u} →
  {fg : I → Type v} →
    [inst : (i : I) → Group (fg i)] →
      {fp : I → Type w} → [(i : I) → Torsor (fg i) (fp i)] → Torsor ((i : I) → fg i) ((i : I) → fp i)
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsLower.isTopologicalSpace_basis : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] [t : TopologicalSpace α] [Topology.IsLower α] (U : Set α),
  IsOpen U ↔ U = Set.univ ∨ ∃ a, (Set.Ici a)ᶜ = U
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
HomotopyCategory.Plus.localizerMorphism_derives : ∀ {C : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} H] (F : CategoryTheory.Functor (HomotopyCategory.Plus C) H),
  (HomotopyCategory.Plus.localizerMorphism C).Derives F
-- Init.GrindInstances.ToInt
Lean.Grind.instDivUInt32UintOfNatNat : Lean.Grind.ToInt.Div UInt32 (Lean.Grind.IntInterval.uint 32)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.instLE : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → LE hI.SubDPIdeal
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.vonStaudtIndicator.eq_1 : ∀ (k p : ℕ), Bernoulli.vonStaudtIndicator✝ k p = if p - 1 ∣ k then 1 else 0
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv,
and the derivative of the `n`-th derivative.  -/
iteratedFDeriv_succ_eq_comp_left : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : ℕ},
  iteratedFDeriv 𝕜 (n + 1) f =
    ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)
-- Mathlib.Order.Preorder.Chain
IsChain.superChain_succChain : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsChain r s → ¬IsMaxChain r s → SuperChain r s (SuccChain r s)
-- Std.Do.PostCond
Std.Do.ExceptConds.false_imp : ∀ {ps : Std.Do.PostShape} {x : Std.Do.ExceptConds ps}, (Std.Do.ExceptConds.false →ₑ x) = Std.Do.ExceptConds.true
-- Lean.Level
Lean.instReprLevel.repr : Lean.Level → ℕ → Std.Format
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isSeparator_separator : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.HasSeparator C],
  CategoryTheory.IsSeparator (CategoryTheory.separator C)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.id_toAffineMap : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P],
  AffineIsometry.id.toAffineMap = AffineMap.id 𝕜 P
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyMap_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.ShortComplex.leftHomologyMap 0 = 0
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.coe_top : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], ↑⊤ = Set.univ
-- Mathlib.Data.Real.Basic
Real.ofCauchy_add : ∀ (a b : CauSeq.Completion.Cauchy abs), { cauchy := a + b } = { cauchy := a } + { cauchy := b }
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot : ∀ {X : AlgebraicGeometry.Scheme}, Subsingleton ↑(X.presheaf.obj (Opposite.op ⊥))
-- Mathlib.Topology.TietzeExtension
/-- **Tietze extension theorem** for real-valued bounded continuous maps, a version with a closed
embedding and bundled composition. If `e : C(X, Y)` is a closed embedding of a topological space
into a normal topological space and `f : X →ᵇ ℝ` is a bounded continuous function, then there exists
a bounded continuous function `g : Y →ᵇ ℝ` of the same norm such that `g ∘ e = f`.  -/
BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding' : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NormalSpace Y]
  (f : BoundedContinuousFunction X ℝ) (e : C(X, Y)),
  Topology.IsClosedEmbedding ⇑e → ∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.harmonicOnNhd : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → InnerProductSpace.HarmonicOnNhd f s
-- Mathlib.Topology.Order.DenselyOrdered
right_nhdsWithin_Ioo_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  a < b → (nhdsWithin b (Set.Ioo a b)).NeBot
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (x, y / x)` as a `MeasurableEquiv` with inverse `(x, y) ↦ (x, yx)`  -/
MeasurableEquiv.shearDivRight : (G : Type u_1) →
  [inst : MeasurableSpace G] → [inst_1 : Group G] → [MeasurableMul₂ G] → [MeasurableInv G] → G × G ≃ᵐ G × G
-- Init.Data.Vector.Lemmas
Vector.any_eq_false : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.any p = false ↔ ∀ (i : ℕ) (x : i < n), ¬p xs[i] = true
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Limits.limitCompCoyonedaIsoCone_hom : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) (X : C),
  (CategoryTheory.Limits.limitCompCoyonedaIsoCone F X).hom =
    TypeCat.ofHom fun a =>
      {
        app := fun j =>
          (CategoryTheory.ConcreteCategory.hom
              (CategoryTheory.Limits.limit.π (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))) j))
            a,
        naturality := ⋯ }
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `α ≫ (β ≫ η ≫ ηs)`  -/
Mathlib.Tactic.BicategoryLike.MkEvalComp.mkEvalCompNilCons : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalComp m] →
    Mathlib.Tactic.BicategoryLike.Structural →
      Mathlib.Tactic.BicategoryLike.Structural →
        Mathlib.Tactic.BicategoryLike.WhiskerLeft → Mathlib.Tactic.BicategoryLike.NormalExpr → m Lean.Expr
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
/-- Given a family of maps `f : K → (j ⟶ j')` in a `κ`-filtered category `J`,
with `HasCardinalLT K κ`, and `k : K`, this is a choice of morphism `j' ⟶ coeq f hK`.  -/
CategoryTheory.IsCardinalFiltered.coeqHom : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {κ : Cardinal.{w}} →
      [hκ : Fact κ.IsRegular] →
        [inst_1 : CategoryTheory.IsCardinalFiltered J κ] →
          {K : Type v'} →
            {j j' : J} →
              (f : K → (j ⟶ j')) → (hK : HasCardinalLT K κ) → j' ⟶ CategoryTheory.IsCardinalFiltered.coeq f hK
-- Mathlib.RingTheory.TensorProduct.Basic
TensorProduct.mk_surjective : ∀ (R : Type u_1) (M : Type u_2) (S : Type u_3) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring S] [inst_4 : Algebra R S],
  Function.Surjective ⇑(algebraMap R S) → Function.Surjective ⇑((TensorProduct.mk R S M) 1)
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- Compose two partial isomorphisms, restricting to the intersection of the intermediate opens.  -/
AlgebraicGeometry.Scheme.PartialIso.trans : {X Y Z : AlgebraicGeometry.Scheme} → X.PartialIso Y → Y.PartialIso Z → X.PartialIso Z
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.forget_obj : ∀ (X : AlgebraicGeometry.Scheme), AlgebraicGeometry.Scheme.forget.obj X = ↥X
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map'_comp_π : ∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct g] (p : β → α)
  (q : (b : β) → f (p b) ⟶ g b) (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.Limits.Pi.π g b) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (p b)) (q b)
-- Lean.Compiler.IR.Basic
/-- Store `y : Usize` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1.  -/
Lean.IR.FnBody.uset : Lean.IR.VarId → ℕ → Lean.IR.VarId → Lean.IR.FnBody → Lean.IR.FnBody
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.mapId_inv_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] {X : B} (M : P.Obj X),
  (P.mapId X).inv.app M = CategoryTheory.ObjectProperty.homMk ((F.mapId X).inv.toNatTrans.app M.obj)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_eq_cons_iff : ∀ {xs : List ℤ} {m n a : ℤ}, (m<...=n).toList = a :: xs ↔ m + 1 = a ∧ m < n ∧ ((m + 1)<...=n).toList = xs
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
Std.Iterators.Types.DropWhile.PlausibleStep.dropped : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} {it : Std.IterM m β} {it' : Std.IterM m β} {out : β},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out) →
    it.internalState.dropping = true →
      (P out).Property { down := true } →
        Std.Iterators.Types.DropWhile.PlausibleStep it
          (Std.IterStep.skip (Std.IterM.Intermediate.dropWhileWithPostcondition P true it'))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntryD_cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  {fallback : (a : α) × β a},
  Std.Internal.List.getEntryD a fallback (⟨k, v⟩ :: l) =
    bif k == a then ⟨k, v⟩ else Std.Internal.List.getEntryD a fallback l
-- Init.Data.List.MinMax
List.min?_eq_min?_attach : ∀ {α : Type u_1} [inst : Min α] [inst_1 : Std.MinEqOr α] {xs : List α}, xs.min? = Option.map Subtype.val xs.attach.min?
-- Init.Data.List.Find
List.find?_flatten : ∀ {α : Type u_1} {xss : List (List α)} {p : α → Bool}, List.find? p xss.flatten = List.findSome? (List.find? p) xss
-- Std.Time.Time.PlainTime
/-- Adds hours to a `PlainTime`.
 -/
Std.Time.PlainTime.addHours : Std.Time.PlainTime → Std.Time.Hour.Offset → Std.Time.PlainTime
-- Mathlib.Data.Set.Pairwise.Basic
/-- For a nonempty set `s`, a function `f` takes pairwise equal values on `s` if and only if
for some `z` in the codomain, `f` takes value `z` on all `x ∈ s`. See also
`Set.pairwise_eq_iff_exists_eq` for a version that assumes `[Nonempty ι]` instead of
`Set.Nonempty s`.  -/
Set.Nonempty.pairwise_eq_iff_exists_eq : ∀ {α : Type u_1} {ι : Type u_4} {s : Set α},
  s.Nonempty → ∀ {f : α → ι}, (s.Pairwise fun x y => f x = f y) ↔ ∃ z, ∀ x ∈ s, f x = z
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.range_coe : ∀ {R : Type u_1} [inst : Zero R], Set.range DFunLike.coe = {f | f 0 = 0}
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support : ∀ {α : Type u_2} {x y : α} {f : Equiv.Perm α} [inst : DecidableEq α] [inst_1 : Fintype α],
  f.SameCycle x y → x ∈ f.support → ∃ i < (f.cycleOf x).support.card, (f ^ i) x = y
-- Init.Data.List.Nat.TakeDrop
/-- Dropping the elements up to `i` in `l₁ ++ l₂` is the same as dropping the elements up to `i`
in `l₁`, dropping the elements up to `i - l₁.length` in `l₂`, and appending them.  -/
List.drop_append : ∀ {α : Type u_1} {l₁ l₂ : List α} {i : ℕ}, List.drop i (l₁ ++ l₂) = List.drop i l₁ ++ List.drop (i - l₁.length) l₂
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.comap_id : ∀ {K : Type u_2} [inst : Field K] (w : NumberField.InfinitePlace K), w.comap (RingHom.id K) = w
-- Mathlib.Data.List.GetD
List.getD_eq_getElem? : ∀ {α : Type u} (l : List α) (d : α) (i : Fin l.length), l.getD (↑i) d = l[i]?.get ⋯
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_sub : ∀ (a b : UInt64), (a - b).toUInt32 = a.toUInt32 - b.toUInt32
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Algebra.IsIntegral.of_injective : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_5} {B : Type u_6} [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
  Function.Injective ⇑f → ∀ [Algebra.IsIntegral R B], Algebra.IsIntegral R A
-- Mathlib.Data.Finmap
Finmap.instDecidableRelDisjoint : {α : Type u} → {β : α → Type v} → [DecidableEq α] → DecidableRel Finmap.Disjoint
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mul_nonsing_inv_cancel_left : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (A : Matrix n n α) (B : Matrix n m α), IsUnit A.det → A * (A⁻¹ * B) = B
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
MonoidAlgebra.comul_single : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] {X : Type u_3} [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (x : X) (a : A),
  CoalgebraStruct.comul (MonoidAlgebra.single x a) =
    (TensorProduct.map (MonoidAlgebra.lsingle x) (MonoidAlgebra.lsingle x)) (CoalgebraStruct.comul a)
-- Init.Data.List.Count
List.countP_le_length : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.countP p l ≤ l.length
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- **Alias** of `ContMDiff.smoothSheafHom_hom_app_hom`. -/
ContMDiff.smoothSheafHom_hom_app_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} {M : Type u} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] {N : Type u}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H N] {EP : Type u_7} [inst_11 : NormedAddCommGroup EP]
  [inst_12 : NormedSpace 𝕜 EP] {HP : Type u_8} [inst_13 : TopologicalSpace HP] (IP : ModelWithCorners 𝕜 EP HP)
  (P : Type u) [inst_14 : TopologicalSpace P] [inst_15 : ChartedSpace HP P] (f : M → P) (hf : ContMDiff IM IP (↑⊤) f)
  (U : (TopologicalSpace.Opens ↑(TopCat.of P))ᵒᵖ),
  CategoryTheory.ConcreteCategory.hom ((ContMDiff.smoothSheafHom IP P f hf).hom.app U) =
    { toFun := fun g => ⟨↑g ∘ (↑(Opposite.unop U)).restrictPreimage f, ⋯⟩ }
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.Lp.indicatorConstLp_compMeasurePreserving : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {β : Type u_3} [inst_1 : MeasurableSpace β] {μb : MeasureTheory.Measure β} {f : α → β}
  {s : Set β} (hs : MeasurableSet s) (hμs : μb s ≠ ⊤) (c : E) (hf : MeasureTheory.MeasurePreserving f μ μb),
  (MeasureTheory.Lp.compMeasurePreserving f hf) (MeasureTheory.indicatorConstLp p hs hμs c) =
    MeasureTheory.indicatorConstLp p ⋯ ⋯ c
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.compLpₗ₂_apply : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] {𝕜 : Type u_6} [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : NormedSpace 𝕜 E]
  {F : Type u_8} {G : Type u_9} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (B : G →L[𝕜] E →L[𝕜] F) (g : G),
  (ContinuousLinearMap.compLpₗ₂ p μ B) g = ContinuousLinearMap.compLpₗ p μ (B g)
-- Init.Grind.AC
Lean.Grind.AC.Seq.sort'_k_eq_sort' : ∀ (s acc : Lean.Grind.AC.Seq), s.sort'_k acc = s.sort' acc
-- Init.Data.Bool
Bool.xor_left_inj : ∀ {x y z : Bool}, (x ^^ z) = (y ^^ z) ↔ x = y
-- Mathlib.RingTheory.Jacobson.Radical
Module.jacobson_lt_top : ∀ (R : Type u_1) (M : Type u_3) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial M]
  [IsCoatomic (Submodule R M)], Module.jacobson R M < ⊤
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeffOn.const_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} (f : ℝ → E) (c : ℂ) (n : ℤ)
  (hab : a < b), fourierCoeffOn hab (c • f) n = c • fourierCoeffOn hab f n
-- Mathlib.CategoryTheory.PEmpty
/-- Equivalence between two empty categories.  -/
CategoryTheory.emptyEquivalence : CategoryTheory.Discrete PEmpty.{w + 1} ≌ CategoryTheory.Discrete PEmpty.{v + 1}
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Trie.node : {α : Type} →
  Array α →
    Lean.Meta.LazyDiscrTree.TrieIndex →
      Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex →
        Array (Lean.Meta.LazyDiscrTree.LazyEntry α) → Lean.Meta.LazyDiscrTree.Trie α
-- Mathlib.Algebra.BigOperators.Pi
eqOn_finsetProd : ∀ {ι : Type u_8} {α : Type u_9} {β : Type u_10} [inst : CommMonoid α] {s : Set β} {f f' : ι → β → α},
  (∀ (i : ι), Set.EqOn (f i) (f' i) s) → ∀ (v : Finset ι), Set.EqOn (∏ i ∈ v, f i) (∏ i ∈ v, f' i) s
-- Lean.Meta.Tactic.Grind.SimpUtil
_private.Lean.Meta.Tactic.Grind.SimpUtil.0.Lean.Meta.Grind.isBoolEqTarget : Lean.Name → Bool
-- Lean.Meta.Match.Match
Lean.Meta.Match.State.mk.inj : ∀ {used : Std.HashSet ℕ} {overlaps : Lean.Meta.Match.Overlaps} {counterExamples : Array (List Lean.Meta.Match.Example)}
  {used_1 : Std.HashSet ℕ} {overlaps_1 : Lean.Meta.Match.Overlaps}
  {counterExamples_1 : Array (List Lean.Meta.Match.Example)},
  { used := used, overlaps := overlaps, counterExamples := counterExamples } =
      { used := used_1, overlaps := overlaps_1, counterExamples := counterExamples_1 } →
    used = used_1 ∧ overlaps = overlaps_1 ∧ counterExamples = counterExamples_1
-- Mathlib.Order.Lattice
Prod.instMin_mathlib : (α : Type u) → (β : Type v) → [Min α] → [Min β] → Min (α × β)
-- Mathlib.Data.Multiset.Sym
Multiset.sym2_eq_zero_iff : ∀ {α : Type u_1} {m : Multiset α}, m.sym2 = 0 ↔ m = 0
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.TZifV1.mk.sizeOf_spec : ∀ (header : Std.Time.TimeZone.TZif.Header) (transitionTimes : Array ℤ) (transitionIndices : Array UInt8)
  (localTimeTypes : Array Std.Time.TimeZone.TZif.LocalTimeType) (abbreviations : Array String)
  (leapSeconds : Array Std.Time.TimeZone.TZif.LeapSecond) (stdWallIndicators utLocalIndicators : Array Bool),
  sizeOf
      { header := header, transitionTimes := transitionTimes, transitionIndices := transitionIndices,
        localTimeTypes := localTimeTypes, abbreviations := abbreviations, leapSeconds := leapSeconds,
        stdWallIndicators := stdWallIndicators, utLocalIndicators := utLocalIndicators } =
    1 + sizeOf header + sizeOf transitionTimes + sizeOf transitionIndices + sizeOf localTimeTypes +
            sizeOf abbreviations +
          sizeOf leapSeconds +
        sizeOf stdWallIndicators +
      sizeOf utLocalIndicators
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_inv : ∀ (x : ℝ), ↑x⁻¹ = (↑x)⁻¹
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.map_ne_zero_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (h : M ≃+ N) {x : M}, h x ≠ 0 ↔ x ≠ 0
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.ofMatrix_symm_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {M : CStarMatrix m n A} {i : m}, CStarMatrix.ofMatrix.symm M i = M i
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_unitOfList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  l.contains k = false → (Std.HashMap.Raw.unitOfList l).getKey? k = none
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instToJsonDidChangeWatchedFilesParams.toJson : Lean.Lsp.DidChangeWatchedFilesParams → Lean.Json
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
/-- `I.minimalPrimes` is the set of ideals that are minimal primes over `I`.  -/
Ideal.minimalPrimes : {R : Type u_1} → [inst : CommSemiring R] → Ideal R → Set (Ideal R)
-- Init.Data.Iterators.Combinators.Take
/-- Given an iterator `it` and a natural number `n`, `it.take n` is an iterator that outputs
up to the first `n` of `it`'s values in order and then terminates.

**Marble diagram:**

```text
it          ---a----b---c--d-e--⊥
it.take 3   ---a----b---c⊥

it          ---a--⊥
it.take 3   ---a--⊥
```

**Termination properties:**

* `Finite` instance: only if `it` is productive
* `Productive` instance: only if `it` is productive

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it`.
 -/
Std.Iter.take : {α β : Type w} → [inst : Std.Iterator α Id β] → ℕ → Std.Iter β → Std.Iter β
-- Lean.Setup
Lean.instInhabitedModuleArtifacts.default : Lean.ModuleArtifacts
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey!_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_4 : Inhabited α] {k k' : α},
  (↑m).WF →
    ∀ {f : Option β → Option β},
      (Std.DHashMap.Internal.Raw₀.Const.alter m k f).getKey! k' =
        if (k == k') = true then if (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).isSome = true then k else default
        else m.getKey! k'
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.tail : ∀ {n : ℕ} {f : List.Vector ℕ n →. ℕ}, Nat.Partrec' f → Nat.Partrec' fun v => f v.tail
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `not_isAddTorsion_iff`.

---

An additive monoid is not a torsion additive monoid if it has an element of infinite order.  -/
AddMonoid.not_isTorsion_iff : ∀ (G : Type u_1) [inst : AddMonoid G], ¬IsAddTorsion G ↔ ∃ g, ¬IsOfFinAddOrder g