mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.isNoetherian : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [IsNoetherian R M], IsNoetherian R (M ⧸ N)
-- Init.Data.UInt.Bitwise
UInt64.or_not_self : ∀ {a : UInt64}, a ||| ~~~a = -1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_insertMany!_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)},
      List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
        (∀ (a : α), Std.DTreeMap.Internal.Impl.contains a t = true → (List.map Sigma.fst l).contains a = false) →
          (↑(t.insertMany! l)).size = t.size + l.length
-- Mathlib.Order.Bounds.Basic
/-- If `a` is the least element of `s` and `b` is the least element of `t`,
then `min a b` is the least element of `s ∪ t`.  -/
IsLeast.union : ∀ {γ : Type u_3} [inst : LinearOrder γ] {a b : γ} {s t : Set γ}, IsLeast s a → IsLeast t b → IsLeast (s ∪ t) (min a b)
-- Mathlib.Algebra.Category.Grp.Adjunctions
instIsRightAdjointGrpCatMonCatUnits : MonCat.units.IsRightAdjoint
-- Init.Data.AC
Lean.Data.AC.Context.evalList_sort_loop_swap : ∀ {α : Sort u_1} {y : ℕ} (ctx : Lean.Data.AC.Context α),
  Std.Commutative ctx.op →
    ∀ (xs ys : List ℕ),
      Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort.loop xs (y :: ys)) =
        Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort.loop (y :: xs) ys)
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseZoneId : String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.mem_iSup_of_directed : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {ι : Sort u_2} [hι : Nonempty ι] {S : ι → NonUnitalSubsemiring R},
  Directed (fun x1 x2 => x1 ≤ x2) S → ∀ {x : R}, x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
-- Mathlib.Order.OrderDual
/-- Transfer `SDiff` across an `Equiv`.  -/
Equiv.sdiff : {α : Type u_1} → {β : Type u_2} → α ≃ β → [SDiff β] → SDiff α
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Functor.diag_map : ∀ (C : Type u₃) [inst : CategoryTheory.Category.{v₃, u₃} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Functor.diag C).map f = CategoryTheory.Prod.mkHom f f
-- Lean.LocalContext
/-- Returns true when the lctx contains the free variable `e`.
Panics if `e` is not an fvar.  -/
Lean.LocalContext.containsFVar : Lean.LocalContext → Lean.Expr → Bool
-- Mathlib.CategoryTheory.Localization.Prod
/-- The product of two (constructed) localized categories satisfies the universal
property of the localized category of the product.  -/
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        (W₁ : CategoryTheory.MorphismProperty C₁) →
          (W₂ : CategoryTheory.MorphismProperty C₂) →
            {E : Type u₅} →
              [inst_2 : CategoryTheory.Category.{v₅, u₅} E] →
                [W₁.ContainsIdentities] →
                  [W₂.ContainsIdentities] →
                    CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (W₁.Q.prod W₂.Q) (W₁.prod W₂) E
-- Std.Data.ExtTreeSet.Basic
/-- Transforms the tree set into a list of elements in ascending order.  -/
Std.ExtTreeSet.toList : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → List α
-- Mathlib.Analysis.Normed.Group.Uniform
uniformContinuous_norm : ∀ {E : Type u_2} [inst : SeminormedAddGroup E], UniformContinuous norm
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.instAddCommSemigroup : (R : Type u) → (X : Type v) → [inst : CommRing R] → AddCommSemigroup (FreeLieAlgebra R X)
-- Init.Data.Int.LemmasAux
Int.natCast_sub : ∀ {n m : ℕ}, n ≤ m → ↑(m - n) = ↑m - ↑n
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.addPrecCheck : ℕ → Lean.PrettyPrinter.ParenthesizerM Unit
-- Init.Data.Nat.Gcd
Nat.pow_gcd_pow_of_gcd_eq_one : ∀ {k l n m : ℕ}, n.gcd m = 1 → (n ^ k).gcd (m ^ l) = 1
-- Mathlib.RingTheory.Invariant.Basic
/-- The stabilizer subgroup of `Q` surjects onto `Aut((B/Q)/(A/P))`.  -/
Ideal.Quotient.stabilizerHom_surjective : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [inst_3 : Group G] [Finite G] [inst_5 : MulSemiringAction G B] [inst_6 : SMulCommClass G A B] (P : Ideal A)
  (Q : Ideal B) [Q.IsPrime] [inst_8 : Q.LiesOver P] [Algebra.IsInvariant A B G],
  Function.Surjective ⇑(Ideal.Quotient.stabilizerHom Q P G)
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Build an isomorphism in the category `CommMonCat` from a `MulEquiv` between `CommMonoid`s.  -/
MulEquiv.toCommMonCatIso : {X Y : Type u} → [inst : CommMonoid X] → [inst_1 : CommMonoid Y] → X ≃* Y → (CommMonCat.of X ≅ CommMonCat.of Y)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapIso_functor_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapIso i).functor.obj X).right = X.right
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.instInfSet.eq_1 : ∀ {M : Type u_1} [inst : Add M],
  AddSubsemigroup.instInfSet = { sInf := fun s => { carrier := ⋂ t ∈ s, ↑t, add_mem' := ⋯ } }
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.eq_add_nullHomotopic : ∀ {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 φ₁ φ₂),
  φ₁ = φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.addOppositeEquiv_symm_apply_coeff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] (x : (HahnSeries Γ R)ᵃᵒᵖ) (a : Γ),
  (HahnSeries.addOppositeEquiv.symm x).coeff a = AddOpposite.op ((AddOpposite.unop x).coeff a)
-- Init.Data.Vector.Lemmas
Vector.toArray_toList : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.toList.toArray = xs.toArray
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rio_eq_none : ∀ {n i : ℕ}, n ≤ i → (*...n).toList[i]? = none
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₂_bind₂ : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] (f : R →+* MvPolynomial σ S) (g : S →+* MvPolynomial σ T) (φ : MvPolynomial σ R),
  (MvPolynomial.bind₂ g) ((MvPolynomial.bind₂ f) φ) = (MvPolynomial.bind₂ ((MvPolynomial.bind₂ g).comp f)) φ
-- Mathlib.Analysis.Fourier.Convolution
/-- Calculate the Fourier transform of the convolution as a symmetric integral.  -/
Real.fourier_bilin_convolution_eq_integral : ∀ {𝕜 : Type u_1} {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedAddCommGroup F₂]
  [inst_4 : NormedAddCommGroup F₃] [inst_5 : InnerProductSpace ℝ E] [inst_6 : FiniteDimensional ℝ E]
  [inst_7 : MeasurableSpace E] [inst_8 : BorelSpace E] [inst_9 : NormedSpace 𝕜 F₁] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : NormedSpace 𝕜 F₃] [inst_12 : NormedSpace ℂ F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) {f₁ : E → F₁} {f₂ : E → F₂},
  MeasureTheory.Integrable f₁ MeasureTheory.volume →
    MeasureTheory.Integrable f₂ MeasureTheory.volume →
      ∀ (ξ : E),
        FourierTransform.fourier (MeasureTheory.convolution f₁ f₂ B MeasureTheory.volume) ξ =
          ∫ (y : E) (x : E), Real.fourierChar (-inner ℝ (y + x) ξ) • (B (f₁ x)) (f₂ y)
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
ArithmeticFunction.ofPowerSeries.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (q : ℕ),
  ArithmeticFunction.ofPowerSeries q =
    {
      toFun := fun f =>
        if hq : 1 < q then
          { toFun := Function.extend (fun x => q ^ x) (fun x => (PowerSeries.coeff x) f) 0, map_zero' := ⋯ }
        else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f),
      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Init.Data.UInt.BasicAux
UInt32.lt_ofNatLT_of_lt : ∀ {n m : ℕ} (h1 : n < UInt32.size), m < UInt32.size → m < n → UInt32.ofNat m < UInt32.ofNatLT n h1
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
Submodule.FG.directLimit.eq_1 : ∀ (R : Type u) [inst : Semiring R] (M : Type u_1) [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq { P // P.FG }],
  Submodule.FG.directLimit R M =
    LinearEquiv.ofBijective
      (Module.DirectLimit.lift R { P // P.FG } (fun P => ↥↑P) (fun ⦃P Q⦄ h => Submodule.inclusion h)
        (fun P => (↑P).subtype) ⋯)
      ⋯
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x},
  IsOpen s → x ∈ s → VectorField.mlieBracketWithin I V W s x = VectorField.mlieBracket I V W x
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.eq_divided_by_X_pow_order_Iff_Unit : ∀ {k : Type u_2} [inst : Field k] {f : PowerSeries k}, f ≠ 0 → (f = f.divXPowOrder ↔ IsUnit f)
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
/-- The internal element which points at the given morphism.  -/
CategoryTheory.internalizeHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {A Y : C} →
        [inst_2 : CategoryTheory.Closed A] → (A ⟶ Y) → (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A ⟹ Y)
-- Init.Data.Float.Float
/-- Non-strict inequality of floating-point numbers. Typically used via the `≤` operator.
 -/
Float.le : Float → Float → Bool
-- Mathlib.Topology.Separation.Hausdorff
Prod.t2Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T2Space X] [inst_2 : TopologicalSpace Y] [T2Space Y],
  T2Space (X × Y)
-- Mathlib.ModelTheory.Complexity
/-- A quantifier-free formula is a formula defined without quantifiers. These are all equivalent
to Boolean combinations of atomic formulas.  -/
FirstOrder.Language.BoundedFormula.IsQF : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → Prop
-- Mathlib.Analysis.Convex.Topology
/-- If we dilate a convex set about a point in its interior by a scale `t > 1`, the interior of
the result includes the closure of the original set.

TODO Generalise this from convex sets to sets that are balanced / star-shaped about `x`.  -/
Convex.closure_subset_interior_image_homothety_of_one_lt : ∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E] {s : Set E},
  Convex ℝ s → ∀ {x : E}, x ∈ interior s → ∀ (t : ℝ), 1 < t → closure s ⊆ interior (⇑(AffineMap.homothety x t) '' s)
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.sum_of : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (j : ι)
  (x : AdicCompletion I (M j)),
  (AdicCompletion.sum I M) ((DirectSum.of (fun i => AdicCompletion I (M i)) j) x) =
    (AdicCompletion.map I (DirectSum.lof R ι M j)) x
-- Mathlib.Data.Multiset.MapFold
Multiset.coe_foldr_swap : ∀ {α : Type u_1} {β : Type v} (f : α → β → β) [inst : LeftCommutative f] (b : β) (l : List α),
  Multiset.foldr f b ↑l = List.foldl (fun x y => f y x) b l
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.instMonoιE : ∀ {C : Type u_2} {ι : Type u_4} [inst : CategoryTheory.Category.{u_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂), CategoryTheory.Mono (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.regulator_eq_regOfFamily_fundSystem : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.Units.regulator K = NumberField.Units.regOfFamily (NumberField.Units.fundSystem K)
-- Init.Data.Format.Basic
Std.Format.FlattenBehavior.allOrNone.sizeOf_spec : sizeOf Std.Format.FlattenBehavior.allOrNone = 1
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoOps.toDoOpsRef : Lean.Elab.Do.DoOps → Lean.Elab.Do.DoOpsRef
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.isSheaf_of_isTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) {X : A} (hX : CategoryTheory.Limits.IsTerminal X),
  CategoryTheory.Presheaf.IsSheaf J ((CategoryTheory.Functor.const Cᵒᵖ).obj X)
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.mem_of_isSquare : ∀ {R : Type u_1} [inst : CommRing R] (P : RingPreordering R) {x : R}, IsSquare x → x ∈ P
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.maxEntry?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxEntry? = t₂.maxEntry?
-- Mathlib.NumberTheory.FLT.Basic
isCoprime_of_gcd_eq_one_of_FLT : ∀ {n : ℕ} {a b c : ℤ}, {a, b, c}.gcd id = 1 → a ^ n + b ^ n + c ^ n = 0 → IsCoprime a b
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
/-- **Alias** of `ModularForm.eisensteinSeriesMF`.

---

This defines Eisenstein series as modular forms of weight `k`, level `Γ(N)` and congruence
condition given by `a : Fin 2 → ZMod N`.  -/
ModularForm.eisensteinSeries_MF : {k : ℤ} →
  {N : ℕ} →
    [NeZero N] →
      3 ≤ k →
        (Fin 2 → ZMod N) → ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Polarization identity: The real inner product, in terms of the norm.  -/
real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  inner ℝ x y = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.functorToCore_inclusion : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Core.functorToCore (CategoryTheory.Core.inclusion C) =
    CategoryTheory.Functor.id (CategoryTheory.Core C)
-- Mathlib.Topology.Algebra.Ring.Compact
IsDedekindDomain.isOpen_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R]
  [IsDedekindDomain R], ¬IsField R → ∀ {I : Ideal R}, IsOpen ↑I ↔ I ≠ ⊥
-- Mathlib.Topology.ContinuousMap.Basic
Topology.IsQuotientMap.homeomorph_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)}
  (hf : Topology.IsQuotientMap ⇑f) (a : Quotient (Setoid.ker ⇑f)), hf.homeomorph a = Setoid.kerLift (⇑f) a
-- Mathlib.ModelTheory.DirectLimit
/-- Given a chain of embeddings of structures indexed by `ℕ`, defines a `DirectedSystem` by
composing them.  -/
FirstOrder.Language.DirectedSystem.natLERec : {L : FirstOrder.Language} →
  {G' : ℕ → Type w} →
    [inst : (i : ℕ) → L.Structure (G' i)] →
      ((n : ℕ) → L.Embedding (G' n) (G' (n + 1))) → (m n : ℕ) → m ≤ n → L.Embedding (G' m) (G' n)
-- Lean.Data.Json.FromToJson.Basic
Lean.Option.toJson : {α : Type u_1} → [Lean.ToJson α] → Option α → Lean.Json
-- Mathlib.Computability.EpsilonNFA
εNFA.accept_zero : ∀ {α : Type u} {σ : Type v}, εNFA.accept 0 = ∅
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.probReal_compl_eq_one_sub₀ : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.NullMeasurableSet s μ → μ.real sᶜ = 1 - μ.real s
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.leadingCoeff_cubic : ∀ {R : Type u} {a b c d : R} [inst : Semiring R],
  a ≠ 0 →
    (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X +
          Polynomial.C d).leadingCoeff =
      a
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_empty : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] (f : α → M), ∅.mulIndicator f = fun x => 1
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.coveringNumber_eq_one_of_ediam_le : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal},
  A.Nonempty → Metric.ediam A ≤ ↑ε → Metric.coveringNumber ε A = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)} (h : m.WF) {hc : k' ∈ m.alter k f},
  (m.alter k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.sigma_condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} (K : CategoryTheory.Limits.Multicofork I)
  {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c)
  {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d) {Z : C} (h : K.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.fstSigmaMapOfIsColimit d hc)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.IsColimit.desc hd K.π) h) =
    CategoryTheory.CategoryStruct.comp (I.sndSigmaMapOfIsColimit d hc)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.IsColimit.desc hd K.π) h)
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.insertIfNew_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α}
  {b : β a}, m.insertIfNew a b = ↑(Std.DHashMap.Internal.Raw₀.insertIfNew ⟨m, ⋯⟩ a b)
-- Init.Data.BitVec.Lemmas
BitVec.lt_ofFin : ∀ {n : ℕ} {x : BitVec n} {y : Fin (2 ^ n)}, x < { toFin := y } ↔ x.toFin < y
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] {A : E →SL[σ] F} {x : E},
  (ContinuousLinearMapWOT.ofCLM A) x = A x
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- A point in the mulAntidiagonal is determined by its second coordinate.

See also `Finset.mulAntidiagonal_congr`.  -/
Finset.HasMulAntidiagonal.mulAntidiagonal_congr' : ∀ {A : Type u_1} [inst : CancelCommMonoid A] [inst_1 : Finset.HasMulAntidiagonal A] {p q : A × A} {n : A},
  p ∈ Finset.HasMulAntidiagonal.mulAntidiagonal n →
    q ∈ Finset.HasMulAntidiagonal.mulAntidiagonal n → (p = q ↔ p.2 = q.2)
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.coe_inv_coe : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {X Y : ↑S.objs}
  (p : ↑(S.arrows ↑X ↑Y)), ↑(CategoryTheory.Groupoid.inv p) = CategoryTheory.Groupoid.inv ↑p
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.instIsScalarTower : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] (I : Ideal R) (M : Type u_4)
  [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : SMul S T] [inst_4 : SMul S R] [inst_5 : SMul T R]
  [inst_6 : SMul S M] [inst_7 : SMul T M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower T R M]
  [IsScalarTower S T M], IsScalarTower S T (AdicCompletion I M)
-- Init.Data.Nat.Basic
Nat.zero_mul : ∀ (n : ℕ), 0 * n = 0
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Over the complex numbers, present the logarithmic counting function attached to the divisor of a
meromorphic function `f` as a circle average over `log ‖f ·‖`.

This is a reformulation of Jensen's formula of complex analysis. See
`MeromorphicOn.circleAverage_log_norm` for Jensen's formula in the original context.
 -/
Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const : ∀ {R : ℝ} {f : ℂ → ℂ},
  Meromorphic f →
    R ≠ 0 →
      Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f Set.univ) R =
        Real.circleAverage (fun x => Real.log ‖f x‖) 0 R - Real.log ‖meromorphicTrailingCoeffAt f 0‖
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
CategoryTheory.Limits.PreservesColimitsOfShape.underPost : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {X : C} {F : CategoryTheory.Functor C D}
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.WithInitial J) F],
  CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.Under.post F)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.singleton_eq_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a : α}, {a} = ∅.insert a
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
ConditionallyCompleteLinearOrderBot.mk : {α : Type u_5} →
  [toConditionallyCompleteLinearOrder : ConditionallyCompleteLinearOrder α] →
    [toOrderBot : OrderBot α] → sSup ∅ = ⊥ → ConditionallyCompleteLinearOrderBot α
-- Mathlib.Algebra.Group.Units.Defs
/-- `IsUnit x` is decidable if we can decide if `x` comes from `Mˣ`.  -/
IsUnit.instDecidableOfExistsUnitsEqVal : {M : Type u_1} → [inst : Monoid M] → (x : M) → [h : Decidable (∃ u, ↑u = x)] → Decidable (IsUnit x)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.incl_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : C) (x : PUnit.{w + 1}),
  ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X).obj x = X
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.ofArchimedean_apply : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {R : Type u_2}
  [inst_3 : LinearOrder R] [inst_4 : CommRing R] [inst_5 : IsStrictOrderedRing R] [inst_6 : Archimedean R]
  (f : R →+*o K) (r : R),
  (ArchimedeanClass.FiniteResidueField.ofArchimedean f) r =
    ArchimedeanClass.FiniteResidueField.mk (ArchimedeanClass.FiniteElement.mk (f r) ⋯)
-- Init.System.IO
_private.Init.System.IO.0.IO.Process.Child.mk : {cfg : IO.Process.StdioConfig} →
  cfg.stdin.toHandleType → cfg.stdout.toHandleType → cfg.stderr.toHandleType → IO.Process.Child cfg
-- Mathlib.Algebra.Notation.Support
Function.support_prodMk : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N] (f : ι → M) (g : ι → N),
  (Function.support fun x => (f x, g x)) = Function.support f ∪ Function.support g
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
/-- If `F` is a field, `A` is an `F`-algebra with fraction field `K`, `L` is a field,
`g : A →ₐ[F] L` lifts to `f : K →ₐ[F] L`,
then the image of `f` is the field generated by the image of `g`.
Note: this does not require `IsScalarTower F A K`.  -/
IsFractionRing.algHom_fieldRange_eq_of_comp_eq : ∀ {F : Type u_1} {A : Type u_2} {K : Type u_3} {L : Type u_4} [inst : Field F] [inst_1 : CommRing A]
  [inst_2 : Algebra F A] [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra A K] [IsFractionRing A K]
  [inst_7 : Field L] [inst_8 : Algebra F L] {g : A →ₐ[F] L} {f : K →ₐ[F] L},
  (↑f).comp (algebraMap A K) = ↑g → f.fieldRange = IntermediateField.adjoin F ↑g.range