mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.LittleWedderburn
_private.Mathlib.RingTheory.LittleWedderburn.0.LittleWedderburn.InductionHyp : (D : Type u_1) → [DivisionRing D] → Prop
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.coeff_toMultiplicativeAlgEquiv_symm_apply : ∀ (R : Type u_1) (A : Type u_4) (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M] (x : MonoidAlgebra A (Multiplicative M)),
  ((AddMonoidAlgebra.toMultiplicativeAlgEquiv R A M).symm x).coeff = Finsupp.mapDomain (⇑Multiplicative.toAdd) x.coeff
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta.eq_1 : ∀ (x : ℝ), Chebyshev.theta x = ∑ p ∈ Finset.Ioc 0 ⌊x⌋₊ with Nat.Prime p, Real.log ↑p
-- Init.Data.List.Count
/-- This lemma is only relevant for `grind`.  -/
Std.Internal.List.countP_eq_zero_of_forall : ∀ {α : Type u_1} {p : α → Bool} {xs : List α}, (∀ x ∈ xs, ¬p x = true) → List.countP p xs = 0
-- Mathlib.RingTheory.Nilpotent.Defs
IsNilpotent.map_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : MonoidWithZero R] [inst_1 : MonoidWithZero S] {r : R} {F : Type u_3}
  [inst_2 : FunLike F R S] [MonoidWithZeroHomClass F R S] {f : F},
  Function.Injective ⇑f → (IsNilpotent (f r) ↔ IsNilpotent r)
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.opEquiv.match_5.eq_1 : ∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] {x y : (CategoryTheory.WithInitial C)ᵒᵖ}
  (motive : (x ⟶ y) → Sort u_3) (f : Opposite.unop y ⟶ Opposite.unop x)
  (h_1 : (f : Opposite.unop y ⟶ Opposite.unop x) → motive (Opposite.op f)),
  (match Opposite.op f with
    | Opposite.op f => h_1 f) =
    h_1 f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?_snd : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β},
  (Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew? t k v ⋯).2 =
    (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl
-- Mathlib.Data.Finsupp.AList
AList.lookupFinsupp.eq_1 : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (l : AList fun _x => M),
  l.lookupFinsupp =
    { support := (List.filter (fun x => decide (x.snd ≠ 0)) l.entries).keys.toFinset,
      toFun := fun a => (AList.lookup a l).getD 0, mem_support_toFun := ⋯ }
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.inclusion.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (h : H ≤ K),
  Subgroup.inclusion h = MonoidHom.mk' (fun x => ⟨↑x, ⋯⟩) ⋯
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.parseFirstByte_eq_threeMore_of_utf8DecodeChar?_eq_some : ∀ {b : ByteArray} {i : ℕ} {c : Char},
  b.utf8DecodeChar? i = some c →
    c.utf8Size = 4 →
      ∀ (h' : i < b.size), ByteArray.utf8DecodeChar?.parseFirstByte b[i] = ByteArray.utf8DecodeChar?.FirstByte.threeMore
-- Std.Time.Format.Modifier
Std.Time.Modifier.Z.injEq : ∀ (presentation presentation_1 : Std.Time.OffsetZ),
  (Std.Time.Modifier.Z presentation = Std.Time.Modifier.Z presentation_1) = (presentation = presentation_1)
-- Mathlib.Algebra.Group.Basic
add_neg_eq_iff_eq_add : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a + -b = c ↔ a = c + b
-- Lean.Data.LBool
Lean.instBEqLBool.beq : Lean.LBool → Lean.LBool → Bool
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.insertIdx.loop.eq_1 : ∀ {α : Type u} (i : ℕ) (as : Array α) (j : Fin as.size),
  Array.insertIdx.loop✝ i as j =
    if i < ↑j then
      let j' := ⟨↑j - 1, ⋯⟩;
      let as_1 := as.swap ↑j' ↑j ⋯ ⋯;
      Array.insertIdx.loop✝ i as_1 ⟨↑j', ⋯⟩
    else as
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.linearEquiv_symm_apply : ∀ (p : ENNReal) (K : Type u_1) (V : Type u_4) [inst : Semiring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (a : V), (WithLp.linearEquiv p K V).symm a = (WithLp.addEquiv p V).invFun a
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.FindMin.HasSize : {α : Type u_1} → Batteries.BinomialHeap.Imp.FindMin α → ℕ → Prop
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_finite : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G}, s.Nonempty → s.Finite → (↑(AddAction.stabilizer G s)).Finite
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.debug.byAsSorry : Lean.Option Bool
-- Std.Http.Data.Chunk
/-- Quotes an extension value if it contains non-token characters, otherwise returns it as-is.
 -/
Std.Http.Chunk.ExtensionValue.quote : Std.Http.Chunk.ExtensionValue → String
-- Mathlib.Data.Set.Insert
Set.subset_pair_iff_eq : ∀ {α : Type u_1} {s : Set α} {x y : α}, s ⊆ {x, y} ↔ s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y}
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
/-- Given a morphism of cochain complexes `φ`, this is the short complex
given by `(triangle φ).rotate`.  -/
CochainComplex.mappingCone.triangleRotateShortComplex : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K L : CochainComplex C ℤ} → (K ⟶ L) → CategoryTheory.ShortComplex (CochainComplex C ℤ)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.ofList_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v}, Std.DTreeMap.Raw.Const.ofList [] cmp = ∅
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α}, Std.ExtDTreeMap.Const.get? (t.erase k) k = none
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.next' : Lean.ParseImports.State →
  (input : String) → (pos : String.Pos.Raw) → ¬String.Pos.Raw.atEnd input pos = true → Lean.ParseImports.State
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_union_of_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₁ → k ∈ m₁ ∪ m₂
-- Mathlib.Data.Finset.Prod
Finset.diag_insert : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α] (a : α), (insert a s).diag = insert (a, a) s.diag
-- Mathlib.Logic.Nontrivial.Defs
instNontrivialProp : Nontrivial Prop
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m.toList.isEmpty = m.isEmpty
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_le_maxKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false →
    ∀ {k : α} {v : β} {fallback : α}, (cmp (t.maxKeyD fallback) ((t.insert k v).maxKeyD fallback)).isLE = true
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_ge_nat : ∀ {f : ℝ → ℝ} {b : ℝ},
  b ∈ Set.Ioo 0 1 →
    AkraBazziRecurrence.GrowsPolynomially f →
      ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, c * f ↑n ≤ f u
-- Mathlib.Algebra.Field.Defs
/-- However `Rat.cast q` is defined, it must be propositionally equal to `q.num / q.den`.

Do not use this lemma directly. Use `Rat.cast_def` instead.  -/
Field.ratCast_def : ∀ {K : Type u} [self : Field K] (q : ℚ), ↑q = ↑q.num / ↑q.den
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.iSup_filtration : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι) [P.IsProper]
  [OrderBot ι] [SuccOrder ι] [NoMaxOrder ι], ⨆ i, f.filtration i = ⊤
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.coe_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ}
  (z : CochainComplex.HomComplex.Cocycle F G n) (x : R), ↑(x • z) = x • ↑z
-- Lean.Elab.Command
Lean.Elab.Command.liftCoreM : {α : Type} → Lean.CoreM α → Lean.Elab.Command.CommandElabM α
-- Mathlib.LinearAlgebra.Quotient.Defs
/-- Map associating to an element of `M` the corresponding element of `M/p`,
when `p` is a submodule of `M`.  -/
Submodule.Quotient.mk : {R : Type u_1} →
  {M : Type u_2} → [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {p : Submodule R M} → M → M ⧸ p
-- Mathlib.Algebra.Order.Interval.Set.Instances
/-- like `coe_le_one`, but with the inequality in `Icc (0:R) 1`.  -/
Set.Icc.le_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {t : ↑(Set.Icc 0 1)}, t ≤ 1
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushoutShape.subsingleton_hom : ∀ {J : Type w}, Quiver.IsThin (CategoryTheory.Limits.WidePushoutShape J)
-- Mathlib.Algebra.Category.Ring.Small
CommRingCat.essentiallySmall_of_finiteType : ∀ {P Q : CategoryTheory.ObjectProperty CommRingCat} [CategoryTheory.ObjectProperty.EssentiallySmall.{u, u, u + 1} Q],
  (∀ (S : CommRingCat), P S → ∃ R, Q R ∧ ∃ f, (CommRingCat.Hom.hom f).FiniteType) →
    CategoryTheory.ObjectProperty.EssentiallySmall.{u, u, u + 1} P
-- Mathlib.Topology.Algebra.Group.Defs
/-- A typeclass saying that `p : G × G ↦ p.1 - p.2` is a continuous function. This property
automatically holds for topological additive groups but it also holds, e.g., for `ℝ≥0`.  -/
ContinuousSub : (G : Type u_4) → [TopologicalSpace G] → [Sub G] → Prop
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalars.map_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {M M' : ModuleCat S} (g : M ⟶ M')
  (x : ↑((ModuleCat.restrictScalars f).obj M)),
  (CategoryTheory.ConcreteCategory.hom ((ModuleCat.restrictScalars f).map g)) x =
    (CategoryTheory.ConcreteCategory.hom g) x
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.throwScopeNameMismatch : Lean.Name → List Lean.Elab.Command.Scope → ℕ → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Probability.Process.Adapted
MeasureTheory.StronglyAdapted.div' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → TopologicalSpace (β i)] {u v : (i : ι) → Ω → β i}
  [inst_2 : (i : ι) → Div (β i)] [∀ (i : ι), ContinuousDiv (β i)],
  MeasureTheory.StronglyAdapted f u → MeasureTheory.StronglyAdapted f v → MeasureTheory.StronglyAdapted f (u / v)
-- Init.Data.Int.Linear
Int.Internal.Linear.le_of_le_cert.match_1.congr_eq_1 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (p₁ p₂ : Int.Internal.Linear.Poly)
  (h_1 :
    (k : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k_1 : ℤ) → motive (Int.Internal.Linear.Poly.add k v p) (Int.Internal.Linear.Poly.num k_1))
  (h_2 :
    (k k_1 : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k) (Int.Internal.Linear.Poly.add k_1 v p))
  (h_3 : (c₁ c₂ : ℤ) → motive (Int.Internal.Linear.Poly.num c₁) (Int.Internal.Linear.Poly.num c₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂))
  (k : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly) (k_1 : ℤ),
  p₁ = Int.Internal.Linear.Poly.add k v p →
    p₂ = Int.Internal.Linear.Poly.num k_1 →
      (match p₁, p₂ with
        | Int.Internal.Linear.Poly.add k v p, Int.Internal.Linear.Poly.num k_2 => h_1 k v p k_2
        | Int.Internal.Linear.Poly.num k, Int.Internal.Linear.Poly.add k_2 v p => h_2 k k_2 v p
        | Int.Internal.Linear.Poly.num c₁, Int.Internal.Linear.Poly.num c₂ => h_3 c₁ c₂
        | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) ≍
        h_1 k v p k_1
-- Mathlib.Analysis.Normed.Lp.ProdLp
IsometryEquiv.withLpProdUnique_symm_apply : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] [inst_2 : Unique β] (a : α),
  (IsometryEquiv.withLpProdUnique p α β).symm a = WithLp.toLp p (a, default)
-- Mathlib.Data.Set.Piecewise
Set.piecewise_mono : ∀ {α : Type u_1} {δ : α → Type u_8} [inst : (i : α) → Preorder (δ i)] {s : Set α} [inst_1 : (j : α) → Decidable (j ∈ s)]
  {f₁ f₂ g₁ g₂ : (i : α) → δ i}, (∀ i ∈ s, f₁ i ≤ g₁ i) → (∀ i ∉ s, f₂ i ≤ g₂ i) → s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂
-- Mathlib.Order.Ideal
/-- The partial ordering by subset inclusion, inherited from `Set P`.  -/
Order.Ideal.instPartialOrder : {P : Type u_1} → [inst : LE P] → PartialOrder (Order.Ideal P)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.EToCycles.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁)
  (hn₂ : n₁ + 1 = n₂),
  X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂ =
    X.liftCycles f₁ f₂₃ n₁ n₂ hn₂
      (CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁)) ⋯
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.Quotient.mapsTo_smul_orbit : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (g : G) (x : MulAction.orbitRel.Quotient G α),
  Set.MapsTo (fun x => g • x) x.orbit x.orbit
-- Mathlib.Data.Multiset.FinsetOps
Multiset.coe_ndunion : ∀ {α : Type u_1} [inst : DecidableEq α] (l₁ l₂ : List α), (↑l₁).ndunion ↑l₂ = ↑(l₁ ∪ l₂)
-- Std.Http.Data.URI.Basic
/-- Returns the decoded password when present, or `none` if absent or decoding fails UTF-8 validation.
 -/
Std.Http.URI.UserInfo.password? : Std.Http.URI.UserInfo → Option String
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.inv_map_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X Y : C} (e : X ≅ Y) (Z : D),
  CategoryTheory.inv ((F.map e.hom).app Z) = (F.map e.inv).app Z
-- Mathlib.LinearAlgebra.Matrix.Permanent
Matrix.permanent_eq_elem_of_card_eq_one : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R]
  {A : Matrix n n R}, Fintype.card n = 1 → ∀ (k : n), A.permanent = A k k
-- Init.Data.List.Pairwise
List.pairwise_replicate : ∀ {α : Type u_1} {R : α → α → Prop} {n : ℕ} {a : α}, List.Pairwise R (List.replicate n a) ↔ n ≤ 1 ∨ R a a
-- Mathlib.Algebra.Group.Defs
nsmul_add_comm' : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M) (n : ℕ), n • a + a = a + n • a
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α}, (Std.HashMap.Raw.unitOfList l).WF
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.cliqueFinset.eq_1 : ∀ {α : Type u_1} (G : SimpleGraph α) [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : DecidableRel G.Adj] (n : ℕ),
  G.cliqueFinset n = {s | G.IsNClique n s}
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_sUnion : ∀ {α : Type u_1} {G : SimpleGraph α} {S : Set (Set α)},
  DirectedOn (fun x1 x2 => x1 ⊆ x2) S → (G.IsClique (⋃₀ S) ↔ ∀ s ∈ S, G.IsClique s)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1.eq_1 : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m m0 : MeasurableSpace α}
  (hm : m ≤ m0) (μ : MeasureTheory.Measure α) (s : Set α) [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] (x : G),
  MeasureTheory.condExpIndL1 hm μ s x =
    if hs : MeasurableSet s ∧ μ s ≠ ⊤ then MeasureTheory.condExpIndL1Fin hm ⋯ ⋯ x else 0
-- Init.Data.Float.Model.Float
/-- Determine whether `a` is less than `b` according to IEEE rules.

This is not a total ordering.
 -/
Float.Model.lt : Float.Model → Float.Model → Bool
-- Mathlib.Data.Sign.Defs
Int.sign_eq_sign : ∀ (n : ℤ), n.sign = ↑(SignType.sign n)
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.rejected.inj : ∀ {s : String.Slice} {startPos endPos startPos_1 endPos_1 : s.Pos},
  String.Slice.Pattern.SearchStep.rejected startPos endPos =
      String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1 →
    startPos = startPos_1 ∧ endPos = endPos_1
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.surjective : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), Function.Surjective ⇑e
-- Init.Prelude
/-- Create syntax node with 3 children  -/
Lean.Syntax.node3 : Lean.SourceInfo → Lean.SyntaxNodeKind → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.toCotangent_eq_zero : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (x : ↥I), I.toCotangent x = 0 ↔ ↑x ∈ I ^ 2
-- Init.Data.BitVec.Lemmas
/-- Divide-and-conquer worker for `BitVec.flattenList`, returning the underlying
natural number value with the head of the list in the most significant bits.

Splitting the list in half means each bit region is shifted `O(log xs.length)`
times rather than once per element, so flattening a list of length `L` costs
`O(n * L * log L)` instead of the `O(n * L²)` of a left fold (which reshifts the
whole growing accumulator at every step). The recursion depth is `O(log L)`, so
this also does not overflow the stack.
 -/
BitVec.flattenList.toNatAux : {n : ℕ} → List (BitVec n) → ℕ
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.updatePap! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetValue pu → Lean.Name → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.LinearAlgebra.Span.Basic
LinearEquiv.coord_apply_smul : ∀ (R : Type u_1) (M : Type u_4) [inst : Ring R] [inst_1 : IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inst_4 : Module.IsTorsionFree R M] (x : M) (h : x ≠ 0) (y : ↥(R ∙ x)), (LinearEquiv.coord R M x h) y • x = ↑y
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.affineCombinationSingleWeights_apply_self : ∀ (k : Type u_1) [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] (i : ι),
  Finset.affineCombinationSingleWeights k i i = 1
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.mutuallySingularSet.eq_1 : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ),
  κ.mutuallySingularSet η = {p | 1 ≤ κ.rnDerivAux (κ + η) p.1 p.2}
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.eventuallyConst_vadd_set_ae : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) {s : Set α},
  Filter.EventuallyConst (c +ᵥ s) (MeasureTheory.ae μ) ↔ Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.tensorObj_hom_ext_iff : ∀ {x y z : AugmentedSimplexCategory} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj x y ⟶ z},
  f = g ↔
    CategoryTheory.CategoryStruct.comp (x.inl y) f = CategoryTheory.CategoryStruct.comp (x.inl y) g ∧
      CategoryTheory.CategoryStruct.comp (x.inr y) f = CategoryTheory.CategoryStruct.comp (x.inr y) g
-- Mathlib.NumberTheory.MulChar.Basic
/-- If the domain is a ring `R`, then `χ (ringChar R) = 0`.  -/
MulChar.map_ringChar : ∀ {R' : Type u_2} [inst : CommMonoidWithZero R'] {R : Type u_3} [inst_1 : CommSemiring R] [Nontrivial R]
  (χ : MulChar R R'), χ ↑(ringChar R) = 0
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.sInter : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {S : Set (Set X)},
  (∀ s ∈ S, Convexity.IsConvexSet R s) → Convexity.IsConvexSet R (⋂₀ S)
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.instReprHeap.repr : {α : Type u_1} → [Repr α] → Batteries.PairingHeapImp.Heap α → ℕ → Std.Format
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_12 : HSub Std.Time.Second.Offset Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset
-- Lean.SubExpr
/-- monad-fold over the position starting at the leaf and finishing at the root.  -/
Lean.SubExpr.Pos.foldrM : {α : Type} → {M : Type → Type u_1} → [Monad M] → (ℕ → α → M α) → Lean.SubExpr.Pos → α → M α
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.contract_mul_expand : ∀ {R : Type u} [inst : CommSemiring R] {p : ℕ},
  p ≠ 0 → ∀ (f g : Polynomial R), Polynomial.contract p (f * (Polynomial.expand R p) g) = Polynomial.contract p f * g
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_sigma_congrRight : ∀ {ι : Type u} {f g : ι → Type v},
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g i)) → Cardinal.mk ((i : ι) × f i) = Cardinal.mk ((i : ι) × g i)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k} {fallback : α},
  (t.modify k f).maxKeyD fallback = t.maxKeyD fallback
-- Init.Data.SInt.Lemmas
Int32.mod_one : ∀ {a : Int32}, a % 1 = 0
-- Mathlib.Algebra.Polynomial.Module.AEval
/-- Suppose `a` is an element of an `R`-algebra `A` and `M` is an `A`-module.
Loosely speaking, `Module.AEval R M a` is the `R[X]`-module with elements `m : M`,
where the action of a polynomial $f$ is given by $f • m = f(a) • m$.

More precisely, `Module.AEval R M a` has elements `Module.AEval.of R M a m` for `m : M`,
and the action of `f` is `f • (of R M a m) = of R M a ((aeval a f) • m)`.
 -/
Module.AEval : (R : Type u_1) →
  (M : Type u_2) →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module A M] → [inst_5 : Module R M] → [IsScalarTower R A M] → A → Type u_2
-- Mathlib.CategoryTheory.Yoneda
/-- The obvious bijection `F.RepresentableBy Y ≃ (yoneda.obj Y ≅ F)`
when `F : Cᵒᵖ ⥤ Type v₁` and `[Category.{v₁} C]`.  -/
CategoryTheory.Functor.representableByEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} → {Y : C} → F.RepresentableBy Y ≃ (CategoryTheory.yoneda.obj Y ≅ F)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
PreQuasiregular.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : SizeOf R] (val : R), sizeOf { val := val } = 1 + sizeOf val
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- A cocone is a colimit cocone if its extension by an isomorphism is.  -/
CategoryTheory.Limits.IsColimit.ofExtendIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {s : CategoryTheory.Limits.Cocone F} →
            {X : C} →
              (i : s.pt ⟶ X) →
                [CategoryTheory.IsIso i] →
                  CategoryTheory.Limits.IsColimit (s.extend i) → CategoryTheory.Limits.IsColimit s
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
instCompleteLinearOrderWithBot : {α : Type u_1} → [CompleteLinearOrder α] → CompleteLinearOrder (WithBot α)
-- Mathlib.Order.Atoms
le_iff_atom_le_imp : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] [IsAtomistic α] {a b : α},
  a ≤ b ↔ ∀ (c : α), IsAtom c → c ≤ a → c ≤ b