mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.CompleteLattice.Basic
iSup_and : ∀ {α : Type u_1} [inst : CompleteLattice α] {p q : Prop} {s : p ∧ q → α}, iSup s = ⨆ (h₁ : p), ⨆ (h₂ : q), s ⋯
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instHashableLetValue : {pu : Lean.Compiler.LCNF.Purity} → Hashable (Lean.Compiler.LCNF.LetValue pu)
-- Lean.Environment
Lean.ModuleData.mk : Bool →
  Array Lean.Import →
    Array Lean.Name →
      Array Lean.ConstantInfo → Array Lean.Name → Array (Lean.Name × Array Lean.EnvExtensionEntry) → Lean.ModuleData
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
/-- Any matrix power can be computed as the sum of matrix powers less than `Fintype.card n`.

TODO: add the statement for negative powers phrased with `zpow`.  -/
Matrix.pow_eq_aeval_mod_charpoly : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  (k : ℕ), M ^ k = (Polynomial.aeval M) (Polynomial.X ^ k %ₘ M.charpoly)
-- Mathlib.Data.Set.FiniteExhaustion
Set.FiniteExhaustion.instFunLikeNat : {α : Type u_1} → {s : Set α} → FunLike s.FiniteExhaustion ℕ (Set α)
-- Mathlib.Algebra.Lie.Submodule
/-- The Lie submodules of a Lie module form a complete lattice.  -/
LieSubmodule.instCompleteLattice : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → CompleteLattice (LieSubmodule R L M)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_le_preBeth : ∀ {o₁ o₂ : Ordinal.{u_1}}, Cardinal.preBeth o₁ ≤ Cardinal.preBeth o₂ ↔ o₁ ≤ o₂
-- Init.Data.Array.Sort.Basic
Subarray.mergeSort : {α : Type u_1} → Subarray α → autoParam (α → α → Bool) Subarray.mergeSort._auto_1 → Array α
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_pullback_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X : C} (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
  (Y : CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)),
  (CategoryTheory.ChosenPullbacksAlong.pullback f).obj Y =
    CategoryTheory.Over.mk (CategoryTheory.SemiCartesianMonoidalCategory.snd Y.left X)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanDeclIdent.toJson : Lean.Lsp.LeanDeclIdent → Lean.Json
-- Mathlib.RingTheory.Discriminant
/-- Relation between `Algebra.discr A ι b` and
`Algebra.discr A ((P.map (algebraMap A B)) *ᵥ b)`.  -/
Algebra.discr_of_matrix_mulVec : ∀ {A : Type u} {B : Type v} {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra A B] [inst_4 : Fintype ι] (b : ι → B) (P : Matrix ι ι A),
  Algebra.discr A ((P.map ⇑(algebraMap A B)).mulVec b) = P.det ^ 2 * Algebra.discr A b
-- Mathlib.Data.Set.MulAntidiagonal
Set.swap_mem_mulAntidiagonal_aux : ∀ {α : Type u_1} [inst : CommMagma α] {s t : Set α} {a : α} {x : α × α},
  x.2 ∈ s ∧ x.1 ∈ t ∧ x.2 * x.1 = a ↔ x ∈ t.mulAntidiagonal s a
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- The right homotopy expressing that `f ≫ π f` is sent to `0` in `RightFreyd V`.  -/
CategoryTheory.Preadditive.RightFreyd.Candidate.condition : {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.Arrow.RightHomotopy
              (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Preadditive.RightFreyd.Candidate.π f)) 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α}, (t.erase k).get? k = none
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.nontrivial : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [Nonempty ι]
  [NeZero 2], Nontrivial M
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.minD_le_minD_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α},
      (t.erase k).isEmpty = false → ∀ {fallback : α}, (cmp (t.minD fallback) ((t.erase k).minD fallback)).isLE = true
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.NormalExpr.zero : Lean.Expr → Mathlib.Tactic.Abel.NormalExpr
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.map : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {x : α} {n : ℕ},
  Function.IsPeriodicPt fa n x → ∀ {g : α → β}, Function.Semiconj g fa fb → Function.IsPeriodicPt fb n (g x)
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.IsUltrahomogeneous.age_isFraisse : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] [Countable M],
  L.IsUltrahomogeneous M → FirstOrder.Language.IsFraisse (L.age M)
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_val_Ioc : ∀ {n : ℕ} (a b : Fin n), Finset.image Fin.val (Finset.Ioc a b) = Finset.Ioc ↑a ↑b
-- Mathlib.Algebra.Group.Action.Basic
MulAction.toFun.eq_1 : ∀ (M : Type u_2) (α : Type u_5) [inst : Monoid M] [inst_1 : MulAction M α],
  MulAction.toFun M α = { toFun := fun y x => x • y, inj' := ⋯ }
-- Mathlib.RingTheory.Spectrum.Prime.Defs
PrimeSpectrum.ext_iff : ∀ {R : Type u_1} {inst : CommSemiring R} {x y : PrimeSpectrum R}, x = y ↔ x.asIdeal = y.asIdeal
-- Std.Tactic.BVDecide.Syntax
/-- Theorems tagged with the `bv_normalize` attribute are used during the rewriting step of the
`bv_decide` tactic.
 -/
Lean.Parser.bv_normalize : Lean.ParserDescr
-- Init.Core
/-- An equivalence relation `r : α → α → Prop` is a relation that is

* reflexive: `r x x`,
* symmetric: `r x y` implies `r y x`, and
* transitive: `r x y` and `r y z` implies `r x z`.

Equality is an equivalence relation, and equivalence relations share many of the properties of
equality.
 -/
Equivalence : {α : Sort u} → (α → α → Prop) → Prop
-- Mathlib.Data.Finite.Prod
Finite.instProd : ∀ {α : Type u_1} {β : Type u_2} [Finite α] [Finite β], Finite (α × β)
-- Mathlib.Order.ScottContinuity
ScottContinuousOn.id : ∀ {α : Type u_1} [inst : Preorder α] {D : Set (Set α)}, ScottContinuousOn D id
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.le_hsum_support_mem : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  {s : HahnSeries.SummableFamily Γ R α} {g g' : Γ},
  (∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g') → g' ∈ s.hsum.support → g ≤ g'
-- Mathlib.Order.MinMax
Antitone.map_min : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {a b : α},
  Antitone f → f (min a b) = max (f a) (f b)
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- A dependent version of `AddSubmonoid.iSup_induction`.  -/
AddSubmonoid.iSup_induction' : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} (S : ι → AddSubmonoid M)
  {motive : (x : M) → x ∈ ⨆ i, S i → Prop},
  (∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯) →
    motive 0 ⋯ →
      (∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x + y) ⋯) →
        ∀ {x : M} (hx : x ∈ ⨆ i, S i), motive x hx
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.Eqv.of_zero : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (r : R) (f : (i : ι) → s i) (i : ι),
  f i = 0 → PiTensorProduct.Eqv R s (FreeAddMonoid.of (r, f)) 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- This is a more convenient formulation to show that a `BinaryFan` constructed using
`BinaryFan.mk` is a limit cone.
 -/
CategoryTheory.Limits.BinaryFan.isLimitMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y W : C} →
      {fst : W ⟶ X} →
        {snd : W ⟶ Y} →
          (lift : (s : CategoryTheory.Limits.BinaryFan X Y) → s.pt ⟶ W) →
            (∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) fst = s.fst) →
              (∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) snd = s.snd) →
                (∀ (s : CategoryTheory.Limits.BinaryFan X Y) (m : s.pt ⟶ W),
                    CategoryTheory.CategoryStruct.comp m fst = s.fst →
                      CategoryTheory.CategoryStruct.comp m snd = s.snd → m = lift s) →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk fst snd)
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- LDU decomposition of a block matrix with an invertible top-left corner, using the
Schur complement.  -/
Matrix.fromBlocks_eq_of_invertible₁₁ : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype l] [inst_1 : Fintype m]
  [inst_2 : Fintype n] [inst_3 : DecidableEq l] [inst_4 : DecidableEq m] [inst_5 : DecidableEq n] [inst_6 : CommRing α]
  (A : Matrix m m α) (B : Matrix m n α) (C : Matrix l m α) (D : Matrix l n α) [inst_7 : Invertible A],
  Matrix.fromBlocks A B C D =
    Matrix.fromBlocks 1 0 (C * ⅟A) 1 * Matrix.fromBlocks A 0 0 (D - C * ⅟A * B) * Matrix.fromBlocks 1 (⅟A * B) 0 1
-- Mathlib.RingTheory.FractionalIdeal.Operations
IsFractional.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : Submodule R P), IsFractional S I = ∃ a ∈ S, ∀ b ∈ I, IsLocalization.IsInteger R (a • b)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {k : α}, (cmp t.maxKey! k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- The transvection `transvection i j hij b` acts on `e_j = Pi.single j 1` by adding `b·e_i`.  -/
Matrix.SpecialLinearGroup.transvection_smul_single_snd : ∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F] {i j : ι}
  (hij : i ≠ j) (b : F),
  Matrix.SpecialLinearGroup.transvection hij b • Pi.single j 1 = Pi.single j 1 + b • Pi.single i 1
-- Mathlib.Order.Partition.Finpartition
Finpartition.extendOfLE.congr_simp : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableEq α] {a b : α} (P P_1 : Finpartition a),
  P = P_1 → ∀ (hab : a ≤ b), P.extendOfLE hab = P_1.extendOfLE hab
-- Mathlib.Analysis.Calculus.FDeriv.Defs
hasFDerivAt_iff_isLittleOTVS : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E},
  HasFDerivAt f f' x ↔ (fun x' => f x' - f x - f' (x' - x)) =o[𝕜; nhds x] fun x' => x' - x
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.Score.ofInt16! : Int16 → Lean.FuzzyMatching.Score✝
-- Mathlib.Algebra.GroupWithZero.Basic
mul_left_eq_self₀ : ∀ {M₀ : Type u_1} {a b : M₀} [inst : MulZeroOneClass M₀] [IsRightCancelMulZero M₀], a * b = b ↔ a = 1 ∨ b = 0
-- Mathlib.Data.ZMod.Basic
ZMod.cast_mul' : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] [CharP R n] (a b : ZMod n), (a * b).cast = a.cast * b.cast
-- Mathlib.Data.Seq.Computation
Computation.terminates_iff : ∀ {α : Type u} (s : Computation α), s.Terminates ↔ ∃ a, a ∈ s
-- Mathlib.Topology.Category.Stonean.EffectiveEpi
/-- An effective presentation of an `X : CompHaus` with respect to the inclusion functor from `Stonean`
 -/
Stonean.stoneanToCompHausEffectivePresentation : (X : CompHaus) → Stonean.toCompHaus.EffectivePresentation X
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.le_maxKey!_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k t = true → (compare k t.maxKey!).isLE = true
-- Mathlib.Topology.ClusterPt
Filter.HasBasis.mapClusterPt_iff_frequently : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} {ι : Sort u_3}
  {p : ι → Prop} {s : ι → Set X},
  (nhds x).HasBasis p s → (MapClusterPt x F u ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i)
-- Aesop.Builder.Basic
Aesop.RuleBuilderInput.phase : Aesop.RuleBuilderInput → Aesop.PhaseSpec
-- Mathlib.Algebra.Order.Field.Basic
one_half_lt_one : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α], 1 / 2 < 1
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
Matrix.IsPivotedBy.monotone : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Zero R] {A : Matrix m n R} {l : m → WithTop n}
  [inst_1 : LinearOrder n] [inst_2 : PartialOrder m], A.IsPivotedBy l → Monotone l
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.alternating : ∀ {α : Type u_3} [inst : Ring α] [inst_1 : UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] {f : ℕ → α},
  Summable f → Summable fun n => (-1) ^ n * f n
-- Init.Data.Array.Find
Array.exists_of_findSome?_eq_some : ∀ {α : Type u_1} {β : Type u_2} {b : β} {f : α → Option β} {xs : Array α},
  Array.findSome? f xs = some b → ∃ a ∈ xs, f a = some b
-- Mathlib.Algebra.Symmetrized
SymAlg.instSubsingleton : ∀ {α : Type u_1} [Subsingleton α], Subsingleton αˢʸᵐ
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_antitone : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  (∀ (x : β), p x → q x) → Filter.bliminf u f q ≤ Filter.bliminf u f p
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_sup_eq_of_coprime_right : ∀ {R : Type u} [inst : Semiring R] {I J K : Ideal R} [I.IsTwoSided], K ⊔ J = ⊤ → I * K ⊔ J = I ⊔ J
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.isIso_coprod : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z]
  (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.IsIso f] [CategoryTheory.IsIso g],
  CategoryTheory.IsIso (CategoryTheory.Limits.coprod.map f g)
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.range_mulVecLin : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : Fintype n] (M : Matrix m n R),
  M.mulVecLin.range = Submodule.span R (Set.range M.col)
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- The extended GCD `a` value in the equation `gcd x y = x * a + y * b`.  -/
EuclideanDomain.gcdA : {R : Type u} → [EuclideanDomain R] → [DecidableEq R] → R → R → R
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_div_const_Ioi : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => x / a) ⁻¹' Set.Ioi b = Set.Ioi (b * a)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_of_mem_insertMany_list : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α}, k ∈ m.insertMany l → (List.map Sigma.fst l).contains k = false → k ∈ m
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.union_indep_iff_forall_notMem_closure_left : ∀ {α : Type u_2} {M : Matroid α} {I J : Set α},
  M.Indep I → M.Indep J → (M.Indep (I ∪ J) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∩ m₂).get? k = none
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonRenameFile.toJson : Lean.Lsp.RenameFile → Lean.Json
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.mulCayley_monotone : ∀ {M : Type u_1} [inst : Mul M], Monotone fun x => SimpleGraph.mulCayley x
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.instReprPatternArgKind.repr : Lean.Meta.Grind.NormalizePattern.PatternArgKind → ℕ → Std.Format
-- Mathlib.Order.Booleanisation
Booleanisation.comp_inf_comp : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (a b : α),
  Booleanisation.comp a ⊓ Booleanisation.comp b = Booleanisation.comp (a ⊔ b)
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
WithIdeal.uniformContinuous_of_map_le : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : WithIdeal R] {S : Type u_2} [inst_2 : CommRing S] [inst_3 : WithIdeal S]
  {f : R →+* S}, Ideal.map f WithIdeal.i ≤ WithIdeal.i → UniformContinuous ⇑f
-- Init.Data.Float.Float
instNonemptyFloat : Nonempty Float
-- Init.Data.Iterators.Basic
/-- Converts an `Iter.Step` into an `IterM.Step`.
 -/
Std.Iter.Step.toMonadic : {α β : Type w} → [inst : Std.Iterator α Id β] → {it : Std.Iter β} → it.Step → it.toIterM.Step
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Cache.mk : Lean.PHashMap Lean.Name Lean.Meta.Sym.BackwardRule →
  Lean.PHashMap (ℕ × ℕ) Lean.Meta.Sym.BackwardRule →
    Std.HashMap Lean.Elab.Tactic.Grind.SimpCacheKey Lean.Meta.Sym.Simp.State →
      Std.HashMap Lean.Elab.Tactic.Grind.DSimpCacheKey Lean.Meta.Sym.DSimp.State → Lean.Elab.Tactic.Grind.Cache
-- Std.Internal.UV.Signal
/-- `Signal`s are used to generate `IO.Promise`s that resolve when a specific signal is received.

A `Signal` can be in one of 3 states:
- Right after construction it's initial.
- While it is listening for signals it's running.
- If it has stopped for some reason it's finished.

This together with whether it was set up as `repeating` with `Signal.mk` determines the behavior
of all functions on `Signal`s.
 -/
Std.Internal.UV.Signal : Type
-- Init.Data.Ord.Basic
Ordering.isEq_eq_beq_eq : ∀ {o : Ordering}, o.isEq = (o == Ordering.eq)
-- Mathlib.Combinatorics.Graph.Maps
Graph.map_id : ∀ {α : Type u_1} {β : Type u_4} {G : Graph α β}, Graph.map id G = G
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.hasGoodReduction_iff_isElliptic_reduction : ∀ (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}
  [hW : WeierstrassCurve.IsMinimal R W],
  WeierstrassCurve.HasGoodReduction R W ↔ (WeierstrassCurve.reduction R W).IsElliptic
-- Init.Data.Vector.Attach
/-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`.  -/
Vector.map_attach_eq_pmap : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : { x // x ∈ xs } → β},
  Vector.map f xs.attach = Vector.pmap (fun a h => f ⟨a, h⟩) xs ⋯
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, Std.TreeMap.Raw.empty.WF
-- Lean.Compiler.ExternAttr
/-- - `@[extern]`
   encoding: ```.entries = [adhoc `all]```
- `@[extern "level_hash"]`
   encoding: ```.entries = [standard `all "levelHash"]```
- `@[extern cpp "lean::string_size" llvm "lean_str_size"]`
   encoding: ```.entries = [standard `cpp "lean::string_size", standard `llvm "leanStrSize"]```
- `@[extern cpp inline "#1 + #2"]`
   encoding: ```.entries = [inline `cpp "#1 + #2"]```
- `@[extern cpp "foo" llvm adhoc]`
   encoding: ```.entries = [standard `cpp "foo", adhoc `llvm]```
 -/
Lean.ExternAttrData : Type
-- Init.Data.String.Lemmas.Intercalate
String.toList_join : ∀ {l : List String}, (String.join l).toList = List.flatMap String.toList l
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_C : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (p : ℕ) (r : R),
  (MvPolynomial.expand p) (MvPolynomial.C r) = MvPolynomial.C r
-- Init.Data.List.Pairwise
List.getElem_inj : ∀ {α : Type u_1} {i j : ℕ} {xs : List α} {h₀ : i < xs.length} {h₁ : j < xs.length}, xs.Nodup → (xs[i] = xs[j] ↔ i = j)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `inv_mul_lt_iff_lt_mul`. -/
lt_mul_of_inv_mul_lt : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c : α}, b⁻¹ * a < c → a < b * c
-- Mathlib.Order.Partition.Basic
Partition.sSup_eq : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α] (P : Partition s), sSup ↑P = s
-- Mathlib.Combinatorics.Additive.SmallTripling
_private.Mathlib.Combinatorics.Additive.SmallTripling.0.Finset.small_neg_neg_pos_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] {A : Finset G} {K : ℝ},
  ↑(3 • A).card ≤ K * ↑A.card → ↑(-A + -A + A).card ≤ K ^ 2 * ↑A.card
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tan_mul_I : ∀ (x : ℂ), Complex.tan (x * Complex.I) = Complex.tanh x * Complex.I
-- Mathlib.Order.Defs.LinearOrder
/-- In a linearly ordered type, we assume the order relations are all decidable.  -/
LinearOrder.toDecidableEq : {α : Type u_2} → [self : LinearOrder α] → DecidableEq α
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.exists_of_simplex : ∀ {X : SSet.Truncated 2} (s : X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Edge._proof_2 })),
  ∃ x₀ x₁ e, e.edge = s
-- Mathlib.Logic.Relation
Relation.reflTransGen_eq_reflGen : ∀ {α : Type u_1} {r : α → α → Prop} [IsTrans α r], Relation.ReflTransGen r = Relation.ReflGen r
-- Mathlib.Algebra.Ring.NonZeroDivisors
mul_cancel_left_coe_nonZeroDivisors : ∀ {R : Type u_1} [inst : Ring R] {x y : R} {c : ↥(nonZeroDivisors R)}, ↑c * x = ↑c * y ↔ x = y
-- Mathlib.Algebra.Lie.Weights.Basic
/-- For a triangularizable Lie module in finite dimensions, the weight spaces span the entire space.

See also `LieModule.iSup_genWeightSpace_eq_top'`.  -/
LieModule.iSup_genWeightSpace_eq_top : ∀ (K : Type u_1) (L : Type u_3) (M : Type u_4) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [inst_3 : LieRing.IsNilpotent L] [inst_4 : Field K] [inst_5 : LieAlgebra K L] [inst_6 : Module K M]
  [inst_7 : LieModule K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M],
  ⨆ χ, LieModule.genWeightSpace M χ = ⊤
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.top_ne_zero : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α], ⊤ ≠ 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_add : ∀ {x : ℂ} (y z : ℂ), x ≠ 0 → x ^ (y + z) = x ^ y * x ^ z
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.ringEquivOfRingEquiv.congr_simp : ∀ {A : Type u_8} {K : Type u_9} {B : Type u_10} {L : Type u_11} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : CommRing K] [inst_3 : CommRing L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K]
  [inst_6 : Algebra B L] [inst_7 : IsFractionRing B L] (h h_1 : A ≃+* B),
  h = h_1 → IsFractionRing.ringEquivOfRingEquiv h = IsFractionRing.ringEquivOfRingEquiv h_1
-- Mathlib.Combinatorics.Matroid.Basic
/-- A subset of `M.E` is `Dep`endent if it is not `Indep`endent .  -/
Matroid.Dep : {α : Type u_1} → Matroid α → Set α → Prop
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorHom_comp_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) (h : V ⟶ W) {Z_1 : C} (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj Z W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g W) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f g) h) h_1
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange], (P ⊓ Q).IsStableUnderBaseChange