mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
/-- Given a cocone morphism whose object part is an isomorphism, produce an
isomorphism of cocones.
 -/
CategoryTheory.Limits.Cocone.cocone_iso_of_hom_iso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {K : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cocone K} (f : d ⟶ c) [i : CategoryTheory.IsIso f.hom],
  CategoryTheory.IsIso f
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.coe_inj : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  ⦃η η' : ApplicativeTransformation F G⦄, ((fun {α} => η.app α) = fun {α} => η'.app α) → η = η'
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.module : {S : Type u_2} →
  {R : Type u} →
    {M : Type v} →
      [inst : Semiring S] →
        [inst_1 : AddCommMonoid R] →
          [inst_2 : AddCommMonoid M] → [Module S R] → [Module S M] → Module S (TrivSqZeroExt R M)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.insertMany_list : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ (l : List ((a : α) × β a)), m₁.Equiv m₂ → (m₁.insertMany l).Equiv (m₂.insertMany l)
-- Mathlib.Data.LawfulXor.Basic
instLawfulCommIdentityXorOfNat_mathlib : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [inst_2 : LawfulXor α], Std.LawfulCommIdentity XorOp.xor 0
-- Mathlib.LinearAlgebra.Eigenspace.Matrix
/-- The spectrum of the diagonal operator is the range of the diagonal viewed as a function.  -/
spectrum_diagonal : ∀ {R : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : Field R] (d : n → R),
  spectrum R (Matrix.diagonal d) = Set.range d
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
hasSum_mul_left_iff : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α} {a₁ a₂ : α}, a₂ ≠ 0 → (HasSum (fun i => a₂ * f i) (a₂ * a₁) L ↔ HasSum f a₁ L)
-- Mathlib.NumberTheory.Height.NumberField
/-- The multiplicative height of a tuple of rational numbers that consists of coprime integers
is the maximum of the absolute values of the entries.  -/
Rat.mulHeight_eq_max_abs_of_gcd_eq_one : ∀ {ι : Type u_1} [inst : Fintype ι] [Nonempty ι] {x : ι → ℤ},
  Finset.univ.gcd x = 1 → Height.mulHeight (Int.cast ∘ x) = ↑(⨆ i, |x i|)
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.instCoeIntermediateField : (k : Type u_1) →
  (K : Type u_2) →
    [inst : Field k] →
      [inst_1 : Field K] → [inst_2 : Algebra k K] → Coe (FiniteGaloisIntermediateField k K) (IntermediateField k K)
-- Init.Data.SInt.Basic
instModInt32 : Mod Int32
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] {a b : B} {f g : a ⟶ b} (α : f ⟶ g),
  (P.fullsubcategory.map₂ α).toNatTrans = P.map₂ α
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The naturality condition.  -/
CategoryTheory.Oplax.OplaxTrans.Modification.naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (self : CategoryTheory.Oplax.OplaxTrans.Modification η θ)
  {a b : B} (f : a ⟶ b),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.app b)) (θ.naturality f) =
    CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerRight (self.app a) (G.map f))
-- Batteries.Data.UnionFind.Basic
/-- Union-find node type  -/
Batteries.UFNode : Type
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.Stable.exists_forall_le : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {F F' : I.Filtration M}, F.Stable → F.N 0 ≤ F'.N 0 → ∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.Equivalence_mk'_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C)
  (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse)
  (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D)
  (f :
    ∀ (X : C),
      CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) =
        CategoryTheory.CategoryStruct.id (functor.obj X)),
  { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso,
        functor_unitIso_comp := f }.unit =
    unit_iso.hom
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.darts_toPath_subset_darts`. -/
SimpleGraph.Walk.darts_toPath_subset : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), (↑p.toPath).darts ⊆ p.darts
-- Mathlib.Computability.TuringMachine.Config
/-- `rfind f` performs the function of the `rfind` primitive of partial recursive functions.
`rfind f v` returns the smallest `n` such that `(f (n :: v)).head = 0`.

It is implemented as:

    rfind f v = pred (fix (fun (n::v) => f (n::v) :: n+1 :: v) (0 :: v))

The idea is that the initial state is `0 :: v`, and the `fix` keeps `n :: v` as its internal state;
it calls `f (n :: v)` as the exit test and `n+1 :: v` as the next state. At the end we get
`n+1 :: v` where `n` is the desired output, and `pred (n+1 :: v) = [n]` returns the result.
 -/
Turing.ToPartrec.Code.rfind : Turing.ToPartrec.Code → Turing.ToPartrec.Code
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- The substitution `y = x ^ p` in integrals over `Ioi 0` preserves integrability (version
without `|p|` factor)  -/
MeasureTheory.integrableOn_Ioi_comp_rpow_iff' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) {p : ℝ},
  p ≠ 0 →
    (MeasureTheory.IntegrableOn (fun x => x ^ (p - 1) • f (x ^ p)) (Set.Ioi 0) MeasureTheory.volume ↔
      MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume)
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.w.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (D : ℝ) (x : E),
  ExistsContDiffBumpBase.w D x =
    ((∫ (x : E), ExistsContDiffBumpBase.u x ∂MeasureTheory.Measure.addHaar) * |D| ^ Module.finrank ℝ E)⁻¹ •
      ExistsContDiffBumpBase.u (D⁻¹ • x)
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- Multiplication by a nonzero element `a` on the right
as a `DilationEquiv` of a normed division ring.  -/
DilationEquiv.mulRight : {α : Type u_1} → [inst : NormedDivisionRing α] → (a : α) → a ≠ 0 → α ≃ᵈ α
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` preserves limits of shape `Jᵒᵖ`, then `F.rightOp : C ⥤ Dᵒᵖ` preserves colimits
of shape `J`.  -/
CategoryTheory.Limits.preservesColimitsOfShape_rightOp : ∀ {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] (F : CategoryTheory.Functor Cᵒᵖ D)
  [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.PreservesColimitsOfShape J F.rightOp
-- Mathlib.Topology.UniformSpace.ProdApproximation
ContinuousMap.denseRange_tensorHom : ∀ {X : Type u_5} {Y : Type u_6} {R : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] [CompactSpace X] [T2Space X]
  [CompactSpace Y] [TotallyDisconnectedSpace X], DenseRange ⇑ContinuousMap.tensorHom
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.inter_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ → (m₁ ∩ m₃).Equiv (m₂ ∩ m₃)
-- Mathlib.Tactic.LinearCombination
/-- A value, equivalently a proof of `c = c`.  -/
Mathlib.Tactic.LinearCombination.Expanded.const : Lean.Term → Mathlib.Tactic.LinearCombination.Expanded
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.eq_of_le : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  {f : (i j : ι) → (h : i ≤ j) → T h} [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] (x : (i : ι) × F i) (i : ι)
  (h : x.fst ≤ i), ⟦x⟧ = ⟦⟨i, (f x.fst i h) x.snd⟩⟧
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.applyCell.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} {δ : Type u_4} [inst : Ord α] (k : α)
  (motive :
    (l : Std.DTreeMap.Internal.Impl α β) →
      ((c : Std.DTreeMap.Internal.Cell α β (compare k)) →
          (Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → c.contains = true) → δ) →
        Sort u_3)
  (f :
    (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
      (Std.DTreeMap.Internal.Impl.contains' (compare k) Std.DTreeMap.Internal.Impl.leaf = true → c.contains = true) → δ)
  (h_1 :
    (f :
        (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
          (Std.DTreeMap.Internal.Impl.contains' (compare k) Std.DTreeMap.Internal.Impl.leaf = true →
              c.contains = true) →
            δ) →
      motive Std.DTreeMap.Internal.Impl.leaf f)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (f :
                (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
                  (Std.DTreeMap.Internal.Impl.contains' (compare k) (Std.DTreeMap.Internal.Impl.inner size k' v' l r) =
                        true →
                      c.contains = true) →
                    δ) →
              motive (Std.DTreeMap.Internal.Impl.inner size k' v' l r) f),
  (match Std.DTreeMap.Internal.Impl.leaf, f with
    | Std.DTreeMap.Internal.Impl.leaf, f => h_1 f
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r, f => h_2 size k' v' l r f) =
    h_1 f
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.algEquiv_apply : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} [inst_1 : CommSemiring R]
  [inst_2 : Ring S] [inst_3 : Algebra R S] (v : Valuation S Γ₀) (x : WithVal v), (WithVal.algEquiv R v) x = x.ofVal
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.of_div_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t : Finset α}, (s / t).Nonempty → t.Nonempty
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableOn_exp_mul_Iic : ∀ {a : ℝ}, 0 < a → ∀ (c : ℝ), MeasureTheory.IntegrableOn (fun x => Real.exp (a * x)) (Set.Iic c) MeasureTheory.volume
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.symm_trans_target_eq : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e e' : Bundle.Pretrivialization F proj),
  (e.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ
-- Mathlib.CategoryTheory.Category.Pairwise
/-- Morphisms in the category `CategoryTheory.Pairwise ι`. The only non-identity morphisms are
`left i j : single i ⟶ pair i j` and `right i j : single j ⟶ pair i j`.
 -/
CategoryTheory.Pairwise.Hom : {ι : Type v} → CategoryTheory.Pairwise ι → CategoryTheory.Pairwise ι → Type v
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.range_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {ι : Sort u_5} (a : α) (f : ι → β),
  (Set.range fun i => a +ᵥ f i) = a +ᵥ Set.range f
-- Mathlib.Order.SupClosed
SupClosed.prod : ∀ {α : Type u_3} {β : Type u_4} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {s : Set α} {t : Set β},
  SupClosed s → SupClosed t → SupClosed (s ×ˢ t)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF → ∀ {k a : α} {v : β}, (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ k ∉ m then k else m.getKey! a
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.injective_of_mono : ∀ {X Y : Type u} (f : X ⟶ Y) [hf : CategoryTheory.Mono f], Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.coeff_invOfUnit : ∀ {R : Type u_1} [inst : Ring R] (n : ℕ) (φ : PowerSeries R) (u : Rˣ),
  (PowerSeries.coeff n) (φ.invOfUnit u) =
    if n = 0 then ↑u⁻¹
    else
      -↑u⁻¹ *
        ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n,
          if x.2 < n then (PowerSeries.coeff x.1) φ * (PowerSeries.coeff x.2) (φ.invOfUnit u) else 0
-- Mathlib.ModelTheory.Complexity
_private.Mathlib.ModelTheory.Complexity.0.FirstOrder.Language.BoundedFormula.toPrenexImp.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → L.BoundedFormula α x → Sort u_4)
  (n : ℕ) (φ : L.BoundedFormula α (n + 1)) (ψ : L.BoundedFormula α n)
  (h_1 :
    (n : ℕ) →
      (φ : L.BoundedFormula α (n + 1)) →
        (ψ : L.BoundedFormula α n) →
          motive n ((φ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum)
            ψ)
  (h_2 : (n : ℕ) → (φ : L.BoundedFormula α (n + 1)) → (ψ : L.BoundedFormula α n) → motive n φ.all ψ)
  (h_3 : (x : ℕ) → (φ ψ : L.BoundedFormula α x) → motive x φ ψ),
  (match n, (φ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum, ψ with
    | n, (φ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum, ψ =>
      h_1 n φ ψ
    | n, φ.all, ψ => h_2 n φ ψ
    | x, φ, ψ => h_3 x φ ψ) =
    h_1 n φ ψ
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiff.div_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : DivInvMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G]
  {E' : Type u_5} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6}
  [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace H' M] {f : M → G} (c : G), ContMDiff I' I n f → ContMDiff I' I n fun x => f x / c
-- Mathlib.Probability.Distributions.Gaussian.CharFun
/-- Two Gaussian measures are equal if and only if they have same mean and same covariance. This is
`IsGaussian.ext_iff_covarianceBilinDual` specialized to Hilbert spaces.  -/
ProbabilityTheory.IsGaussian.ext_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {μ : MeasureTheory.Measure E} [inst_5 : InnerProductSpace ℝ E]
  {ν : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [ProbabilityTheory.IsGaussian ν],
  μ = ν ↔
    ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν ∧ ProbabilityTheory.covarianceBilin μ = ProbabilityTheory.covarianceBilin ν
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformFun.toFun_ofFun : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), UniformFun.toFun (UniformFun.ofFun f) = f
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.ici_incl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (c : CategoryTheory.TransfiniteCompositionOfShape J f) (j : J), (c.ici j).incl = ⋯.functor.whiskerLeft c.incl
-- Mathlib.Topology.Connected.PathConnected
Quotient.instPathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Setoid X} [PathConnectedSpace X], PathConnectedSpace (Quotient s)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.contMDiffOn_section_of_subsingleton : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] {s : (x : B) → E x} {u : Set B}
  [Subsingleton F], ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) u
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.isAddLeftInvariant_smul_nnreal : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant]
  (c : NNReal), (c • μ).IsAddLeftInvariant
-- Mathlib.Data.NNReal.Defs
Set.OrdConnected.image_real_toNNReal : ∀ {s : Set ℝ}, s.OrdConnected → (Real.toNNReal '' s).OrdConnected
-- Mathlib.Topology.NhdsWithin
eventually_mem_nhdsWithin_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s t : Set α},
  (∀ᶠ (x' : α) in nhdsWithin x s, t ∈ nhdsWithin x' s) ↔ t ∈ nhdsWithin x s
-- Init.Data.String.Termination
String.Slice.Pos.eq_next_of_next?_eq_some : ∀ {s : String.Slice} {p q : s.Pos} (h : p.next? = some q), q = p.next ⋯
-- Mathlib.NumberTheory.ClassNumber.Finite
/-- Each class in the class group contains an ideal `J`
such that `M := Π m ∈ finsetApprox` is in `J`.  -/
ClassGroup.exists_mk0_eq_mk0 : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (bS : Module.Basis ι R S) (adm : abv.IsAdmissible) [inst_6 : Infinite R] [inst_7 : DecidableEq R]
  [inst_8 : IsDedekindDomain S] [Algebra.IsAlgebraic R S] (I : ↥(nonZeroDivisors (Ideal S))),
  ∃ J, ClassGroup.mk0 I = ClassGroup.mk0 J ∧ (algebraMap R S) (∏ m ∈ ClassGroup.finsetApprox bS adm, m) ∈ ↑J
-- Mathlib.Data.SetLike.Basic
/-- A class to indicate that the canonical injection between `A` and `Set B` is order-preserving.

An instance of this class is automatically available on any partial order defined as
`PartialOrder.ofSetLike`.
 -/
IsConcreteLE : (A : Type u_1) → (B : outParam (Type u_2)) → [SetLike A B] → [LE A] → Prop
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.refl_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) {n : ℕ}
  (i : Fin (n + 1)),
  (CategoryTheory.SimplicialObject.Homotopy.refl f).h i =
    CategoryTheory.CategoryStruct.comp (X.σ i) (f.app (Opposite.op { len := n + 1 }))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_right_mono : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftMono α] {a : α}, Monotone fun x => a + x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.insertMany_append : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {l₁ l₂ : List ((a : α) × β a)},
  t.insertMany (l₁ ++ l₂) = (t.insertMany l₁).insertMany l₂
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.UnicodeLinter.findBadUnicodeAux.eq_def : ∀ (s : String) (pos : s.Pos) (c : Char) (err : Array Mathlib.Linter.TextBased.StyleError✝),
  Mathlib.Linter.TextBased.UnicodeLinter.findBadUnicodeAux✝ s pos c err =
    if h : pos < s.endPos then
      let posₙ := pos.next ⋯;
      match posₙ.get? with
      | none =>
        if (!Mathlib.Linter.TextBased.UnicodeLinter.isAllowedCharacter c) = true then
          err.push (Mathlib.Linter.TextBased.StyleError.unwantedUnicode✝ c)
        else err
      | some cₙ =>
        have this := ⋯;
        if (!Mathlib.Linter.TextBased.UnicodeLinter.isAllowedCharacter c) = true then
          Mathlib.Linter.TextBased.UnicodeLinter.findBadUnicodeAux✝ s posₙ cₙ
            (err.push (Mathlib.Linter.TextBased.StyleError.unwantedUnicode✝ c))
        else
          if
              (cₙ == Mathlib.Linter.TextBased.UnicodeLinter.UnicodeVariant.emoji &&
                    !Mathlib.Linter.TextBased.UnicodeLinter.emojis.contains c &&
                  !Mathlib.Linter.TextBased.UnicodeLinter.unrestricted.contains c) =
                true then
            have errₙ := err.push (Mathlib.Linter.TextBased.StyleError.unicodeVariant✝ (String.ofList [c, cₙ]) none);
            Mathlib.Linter.TextBased.UnicodeLinter.findBadUnicodeAux✝ s posₙ cₙ errₙ
          else
            if
                (cₙ == Mathlib.Linter.TextBased.UnicodeLinter.UnicodeVariant.text &&
                      !Mathlib.Linter.TextBased.UnicodeLinter.nonEmojis.contains c &&
                    !Mathlib.Linter.TextBased.UnicodeLinter.unrestricted.contains c) =
                  true then
              have errₙ := err.push (Mathlib.Linter.TextBased.StyleError.unicodeVariant✝ (String.ofList [c, cₙ]) none);
              Mathlib.Linter.TextBased.UnicodeLinter.findBadUnicodeAux✝ s posₙ cₙ errₙ
            else
              if
                  (cₙ != Mathlib.Linter.TextBased.UnicodeLinter.UnicodeVariant.emoji &&
                      Mathlib.Linter.TextBased.UnicodeLinter.emojis.contains c) =
                    true then
                have errₙ :=
                  err.push
                    (Mathlib.Linter.TextBased.StyleError.unicodeVariant✝ c.toString
                      (some Mathlib.Linter.TextBased.UnicodeLinter.UnicodeVariant.emoji));
                Mathlib.Linter.TextBased.UnicodeLinter.findBadUnicodeAux✝ s posₙ cₙ errₙ
              else
                if
                    (cₙ != Mathlib.Linter.TextBased.UnicodeLinter.UnicodeVariant.text &&
                        Mathlib.Linter.TextBased.UnicodeLinter.nonEmojis.contains c) =
                      true then
                  have errₙ :=
                    err.push
                      (Mathlib.Linter.TextBased.StyleError.unicodeVariant✝ c.toString
                        (some Mathlib.Linter.TextBased.UnicodeLinter.UnicodeVariant.text));
                  Mathlib.Linter.TextBased.UnicodeLinter.findBadUnicodeAux✝ s posₙ cₙ errₙ
                else Mathlib.Linter.TextBased.UnicodeLinter.findBadUnicodeAux✝ s posₙ cₙ err
    else err
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.mul_eval_of_const_left : ∀ (l₁ l₂ : Lean.Omega.LinearCombo) (v : Lean.Omega.Coeffs),
  l₁.coeffs.isZero → (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.reflectsLimitsOfShape_subsingleton : ∀ {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] (F : CategoryTheory.Functor C D),
  Subsingleton (CategoryTheory.Limits.ReflectsLimitsOfShape J F)
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rcc.length_iter : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] [inst_6 : Std.Rxc.HasSize α] [Std.Rxc.LawfulHasSize α] {r : Std.Rcc α},
  r.iter.length = r.size
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
/-- Given a sequence of finite sets `s₀ ⊆ s₁ ⊆ s₂ ⋯`, the product of `gᵢ` over `i ∈ sₙ` is equal
to `∏_{i ∈ s₀} gᵢ` * `∏_{j < n, i ∈ sⱼ₊₁ \ sⱼ} gᵢ`.  -/
Finset.prod_eq_prod_range_sdiff : ∀ {α : Type u_3} {β : Type u_4} [inst : DecidableEq α] [inst_1 : CommMonoid β] (s : ℕ → Finset α),
  Monotone s →
    ∀ (g : α → β) (n : ℕ), ∏ i ∈ s n, g i = (∏ i ∈ s 0, g i) * ∏ i ∈ Finset.range n, ∏ j ∈ s (i + 1) \ s i, g j