mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Expr
/-- Arguments in forallE binders can be labelled as implicit or explicit.

Each `lam` or `forallE` binder comes with a `binderInfo` argument (stored in ExprData).
This can be set to
- `default` -- `(x : α)`
- `implicit` --  `{x : α}`
- `strict_implicit` -- `⦃x : α⦄`
- `inst_implicit` -- `[x : α]`.
- `aux_decl` -- Auxiliary definitions are helper methods that
  Lean generates. `aux_decl` is used for `_match`, `_fun_match`,
  `_let_match` and the self reference that appears in recursive pattern matching.

The difference between implicit `{}` and strict-implicit `⦃⦄` is how
implicit arguments are treated that are *not* followed by explicit arguments.
`{}` arguments are applied eagerly, while `⦃⦄` arguments are left partially applied:
```
def foo {x : Nat} : Nat := x
def bar ⦃x : Nat⦄ : Nat := x
#check foo -- foo : Nat
#check bar -- bar : ⦃x : Nat⦄ → Nat
```

See also [the Lean Language Reference](https://lean-lang.org/doc/reference/latest/Terms/Functions/#implicit-functions).
 -/
Lean.BinderInfo : Type
-- Mathlib.Topology.Baire.BaireMeasurable
BaireMeasurableSet.of_mem_residual : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, s ∈ residual α → BaireMeasurableSet s
-- Batteries.Tactic.Init
/-- `by_contra h` proves `⊢ p` by contradiction,
introducing a hypothesis `h : ¬p` and proving `False`.
* If `p` is a negation `¬q`, `h : q` will be introduced instead of `¬¬q`.
* If `p` is decidable, it uses `Decidable.byContradiction` instead of `Classical.byContradiction`.
* If `h` is omitted, the introduced variable will be called `this`.
* `h` can be any pattern supported by `rcases`/`rintro`.
 -/
Batteries.Tactic.byContra : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.checkMaxDegree : Lean.Grind.CommRing.Poly → Lean.Meta.Grind.GoalM Bool
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.appIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} [inst_2 : G.IsCoverDense K] [inst_3 : G.IsLocallyFull K]
  {ℱ ℱ' : CategoryTheory.Sheaf K (Type v)} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) (X : D),
  (CategoryTheory.Functor.IsCoverDense.Types.appIso i X).inv = CategoryTheory.Functor.IsCoverDense.Types.appHom i.inv X
-- Mathlib.Topology.Separation.Regular
regularSpace_sInf : ∀ {X : Type u_3} {T : Set (TopologicalSpace X)}, (∀ t ∈ T, RegularSpace X) → RegularSpace X
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.UnfoldLift.set : ∀ {m : Type u → Type v} {n : Type u → Type u_1} {σ : Type u} [inst : MonadLift m n] [inst_1 : MonadStateOf σ m] (s : σ),
  set s = monadLift (set s)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.foldM_map : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad m]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad n Pred EPred] [inst_8 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_10 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : Std.IterM m β}
  {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄ Std.IterM.foldM (fun d b => g d (f b)) init it ⦃ Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.IterM.map f it) ⦃ Q; eQ ⦄
-- Batteries.Data.Fin.Lemmas
Fin.coe_mkDivMod : ∀ {m n : ℕ} (i : Fin m) (j : Fin n), ↑(i.mkDivMod j) = n * ↑i + ↑j
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppLeft_apply_tmul_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  [inst_7 : AddCommMonoid N] [inst_8 : Module R N] {ι : Type u_5} [inst_9 : DecidableEq ι] (p : ι →₀ M) (n : N) (i : ι),
  ((TensorProduct.finsuppLeft R S M N ι) (p ⊗ₜ[R] n)) i = p i ⊗ₜ[R] n
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.dropPrefix?_string_eq_dropPrefix?_toSlice : ∀ {pat : String} {s : String.Slice}, s.dropPrefix? pat = s.dropPrefix? pat.toSlice
-- Init.Grind.Lemmas
Lean.Grind.not_eq_of_eq_true : ∀ {a : Prop}, a = True → (¬a) = False
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- For `f` a morphism in `Arrow V`, the cokernel cofork of `(quotient V).map f` constructed
in `cokernelCofork` is a colimit cofork.  -/
CategoryTheory.Preadditive.RightFreyd.Candidate.isColimitCokernelCofork : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts V] →
        {u v : CategoryTheory.Arrow V} →
          (f : u ⟶ v) →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Preadditive.RightFreyd.Candidate.cokernelCofork f)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} {h' : k ∈ Std.ExtTreeMap.filter f t},
  (Std.ExtTreeMap.filter f t).getKey k h' = t.getKey k ⋯
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.span_set_smul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_8}
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [SMulCommClass α R M] (s : Set α) (t : Set M),
  Submodule.span R (s • t) = s • Submodule.span R t
-- Mathlib.Analysis.RCLike.Extend
StrongDual.extendRCLikeₗ_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : TopologicalSpace F] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (fr : StrongDual ℝ F), StrongDual.extendRCLikeₗ fr = fr.extendRCLike
-- Mathlib.CategoryTheory.Subobject.NoetherianObject
CategoryTheory.isNoetherianObject.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.isNoetherianObject X = WellFoundedGT (CategoryTheory.Subobject X)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.linearIndependent_cols_of_invertible : ∀ {m : Type u} [inst : DecidableEq m] {K : Type u_3} [inst_1 : Field K] [inst_2 : Fintype m] (A : Matrix m m K)
  [Invertible A], LinearIndependent K A.col
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The continuous intertwining map underlying an equivalence of continuous representations.  -/
ContRepresentation.Equiv.toContIntertwiningMap : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} → π₁.Equiv π₂ → ContIntertwiningMap π₁ π₂
-- Init.Prelude
Membership.mk : {α : outParam (Type u)} → {γ : Type v} → (γ → α → Prop) → Membership α γ
-- Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
AddTorsor.convexCombination.eq_1 : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (s : Convexity.StdSimplex R P),
  AddTorsor.convexCombination s = (Finset.affineCombination R s.weights.support id) ⇑s.weights
-- Mathlib.RingTheory.PowerSeries.Basic
/-- Two formal power series are equal if all their coefficients are equal.  -/
PowerSeries.ext_iff : ∀ {R : Type u_1} [inst : Semiring R] {φ ψ : PowerSeries R},
  φ = ψ ↔ ∀ (n : ℕ), (PowerSeries.coeff n) φ = (PowerSeries.coeff n) ψ
-- Init.Prelude
/-- Appends two names `a` and `b`, propagating macro scopes from `a` or `b`, if any, to the result.
Panics if both `a` and `b` have macro scopes.

This function is used for the `Append Name` instance.

See also `Lean.Name.appendCore`, which appends names without any consideration for macro scopes.
Also consider `Lean.Name.eraseMacroScopes` to erase macro scopes before appending, if appropriate.
 -/
Lean.Name.append : Lean.Name → Lean.Name → Lean.Name
-- Mathlib.Algebra.GroupWithZero.Defs
MonoidWithZero.toMulZeroOneClass : {M₀ : Type u} → [self : MonoidWithZero M₀] → MulZeroOneClass M₀
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instNonUnitalSemiring : {R : Type u_1} → [NonUnitalSemiring R] → NonUnitalSemiring (Lex R)
-- Mathlib.RingTheory.LocalRing.LocalSubring
/-- The localization of a subring at a prime is indeed isomorphic to its abstract localization.  -/
LocalSubring.ofPrimeEquiv : {K : Type u_3} →
  [inst : Field K] →
    (A : Subring K) →
      (P : Ideal ↥A) → [inst_1 : P.IsPrime] → Localization.AtPrime P ≃ₐ[↥A] ↥(LocalSubring.ofPrime A P).toSubring
-- Init.GrindInstances.ToInt
Lean.Grind.instMulIntIi : Lean.Grind.ToInt.Mul ℤ Lean.Grind.IntInterval.ii
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
/-- The equivalence `(ULift ℤ →+ G) ≃ G` for any additive group `G`.  -/
uliftZMultiplesHom : (G : Type u) → [inst : AddGroup G] → G ≃ (ULift.{u, 0} ℤ →+ G)
-- Mathlib.Algebra.Algebra.Defs
Algebra.subsingleton : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [Algebra R A] [Subsingleton R], Subsingleton A
-- Mathlib.LinearAlgebra.Finsupp.SumProd
Finsupp.sumFinsuppLEquivProdFinsupp_symm_apply : ∀ {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_7}
  {β : Type u_8} (a : (α →₀ M) × (β →₀ M)),
  (Finsupp.sumFinsuppLEquivProdFinsupp R).symm a = Finsupp.sumFinsuppAddEquivProdFinsupp.invFun a
-- Mathlib.Data.Set.Lattice
Set.iUnion_subtype : ∀ {α : Type u_1} {β : Type u_2} (p : α → Prop) (s : { x // p x } → Set β), ⋃ x, s x = ⋃ x, ⋃ (hx : p x), s ⟨x, hx⟩
-- Mathlib.Data.Int.Init
Int.div_le_div_iff_of_dvd_of_pos_of_pos : ∀ {a b c d : ℤ}, 0 < b → 0 < d → b ∣ a → d ∣ c → (a / b ≤ c / d ↔ d * a ≤ c * b)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
/-- **Markov's inequality** also known as **Chebyshev's first inequality**. For a version assuming
`AEMeasurable`, see `mul_meas_ge_le_lintegral₀`.  -/
MeasureTheory.mul_meas_ge_le_lintegral : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → ∀ (ε : ENNReal), ε * μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ
-- Mathlib.CategoryTheory.Limits.Indization.Category
/-- This is the functor `(I ⥤ C) ⥤ Ind C` that sends a functor `F` to `colim (Y ∘ F)`, where `Y`
is the Yoneda embedding. It is known as "ind-lim" and denoted `“colim”` in [Kashiwara2006].  -/
CategoryTheory.Ind.lim : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : Type v) →
      [inst_1 : CategoryTheory.SmallCategory I] →
        [CategoryTheory.IsFiltered I] → CategoryTheory.Functor (CategoryTheory.Functor I C) (CategoryTheory.Ind C)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_eq_some_getD_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a fallback : α}, m.contains a = true → m.get? a = some (m.getD a fallback)
-- Mathlib.Algebra.Lie.Basic
LieAlgebra.toModule_injective : ∀ (L : Type u_1) [inst : LieRing L], Function.Injective (@LieAlgebra.toModule ℚ L Rat.commRing inst)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instReprMon : Repr Lean.Grind.CommRing.Mon
-- Init.Data.List.OfFn
List.getElem?_ofFn : ∀ {n : ℕ} {α : Type u_1} {i : ℕ} {f : Fin n → α}, (List.ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none
-- Mathlib.Order.Irreducible
SupPrime.not_isMin : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α}, SupPrime a → ¬IsMin a
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.closure_empty : ∀ {M : Type u_1} [inst : MulOneClass M], Submonoid.closure ∅ = ⊥
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_sub : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {S : NonUnitalSubalgebra R A}
  (x y : ↥S), ↑(x - y) = ↑x - ↑y
-- Mathlib.Data.Multiset.NatAntidiagonal
Multiset.Nat.antidiagonal_succ : ∀ {n : ℕ},
  Multiset.Nat.antidiagonal (n + 1) = (0, n + 1) ::ₘ Multiset.map (Prod.map Nat.succ id) (Multiset.Nat.antidiagonal n)
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_4 : HAdd Std.Time.Nanosecond.Offset Std.Time.Day.Offset Std.Time.Nanosecond.Offset
-- Init.Data.Option.Lemmas
Option.filter.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (val : α), Option.filter p (some val) = if p val = true then some val else none
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- Given a morphism `k : S.cycles ⟶ A` such that `S.toCycles ≫ k = 0`, this is the
induced morphism `S.homology ⟶ A`.  -/
CategoryTheory.ShortComplex.descHomology : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        {A : C} →
          [inst_2 : S.HasHomology] →
            (k : S.cycles ⟶ A) → CategoryTheory.CategoryStruct.comp S.toCycles k = 0 → (S.homology ⟶ A)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_smul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {A : Type u_8} [inst_1 : SMulZeroClass A R] (a : A)
  (x : AddMonoidAlgebra R M), (a • x).coeff = a • x.coeff
-- Init.Data.List.Zip
List.zipWith_self : ∀ {α : Type u_1} {δ : Type u_2} {f : α → α → δ} {l : List α}, List.zipWith f l l = List.map (fun a => f a a) l
-- Mathlib.CategoryTheory.Subobject.Comma
CategoryTheory.StructuredArrow.projectSubobject_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} [inst_2 : CategoryTheory.Limits.HasFiniteLimits C]
  [inst_3 : CategoryTheory.Limits.PreservesFiniteLimits T] {A P : CategoryTheory.StructuredArrow S T} (f : P ⟶ A)
  [inst_4 : CategoryTheory.Mono f],
  CategoryTheory.StructuredArrow.projectSubobject (CategoryTheory.Subobject.mk f) =
    CategoryTheory.Subobject.mk (CategoryTheory.StructuredArrow.Hom.right f)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.coe_inf : ∀ {M : Type u_1} [inst : MulOneClass M] (p p' : Submonoid M), ↑(p ⊓ p') = ↑p ∩ ↑p'
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
SpectrumRestricts.apply_mem : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Semifield S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] {a : A} {f : S → R} [IsScalarTower R S A],
  SpectrumRestricts a f → ∀ {s : S}, s ∈ spectrum S a → f s ∈ spectrum R a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.Cache.get?_eq_some_iff : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {w : ℕ} {refs : aig.RefVec w}
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) (expr : Std.Tactic.BVDecide.BVExpr w),
  cache.get? expr = some refs ↔ cache.map.get? { w := w, expr := expr } = some refs.refs
-- Mathlib.Data.LawfulXor.Basic
zero_xor : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] (a : α), 0 ^^^ a = a
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.single_eq_updateCol_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α] (i : m)
  (j : n) (r : α), Matrix.single i j r = Matrix.updateCol 0 j (Pi.single i r)
-- Mathlib.Topology.Connected.LocallyConnected
/-- A space with discrete topology is a locally connected space.  -/
DiscreteTopology.toLocallyConnectedSpace : ∀ (α : Type u_3) [inst : TopologicalSpace α] [DiscreteTopology α], LocallyConnectedSpace α
-- Mathlib.Data.NNReal.Defs
NNReal.instOrderBot : OrderBot NNReal
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.instZero : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} → [inst : PartialOrder Γ] → [inst_1 : AddCommMonoid R] → Zero (HahnSeries.SummableFamily Γ R α)
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The proposed colimit cocone is a colimit in `GrpCat`.  -/
GrpCat.FilteredColimits.colimitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J GrpCat) → CategoryTheory.Limits.IsColimit (GrpCat.FilteredColimits.colimitCocone F)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- `Context ρ` provides the context for manipulating 2-morphisms in a monoidal category or
bicategory. In particular, we will store `MonoidalCategory` or `Bicategory` instance in a context,
and use this through a reader monad when we construct the lean expressions for 2-morphisms.  -/
Mathlib.Tactic.BicategoryLike.Context : Type → Type
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.closure_preimage_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G), AddSubgroup.closure (⇑(AddSubgroup.closure s).subtype ⁻¹' s) = ⊤
-- Mathlib.Data.Prod.Basic
/-- Delaborator for `Prod.fst x` as `x.1`.  -/
Prod.PrettyPrinting.delabProdFst : Lean.PrettyPrinter.Delaborator.Delab
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
Lean.Grind.CommRing.Power.denoteExpr : {M : Type → Type} →
  [Monad M] →
    [Lean.MonadError M] →
      [MonadLiftT Lean.MetaM M] →
        [Lean.Meta.Sym.Arith.MonadCanon M] →
          [Lean.Meta.Grind.Arith.CommRing.MonadRing M] → Lean.Grind.CommRing.Power → M Lean.Expr
-- Mathlib.Data.Int.Interval
Int.card_Ioc : ∀ (a b : ℤ), (Finset.Ioc a b).card = (b - a).toNat
-- Mathlib.RepresentationTheory.FDRep
FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ : ∀ {R : Type u} {G : Type v} [inst : CommRing R] [inst_1 : Monoid G],
  (CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G)).Faithful
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.dvd_of_dvd_mul_left : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x y → x ∣ y * z → x ∣ z
-- Mathlib.Topology.CompactOpen
ContinuousMap.tendsto_compactOpen_restrict : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {ι : Type u_6} {l : Filter ι}
  {F : ι → C(X, Y)} {f : C(X, Y)},
  Filter.Tendsto F l (nhds f) →
    ∀ (s : Set X), Filter.Tendsto (fun i => ContinuousMap.restrict s (F i)) l (nhds (ContinuousMap.restrict s f))
-- Mathlib.Topology.Order
isClosed_induced : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {s : Set β}, IsClosed s → IsClosed (f ⁻¹' s)
-- Init.Data.UInt.Bitwise
UInt16.zero_shiftLeft : ∀ {a : UInt16}, 0 <<< a = 0
-- Mathlib.Topology.Connected.Basic
IsPreconnected.subset_connectedComponentIn : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α} {x : α} {F : Set α},
  IsPreconnected s → x ∈ s → s ⊆ F → s ⊆ connectedComponentIn F x
-- Mathlib.Topology.UnitInterval
Set.Icc.convexComb_symm : ∀ {a b : ℝ} (x y : ↑(Set.Icc a b)) (t : ↑unitInterval),
  Set.Icc.convexComb x y (unitInterval.symm t) = Set.Icc.convexComb y x t
-- Mathlib.Algebra.Algebra.Field
algebraMap.coe_inv : ∀ {R : Type u_1} (A : Type u_2) [inst : Semifield R] [inst_1 : DivisionSemiring A] [inst_2 : Algebra R A] (r : R),
  ↑r⁻¹ = (↑r)⁻¹
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans_target : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z),
  (e.trans e').target = e'.target ∩ ↑e'.symm ⁻¹' e.target
-- Mathlib.Algebra.Group.Action.Defs
Commute.smul_left : ∀ {M : Type u_1} {α : Type u_5} [inst : SMul M α] [inst_1 : Mul α] [SMulCommClass M α α] [IsScalarTower M α α]
  {a b : α}, Commute a b → ∀ (r : M), Commute (r • a) b
-- Mathlib.Tactic.GRewrite.Core
/-- Execute a generalized rewrite by first using `kabstract` to generate the replacement expression,
and then calling `gcongr` to prove that this is related to the original expression.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.grewriteUsingKAbstract : Lean.MVarId →
  Lean.Expr →
    Lean.Expr →
      Lean.Expr →
        Lean.Expr → Bool → Mathlib.Tactic.GRewrite.Config → Lean.MetaM (Lean.Expr × Lean.Expr × Array Lean.MVarId)
-- Mathlib.Topology.Compactification.StoneCech
continuous_stoneCechUnit : ∀ {α : Type u} [inst : TopologicalSpace α], Continuous stoneCechUnit
-- Mathlib.Analysis.RCLike.Extend
/-- **Alias** of `StrongDual.extendRCLike`.

---

Extend `fr : StrongDual ℝ F` to `StrongDual 𝕜 F`.

Norm properties of this extension can be found in
`Mathlib/Analysis/Normed/Module/RCLike/Extend.lean`.  -/
ContinuousLinearMap.extendTo𝕜' : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {F : Type u_2} →
      [inst_1 : TopologicalSpace F] →
        [inst_2 : AddCommGroup F] →
          [inst_3 : Module 𝕜 F] →
            [ContinuousConstSMul 𝕜 F] → [inst_5 : Module ℝ F] → [IsScalarTower ℝ 𝕜 F] → StrongDual ℝ F → StrongDual 𝕜 F
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The equalizer definition of a sheaf given by `isSheaf'` is equivalent to `isSheaf`.  -/
CategoryTheory.Presheaf.isSheaf_iff_isSheaf' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A' : Type u₂}
  [inst_1 : CategoryTheory.Category.{max v₁ u₁, u₂} A'] (J : CategoryTheory.GrothendieckTopology C)
  (P' : CategoryTheory.Functor Cᵒᵖ A') [inst_2 : CategoryTheory.Limits.HasProducts A']
  [inst_3 : CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.Presheaf.IsSheaf J P' ↔ CategoryTheory.Presheaf.IsSheaf' J P'
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Uniform convergence on the empty set is vacuously true  -/
tendstoUniformlyOn_empty : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι},
  TendstoUniformlyOn F f p ∅
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.weight.eq_1 : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Monoid R] (w : {i j : V} → (i ⟶ j) → R) (x : V),
  Quiver.Path.weight w Quiver.Path.nil = 1
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
/-- Any large enough family of vectors in `R^ι` has a pair of elements
whose remainders are close together, pointwise.  -/
AbsoluteValue.IsAdmissible.exists_approx : ∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} {ι : Type u_2} [inst_1 : Fintype ι] {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (h : abv.IsAdmissible) (A : Fin (h.card ε ^ Fintype.card ι).succ → ι → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_hom : ∀ {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),
  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)
        (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.ofFn.eq_1 : ∀ {α : Type u} {n : ℕ} (f : Fin n → α), Array.ofFn f = Array.ofFn.go✝ f (Array.emptyWithCapacity n) n ⋯
-- Std.Data.ExtDTreeMap.Basic
/-- Support for the `for` loop construct in `do` blocks. Iteration happens in ascending order.  -/
Std.ExtDTreeMap.Const.forInUncurried : {α : Type u} →
  {cmp : α → α → Ordering} →
    {δ : Type w} →
      {m : Type w → Type w₂} →
        [inst : Monad m] →
          [LawfulMonad m] →
            {β : Type v} →
              [Std.TransCmp cmp] → (α × β → δ → m (ForInStep δ)) → δ → Std.ExtDTreeMap α (fun x => β) cmp → m δ