mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- To prove something for an arbitrary measurable function into `ℝ≥0∞`, it suffices to show
that the property holds for (multiples of) characteristic functions with finite mass according to
some sigma-finite measure and is closed under addition and supremum of increasing sequences of
functions.

It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions
can be added once we need them (for example in `h_add` it is only necessary to consider the sum of
a simple function with a multiple of a characteristic function and that the intersection
of their images is a subset of `{0}`).  -/
Measurable.ennreal_sigmaFinite_induction : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  {motive : (α → ENNReal) → Prop},
  (∀ (c : ENNReal) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → motive (s.indicator fun x => c)) →
    (∀ ⦃f g : α → ENNReal⦄,
        Disjoint (Function.support f) (Function.support g) →
          Measurable f → Measurable g → motive f → motive g → motive (f + g)) →
      (∀ ⦃f : ℕ → α → ENNReal⦄,
          (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun x => ⨆ n, f n x) →
        ∀ ⦃f : α → ENNReal⦄, Measurable f → motive f
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropy_empty : ∀ {X : Type u_1} {T : X → X} [inst : UniformSpace X], Dynamics.coverEntropy T ∅ = ⊥
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_1.splitter : {n : ℕ} →
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1) →
    (x : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth) →
        (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty) →
          ((l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
              (b : Bool) → motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b))) →
            (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit) → motive x
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Preconnected.sum_sup_edge : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} {v : V} {w : W},
  G.Preconnected → H.Preconnected → ((G ⊕g H) ⊔ SimpleGraph.edge (Sum.inl v) (Sum.inr w)).Preconnected
-- Mathlib.SetTheory.Cardinal.NatCard
Finite.one_lt_card_iff_nontrivial : ∀ {α : Type u_1} [Finite α], 1 < Nat.card α ↔ Nontrivial α
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- A compact subset has finite measure for a measure which is finite on compacts.  -/
IsCompact.measure_ne_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃K : Set α⦄, IsCompact K → μ K ≠ ⊤
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.SigmaFinite.of_trim : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
  [MeasureTheory.SigmaFinite (μ.trim hm)], MeasureTheory.SigmaFinite μ
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.le_total_ideal : ∀ (A : Type u) [inst : CommRing A] [PreValuationRing A], Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.instFieldCarrierResidueField : (X : AlgebraicGeometry.LocallyRingedSpace) → (x : ↑X.toTopCat) → Field ↑(X.residueField x)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- If `G` is fully faithful, then `post S F G : (S, F) ⥤ (G(S), F ⋙ G)` is an equivalence.  -/
CategoryTheory.StructuredArrow.isEquivalence_post : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) [G.Full] [G.Faithful], (CategoryTheory.StructuredArrow.post S F G).IsEquivalence
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Twice the circumradius of a triangle may be expressed explicitly as the length of a side
divided by the absolute value of the sine of the angle at the third point (a version of the law
of sines or sine rule).  -/
Affine.Triangle.dist_div_sin_oangle_eq_two_mul_circumradius : ∀ {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)]
  (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        dist (t.points i₁) (t.points i₃) / |(EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).sin| =
          2 * Affine.Simplex.circumradius t
-- Mathlib.Topology.Category.TopCat.Basic
/-- The object in `TopCat` associated to a type equipped with the appropriate
typeclasses.  -/
TopCat.of : (carrier : Type u) → [str : TopologicalSpace carrier] → TopCat
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.split.eq_1 : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (i : ι) (x : ℝ),
  BoxIntegral.Prepartition.split I i x = BoxIntegral.Prepartition.ofWithBot {I.splitLower i x, I.splitUpper i x} ⋯ ⋯
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
/-- Superseded by `isAffine_of_isAffineOpen_basicOpen`.  -/
_private.Mathlib.AlgebraicGeometry.Morphisms.Affine.0.AlgebraicGeometry.isAffine_of_isAffineOpen_basicOpen_aux : ∀ {X : AlgebraicGeometry.Scheme} (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))),
  Ideal.span s = ⊤ → (∀ i ∈ s, AlgebraicGeometry.IsAffineOpen (X.basicOpen i)) → QuasiSeparatedSpace ↥X
-- Batteries.Data.AssocList
Batteries.AssocList.beq_cons_nil : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : Batteries.AssocList α β} [inst : BEq α] [inst_1 : BEq β],
  (Batteries.AssocList.cons a b t == Batteries.AssocList.nil) = false
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.toOplaxMonoidal : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {D : Type u₂} →
        {inst_2 : CategoryTheory.Category.{v₂, u₂} D} →
          {inst_3 : CategoryTheory.MonoidalCategory D} →
            {F : CategoryTheory.Functor C D} → [self : F.Monoidal] → F.OplaxMonoidal
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
/-- The function `expNegInvGlue` is not analytic at `0`.  -/
expNegInvGlue.not_analyticAt_zero : ¬AnalyticAt ℝ expNegInvGlue 0
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If a function is `C^n` with `1 ≤ n` around a point, and its derivative at that point is given to
us as `f'`, then `f'` is also a strict derivative.  -/
ContDiffAt.hasStrictDerivAt' : ∀ {n : WithTop ℕ∞} {𝕂 : Type u_1} [inst : RCLike 𝕂] {F' : Type u_3} [inst_1 : NormedAddCommGroup F']
  [inst_2 : NormedSpace 𝕂 F'] {f : 𝕂 → F'} {f' : F'} {x : 𝕂},
  ContDiffAt 𝕂 n f x → HasDerivAt f f' x → n ≠ 0 → HasStrictDerivAt f f' x
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.right_inv : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : Polynomial A),
  (PolyEquivTensor.toFunAlgHom R A) (PolyEquivTensor.invFun R A x) = x
-- Mathlib.InformationTheory.Hamming
hammingDist.congr_simp : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] {inst_1 : (i : ι) → DecidableEq (β i)}
  [inst_2 : (i : ι) → DecidableEq (β i)] (x x_1 : (i : ι) → β i),
  x = x_1 → ∀ (y y_1 : (i : ι) → β i), y = y_1 → hammingDist x y = hammingDist x_1 y_1
-- Mathlib.Data.EReal.Operations
EReal.instSubNegZeroMonoid : SubNegZeroMonoid EReal
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.edist_smul_Lp : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f g : ↥(MeasureTheory.Lp E p μ)), edist (c • f) (c • g) = edist f g
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.coe_positive : ∀ (R : Type u_2) (E : Type u_3) [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] [inst_6 : PartialOrder E]
  [inst_7 : IsOrderedAddMonoid E] [inst_8 : PosSMulMono R E] [inst_9 : OrderClosedTopology E],
  ↑(ProperCone.positive R E) = Set.Ici 0
-- Init.Grind.AC
Lean.Grind.AC.simp_middle_cert.eq_1 : ∀ (lhs rhs head tail s s' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_middle_cert lhs rhs head tail s s' =
    (s.beq' (head.concat_k (lhs.concat_k tail))).and' (s'.beq' (head.concat_k (rhs.concat_k tail)))
-- Mathlib.Order.Filter.Pointwise
Filter.mem_vadd_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter β} {s : Set β} {a : α},
  s ∈ a +ᵥ f ↔ (fun x => a +ᵥ x) ⁻¹' s ∈ f
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.tmul_one_mul_one_tmul : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] (a₁ : A) (b₂ : B), a₁ ᵍ⊗ₜ[R] 1 * 1 ᵍ⊗ₜ[R] b₂ = a₁ ᵍ⊗ₜ[R] b₂
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aevalTower_toAlgHom : ∀ {R : Type u} {S : Type v} {A' : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring A'] [inst_2 : CommSemiring S]
  [inst_3 : Algebra S R] [inst_4 : Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R),
  (Polynomial.aevalTower g y) ((IsScalarTower.toAlgHom S R (Polynomial R)) x) = g x
-- Mathlib.Algebra.Field.Defs
/-- For a nonzero `a`, `a⁻¹` is a right multiplicative inverse.  -/
Field.mul_inv_cancel : ∀ {K : Type u} [self : Field K] (a : K), a ≠ 0 → a * a⁻¹ = 1
-- Mathlib.Analysis.Real.Pi.Irrational
/-- Auxiliary for the proof that `π` is irrational.
The recursive formula for `I (n + 2) θ * θ ^ 2` in terms of `I n θ` and `I (n + 1) θ`.
 -/
_private.Mathlib.Analysis.Real.Pi.Irrational.0.recursion : ∀ {θ : ℝ} (n : ℕ), I✝ (n + 2) θ * θ ^ 2 = 2 * (↑n + 2) * (2 * ↑n + 3) * I✝ (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I✝ n θ
-- Lean.Elab.Quotation
/-- other, complicated match step that will probably only cover identical patterns
example: antiquotation splices `($[...]*)  -/
Lean.Elab.Term.Quotation.HeadCheck.other : Lean.Syntax → Lean.Elab.Term.Quotation.HeadCheck
-- Init.Prelude
/-- Bijection between `α` and `PLift α`  -/
PLift.down_up : ∀ {α : Sort u} (a : α), { down := a }.down = a
-- Lean.Elab.ConfigEval.Types
Lean.Elab.ConfigEval.ConfigItem.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (option : Lean.Ident) (value : Lean.Syntax) (bool? : Option Bool) (origOptionName : Lean.Name)
  (optionComps prevOptionComps : List Lean.Syntax),
  sizeOf
      { ref := ref, option := option, value := value, bool? := bool?, origOptionName := origOptionName,
        optionComps := optionComps, prevOptionComps := prevOptionComps } =
    1 + sizeOf ref + sizeOf option + sizeOf value + sizeOf bool? + sizeOf origOptionName + sizeOf optionComps +
      sizeOf prevOptionComps
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- A sheaf of modules is a presheaf of modules such that the underlying presheaf
of abelian groups is a sheaf.  -/
SheafOfModules : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      CategoryTheory.Sheaf J RingCat → Type (max (max (max u u₁) (v + 1)) v₁)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.equiv'_symm_apply : ∀ {ι' : Type u_2} {ι : Type u_10} {R : Type u_14} {M : Type u_15} {M' : Type u_16} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  (b : Module.Basis ι R M) (b' : Module.Basis ι' R M') [inst_5 : SMulCommClass R R M'] (f : M → M') (g : M' → M)
  (hf : ∀ (i : ι), f (b i) ∈ Set.range ⇑b') (hg : ∀ (i : ι'), g (b' i) ∈ Set.range ⇑b)
  (hgf : ∀ (i : ι), g (f (b i)) = b i) (hfg : ∀ (i : ι'), f (g (b' i)) = b' i) (i : ι'),
  (b.equiv' b' f g hf hg hgf hfg).symm (b' i) = g (b' i)
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dKernelSequence_g : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_5),
  (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃).g = X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeff_liftIco_eq : ∀ {T : ℝ} [hT : Fact (0 < T)] {a : ℝ} (f : ℝ → ℂ) (n : ℤ),
  fourierCoeff (AddCircle.liftIco T a f) n = fourierCoeffOn ⋯ f n
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_le_iff : ∀ {α : Type u} {M : Matroid α} {X : Set α} {κ : Cardinal.{u}},
  M.cRk X ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → Cardinal.mk ↑I ≤ κ
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.Shatters.mono_left : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 ℬ : Finset (Finset α)} {s : Finset α}, 𝒜 ⊆ ℬ → 𝒜.Shatters s → ℬ.Shatters s
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.foldM_mapM : ∀ {α β γ δ : Type w} {ps : Std.Do.PostShape} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n]
  [inst_5 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Monad o] [LawfulMonad o]
  [inst_10 : Std.Do.WPMonad o ps] [inst_11 : Std.IteratorLoop α m n] [inst_12 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o] [inst_15 : MonadLiftT m n] [inst_16 : MonadLiftT n o]
  [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → n γ} {g : δ → γ → o δ} {init : δ} {it : Std.IterM m β}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.IterM.foldM
        (fun d b => do
          let c ← liftM (f b)
          g d c)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.IterM.mapM f it) ⦃Q⦄
-- Init.Control.Lawful.Instances
MonadExcept.orElse.eq_1 : ∀ {ε : Type u} {m : Type v → Type w} [inst : MonadExcept ε m] {α : Type v} (t₁ : m α) (t₂ : Unit → m α),
  MonadExcept.orElse t₁ t₂ = tryCatch t₁ fun x => t₂ ()
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instTop.eq_1 : ∀ {α : Type u_1} [inst : LE α], LowerSet.instTop = { top := { carrier := Set.univ, lower' := ⋯ } }
-- Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
/-- The bijection `ShiftedHom X Y n ≃ ShiftedHom (Opposite.op Y) (Opposite.op X) n` when
`n : ℤ`, and `X` and `Y` are objects of a category equipped with a shift by `ℤ`.  -/
CategoryTheory.ShiftedHom.opEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {X Y : C} →
        (n : ℤ) → CategoryTheory.ShiftedHom X Y n ≃ CategoryTheory.ShiftedHom (Opposite.op Y) (Opposite.op X) n
-- Mathlib.FieldTheory.RatFunc.Luroth
RatFunc.Luroth.generator_mem : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, RatFunc.Luroth.generator E ∈ E
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- In a `p ^ (k + 1)`-th cyclotomic extension of `ℚ`, we have that
`ζ - 1` divides `p` in `𝓞 K`.  -/
IsPrimitiveRoot.toInteger_sub_one_dvd_prime : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))), hζ.toInteger - 1 ∣ ↑p
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.takeEndWhile_eq_takeEndWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.takeEndWhile pat = s.toSlice.takeEndWhile pat
-- Mathlib.Data.Multiset.MapFold
Multiset.map_const' : ∀ {α : Type u_1} {β : Type v} (s : Multiset α) (b : β), Multiset.map (fun x => b) s = Multiset.replicate s.card b
-- Mathlib.LinearAlgebra.Projectivization.Independence
/-- Two points are independent if and only if their underlying vectors are linearly independent.  -/
Projectivization.independent_mk_iff_LinearIndependent : ∀ {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {u v : V}
  (hu : u ≠ 0) (hv : v ≠ 0),
  Projectivization.Independent ![Projectivization.mk K u hu, Projectivization.mk K v hv] ↔ LinearIndependent K ![u, v]
-- Mathlib.Analysis.Normed.Ring.Basic
SubringClass.toNormMulClass : ∀ {S : Type u_5} {R : Type u_6} [inst : SetLike S R] [inst_1 : SeminormedRing R] [NormMulClass R]
  [inst_3 : SubringClass S R] (s : S), NormMulClass ↥s
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.smul_finset_univ₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β] {a : α}
  [inst_3 : Fintype β], a ≠ 0 → a • Finset.univ = Finset.univ
-- Init.Data.Int.Lemmas
Int.subNatNat_add_left : ∀ {m n : ℕ}, Int.subNatNat (m + n) m = ↑n
-- Mathlib.Algebra.Polynomial.Lifts
Polynomial.lifts_iff_set_range : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} (p : Polynomial S),
  p ∈ Polynomial.lifts f ↔ p ∈ Set.range (Polynomial.map f)
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_isBot : ∀ (α : Type u_1) [inst : PartialOrder α], {x | IsBot x}.Subsingleton
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.SafePrefixState.mk.sizeOf_spec : ∀ (goals : Array Lean.MVarId), sizeOf { goals := goals } = 1 + sizeOf goals
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.leibniz_lie : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x : L)
  (D₁ D₂ : LieDerivation R L L), ⁅x, ⁅D₁, D₂⁆⁆ = ⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆
-- Mathlib.Analysis.Complex.TaylorSeries
/-- A function that is complex differentiable on the open ball of radius `r` around `c`
is given by evaluating its Taylor series at `c` on this open ball.  -/
Complex.taylorSeries_eq_on_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : ℝ⦄,
  DifferentiableOn ℂ f (Metric.ball c r) →
    ∀ ⦃z : ℂ⦄, z ∈ Metric.ball c r → ∑' (n : ℕ), (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z
-- Mathlib.Combinatorics.Graph.Basic
Graph.edgeSet_banana : ∀ {α : Type u_1} {β : Type u_2} (u v : α) (edgeSet : Set β), (Graph.banana u v edgeSet).edgeSet = edgeSet
-- Mathlib.CategoryTheory.Triangulated.Functor
_private.Mathlib.CategoryTheory.Triangulated.Functor.0.CategoryTheory.Functor.mapTriangleCommShiftIso_add : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] (n m : ℤ),
  F.mapTriangleCommShiftIso (n + m) =
    CategoryTheory.Functor.CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m)
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.instMembershipOfEquivBEqOfLawfulHashable : {α : Type u} →
  [inst : BEq α] → [inst_1 : Hashable α] → [EquivBEq α] → [LawfulHashable α] → Membership α (Std.ExtHashSet α)
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.addLeftCosetsCompSubtypeVal.eq_1 : ∀ {G : Type u} [inst : AddGroup G] (H I : AddSubgroup G),
  AddAction.addLeftCosetsCompSubtypeVal H I = AddAction.compHom (G ⧸ H) I.subtype
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The bundled commutative ring giving the colimit of a diagram.  -/
CommRingCat.Colimits.colimit : {J : Type v} → [inst : CategoryTheory.SmallCategory J] → CategoryTheory.Functor J CommRingCat → CommRingCat
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] {W : C}
  {i j : CategoryTheory.Limits.multicoequalizer I ⟶ W},
  i = j ↔
    ∀ (b : J.R),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) i =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) j
-- Init.Data.Array.Find
Array.getElem?_zero_filter : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, (Array.filter p xs)[0]? = Array.find? p xs
-- Mathlib.Data.Multiset.Sym
Multiset.sym2_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (m : Multiset α), (Multiset.map f m).sym2 = Multiset.map (Sym2.map f) m.sym2
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.IsTriangulated.toIsStableUnderShift : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.HasShift C ℤ} {inst_3 : CategoryTheory.Preadditive C}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_5 : CategoryTheory.Pretriangulated C}
  {P : CategoryTheory.ObjectProperty C} [self : P.IsTriangulated], P.IsStableUnderShift ℤ
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instCommSemigroup : {α : Type u_1} → [CommSemigroup α] → CommSemigroup αᵒᵈ
-- Mathlib.Order.Monotone.Defs
StrictMono.prodMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] {f : α → γ} {g : β → δ},
  StrictMono f → StrictMono g → StrictMono (Prod.map f g)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.toSL2R_apply : ∀ (z : UpperHalfPlane), z.toSL2R = ⟨!![√z.im, z.re / √z.im; 0, 1 / √z.im], ⋯⟩
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.isAlgebraic_iff : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {S : IntermediateField K L}
  {x : ↥S}, IsAlgebraic K x ↔ IsAlgebraic K ↑x