mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Strict
strictConvex_Ico : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace β]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [OrderTopology β]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β), StrictConvex 𝕜 (Set.Ico r s)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β] {f : Option β → Option β},
  (m.alter k f)[k]! = (f m[k]?).get!
-- Mathlib.Order.Interval.Finset.Defs
Set.finite_Ioc : ∀ {α : Type u_1} [inst : Preorder α] [LocallyFiniteOrder α] (b a : α), (Set.Ioc b a).Finite
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.invariantCardinalRank_iff : ∀ {α : Type u} (M : Matroid α),
  M.InvariantCardinalRank ↔
    ∀ ⦃I J X : Set α⦄, M.IsBasis I X → M.IsBasis J X → Cardinal.mk ↑(I \ J) = Cardinal.mk ↑(J \ I)
-- Lean.Meta.Tactic.Backtrack
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.run.match_7.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Data.Finset.Powerset
Finset.powerset_eq_singleton_empty : ∀ {α : Type u_1} {s : Finset α}, s.powerset = {∅} ↔ s = ∅
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.cellFrontier_subset_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.cellFrontier n j ⊆ C
-- Mathlib.Logic.Embedding.Set
/-- For an indexed family `s : ι → Set α` of disjoint sets,
the natural injection from the sigma-type `(i : ι) × ↑(s i)` to `α`.  -/
Function.Embedding.sigmaSet : {α : Type u_1} → {ι : Type u_2} → {s : ι → Set α} → Pairwise (Function.onFun Disjoint s) → (i : ι) × ↑(s i) ↪ α
-- Mathlib.Order.Interval.Finset.Defs
Finset.Icc_toDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  Finset.Icc (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Icc b a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.toList_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} {f : α → β → Bool},
  m.WF →
    (Std.DHashMap.Raw.Const.toList (Std.DHashMap.Raw.filter f m)).Perm
      (List.filter (fun p => f p.1 p.2) (Std.DHashMap.Raw.Const.toList m))
-- Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
/-- Instance of the continuous functional calculus for a Hermitian matrix over `𝕜` with
`RCLike 𝕜`.  -/
Matrix.IsHermitian.instContinuousFunctionalCalculus : ∀ {n : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  ContinuousFunctionalCalculus ℝ (Matrix n n 𝕜) IsSelfAdjoint
-- Mathlib.Algebra.Order.Group.Cyclic
/-- Given a subgroup of a cyclic linearly ordered commutative group, this is a generator of
the subgroup that is `< 1`.  -/
LinearOrderedCommGroup.Subgroup.genLTOne : {G : Type u_1} →
  [inst : CommGroup G] →
    [inst_1 : LinearOrder G] → [IsOrderedMonoid G] → (H : Subgroup G) → [Nontrivial ↥H] → [hH : IsCyclic ↥H] → G
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanFinset_ne_zero : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] {ι : Type u_5} {s : Finset ι} {f : ι → K},
  FractionalIdeal.spanFinset R₁ s f ≠ 0 ↔ ∃ j ∈ s, f j ≠ 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.unionProd.ι₂_ι : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.unionProd.ι₂ S T) (S.unionProd T).ι =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight S.ι Y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_obj_snd : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (x : X), (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.obj S).obj x).snd = S.snd.obj x
-- Mathlib.RingTheory.DividedPowers.Padic
/-- The family `ℕ → Ideal.span {(p : ℤ_[p])} → ℤ_[p]` given by `dpow n x = x ^ n / n!` is a
divided power structure on the `ℤ_[p]`-ideal `(p)`.  -/
PadicInt.dividedPowers : (p : ℕ) → [hp : Fact (Nat.Prime p)] → DividedPowers (Ideal.span {↑p})
-- Mathlib.Topology.Algebra.Module.Star
starL_symm_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousStar A] (x : A), (starL R).symm x = starAddEquiv.symm x
-- Mathlib.Algebra.Order.UpperLower
upperClosure_smul : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α] (s : Set α) (a : α),
  upperClosure (a • s) = a • upperClosure s
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLEAntisymmOpposite : ∀ {α : Type u_1} {i : LE α} [Std.Antisymm fun x1 x2 => x1 ≤ x2], Std.Antisymm fun x1 x2 => x1 ≤ x2
-- Mathlib.Dynamics.PeriodicPts.Defs
MulAction.pow_smul_eq_iff_period_dvd : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] {n : ℕ} {m : M} {a : α},
  m ^ n • a = a ↔ MulAction.period m a ∣ n
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.instMonoZero : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D]
  (M : D) [inst_2 : CategoryTheory.AddMonObj M], CategoryTheory.Mono CategoryTheory.AddMonObj.zero
-- Mathlib.Algebra.CharP.Quotient
CharP.ker_intAlgebraMap_eq_span : ∀ {R : Type u_1} [inst : Ring R] (p : ℕ) [CharP R p], RingHom.ker (algebraMap ℤ R) = Ideal.span {↑p}
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstNegInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Analysis.Normed.Module.WeakDual
WeakDual.polar_def : ∀ (𝕜 : Type u_1) {M : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module 𝕜 M] (s : Set M), WeakDual.polar 𝕜 s = {f | ∀ x ∈ s, ‖f x‖ ≤ 1}
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Comma.costructuredArrowSndInclusion_obj_right_as : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow L (R.obj b)),
  ((CategoryTheory.Comma.costructuredArrowSndInclusion L R b).obj X).right.as = PUnit.unit
-- Init.Data.String.Basic
String.Slice.Pos.sliceFrom_ofSliceFrom : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos}, p₀.sliceFrom (String.Slice.Pos.ofSliceFrom p) ⋯ = p
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.Cache.denote_eq_eval_of_get?_eq_some_of_Inv : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {w : ℕ} {assign : Std.Tactic.BVDecide.BVExpr.Assignment}
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) (expr : Std.Tactic.BVDecide.BVExpr w) (refs : aig.RefVec w),
  cache.get? expr = some refs →
    Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig cache →
      ∀ (i : ℕ) (h : i < w),
        ⟦assign.toAIGAssignment, { aig := aig, ref := refs.get i h }⟧ =
          (Std.Tactic.BVDecide.BVExpr.eval assign expr).getLsbD i
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instDecidableEqDecl.decEq : {α : Type} → [DecidableEq α] → (x x_1 : Std.Sat.AIG.Decl α) → Decidable (x = x_1)
-- Mathlib.RingTheory.DedekindDomain.SInteger
Set.coe_unit : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R))
  (K : Type v) [inst_2 : Field K] [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K],
  ↑(S.unit K) = {x | ∀ v ∉ S, (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑x = 1}
-- Mathlib.Algebra.Group.Prod
Prod.instLeftCancelSemigroup : {G : Type u_1} → {H : Type u_2} → [LeftCancelSemigroup G] → [LeftCancelSemigroup H] → LeftCancelSemigroup (G × H)
-- Init.Core
imp_not_comm : ∀ {a b : Prop}, a → ¬b ↔ b → ¬a
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The bijection `normalized_factors_equiv_span_normalized_factors.symm` between the set of prime
factors of the ideal `⟨r⟩` and the set of prime factors of `r` preserves multiplicities.  -/
Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  [inst_3 : NormalizationMonoid R] {r : R} (hr : r ≠ 0)
  (I : ↑{I | I ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})}),
  emultiplicity (↑((Ideal.normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r =
    emultiplicity (↑I) (Ideal.span {r})
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine X],
  CategoryTheory.CategoryStruct.comp X.isoSpec.inv X.toSpecΓ =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op ⊤)))
-- Mathlib.Algebra.Lie.Basic
LieHom.ext_iff : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] {f g : L₁ →ₗ⁅R⁆ L₂}, f = g ↔ ∀ (x : L₁), f x = g x
-- Init.Data.UInt.Lemmas
USize.toFin_ofBitVec : ∀ {b : BitVec System.Platform.numBits}, { toBitVec := b }.toFin = b.toFin
-- Mathlib.Algebra.Lie.Basis.Prod
/-- The Lie subalgebra `LieAlgebra.Basis.prod` is a copy of the Cartan subalgebra of the input.  -/
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.prodCartanEquiv : {ι₁ : Type u_1} →
  {ι₂ : Type u_2} →
    {L₁ : Type u_3} →
      {L₂ : Type u_4} →
        [inst : Finite ι₁] →
          [inst_1 : Finite ι₂] →
            (eι : ι₁ ≃ ι₂) →
              [inst_2 : LieRing L₁] →
                [inst_3 : LieRing L₂] →
                  {R : Type u_5} →
                    [inst_4 : CommRing R] →
                      [inst_5 : LieAlgebra R L₁] →
                        {H₁ : LieSubalgebra R L₁} →
                          (b₁ : LieAlgebra.Basis ι₁ H₁) →
                            [inst_6 : LieAlgebra R L₂] →
                              {H₂ : LieSubalgebra R L₂} →
                                (b₂ : LieAlgebra.Basis ι₂ H₂) → ↥(LieAlgebra.Basis.prodCartan✝ eι b₁ b₂) ≃ₗ[R] ↥H₁
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelDesc_comp_eq_zero : ∀ {X Y Z W : SemiNormedGrp} {f : X ⟶ Y} {g : Y ⟶ Z} {h : Z ⟶ W} (cond : CategoryTheory.CategoryStruct.comp f g = 0),
  CategoryTheory.CategoryStruct.comp g h = 0 →
    CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelDesc cond) h = 0
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_inv_nhdsLE_inv : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousInv H] {a : H}, Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Iic a⁻¹)) (nhdsWithin a (Set.Ici a))
-- Mathlib.Topology.Order.LeftRight
nhdsGT_sup_nhdsWithin_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] (a : α),
  nhdsWithin a (Set.Ioi a) ⊔ nhdsWithin a {a} = nhdsWithin a (Set.Ici a)
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.instCoeSortType : CoeSort CommMonCat (Type u)
-- Mathlib.Algebra.Lie.CartanSubalgebra
LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [Nontrivial L]
  (H : LieSubalgebra R L) [H.IsCartanSubalgebra], Nontrivial ↥H
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
Finset.centroidWeights.eq_1 : ∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι),
  Finset.centroidWeights k s = Function.const ι (↑s.card)⁻¹
-- Mathlib.Tactic.Peel
/-- This is the core to the `peel` tactic.

It tries to match `e` and `goal` as quantified statements (using `∀` and the quantifiers in
the `quantifiers` list), then applies "peel theorems" using `applyPeelThm`.

We treat `∧` as a quantifier for sake of dealing with quantified statements
like `∃ δ > (0 : ℝ), q δ`, which is notation for `∃ δ, δ > (0 : ℝ) ∧ q δ`.  -/
Mathlib.Tactic.Peel.peelCore : Lean.MVarId → Lean.Expr → Option Lean.Name → Lean.Name → Bool → Lean.MetaM (Lean.FVarId × List Lean.MVarId)
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instInter : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Inter (Std.DTreeMap.Raw α β cmp)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_eq_two_mul_T_comp_half_mul_X : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible 2] (n : ℤ),
  Polynomial.Chebyshev.C R n = 2 * (Polynomial.Chebyshev.T R n).comp (Polynomial.C ⅟2 * Polynomial.X)
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.degBound_casesOn_succ : ∀ (k₀ k : ℕ) (D : ℕ → ℕ) (n : ℕ),
  ChevalleyThm.MvPolynomialC.degBound k₀ (fun t => Nat.casesOn t k D) (n + 1) =
    (k₀ * k) ^ (k₀ * k) * ChevalleyThm.MvPolynomialC.degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n
-- Mathlib.LinearAlgebra.Contraction
zero_prodMap_dualTensorHom : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (g : Module.Dual R N) (q : Q),
  LinearMap.prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) =
    (dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ LinearMap.snd R M N) ⊗ₜ[R] (LinearMap.inr R P Q) q)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCancelCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] (D : A →ₗ[R] M)
  (h : ∀ (a b : A), D (a * b) = a • D b + b • D a), ⇑(Derivation.mk' D h) = ⇑D
-- Mathlib.Order.LatticeIntervals
Set.Iic.complementedLattice_iff : ∀ {α : Type u_1} {a : α} [inst : Lattice α] [inst_1 : OrderBot α],
  ComplementedLattice ↑(Set.Iic a) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k k' : α} {f : Option β → Option β} {h : k' ∈ m.alter k f},
  (m.alter k f).getKey k' h = if heq : (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- The canonical (semiring) equivalence between `WithAbs v` and `R`.  -/
WithAbs.equiv : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] → [inst_1 : PartialOrder S] → [inst_2 : Semiring R] → (v : AbsoluteValue R S) → WithAbs v ≃+* R
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.exists_edist_eq_ediam_of_finite : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α] [Finite α], ∃ u v, G.edist u v = G.ediam
-- Mathlib.Topology.ContinuousMap.Basic
Homeomorph.coe_refl : ∀ {α : Type u_1} [inst : TopologicalSpace α], ↑(Homeomorph.refl α) = ContinuousMap.id α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.braiding_inv_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C),
  CategoryTheory.CategoryStruct.comp (β_ X Y).inv (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) =
    CategoryTheory.SemiCartesianMonoidalCategory.snd Y X
-- Init.Tactics
/-- Optional configuration option for tactics. (Deprecated. Replace `(config)?` with `optConfig`.)  -/
Lean.Parser.Tactic.config : Lean.ParserDescr
-- Mathlib.Algebra.Order.Monovary
Monovary.div_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f : ι → α} {g₁ g₂ : ι → β},
  0 ≤ g₁ → StrongLT 0 g₂ → Monovary f g₁ → Antivary f g₂ → Monovary f (g₁ / g₂)
-- Init.Data.List.Monadic
List.zipWithM.loop.induct_unfolding : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type x} {γ : Type u} (f : α → β → m γ)
  (motive : List α → List β → Array γ → m (List γ) → Prop),
  (∀ (a : α) (as : List α) (b : β) (bs : List β) (acc : Array γ),
      (∀ (__do_lift : γ), motive as bs (acc.push __do_lift) (List.zipWithM.loop f as bs (acc.push __do_lift))) →
        motive (a :: as) (b :: bs) acc do
          let __do_lift ← f a b
          List.zipWithM.loop f as bs (acc.push __do_lift)) →
    (∀ (t : List α) (x : List β) (acc : Array γ),
        (∀ (a : α) (as : List α) (b : β) (bs : List β), t = a :: as → x = b :: bs → False) →
          motive t x acc (pure acc.toList)) →
      ∀ (x : List α) (x_1 : List β) (x_2 : Array γ), motive x x_1 x_2 (List.zipWithM.loop f x x_1 x_2)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.instInhabitedId : {X : Type u} → [inst : TopologicalSpace X] → Inhabited ((ContinuousMap.id X).Homotopy (ContinuousMap.id X))
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_one_comp_σ₂_one : ∀ {n : ℕ} (hn : autoParam ({ len := n + 1 }.len ≤ 2) SimplexCategory.Truncated.δ₂_one_comp_σ₂_one._auto_1)
  (hn' : autoParam ({ len := n + 1 + 1 }.len ≤ 2) SimplexCategory.Truncated.δ₂_one_comp_σ₂_one._auto_3),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.δ₂ 1 hn hn') (SimplexCategory.Truncated.σ₂ 1 hn' hn) =
    CategoryTheory.CategoryStruct.id { obj := { len := n + 1 }, property := hn }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {f : β k → β k}, (t.modify k f).get? k = Option.map f (t.get? k)
-- Std.Data.HashSet.Basic
/-- Returns the number of buckets in the internal representation of the hash set. This function may
be useful for things like monitoring system health, but it should be considered an internal
implementation detail.
 -/
Std.HashSet.Internal.numBuckets : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → ℕ
-- Mathlib.AlgebraicGeometry.Scheme
/-- **Alias** of `AlgebraicGeometry.Scheme.homeoOfIso`.

---

An isomorphism of schemes induces a homeomorphism of the underlying topological spaces.  -/
CategoryTheory.Iso.schemeIsoToHomeo : {X Y : AlgebraicGeometry.Scheme} → (X ≅ Y) → ↥X ≃ₜ ↥Y
-- Init.Data.String.Termination
/-- Use `termination_by pos.down` to signify that in a recursive call, the parameter `pos` is
expected to decrease.  -/
String.Slice.Pos.down : {s : String.Slice} → s.Pos → String.Slice.Pos.Down s
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- If `G` is a commutative ring object, then `Hom(X, G)` has a commutative ring structure.  -/
CategoryTheory.Hom.commRing : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → {R X : C} → [CategoryTheory.CommRingObj R] → CommRing (X ⟶ R)
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
/-- Exponential as a function from `EReal` to `ℝ≥0∞`.  -/
EReal.exp : EReal → ENNReal
-- Mathlib.AlgebraicGeometry.LimitsOver
AlgebraicGeometry.instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst : CategoryTheory.Category.{v_1, u_1} J] (F : CategoryTheory.Functor J (P.Over ⊤ S))
  [(F.comp
        ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp
          ((CategoryTheory.Over.forget S).comp AlgebraicGeometry.Scheme.forget))).IsLocallyDirected],
  (((F.comp (CategoryTheory.MorphismProperty.Over.forget P ⊤ S)).comp (CategoryTheory.Over.forget S)).comp
      AlgebraicGeometry.Scheme.forget).IsLocallyDirected
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Cardinal.sSup_lt_of_lt_cof_ord : ∀ {s : Set Cardinal.{u}} {a : Cardinal.{u}},
  Cardinal.mk ↑s < (Cardinal.lift.{u + 1, u} a).ord.cof → (∀ i ∈ s, i < a) → sSup s < a
-- Mathlib.Order.Interval.Set.Fin
Fin.image_val_uIcc : ∀ {n : ℕ} (i j : Fin n), Fin.val '' Set.uIcc i j = Set.uIcc ↑i ↑j
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.swap_comp_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  (Monoid.Coprod.swap M N).comp Monoid.Coprod.inl = Monoid.Coprod.inr
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The restriction of a monoidal category along an object property
that's closed under the monoidal structure.  -/
CategoryTheory.MonoidalCategory.fullSubcategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (P : CategoryTheory.ObjectProperty C) →
        P (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) →
          (∀ (X Y : C), P X → P Y → P (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) →
            CategoryTheory.MonoidalCategory P.FullSubcategory
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.nilpotent_of_surjective`.

---

The range of a surjective homomorphism from a nilpotent group is nilpotent.  -/
nilpotent_of_surjective : ∀ {G : Type u_1} [inst : Group G] {G' : Type u_2} [inst_1 : Group G'] [h : Group.IsNilpotent G] (f : G →* G'),
  Function.Surjective ⇑f → Group.IsNilpotent G'
-- Mathlib.Data.Fin.Tuple.Basic
Fin.tail_def : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} {q : (i : Fin (n + 1)) → α i}, (Fin.tail fun k => q k) = fun k => q k.succ
-- Init.Conv
/-- Extracts `let` and `have` expressions from within the target expression.
This is the conv mode version of the `extract_lets` tactic.

- `extract_lets` extracts all the lets from the target.
- `extract_lets x y z` extracts all the lets from the target and uses `x`, `y`, and `z` for the first names.
  Using `_` for a name leaves it unnamed.

Limitation: the extracted local declarations do not persist outside of the `conv` goal.
See also `lift_lets`, which does not extract lets as local declarations.
 -/
Lean.Parser.Tactic.Conv.extractLets : Lean.ParserDescr
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Alt.toMessageData : Lean.Meta.Match.Alt → Lean.MetaM Lean.MessageData
-- Mathlib.Analysis.Complex.Basic
Complex.isUniformEmbedding_equivRealProd : IsUniformEmbedding ⇑Complex.equivRealProd
-- Init.Data.UInt.Lemmas
UInt16.ofFin_add : ∀ (a b : Fin UInt16.size), UInt16.ofFin (a + b) = UInt16.ofFin a + UInt16.ofFin b
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight_comp_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} [Finite ι]
  [Finite ι'] (f : ι → ι') (x : ι' → K), Height.mulHeight (x ∘ f) ≤ Height.mulHeight x
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.instSpectralSpace : ∀ {R : Type u} [inst : CommSemiring R], SpectralSpace (PrimeSpectrum R)
-- Mathlib.RingTheory.Ideal.Operations
instNonUnitalSubsemiringClassIdeal : ∀ {R : Type u_1} [inst : Semiring R], NonUnitalSubsemiringClass (Ideal R) R
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.quot_mk_eq_mk : ∀ {α : Type u} {L : List (α × Bool)}, Quot.mk FreeAddGroup.Red.Step L = FreeAddGroup.mk L
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.dual_id : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α],
  BoundedLatticeHom.dual (BoundedLatticeHom.id α) = BoundedLatticeHom.id αᵒᵈ