mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Torsor.Basic
Function.Injective.torsor.eq_1 : ∀ {G : Type u_1} {P : Type u_2} {Q : Type u_3} [inst : Group G] [inst_1 : Torsor G P] [inst_2 : SMul G Q]
  [inst_3 : SDiv G Q] [inst_4 : Nonempty Q] (f : Q → P) (hf : Function.Injective f)
  (smul : ∀ (c : G) (x : Q), f (c • x) = c • f x) (sdiv : ∀ (x y : Q), x /ₛ y = f x /ₛ f y),
  Function.Injective.torsor f hf smul sdiv =
    { toMulAction := Function.Injective.mulAction f hf smul, toSDiv := inst_3, nonempty := inst_4, sdiv_smul' := ⋯,
      smul_sdiv' := ⋯ }
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.parser : Lean.Name → Lean.Name → Bool → Lean.Parser.Parser → ℕ → Lean.Parser.ParserExtension.Entry
-- Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Module.Basis.ofIsCoprimeDifferentIdeal.eq_1 : ∀ (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [inst : CommRing A] [inst_1 : Field K]
  [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K] [inst_4 : CommRing B] [inst_5 : Field L] [inst_6 : Algebra B L]
  [inst_7 : Algebra A L] [inst_8 : Algebra K L] [inst_9 : FiniteDimensional K L] [inst_10 : IsScalarTower A K L]
  (R₁ : Type u_5) (R₂ : Type u_6) [inst_11 : CommRing R₁] [inst_12 : CommRing R₂] [inst_13 : IsDomain R₁]
  [inst_14 : Algebra A R₁] [inst_15 : Algebra A R₂] [inst_16 : Algebra R₁ B] [inst_17 : Algebra R₂ B]
  [inst_18 : Algebra R₁ L] [inst_19 : Algebra R₂ L] [inst_20 : IsScalarTower A R₁ L] [inst_21 : IsScalarTower R₁ B L]
  [inst_22 : IsScalarTower R₂ B L] [inst_23 : Module.Finite A R₂] {F₁ F₂ : IntermediateField K L}
  [inst_24 : Algebra R₁ ↥F₁] [inst_25 : Algebra R₂ ↥F₂] [inst_26 : Module.IsTorsionFree R₁ ↥F₁]
  [inst_27 : IsScalarTower A (↥F₂) L] [inst_28 : IsScalarTower A R₂ ↥F₂] [inst_29 : IsScalarTower R₁ (↥F₁) L]
  [inst_30 : IsScalarTower R₂ (↥F₂) L] [inst_31 : Algebra.IsSeparable K ↥F₂] [inst_32 : Algebra.IsSeparable (↥F₁) L]
  [inst_33 : IsDomain A] [inst_34 : IsDedekindDomain B] [inst_35 : IsDedekindDomain R₁] [inst_36 : IsDedekindDomain R₂]
  [inst_37 : IsFractionRing B L] [inst_38 : IsFractionRing R₁ ↥F₁] [inst_39 : IsFractionRing R₂ ↥F₂]
  [inst_40 : IsIntegrallyClosed A] [inst_41 : IsIntegralClosure B R₁ L] [inst_42 : Module.IsTorsionFree R₁ B]
  [inst_43 : Module.IsTorsionFree R₂ B], ⋯
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.compl : ∀ {α : Type u} {s t : Set α} {l : Filter α}, s =ᶠ[l] t → sᶜ =ᶠ[l] tᶜ
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsInverseImageOfPreservesEpimorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderQuotients] (F : CategoryTheory.Functor D C)
  [F.PreservesEpimorphisms], (P.inverseImage F).IsClosedUnderQuotients
-- Mathlib.Topology.Constructions.SumProd
isClosedMap_inr : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsClosedMap Sum.inr
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.instIsIsoSchemeToImage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f],
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.toImage f)
-- Batteries.Tactic.GeneralizeProofs
/-- Inserts a prop/fvar pair into the `propToFVar` map.  -/
Batteries.Tactic.GeneralizeProofs.MGen.insertFVar : Lean.Expr → Lean.Expr → Batteries.Tactic.GeneralizeProofs.MGen Unit
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.adjp_none_some : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ) (i : n)
  (A : Matrix (Option n) (Option n) R),
  Matrix.adjp s A none (some i) = Matrix.detp (-s) (A.submatrix (Function.update some i none) some)
-- Mathlib.Topology.GDelta.Basic
/-- A set is meagre if it is meagre in some subspace.  -/
IsMeagre.image_val : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} {m : Set ↑s}, IsMeagre m → IsMeagre (Subtype.val '' m)
-- Mathlib.Topology.DiscreteSubset
IsDiscrete.of_nhdsWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, (∀ x ∈ s, nhdsWithin x s ≤ pure x) → IsDiscrete s
-- Mathlib.Algebra.Tropical.Basic
Tropical.instCommSemiring : {R : Type u} → [LinearOrderedAddCommMonoidWithTop R] → CommSemiring (Tropical R)
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_apply_finset' : ∀ {Ω : Type u_2} [inst : DecidableEq Ω] {x : MeasurableSpace Ω} {s t : Finset Ω},
  MeasurableSet ↑s → MeasurableSet ↑t → (ProbabilityTheory.uniformOn ↑s) ↑t = ↑(s ∩ t).card / ↑s.card
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_blastDivSubtractShift_wn : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : BitVec w)
  (n d : aig.RefVec w) (wn wr : ℕ) (q r : aig.RefVec w) (qbv rbv : BitVec w),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).wn =
    (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).wn
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` creates the limit of `K` and `K ⋙ F` has a limit, then `K` has a limit.  -/
CategoryTheory.hasLimit_of_created : ∀ {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] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasLimit (K.comp F)] [CategoryTheory.CreatesLimit K F],
  CategoryTheory.Limits.HasLimit K
-- Mathlib.Algebra.Order.Ring.Abs
abs_dvd_abs : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] (a b : α), |a| ∣ |b| ↔ a ∣ b
-- Mathlib.Computability.NFA
NFA.Path.cons.sizeOf_spec : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} [inst : SizeOf α] [inst_1 : SizeOf σ] (t s u : σ) (a : α) (x : List α)
  (a_1 : t ∈ M.step s a) (a_2 : M.Path t u x),
  sizeOf (NFA.Path.cons t s u a x a_1 a_2) =
    1 + sizeOf t + sizeOf s + sizeOf u + sizeOf a + sizeOf x + sizeOf a_1 + sizeOf a_2
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the forward direction of the isomorphism
`PreservesColimit₂.isoObjCoconePointsOfIsColimit` w.r.t. the canonical maps to the colimit.  -/
CategoryTheory.Limits.PreservesColimit₂.map_ι_comp_isoObjConePointsOfIsColimit_hom : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G] {c₁ : CategoryTheory.Limits.Cocone K₁}
  (hc₁ : CategoryTheory.Limits.IsColimit c₁) {c₂ : CategoryTheory.Limits.Cocone K₂}
  (hc₂ : CategoryTheory.Limits.IsColimit c₂)
  {c₃ :
    CategoryTheory.Limits.Cocone
      (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
  (hc₃ : CategoryTheory.Limits.IsColimit c₃) (j : J₁ × J₂),
  CategoryTheory.CategoryStruct.comp ((G.map (c₁.ι.app j.1)).app (K₂.obj j.2))
      (CategoryTheory.CategoryStruct.comp ((G.obj c₁.pt).map (c₂.ι.app j.2))
        (CategoryTheory.Limits.PreservesColimit₂.isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).hom) =
    c₃.ι.app j
-- Mathlib.Algebra.WithConv
WithConv.toConv_neg : ∀ {A : Type u_2} [inst : AddGroup A] (x : A), WithConv.toConv (-x) = -WithConv.toConv x
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.BalancedTree.mk : {α : Type u} →
  {β : α → Type v} →
    (impl : Std.DTreeMap.Internal.Impl α β) → impl.Balanced → Std.DTreeMap.Internal.Impl.BalancedTree α β
-- Batteries.Recycling.RBTree.Basic
/-- The `erase cut t` function removes an element from the tree `t`.
The `cut` function is used to locate an element in the tree:
it returns `.gt` if we go too high and `.lt` if we go too low;
if it returns `.eq` we will remove the element.
(The function `cmp k` for some key `k` is a valid cut function, but we can also use cuts that
are not of this form as long as they are suitably monotonic.)
 -/
RBTree.RBNode.erase : {α : Type u_1} → (α → Ordering) → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.Analysis.RCLike.Basic
RCLike.exists_norm_mul_eq_self : ∀ {K : Type u_1} [inst : RCLike K] (x : K), ∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x
-- Mathlib.RingTheory.AdicCompletion.Basic
Submodule.factorPow.eq_1 : ∀ {R : Type u_1} [inst : Ring R] (I : Ideal R) (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m n : ℕ}
  (le : m ≤ n), Submodule.factorPow I M le = Submodule.factor ⋯
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.π_natTransTruncGEOfLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b),
  CategoryTheory.CategoryStruct.comp (t.truncGEπ a) (t.natTransTruncGEOfLE a b h) = t.truncGEπ b
-- Mathlib.Data.Sign.Basic
SignType.pow_even : ∀ (s : SignType) {n : ℕ}, Even n → s ≠ 0 → s ^ n = 1
-- Mathlib.Algebra.Order.Quantale
Quantale.leftMulResiduation.eq_1 : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : CompleteLattice α] (x y : α),
  Quantale.leftMulResiduation x y = sSup {z | z * x ≤ y}
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.Walk.setOfPred_length_eq_zero_of_ne : ∀ {V : Type u} (G : SimpleGraph V) {u v : V}, u ≠ v → {p | p.length = 0} = ∅
-- Mathlib.Algebra.Order.Sub.Unbundled.Hom
le_tsub_mul : ∀ {R : Type u_3} [inst : NonUnitalCommSemiring R] [inst_1 : Preorder R] [inst_2 : Sub R] [OrderedSub R] [MulLeftMono R]
  {a b c : R}, a * c - b * c ≤ (a - b) * c
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.ParamKind.mk.sizeOf_spec : ∀ (name : Lean.Name) (bInfo : Lean.BinderInfo) (defVal : Option Lean.Expr) (isAutoParam : Bool),
  sizeOf { name := name, bInfo := bInfo, defVal := defVal, isAutoParam := isAutoParam } =
    1 + sizeOf name + sizeOf bInfo + sizeOf defVal + sizeOf isAutoParam
-- Mathlib.RingTheory.MvPowerSeries.Equiv
/-- An inverse function of `toAdicCompletion`.  -/
MvPowerSeries.toAdicCompletionInv : (σ : Type u_3) →
  (R : Type u_4) →
    [inst : CommRing R] → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) → MvPowerSeries σ R
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp] {k : α}, k ∉ t₂ → (t₁ ∪ t₂).getKey! k = t₁.getKey! k
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.id_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : C(α, β)),
  (ContinuousMap.id β).comp f = f
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.nnratCast_mem : ∀ {K : Type u} [inst : DivisionRing K] {S : Type u_1} [inst_1 : SetLike S K] [h : SubfieldClass S K] (s : S) (q : ℚ≥0),
  ↑q ∈ s
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.invOfUnit_eq : ∀ {k : Type u_2} [inst : Field k] (φ : PowerSeries k) (h : PowerSeries.constantCoeff φ ≠ 0),
  φ.invOfUnit (Units.mk0 (PowerSeries.constantCoeff φ) h) = φ⁻¹
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance.congr_simp : ∀ (pat pat_1 : String.Slice) (e_pat : pat = pat_1) (patByte patByte_1 : UInt8),
  patByte = patByte_1 →
    ∀ (table : Array ℕ) (ht : table.size ≤ pat.utf8ByteSize) (h : ∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i)
      (guess guess_1 : ℕ) (e_guess : guess = guess_1) (hg : guess < table.size),
      String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝ pat patByte table ht h guess hg =
        String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝ pat_1 patByte_1 table ⋯ h guess_1 ⋯
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.instEMetricSpace : {α : Type u_1} → {β : Type u_4} → [EMetricSpace β] → EMetricSpace (UniformFun α β)
-- Mathlib.Order.Filter.Extr
isMinFilter_const : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsMinFilter (fun x => b) l a
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- `iteratedFDerivLM 𝕜 n k i` is the `𝕜`-linear-map sending `f : 𝓓^{n}_{K}(E, F)` to
its `i`-th iterated derivative as an element of `𝓓^{k}_{K}(E, E [×i]→L[ℝ] F)`.
This only makes mathematical sense if `k + i ≤ n`, otherwise we define it as the zero map.

This is subsumed by `iteratedFDerivCLM` (not yet in Mathlib), which also bundles the
continuity.  -/
ContDiffMapSupportedIn.iteratedFDerivLM : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace ℝ E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace ℝ F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] →
                    (n k : ℕ∞) →
                      {K : TopologicalSpace.Compacts E} →
                        (i : ℕ) → ContDiffMapSupportedIn E F n K →ₗ[𝕜] ContDiffMapSupportedIn E (E [×i]→L[ℝ] F) k K
-- Mathlib.Algebra.Algebra.Equiv
/-- The equivalence between `RingEquiv` and `ℕ`-algebra isomorphisms.  -/
RingEquiv.equivNatAlgEquiv : (R : Type u_1) → (S : Type u_2) → [inst : Semiring R] → [inst_1 : Semiring S] → R ≃+* S ≃ R ≃ₐ[ℕ] S
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.ofIso_inv : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : AddCommGroup X] [inst_2 : Module R X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module R Y] {Q₁ : QuadraticForm R X} {Q₂ : QuadraticForm R Y}
  (e : QuadraticMap.IsometryEquiv Q₁ Q₂), (QuadraticModuleCat.ofIso e).inv = QuadraticModuleCat.ofHom e.symm.toIsometry
-- Mathlib.Data.Set.Insert
Set.subset_singleton_iff : ∀ {α : Type u_3} {s : Set α} {x : α}, s ⊆ {x} ↔ ∀ y ∈ s, y = x
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Helper lemma for `meromorphicNFAt_iff_meromorphicNFAt_of_smul_analytic`: if
`f` is meromorphic in normal form at `x` and `g` is analytic without zero at
`x`, then `g • f` is meromorphic in normal form at `x`.  -/
MeromorphicNFAt.smul_analytic : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {g : 𝕜 → 𝕜} {x : 𝕜},
  MeromorphicNFAt f x → AnalyticAt 𝕜 g x → g x ≠ 0 → MeromorphicNFAt (g • f) x
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.Entrypoint.relabel_size_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Type} [inst_2 : Hashable β] [inst_3 : DecidableEq β]
  {entry : Std.Sat.AIG.Entrypoint α} {r : α → β},
  (Std.Sat.AIG.Entrypoint.relabel r entry).aig.decls.size = entry.aig.decls.size
-- Mathlib.Algebra.Order.Monoid.WithTop
WithBot.le_add_self : ∀ {α : Type u} [inst : AddCommMagma α] [inst_1 : LE α] [CanonicallyOrderedAdd α] {x : WithBot α},
  x ≠ ⊥ → ∀ (y : WithBot α), y ≤ x + y
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_prod_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] (a b : α × β),
  Set.uIcc a b = Set.uIcc a.1 b.1 ×ˢ Set.uIcc a.2 b.2
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.NormalExpr.nterm.sizeOf_spec : ∀ (e : Lean.Expr) (n : Lean.Expr × ℤ) (x : ℕ × Lean.Expr) (a : Mathlib.Tactic.Abel.NormalExpr),
  sizeOf (Mathlib.Tactic.Abel.NormalExpr.nterm e n x a) = 1 + sizeOf e + sizeOf n + sizeOf x + sizeOf a
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- The adjunction `lightCondSetToTopCat ⊣ topCatToLightCondSet`  -/
LightCondSet.topCatAdjunction : lightCondSetToTopCat ⊣ topCatToLightCondSet
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_add_le : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f g : M →ₛₗ[τ₁₂] M₂), (f + g).range ≤ f.range ⊔ g.range
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.mk.sizeOf_spec : ∀ {R : Type u_7} {S : Type u_8} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] [inst_4 : SizeOf R]
  [inst_5 : SizeOf S] (toEquiv : R ≃ S)
  (map_mul' : ∀ (x y : R), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y)
  (map_add' : ∀ (x y : R), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y),
  sizeOf { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' } = 1 + sizeOf toEquiv
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.instIsClosedUnderIsomorphismsIsPointwiseLeftKanExtensionAt : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.LeftExtension F),
  E.isPointwiseLeftKanExtensionAt.IsClosedUnderIsomorphisms
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_eq_some_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.min? = some (t.minD fallback)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.Adj.right_triangle_components_assoc : ∀ {C₁ C₂ : CategoryTheory.Bicategory.Adj CategoryTheory.Cat} (α : C₁ ⟶ C₂) (X : ↑C₂.obj) {Z : ↑C₁.obj}
  (h : α.r.toFunctor.obj ((CategoryTheory.CategoryStruct.id C₂.obj).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.adj.unit.toNatTrans.app (α.r.toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp (α.r.toFunctor.map (α.adj.counit.toNatTrans.app X)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (α.r.toFunctor.obj X)) h
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.structuredArrowEquivalence_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)),
  (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id F.Elements)
-- Mathlib.Tactic.Positivity.Core
_private.Mathlib.Tactic.Positivity.Core.0.Mathlib.Meta.Positivity.mkPositivityExt.unsafe_impl_2 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Mathlib.Meta.Positivity.PositivityExt
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.toList_insert_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : BEq α]
  [Std.TransCmp cmp] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {k : α} {v : β},
      (Std.DTreeMap.Raw.Const.toList (t.insert k v)).Perm
        ((k, v) :: List.filter (fun x => decide ¬(k == x.1) = true) (Std.DTreeMap.Raw.Const.toList t))
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_natCast : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (↑n).toFinsupp = ↑n
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instIsNegApply : ∀ {𝕜₁ : 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 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  (𝔖 : Set (Set E)), IsNegApply (UniformConvergenceCLM σ F 𝔖) E F
-- Init.Data.Iterators.Basic
/-- Termination measure to be used in recursive functions built with `WellFounded.extrinsicFix`
recursing over a productive iterator without requiring a proof of productiveness
(see also `Productive`).
 -/
Std.IterM.finitelyManySkips! : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → [inst : Std.Iterator α m β] → Std.IterM m β → Std.IterM.TerminationMeasures.Productive α m
-- Mathlib.Algebra.Group.Basic
left_eq_add : ∀ {M : Type u_4} [inst : AddMonoid M] [IsLeftCancelAdd M] {a b : M}, a = a + b ↔ b = 0
-- Mathlib.Algebra.Group.Hom.Instances
ZeroHom.instNSMul : {M : Type uM} → {N : Type uN} → [inst : Zero M] → [inst_1 : AddMonoid N] → SMul ℕ (ZeroHom M N)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_le_add_measure_right : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ε : Type u_7} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  (f : α → ε) (μ ν : MeasureTheory.Measure α) {p : ENNReal},
  MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm f p (μ + ν)
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_fmod_sub_self : ∀ {x m : ℤ}, m ∣ x.fmod m - x
-- Init.Data.String.Bootstrap
String.Internal.pushn : String → Char → ℕ → String
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R],
  0 ≤ a * b → 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
/-- Pull-out property of the conditional expectation.  -/
MeasureTheory.condExp_mul_of_stronglyMeasurable_left : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f g : Ω → ℝ},
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.Integrable (f * g) μ → MeasureTheory.Integrable g μ → μ[f * g | m] =ᵐ[μ] f * μ[g | m]
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.map₂_def : ∀ {ι : Type u_1} [inst : Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {F : ι → Type u_4}
  {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} (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)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7}
  (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)]
  [inst_4 : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_5 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_6 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_7 : IsDirectedOrder ι]
  (ih : (i : ι) → F₁ i → F₂ i → F i)
  (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), (f i j h) (ih i x y) = ih j ((f₁ i j h) x) ((f₂ i j h) y))
  (i : ι) (x : F₁ i) (y : F₂ i), DirectLimit.map₂ f₁ f₂ f ih compat ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ = ⟦⟨i, ih i x y⟩⟧
-- Std.Do.SPred.SPred
_private.Std.Do.SPred.SPred.0.Std.Do.SPred.conjunction.match_1.eq_1 : ∀ {σs : List (Type u_1)} (motive : List (Std.Do.SPred σs) → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (P : Std.Do.SPred σs) → (env : List (Std.Do.SPred σs)) → motive (P :: env)),
  (match [] with
    | [] => h_1 ()
    | P :: env => h_2 P env) =
    h_1 ()
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.eval_const : ∀ (n m : ℕ), (Nat.Partrec.Code.const n).eval m = Part.some n
-- Lean.Meta.Tactic.Grind.Inv
/-- Checks invariants if `grind.debug` is enabled.  -/
Lean.Meta.Grind.checkInvariants : optParam Bool false → Lean.Meta.Grind.GoalM Unit
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.restrict_restrict : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ],
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ (g : G) (t : Set α), (μ.restrict t).restrict (g • s) = μ.restrict (g • s ∩ t)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
Real.dimH_ball_pi_fin : ∀ {n : ℕ} (x : Fin n → ℝ) {r : ℝ}, 0 < r → dimH (Metric.ball x r) = ↑n