mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {he : t.isEmpty = false} {km : α}, t.minKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (compare km k).isLE = true
-- Lean.DocString.Types
Lean.Doc.Block.other.sizeOf_spec : ∀ {i : Type u} {b : Type v} [inst : SizeOf i] [inst_1 : SizeOf b] (container : b)
  (content : Array (Lean.Doc.Block i b)),
  sizeOf (Lean.Doc.Block.other container content) = 1 + sizeOf container + sizeOf content
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_irrefl : ∀ (x : ZFSet.{u_1}), x ∉ x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {outWidth w : ℕ} {x : aig.RefVec w}
  {h : outWidth = w * w} {w_1 : ℕ} {x_1 : aig.RefVec w_1} {h_1 : outWidth = w_1 * w_1},
  { w := w, x := x, h := h } = { w := w_1, x := x_1, h := h_1 } → w = w_1 ∧ x ≍ x_1
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Unitization.mem_spectrum_inr_of_not_isUnit : ∀ {R : Type u_3} {A : Type u_4} [inst : CommRing R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (a : A) (r : R), ¬IsUnit r → r ∈ spectrum R ↑a
-- Mathlib.Data.Sym.Basic
/-- Multisets of cardinality n are equivalent to length-n vectors up to permutations.
 -/
Sym.symEquivSym' : {α : Type u_3} → {n : ℕ} → Sym α n ≃ Sym.Sym' α n
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- The binary fan whose point is `prod F G`.  -/
CategoryTheory.FunctorToTypes.binaryProductCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G : CategoryTheory.Functor C (Type w)) → CategoryTheory.Limits.BinaryFan F G
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a normed group from a translation-invariant distance.  -/
NormedAddGroup.ofAddDist : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : AddGroup E] →
      [inst_2 : MetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 0 x) → (∀ (x y z : E), dist x y ≤ dist (z + x) (z + y)) → NormedAddGroup E
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_dirac : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [hE : CompleteSpace E]
  [inst_2 : MeasurableSpace α] [MeasurableSingletonClass α] (f : α → E) (a : α),
  ∫ (x : α), f x ∂MeasureTheory.Measure.dirac a = f a
-- Mathlib.Data.Finset.Sum
Finset.toLeft_insert_inl : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {a : α} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  (insert (Sum.inl a) u).toLeft = insert a u.toLeft
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.iteratedFDeriv_zero_on_compl : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K) {i : ℕ},
  Set.EqOn (iteratedFDeriv ℝ i ⇑f) 0 (↑K)ᶜ
-- Mathlib.RepresentationTheory.Continuous.TopRep
_private.Mathlib.RepresentationTheory.Continuous.TopRep.0.TopRep.Hom.mk : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] →
      [inst_1 : Ring k] →
        [inst_2 : Monoid G] → {A : TopRep k G} → {B : TopRep k G} → ContIntertwiningMap A.ρ B.ρ → A.Hom B
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableWithinAt_prod_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F' : Type u_14}
  [inst_11 : NormedAddCommGroup F'] [inst_12 : NormedSpace 𝕜 F'] {G' : Type u_15} [inst_13 : TopologicalSpace G']
  {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [inst_14 : TopologicalSpace N'] [inst_15 : ChartedSpace G' N']
  {s : Set M} {x : M} (f : M → M' × N'), MDiffAt[s] f x ↔ MDiffAt[s] (Prod.fst ∘ f) x ∧ MDiffAt[s] (Prod.snd ∘ f) x
-- Init.Prelude
/-- Notation typeclass for the `∣` operation (typed as `\|`), which represents divisibility.  -/
Dvd : Type u_1 → Type u_1
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- Formula for geometric series.  -/
PowerSeries.WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero : ∀ {R : Type u_3} [inst : TopologicalSpace R] [inst_1 : Ring R] [IsTopologicalRing R] [T2Space R] {f : PowerSeries R},
  PowerSeries.constantCoeff f = 0 → (1 - f) * ∑' (i : ℕ), f ^ i = 1
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.map.of : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C} {s : CategoryTheory.Presieve X} {Y : C} {u : Y ⟶ X},
  s u → CategoryTheory.Presieve.map F s (F.map u)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.hom_comp_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K₁ K₂ : CategoryTheory.Limits.Multifork I) (f : K₁ ⟶ K₂) (j : J.L),
  CategoryTheory.CategoryStruct.comp f.hom (K₂.ι j) = K₁.ι j
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.discr.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R),
  f.discr = f.sylvesterDeriv.det * (-1) ^ (f.natDegree * (f.natDegree - 1) / 2)
-- Mathlib.Order.Partition.Basic
Partition.IsRepFun.apply_eq_apply_iff' : ∀ {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α} {a b : α},
  P.IsRepFun f → (f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel a b)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.exp_sub_cosh : ∀ (x : ℂ), Complex.exp x - Complex.cosh x = Complex.sinh x
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_b_le_r : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), b i * ↑n - ↑n / Real.log ↑n ^ 2 ≤ ↑(r i n)
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint_a : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra}
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor]
  [inst_3 : CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor],
  (CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint c t).a = CategoryTheory.Comonad.ForgetCreatesLimits'.lambda c t
-- Mathlib.Topology.MetricSpace.Perfect
/-- A refinement of `Perfect.splitting` for metric spaces, where we also control
the diameter of the new perfect sets.  -/
Perfect.small_diam_splitting : ∀ {α : Type u_1} [inst : MetricSpace α] {C : Set α} {ε : ENNReal},
  Perfect C →
    C.Nonempty →
      0 < ε →
        ∃ C₀ C₁,
          (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ Metric.ediam C₀ ≤ ε) ∧
            (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ Metric.ediam C₁ ≤ ε) ∧ Disjoint C₀ C₁
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.IsAddModHom.vadd_hom : ∀ {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.MonoidalLeftAction C D}
  {M' N' : D} {A : C} {inst_4 : CategoryTheory.AddMonObj A} {inst_5 : CategoryTheory.AddModObj A M'}
  {inst_6 : CategoryTheory.AddModObj A N'} {f : M' ⟶ N'} [self : CategoryTheory.IsAddModHom A f],
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
      CategoryTheory.AddModObj.vadd
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_rio_eq_zero_iff : ∀ {n i : ℕ}, (*...n).toList[i]! = 0 ↔ n ≤ i ∨ i = 0
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C) {Z : C} (h : ((HomologicalComplex.single C c j).obj A).opcycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j A).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom h) =
    CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).homologyι j) h
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.matchesAt_iff_matchesAt_toSlice : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.MatchesAt pat pos ↔ String.Slice.Pattern.Model.MatchesAt pat.toSlice pos
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_inter_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₁.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Mathlib.Algebra.CharP.MixedCharZero
MixedCharZero.toCharZero : ∀ {R : Type u_1} {inst : CommRing R} (p : ℕ) [self : MixedCharZero R p], CharZero R
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalGroup.exist_mul_closure_nhds : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [CompactSpace G] {W : Set G},
  IsClopen W → ∃ T ∈ nhds 1, W * T ⊆ W
-- Mathlib.Analysis.Normed.Ring.Lemmas
Int.instNormMulClass : NormMulClass ℤ
-- Mathlib.NumberTheory.ModularForms.LFunction
_private.Mathlib.NumberTheory.ModularForms.LFunction.0.termH : Lean.ParserDescr
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_ne_zero : ∀ {n k : ℕ}, k ≤ n → n.choose k ≠ 0
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.natDegree_eq_support_max' : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} (h : p ≠ 0), p.natDegree = p.support.max' ⋯
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.fillNones.match_1.eq_3 : ∀ {α : Type u_1} (motive : List (Option α) → List α → Sort u_2) (as : List (Option α))
  (h_1 : (x : List α) → motive [] x)
  (h_2 : (a : α) → (as : List (Option α)) → (as' : List α) → motive (some a :: as) as')
  (h_3 : (as : List (Option α)) → motive (none :: as) [])
  (h_4 : (as : List (Option α)) → (a : α) → (as' : List α) → motive (none :: as) (a :: as')),
  (match none :: as, [] with
    | [], x => h_1 x
    | some a :: as, as' => h_2 a as as'
    | none :: as, [] => h_3 as
    | none :: as, a :: as' => h_4 as a as') =
    h_3 as
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
PolynormableSpace.withSeminorms' : ∀ {𝕜 : Type u_2} {E : Type u_6} {inst : NormedField 𝕜} {inst_1 : AddCommGroup E} {inst_2 : Module 𝕜 E}
  {topology : TopologicalSpace E} [self : PolynormableSpace 𝕜 E], WithSeminorms fun p => ↑p
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_insert : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α}, (m.insert k).size = if k ∈ m then m.size else m.size + 1
-- Batteries.Data.List.Basic
/-- A list of length 1 is a chain.  -/
List.IsChain.singleton : ∀ {α : Type u_1} {R : α → α → Prop} (a : α), List.IsChain R [a]
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstr.p : Lean.Meta.Grind.Arith.Linear.RingEqCnstr → Lean.Grind.CommRing.Poly
-- Mathlib.Topology.Algebra.Star
/-- The `star` operator is continuous.  -/
ContinuousStar.continuous_star : ∀ {R : Type u_1} {inst : TopologicalSpace R} {inst_1 : Star R} [self : ContinuousStar R], Continuous star
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- A right homology data for a short complex `S` consists of morphisms `p : S.X₂ ⟶ Q` and
`ι : H ⟶ Q` such that `p` identifies `Q` with the cokernel of `f : S.X₁ ⟶ S.X₂`,
and that `ι` identifies `H` with the kernel of the induced map `g' : Q ⟶ S.X₃`  -/
CategoryTheory.ShortComplex.RightHomologyData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ShortComplex C → Type (max u_1 v_1)
-- Mathlib.Data.Sym.Sym2
Sym2.Mem.decidable : {α : Type u_1} → [DecidableEq α] → (x : α) → (z : Sym2 α) → Decidable (x ∈ z)
-- Mathlib.Analysis.Calculus.Deriv.Support
HasDerivWithinAt.of_notMem_tsupport : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {s : Set 𝕜}, x ∉ tsupport f → HasDerivWithinAt f 0 s x
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.instBEqGCongrKey.beq : Mathlib.Tactic.GCongr.GCongrKey → Mathlib.Tactic.GCongr.GCongrKey → Bool
-- Mathlib.Topology.Algebra.Monoid
AddSubmonoid.topologicalClosure_minimal : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : SeparatelyContinuousAdd M]
  (s : AddSubmonoid M) {t : AddSubmonoid M}, s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Batteries.Lean.Except
ExceptT.map_mk : ∀ {m : Type u_1 → Type u_2} {α β ε : Type u_1} [inst : Monad m] [LawfulMonad m] (f : α → β) (x : m (Except ε α)),
  f <$> ExceptT.mk x = ExceptT.mk ((fun x => f <$> x) <$> x)
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_pow : ∀ {a : ENNReal} {n : ℕ}, (a ^ n)⁻¹ = a⁻¹ ^ n
-- Batteries.Recycling.MonadSatisfying.Basic
_private.Batteries.Recycling.MonadSatisfying.Basic.0.SatisfiesM_ExceptT_eq.match_1_11.eq_1 : ∀ {α ρ : Type u_1} {p : α → Prop} (motive : { a // (fun x => ∀ (a : α), x = Except.ok a → p a) a } → Sort u_2) (a : α)
  (h : ∀ (a_1 : α), Except.ok a = Except.ok a_1 → p a_1)
  (h_1 : (a : α) → (h : ∀ (a_1 : α), Except.ok a = Except.ok a_1 → p a_1) → motive ⟨Except.ok a, h⟩)
  (h_2 : (e : ρ) → (property : ∀ (a : α), Except.error e = Except.ok a → p a) → motive ⟨Except.error e, property⟩),
  (match ⟨Except.ok a, h⟩ with
    | ⟨Except.ok a, h⟩ => h_1 a h
    | ⟨Except.error e, property⟩ => h_2 e property) =
    h_1 a h
-- Std.Data.Iterators.Lemmas.Producers.Empty
Std.Iter.step_empty : ∀ {β : Type u_1}, (Std.Iter.empty β).step = ⟨Std.IterStep.done, ⋯⟩
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Rat.toDyadic.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_1 n
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- This holds in any inner product space, but we need this to set up the instance.
This is a helper lemma for showing that this inner product is positive definite.  -/
_private.Mathlib.Analysis.InnerProductSpace.TensorProduct.0.TensorProduct.inner_self : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {ι : Type u_6}
  {ι' : Type u_7} [inst_5 : Fintype ι] [inst_6 : Fintype ι'] (x : TensorProduct 𝕜 E F) (e : OrthonormalBasis ι 𝕜 E)
  (f : OrthonormalBasis ι' 𝕜 F), inner 𝕜 x x = ↑(∑ i, ‖((e.toBasis.tensorProduct f.toBasis).repr x) i‖ ^ 2)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_mul_inv_nhds_one_swapped : ∀ (Gᵣ : Type u_3) [inst : UniformSpace Gᵣ] [inst_1 : Group Gᵣ] [IsRightUniformGroup Gᵣ],
  uniformity Gᵣ = Filter.comap (fun x => x.1 * x.2⁻¹) (nhds 1)
-- Aesop.Frontend.RuleExpr
_private.Aesop.Frontend.RuleExpr.0.Aesop.Frontend.elabSingleIndexingMode.elabKeys : Lean.Syntax → Aesop.ElabM (Array Lean.Meta.DiscrTree.Key)
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `antitoneOn_comp_ofDual_iff`. -/
MonotoneOn.dual_left : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  MonotoneOn f s → AntitoneOn (f ∘ ⇑OrderDual.ofDual) s
-- Mathlib.Util.CompileInductive
/-- Compile the definition `dv` by adding a second definition `dv✝` with the same body,
and registering a `csimp`-lemma `dv = dv✝`.
 -/
Mathlib.Util.compileDefn : Lean.DefinitionVal → Lean.MetaM Unit
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.preimage_smul_inv : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] (a : α) (t : Set β),
  (fun x => a⁻¹ • x) ⁻¹' t = a • t
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.const_apply : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (c : ℝ) (x : R),
  ↑(StieltjesFunction.const R c) x = c
-- Mathlib.Data.Int.ModEq
Int.mod_coprime : ∀ {a b : ℕ}, a.Coprime b → ∃ y, ↑a * y ≡ 1 [ZMOD ↑b]
-- Mathlib.Analysis.Convex.Body
ConvexBody.coe_smul : ∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V]
  [inst_3 : ContinuousSMul ℝ V] (c : ℝ) (K : ConvexBody V), ↑(c • K) = c • ↑K
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.ofClass_carrier : ∀ {S : Type u_1} {R : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : SetLike S R]
  [inst_2 : NonUnitalSubringClass S R] (s : S), ↑(NonUnitalSubring.ofClass s) = ↑s
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.map_sub_roots_sprod_eq_prod_map_eval : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (s : Multiset R) (g : Polynomial R),
  g.Monic →
    g.Splits →
      (Multiset.map (fun ij => ij.1 - ij.2) (g.roots ×ˢ s)).prod =
        (-1) ^ (s.card * g.roots.card) * (Multiset.map (fun x => Polynomial.eval x g) s).prod
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.IsDiag.conjTranspose : ∀ {α : Type u_1} {n : Type u_4} [inst : NonUnitalNonAssocSemiring α] [inst_1 : StarRing α] {A : Matrix n n α},
  A.IsDiag → A.conjTranspose.IsDiag
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.mem_bot : ∀ {R : Type u} [inst : Semiring R] {x : R}, x ∈ ⊥ ↔ x = 0
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instIsZeroApplyUpperHalfPlaneComplex : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ}, IsZeroApply (ModularForm Γ k) UpperHalfPlane ℂ
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyOpIso_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] {Z : Cᵒᵖ}
  (h : Opposite.op S₁.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (CategoryTheory.ShortComplex.opMap φ))
      (CategoryTheory.CategoryStruct.comp S₁.homologyOpIso.hom h) =
    CategoryTheory.CategoryStruct.comp S₂.homologyOpIso.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ).op h)
-- Init.Data.String.Iterate
/-- Creates an iterator over all valid positions within `s`.

Examples

* `("abc".positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', 'c']`

* `("abc".positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2]`

* `("ab∀c".positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', '∀', 'c']`

* `("ab∀c".positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2, 5]`
 -/
String.positions : (s : String) → Std.Iter { p // p ≠ s.endPos }
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_smul : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : SMulZeroClass S R] (r : S) (p : Polynomial R) (n : ℕ),
  (r • p).coeff n = r • p.coeff n
-- Mathlib.Order.Sublocale
/-- The set corresponding to the sublocale.  -/
Sublocale.carrier : {X : Type u_2} → [inst : Order.Frame X] → Sublocale X → Set X
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_eq_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited α] {k : α}, m.contains k = true → m.getKey! k = k
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_eq_minD_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.min! = t.minD default
-- Std.Data.HashMap.Lemmas
Std.HashMap.containsThenInsertIfNew_fst : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {k : α} {v : β},
  (m.containsThenInsertIfNew k v).1 = m.contains k
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.instNormOneClass : ∀ {R : Type u_3} {M : Type u_4} [inst : SeminormedRing R] [inst_1 : SeminormedAddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsBoundedSMul R M] [inst_4 : Module Rᵐᵒᵖ M] [inst_5 : IsBoundedSMul Rᵐᵒᵖ M]
  [inst_6 : SMulCommClass R Rᵐᵒᵖ M] [NormOneClass R], NormOneClass (TrivSqZeroExt R M)
-- Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Subalgebra.pointwise_smul_toSubring : ∀ {R' : Type u_4} {R : Type u_5} {A : Type u_6} [inst : Semiring R'] [inst_1 : CommRing R] [inst_2 : Ring A]
  [inst_3 : MulSemiringAction R' A] [inst_4 : Algebra R A] [inst_5 : SMulCommClass R' R A] (m : R')
  (S : Subalgebra R A), (m • S).toSubring = m • S.toSubring
-- Init.Data.Range.Polymorphic.PRange
Std.Roi.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (lower : α), sizeOf lower<...* = 1 + sizeOf lower
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isSome_getElem?_toList_roc_eq : ∀ {m n i : ℕ}, ((m<...=n).toList[i]?.isSome = true) = (i < n - m)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_hom_hom_inv_hom_hom_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e)
  {Z : a ⟶ e}
  (h_1 :
    CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g h) i) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv) h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom h_1)
-- Init.Prelude
/-- Catches errors, recovering using `handle`. The exception type is specified explicitly. This is useful when a monad
supports throwing or handling more than one type of exception.

Use `tryCatch`, for a version that expects the exception type to be inferred from `m`.
 -/
tryCatchThe : (ε : Type u) → {m : Type v → Type w} → [MonadExceptOf ε m] → {α : Type v} → m α → (ε → m α) → m α
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.comp_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z)
  (z₃ : W.LeftFraction z₁.Y' z₂.Y'),
  CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f →
    z₁.comp z₂ = CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk (z₁.comp₀ z₂ z₃)
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The square of `J(a | b)` is `1` when `a` and `b` are coprime.  -/
jacobiSym.sq_one : ∀ {a : ℤ} {b : ℕ}, a.gcd ↑b = 1 → jacobiSym a b ^ 2 = 1
-- Lean.Data.Lsp.Extra
Lean.Lsp.instInhabitedLeanFileProgressKind : Inhabited Lean.Lsp.LeanFileProgressKind