mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.PiL2
Module.Basis.coe_toOrthonormalBasis_repr : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (v : Module.Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v),
  ⇑(v.toOrthonormalBasis hv).repr = ⇑(v.equivFun ≪≫ₗ (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm)
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- A relative morphism is homotopic to itself.  -/
SSet.RelativeMorphism.Homotopy.refl : {X Y : SSet} →
  {A : X.Subcomplex} → {B : Y.Subcomplex} → {φ : A.toSSet ⟶ B.toSSet} → (f : SSet.RelativeMorphism A B φ) → f.Homotopy f
-- Init.Grind.AC
Lean.Grind.AC.Seq.contains_k_cons : ∀ (y x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
  (Lean.Grind.AC.Seq.cons y s).contains_k x = (x == y || s.contains_k x)
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.mul_div_cancel_right` for a simpler version assuming `b ≠ 0`, `b ≠ ∞`.  -/
ENNReal.mul_div_cancel_right' : ∀ {a b : ENNReal}, (b = 0 → a = 0) → (b = ⊤ → a = 0) → a * b / b = a
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- `repr` is the isomorphism between the group `G` and the free group generated by `ι`.  -/
FreeGroupBasis.repr : {ι : Type u_1} → {G : Type u_2} → [inst : Group G] → FreeGroupBasis ι G → G ≃* FreeGroup ι
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.intersperseTR.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) →
      (Unit → motive []) → ((x : α) → motive [x]) → ((x y : α) → (xs : List α) → motive (x :: y :: xs)) → motive x
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.rooIterator : {α : Type u_1} → {β : α → Type u_2} → [inst : Ord α] → Std.DTreeMap.Internal.Impl α β → α → α → Std.Iter ((a : α) × β a)
-- Mathlib.Data.ENat.Lattice
ENat.add_biSup' : ∀ {ι : Sort u_2} {a : ℕ∞} {p : ι → Prop},
  (∃ i, p i) → ∀ (f : ι → ℕ∞), a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_range_add : ∀ {M : Type u_4} [inst : AddCommMonoid M] (f : ℕ → M) (n m : ℕ),
  ∑ x ∈ Finset.range (n + m), f x = ∑ x ∈ Finset.range n, f x + ∑ x ∈ Finset.range m, f (n + x)
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Entry.global.inj : ∀ {α : Type} {a a_1 : α}, Lean.ScopedEnvExtension.Entry.global a = Lean.ScopedEnvExtension.Entry.global a_1 → a = a_1
-- Init.SimpLemmas
Bool.not_eq_true' : ∀ (b : Bool), ((!b) = true) = (b = false)
-- Mathlib.Algebra.MonoidAlgebra.Division
/-- Divide by `of' k G g`, discarding terms not divisible by this.  -/
AddMonoidAlgebra.divOf : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Semiring k] → [inst_1 : AddCommMonoid G] → [IsCancelAdd G] → AddMonoidAlgebra k G → G → AddMonoidAlgebra k G
-- Lean.Meta.Basic
/-- Convert `isDefEq` and `WHNF` relevant parts into a key for caching results  -/
_private.Lean.Meta.Basic.0.Lean.Meta.Config.toKey : Lean.Meta.Config → UInt64
-- Mathlib.Condensed.Light.Small
CategoryTheory.Equivalence.sheafCongr.inverse.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e e_1 : C ≌ D)
  (e_e : e = e_1) (A : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse],
  CategoryTheory.Equivalence.sheafCongr.inverse J K e A = CategoryTheory.Equivalence.sheafCongr.inverse J K e_1 A
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.exact₃' : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (self : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁)
  (D : CategoryTheory.ComposableArrows ι 2),
  (CategoryTheory.ComposableArrows.mk₂
      ((self.H n₀).map
        ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2 CategoryTheory.Abelian.SpectralObject._proof_8
              CategoryTheory.Abelian.SpectralObject._proof_2 CategoryTheory.Abelian.SpectralObject._proof_6
              CategoryTheory.Abelian.SpectralObject._proof_4 CategoryTheory.Abelian.SpectralObject._proof_4).app
          D))
      ((self.δ' n₀ n₁ h).app D)).Exact
-- Mathlib.Order.Antisymmetrization
Antisymmetrization.prodEquiv_symm_apply_mk : ∀ (α : Type u_1) (β : Type u_2) [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β},
  (Antisymmetrization.prodEquiv α β).symm (⟦a⟧, ⟦b⟧) = ⟦(a, b)⟧
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.instSMul : {M : Type u_2} →
  {N : Type u_4} →
    {ι : Type u_6} →
      [inst : AddCommMonoid M] →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : TopologicalSpace N] →
              {R' : Type u_7} →
                {A : Type u_9} →
                  [inst_4 : Monoid R'] →
                    [inst_5 : Semiring A] →
                      [inst_6 : Module A M] →
                        [inst_7 : Module A N] →
                          [inst_8 : DistribMulAction R' N] →
                            [ContinuousConstSMul R' N] → [SMulCommClass A R' N] → SMul R' (M [⋀^ι]→L[A] N)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Const.alterKey_cons_perm.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (v : β) (h_1 : Unit → motive none) (h_2 : (v : β) → motive (some v)),
  (match some v with
    | none => h_1 ()
    | some v => h_2 v) =
    h_2 v
-- Mathlib.Order.SuccPred.Basic
Order.le_iff_eq_or_succ_le' : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a b : α}, a ≤ b ↔ b = a ∨ Order.succ a ≤ b
-- Init.Data.Nat.Lemmas
Nat.add_sub_sub_add_right : ∀ (n m k l : ℕ), n + l - m - (k + l) = n - m - k
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Semiring.mk.inj : ∀ {id : ℕ} {type : Lean.Expr} {u : Lean.Level} {semiringInst : Lean.Expr}
  {addFn? mulFn? powFn? natCastFn? : Option Lean.Expr}
  {denote : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.SemiringExpr}
  {vars : Lean.PArray Lean.Expr} {varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var} {id_1 : ℕ}
  {type_1 : Lean.Expr} {u_1 : Lean.Level} {semiringInst_1 : Lean.Expr}
  {addFn?_1 mulFn?_1 powFn?_1 natCastFn?_1 : Option Lean.Expr}
  {denote_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.SemiringExpr}
  {vars_1 : Lean.PArray Lean.Expr} {varMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var},
  { id := id, type := type, u := u, semiringInst := semiringInst, addFn? := addFn?, mulFn? := mulFn?, powFn? := powFn?,
        natCastFn? := natCastFn?, denote := denote, vars := vars, varMap := varMap } =
      { id := id_1, type := type_1, u := u_1, semiringInst := semiringInst_1, addFn? := addFn?_1, mulFn? := mulFn?_1,
        powFn? := powFn?_1, natCastFn? := natCastFn?_1, denote := denote_1, vars := vars_1, varMap := varMap_1 } →
    id = id_1 ∧
      type = type_1 ∧
        u = u_1 ∧
          semiringInst = semiringInst_1 ∧
            addFn? = addFn?_1 ∧
              mulFn? = mulFn?_1 ∧
                powFn? = powFn?_1 ∧ natCastFn? = natCastFn?_1 ∧ denote = denote_1 ∧ vars = vars_1 ∧ varMap = varMap_1
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.tprod_le_of_prod_le : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α} [L.NeBot],
  Multipliable f L → (∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂) → ∏'[L] (i : ι), f i ≤ a₂
-- Lean.Elab.Tactic.Simp
/-- Generic `simp` configuration elaborator, with an `evalConfig` argument for overriding how
the `(config := ...)` syntax is elaborated.
 -/
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.elabSimpConfigAux : (Lean.Term → Lean.Elab.TermElabM Lean.Meta.Simp.Config) →
  Lean.Syntax →
    optParam Lean.Meta.Simp.ConfigWithOptions { } →
      optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Meta.Simp.ConfigWithOptions
-- Mathlib.Algebra.Order.Ring.Basic
pow_four_le_pow_two_of_pow_two_le : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsOrderedRing R] [ExistsAddOfLE R] {a b : R},
  a ^ 2 ≤ b → a ^ 4 ≤ b ^ 2
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.MorphismProperty.isCardinalAccessible_ι_isLocal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [CategoryTheory.HasCardinalFilteredColimits C κ],
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → CategoryTheory.IsCardinalPresentable X κ ∧ CategoryTheory.IsCardinalPresentable Y κ) →
    W.isLocal.ι.IsCardinalAccessible κ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryLT_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {he : ∃ a ∈ t₁, compare a k = Ordering.lt},
  Std.DTreeMap.Internal.Impl.getEntryLT k t₁ ⋯ he = Std.DTreeMap.Internal.Impl.getEntryLT k t₂ ⋯ ⋯
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
/-- The two definitions of the conditional expectation `condExp` and `condLExp` (for Bochner and
Lebesgue integrals respectively) agree almost everywhere.  -/
MeasureTheory.toReal_condLExp : ∀ {𝓧 : Type u_1} (m : MeasurableSpace 𝓧) {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {f : 𝓧 → ENNReal},
  AEMeasurable f μ → ∫⁻ (x : 𝓧), f x ∂μ ≠ ⊤ → (fun x => (μ⁻[f | m] x).toReal) =ᵐ[μ] μ[fun x => (f x).toReal | m]
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Equiv.impl : ∀ {α : Type u} {β : α → Type v} {t t' : Std.DTreeMap.Internal.Impl α β}, t.Equiv t' → t.toListModel.Perm t'.toListModel
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.cylinder_anti : ∀ {E : ℕ → Type u_1} (x : (n : ℕ) → E n) {m n : ℕ}, m ≤ n → PiNat.cylinder x n ⊆ PiNat.cylinder x m
-- Mathlib.FieldTheory.KummerExtension
X_pow_sub_C_irreducible_iff_of_prime_pow : ∀ {K : Type u} [inst : Field K] {p : ℕ},
  Nat.Prime p →
    p ≠ 2 → ∀ {n : ℕ}, n ≠ 0 → ∀ {a : K}, Irreducible (Polynomial.X ^ p ^ n - Polynomial.C a) ↔ ∀ (b : K), b ^ p ≠ a
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.rank_adjoin_eq_one_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E},
  Module.rank F ↥(IntermediateField.adjoin F S) = 1 ↔ S ⊆ ↑⊥
-- Mathlib.Analysis.Matrix.Normed
Matrix.nnnorm_def : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] (A : Matrix m n α), ‖A‖₊ = ‖fun i j => A i j‖₊
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.ppAC : Lean.Meta.Grind.M✝ Unit
-- Init.Data.SInt.Lemmas
Int8.div_one : ∀ {a : Int8}, a / 1 = a
-- Mathlib.Order.Basic
/-- **Alias** of `strongLT_of_le_of_strongLT`. -/
LE.le.trans_strongLT : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → Preorder (π i)] {a b c : (i : ι) → π i},
  c ≤ b → StrongLT b a → StrongLT c a
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.modMonomial_add_divMonomial_single : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (x : MvPolynomial σ R) (i : σ),
  ((x.modMonomial fun₀ | i => 1) + MvPolynomial.X i * x.divMonomial fun₀ | i => 1) = x
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.gcdCoeffs.eq_1 : ∀ (x k : ℤ), (Int.Internal.Linear.Poly.num k).gcdCoeffs x = x
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.alternatingWord_succ : ∀ {B : Type u_1} (i i' : B) (m : ℕ),
  CoxeterSystem.alternatingWord i i' (m + 1) = (CoxeterSystem.alternatingWord i' i m).concat i'
-- Mathlib.RingTheory.RootsOfUnity.Basic
/-- Restrict a monoid isomorphism to the nth roots of unity.  -/
MulEquiv.restrictRootsOfUnity : {R : Type u_4} →
  {S : Type u_5} →
    [inst : CommMonoid R] → [inst_1 : CommMonoid S] → R ≃* S → (n : ℕ) → ↥(rootsOfUnity n R) ≃* ↥(rootsOfUnity n S)
-- Mathlib.Topology.FiberBundle.Constructions
/-- Given trivializations `e₁`, `e₂` for fiber bundles `E₁`, `E₂` over a base `B`, the inverse
function for the construction `Trivialization.prod`, the induced
trivialization for the fiberwise product of `E₁` and `E₂`.  -/
Bundle.Trivialization.Prod.invFun' : {B : Type u_1} →
  [inst : TopologicalSpace B] →
    {F₁ : Type u_2} →
      [inst_1 : TopologicalSpace F₁] →
        {E₁ : B → Type u_3} →
          [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
            {F₂ : Type u_4} →
              [inst_3 : TopologicalSpace F₂] →
                {E₂ : B → Type u_5} →
                  [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                    Bundle.Trivialization F₁ Bundle.TotalSpace.proj →
                      Bundle.Trivialization F₂ Bundle.TotalSpace.proj →
                        [(x : B) → Zero (E₁ x)] →
                          [(x : B) → Zero (E₂ x)] → B × F₁ × F₂ → Bundle.TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal mono becomes a normal epi in the opposite category.  -/
CategoryTheory.normalEpiOfNormalMonoUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : Cᵒᵖ} → (f : X ⟶ Y) → CategoryTheory.NormalMono f.unop → CategoryTheory.NormalEpi f
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- `S : IntermediateField K L` is a subset of `L` such that there is a field
tower `L / S / K`.  -/
IntermediateField : (K : Type u_1) → (L : Type u_2) → [inst : Field K] → [inst_1 : Field L] → [Algebra K L] → Type u_2
-- Mathlib.Algebra.Ring.Defs
CommRing.toAddCommGroupWithOne : {α : Type u} → [s : CommRing α] → AddCommGroupWithOne α
-- Mathlib.GroupTheory.Generators
/-- The subgroup closure of the generators is the whole group.  -/
Group.Generators.closure_eq_top : ∀ {G : Type u_5} [inst : Group G] {ι : Type u_6} (self : Group.Generators G ι),
  Subgroup.closure (Set.range self.val) = ⊤
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.instAlgebraSubtypeMem : {K : Type u} → [inst : Field K] → (A : ValuationSubring K) → Algebra (↥A) K
-- Mathlib.Logic.Basic
or_not : ∀ {p : Prop}, p ∨ ¬p
-- Init.Data.UInt.Bitwise
UInt8.toFin_and : ∀ (a b : UInt8), (a &&& b).toFin = a.toFin &&& b.toFin
-- Mathlib.Algebra.Order.Monoid.OrderDual
OrderDual.isOrderedMonoid : ∀ {α : Type u} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α], IsOrderedMonoid αᵒᵈ
-- Mathlib.CategoryTheory.Abelian.Opposite
/-- The cokernel of `g.unop` is the opposite of `kernel g`.  -/
CategoryTheory.cokernelUnopUnop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {A B : Cᵒᵖ} → (g : A ⟶ B) → CategoryTheory.Limits.cokernel g.unop ≅ Opposite.unop (CategoryTheory.Limits.kernel g)
-- Mathlib.CategoryTheory.Comma.CatCommSq
CategoryTheory.Arrow.catCommSq_iso : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{u_5, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{u_6, u_2} C₂] [inst_2 : CategoryTheory.Category.{u_7, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{u_8, u_4} D₂] (T : CategoryTheory.Functor C₁ C₂) (L : CategoryTheory.Functor C₁ D₁)
  (R : CategoryTheory.Functor C₂ D₂) (B : CategoryTheory.Functor D₁ D₂) [inst_4 : CategoryTheory.CatCommSq T L R B],
  CategoryTheory.CatCommSq.iso T.mapArrow L.mapArrow R.mapArrow B.mapArrow =
    (CategoryTheory.Functor.mapArrowFunctor C₁ D₂).mapIso (CategoryTheory.CatCommSq.iso T L R B)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Iio_castSucc : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n),
  ∏ i < a.castSucc, f i = ∏ i < a, f i.castSucc
-- Mathlib.Data.Set.Operations
/-- The preimage of `s : Set β` by `f : α → β`, written `f ⁻¹' s`,
is the set of `x : α` such that `f x ∈ s`.  -/
Set.preimage : {α : Type u} → {β : Type v} → (α → β) → Set β → Set α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasMultiplicativeReduction.toIsMinimal : ∀ {R : Type u_1} {inst : CommRing R} {inst_1 : IsDomain R} {inst_2 : IsDiscreteValuationRing R} {K : Type u_2}
  {inst_3 : Field K} {inst_4 : Algebra R K} {inst_5 : IsFractionRing R K} {W : WeierstrassCurve K}
  [self : WeierstrassCurve.HasMultiplicativeReduction R W], WeierstrassCurve.IsMinimal R W
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.descColimitType_ιColimitType_apply : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w₀)) (c : F.CoconeTypes)
  (j : J) (x : F.obj j), F.descColimitType c (F.ιColimitType j x) = c.ι j x
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_of_mul_dvd_mul_right : ∀ {a m n : ℤ}, a ≠ 0 → m * a ∣ n * a → m ∣ n
-- Lean.Elab.PreDefinition.WF.Fix
/-- Refine `F` over `PSigma.casesOn`  -/
_private.Lean.Elab.PreDefinition.WF.Fix.0.Lean.Elab.WF.processPSigmaCasesOn : Lean.Expr →
  Lean.Expr → Lean.Expr → (Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Expr) → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `setOfPred_gauge_lt_eq`. -/
gauge_lt_eq : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  Absorbent ℝ s → ∀ (a : ℝ), {x | gauge s x < a} = ⋃ r ∈ Set.Ioo 0 a, r • s
-- Mathlib.Topology.MetricSpace.Bounded
/-- If the distance between any two points in a nonempty set is bounded by some constant,
this constant bounds the diameter.  -/
Metric.diam_le_of_forall_dist_le_of_nonempty : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α],
  s.Nonempty → ∀ {C : ℝ}, (∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) → Metric.diam s ≤ C
-- Lean.Expr
Lean.Expr.isCharLit : Lean.Expr → Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.find?_toList_eq_some_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k}, List.find? (fun x_2 => x_2.fst == k) m.toList = some ⟨k, v⟩ ↔ m.get? k = some v
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsUniformAddGroup.of_compactSpace : ∀ {β : Type u_2} [inst : UniformSpace β] [inst_1 : AddGroup β] [ContinuousSub β] [CompactSpace β], IsUniformAddGroup β
-- Std.Data.TreeMap.Slice
Std.TreeMap.toList_roc : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.toList_roc._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap α β cmp} {lowerBound upperBound : α},
  Std.Slice.toList (Std.Roc.Sliceable.mkSlice t lowerBound<...=upperBound) =
    List.filter (fun e => decide ((cmp e.1 lowerBound).isGT = true ∧ (cmp e.1 upperBound).isLE = true)) t.toList
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.oneGtZero : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Lean.Environment
/-- Constructs a declaration from a theorem, resorting to an unsafe def if needed  -/
Lean.mkThmOrUnsafeDef : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.TheoremVal → m Lean.Declaration
-- Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_hom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom =
    CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.initial.to X) (CategoryTheory.CategoryStruct.id X)
-- Mathlib.Algebra.Order.Group.Cone
PartialOrder.mkOfAddGroupCone_le_iff : ∀ {S : Type u_3} {G : Type u_4} [inst : AddCommGroup G] [inst_1 : SetLike S G] [inst_2 : AddGroupConeClass S G] {C : S}
  {a b : G}, a ≤ b ↔ b - a ∈ C
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.W.dest_mk : ∀ {P : PFunctor.{uA, uB}} (p : ↑P P.W), (PFunctor.W.mk p).dest = p
-- Lean.Attributes
/-- Predicate run on each declaration-param pair to check whether it should be exported. By default,
only params on public declarations are exported.
 -/
Lean.ParametricAttributeImpl.filterExport : {α : Type} → Lean.ParametricAttributeImpl α → Lean.Environment → Lean.Name → α → Bool
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The Dirac delta distribution  -/
TemperedDistribution.delta : {E : Type u_3} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℝ E] → E → TemperedDistribution E ℂ
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
/-- Let `it₁` and `it₂` be iterators and `f` a monadic function mapping `it₁`'s outputs to iterators
of the same type as `it₂`. Then `it₁.flatMapAfterM f it₂` first goes over `it₂` and then over
`it₁.flatMap f it₂`, emitting all their values.

The main purpose of this combinator is to represent the intermediate state of a `flatMap` iterator
that is currently iterating over one of the inner iterators.

**Marble diagram (without monadic effects):**

```text
it₁                            --b      c    --d -⊥
it₂                      a1-a2⊥
f b                               b1-b2⊥
f c                                      c1-c2⊥
f d                                             ⊥
it.flatMapAfterM f it₂   a1-a2----b1-b2--c1-c2----⊥
```

**Termination properties:**

* `Finite` instance: only if `it₁`, `it₂` and the inner iterators are finite
* `Productive` instance: only if `it₁` is finite and `it₂` and the inner iterators are productive

For certain functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer
iterator is productive and the inner
iterators are productive *and provably never empty*, then the resulting iterator is also productive.

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it₁`, `it₂` or an internal
iterator.

For each value emitted by the outer iterator `it₁`, this combinator calls `f`.
 -/
Std.IterM.flatMapAfterM : {α β α₂ γ : Type w} →
  {m : Type w → Type w'} →
    [inst : Monad m] →
      [inst_1 : MonadAttach m] →
        [Std.Iterator α m β] →
          [Std.Iterator α₂ m γ] → (f : β → m (Std.IterM m γ)) → Std.IterM m β → Option (Std.IterM m γ) → Std.IterM m γ
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.symm_involutive : ∀ {V : Type u_1} {G : SimpleGraph V}, Function.Involutive SimpleGraph.Dart.symm
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverMincard_antitone : ∀ {X : Type u_1} (T : X → X) (F : Set X) (n : ℕ), Antitone fun U => Dynamics.coverMincard T F U n
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.truncGELTToLTGE.eq_1 : ∀ {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) [inst_6 : CategoryTheory.IsTriangulated C] (a b : ℤ),
  t.truncGELTToLTGE a b =
    {
      app := fun X =>
        t.liftTruncLT
          (t.descTruncGE (CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) ((t.truncGEπ a).app X)) a) (b - 1) b
          ⋯,
      naturality := ⋯ }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α},
  (m.erase k).get? a = if (k == a) = true then none else m.get? a
-- Mathlib.Algebra.GradedMulAction
/-- A graded version of `MulAction`.  -/
GradedMonoid.GMulAction : {ιA : Type u_1} →
  {ιM : Type u_3} →
    (A : ιA → Type u_4) →
      (ιM → Type u_5) →
        [inst : AddMonoid ιA] → [VAdd ιA ιM] → [GradedMonoid.GMonoid A] → Type (max (max (max u_1 u_3) u_4) u_5)
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.sub_coeffs : ∀ {l₁ l₂ : Lean.Omega.LinearCombo}, (l₁ - l₂).coeffs = l₁.coeffs - l₂.coeffs