mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharTwoJNeZeroNF.eq_1 : ∀ {F : Type u_2} [inst : Field F] (W : WeierstrassCurve F) (ha₁ : W.a₁ ≠ 0),
  W.toCharTwoJNeZeroNF ha₁ =
    { u := Units.mk0 W.a₁ ha₁, r := W.a₃ / W.a₁, s := 0, t := (W.a₁ ^ 2 * W.a₄ + W.a₃ ^ 2) / W.a₁ ^ 3 }
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.forIn_eq_forIn_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ}, forIn t init f = forIn t.toList init f
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_mulIndicator : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] (s t : Set α) (f : α → M),
  s.mulIndicator (t.mulIndicator f) = (s ∩ t).mulIndicator f
-- Mathlib.RingTheory.Coalgebra.GroupLike
IsGroupLikeElem.ne_zero : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] {a : A} [Nontrivial R], IsGroupLikeElem R a → a ≠ 0
-- Mathlib.Topology.Instances.ZMod
ZMod.instDiscreteTopology : ∀ {N : ℕ}, DiscreteTopology (ZMod N)
-- Mathlib.ModelTheory.Order
/-- Joins two terms `t₁, t₂` in a formula representing `t₁ ≤ t₂`.  -/
FirstOrder.Language.Term.le : {L : FirstOrder.Language} →
  {α : Type w} → {n : ℕ} → [L.IsOrdered] → L.Term (α ⊕ Fin n) → L.Term (α ⊕ Fin n) → L.BoundedFormula α n
-- Mathlib.RingTheory.Invariant.Basic
MulSemiringAction.smul_coeff_charpoly : ∀ {B : Type u_2} {G : Type u_3} [inst : CommRing B] [inst_1 : Group G] [inst_2 : MulSemiringAction G B]
  [inst_3 : Fintype G] (b : B) (n : ℕ) (g : G),
  g • (MulSemiringAction.charpoly G b).coeff n = (MulSemiringAction.charpoly G b).coeff n
-- Aesop.RuleTac.Basic
/-- A tactic generator is a special sort of rule tactic, intended for use with
generative machine learning methods. It generates zero or more tactics
(represented as strings) that could be applied to the goal, plus a success
probability for each tactic. When Aesop executes a tactic generator, it executes
each of the tactics and, if the tactic succeeds, adds a rule application for it.
The tactic's success probability (which must be between 0 and 1, inclusive)
becomes the success probability of the rule application. A `TacGen` rule
succeeds if at least one of its suggested tactics succeeds.
 -/
Aesop.TacGen : Type
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval : ∀ (R : Type u) [inst : CommSemiring R] {σ : Type u_1} (A : Type u_4) [inst_1 : CommSemiring A] [inst_2 : Algebra R A],
  (AlgHom.restrictScalars R ↑(MvPolynomial.algebraTensorAlgEquiv R A).symm).comp
      (MvPolynomial.mapAlgHom (Algebra.ofId R A)) =
    Algebra.TensorProduct.includeRight
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.stableUnderComposition : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q],
  (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q) → P.IsStableUnderComposition
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.ppCommRing : Lean.Meta.Grind.M✝ Unit
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_le_iff_sle : ∀ (a b : BitVec System.Platform.numBits), ISize.ofBitVec a ≤ ISize.ofBitVec b ↔ a.sle b = true
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.covarianceBilinDual_of_not_memLp' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [inst_1 : NormedSpace ℝ E] [inst_2 : BorelSpace E],
  ¬MeasureTheory.MemLp (fun x => x - ∫ (y : E), y ∂μ) 2 μ →
    ∀ (L₁ L₂ : StrongDual ℝ E), ((ProbabilityTheory.covarianceBilinDual μ) L₁) L₂ = 0
-- Mathlib.Data.Rat.Lemmas
Rat.natCast_div_self : ∀ (n : ℕ), ↑(n / n) = ↑n / ↑n
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.getEntryLT.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.Ordered → (∃ a ∈ x, compare a k = Ordering.lt) → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.lt)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.lt) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.lt) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.leaf, x, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_1 x he
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instInhabitedStdWall.default : Std.Time.TimeZone.StdWall
-- Mathlib.RepresentationTheory.Character
/-- The character of isomorphic representations is the same.  -/
Representation.char_iso : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Field k]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  {ρ : Representation k G V} {σ : Representation k G W} (φ : ρ.Equiv σ), ρ.character = σ.character
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_restoreM_StateT_apply : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α σ : Type u}
  {epost : EPred} {post : α → σ → Pred} (x : m (α × σ)),
  Lean.Order.PartialOrder.rel
    (fun x_1 =>
      Std.Internal.Do.wp x
        (fun x =>
          match x with
          | (a, s) => post a s)
        epost)
    (Std.Internal.Do.wp (MonadControl.restoreM x) post epost)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.instCoeSubtypeGeneralLinearGroupMemSubgroupGLPos : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} →
        [inst_2 : CommRing R] →
          [inst_3 : LinearOrder R] →
            [inst_4 : IsStrictOrderedRing R] → Coe (Matrix.SpecialLinearGroup n R) ↥(Matrix.GLPos n R)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.length_toList_rco : ∀ {a b : ℤ}, (a...b).toList.length = (b - a).toNat
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.instLawfulBackwardPatternForallCharBool : ∀ {p : Char → Bool}, String.Slice.Pattern.LawfulBackwardPattern p
-- Mathlib.Computability.RegularExpressions
RegularExpression.deriv.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α), RegularExpression.zero.deriv x = 0
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Given an `R`-algebra `A`, `mkPiAlgebraFin` is the multilinear map on `A^n` associating
to `m` the product of all the `m i`.

See also `MultilinearMap.mkPiAlgebra` for a version that assumes `[CommSemiring A]` but works
for `A^ι` with any finite type `ι`.  -/
MultilinearMap.mkPiAlgebraFin : (R : Type uR) →
  (n : ℕ) →
    [inst : CommSemiring R] →
      (A : Type u_1) → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → MultilinearMap R (fun x => A) A
-- Lean.Meta.Basic
Lean.Meta.mkExprConfigCacheKey : Lean.Expr → Lean.MetaM Lean.Meta.ExprConfigCacheKey
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instMulOneClassQuotient : {R : Type u_1} → [inst : Add R] → [inst_1 : MulOneClass R] → (c : RingCon R) → MulOneClass c.Quotient
-- Std.Data.DHashMap.Internal.AssocList.Basic
Std.DHashMap.Internal.AssocList.brecOn.go : {α : Type u} →
  {β : α → Type v} →
    {motive : Std.DHashMap.Internal.AssocList α β → Sort u_1} →
      (t : Std.DHashMap.Internal.AssocList α β) →
        ((t : Std.DHashMap.Internal.AssocList α β) → Std.DHashMap.Internal.AssocList.below t → motive t) →
          motive t ×' Std.DHashMap.Internal.AssocList.below t
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- The power of a point with respect to a sphere equals the square of its tangent length.  -/
EuclideanGeometry.Sphere.IsTangentAt.power_eq_dist_sq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {t p : P},
  s.IsTangentAt t line[ℝ, p, t] → s.power p = dist p t ^ 2
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.instCoeAdjoinAuxSingletonSet : ∀ {α : Type u_1} (x : α), Algebra.CoeAdjoinAux x {x}
-- Init.Data.Format.Basic
/-- Creates a format `l ++ f ++ r` with a flattening group, nesting the contents by the length of `l`.

The group's `FlattenBehavior` is `fill`; for `allOrNone` use `Std.Format.bracket`.
 -/
Std.Format.bracketFill : String → Std.Format → String → Std.Format
-- Mathlib.Topology.Category.Profinite.Extend
/-- Given a functor `G` from `Profiniteᵒᵖ` and `S : Profinite`, we obtain a cocone on
`(CostructuredArrow.proj toProfinite.op ⟨S⟩ ⋙ toProfinite.op ⋙ G)` with cocone point `G.obj ⟨S⟩`.

Whiskering this cocone with `Profinite.Extend.functorOp c` gives `G.mapCocone c.op` as we check in
the example below.
 -/
Profinite.Extend.cocone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (G : CategoryTheory.Functor Profiniteᵒᵖ C) →
      (S : Profinite) →
        CategoryTheory.Limits.Cocone
          ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op (Opposite.op S)).comp
            (FintypeCat.toProfinite.op.comp G))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {km : α}, t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Prototile.mk.inj : ∀ {G : Type u_1} {X : Type u_2} {inst : Group G} {inst_1 : MulAction G X} {carrier : Set X}
  {symmetries : Subgroup ↥(MulAction.stabilizer G carrier)} {carrier_1 : Set X}
  {symmetries_1 : Subgroup ↥(MulAction.stabilizer G carrier_1)},
  { carrier := carrier, symmetries := symmetries } = { carrier := carrier_1, symmetries := symmetries_1 } →
    carrier = carrier_1 ∧ symmetries ≍ symmetries_1
-- Init.Data.Order.Ord
Std.LawfulEqCmp.compare_eq_iff_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] {a b : α}, cmp a b = Ordering.eq ↔ a = b
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.instMaxNilpotentSubmoduleIsNilpotent : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M] [IsNoetherian R M],
  LieModule.IsNilpotent L ↥(LieModule.maxNilpotentSubmodule R L M)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ_even : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (m : ℤ),
  W.preΨ (2 * m) = W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.match_1.eq_1 : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  {n : Type u_1 → Type u_3} (γ : Type u_1) (Pl : α → γ → ForInStep γ → Prop)
  (motive :
    (it : Std.IterM Id α) → ((b : α) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) → Sort u_2)
  (next upperBound : α)
  (f :
    (b : α) →
      { internalState := { next := some next, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
        (c : γ) → n (Subtype (Pl b c)))
  (h_1 :
    (next upperBound : α) →
      (f :
          (b : α) →
            { internalState := { next := some next, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
              (c : γ) → n (Subtype (Pl b c))) →
        motive { internalState := { next := some next, upperBound := upperBound } } f)
  (h_2 :
    (upperBound : α) →
      (f :
          (b : α) →
            { internalState := { next := none, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
              (c : γ) → n (Subtype (Pl b c))) →
        motive { internalState := { next := none, upperBound := upperBound } } f),
  (match { internalState := { next := some next, upperBound := upperBound } }, f with
    | { internalState := { next := some next, upperBound := upperBound } }, f => h_1 next upperBound f
    | { internalState := { next := none, upperBound := upperBound } }, f => h_2 upperBound f) =
    h_1 next upperBound f
-- Mathlib.RepresentationTheory.Homological.Resolution
classifyingSpaceUniversalCover_map : ∀ (G : Type u) [inst : Monoid G] {X Y : SimplexCategoryᵒᵖ} (f : X ⟶ Y),
  (classifyingSpaceUniversalCover G).map f =
    { hom := TypeCat.ofHom fun x => x ∘ ⇑(SimplexCategory.Hom.toOrderHom f.unop), comm := ⋯ }
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.mk_symm : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : ∀ (x : B), Nonempty (E x)] (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) {b : B},
  b ∈ e.baseSet → ∀ (y : F), ⟨b, e.symm b y⟩ = ↑e.symm (b, y)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_alter_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : Inhabited α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.getKey! k = if (f (t.get? k)).isSome = true then k else default
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.map_map : ∀ {V : Type u_1} {W : Type u_2} {X : Type u_3} (G : SimpleGraph V) (f : V → W) (g : W → X),
  SimpleGraph.map g (SimpleGraph.map f G) = SimpleGraph.map (g ∘ f) G
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.complex_exactAt_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) (n : ℕ),
  HomologicalComplex.ExactAt P.complex (n + 1)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- In conditionally complete orders with a bottom element, the nonempty condition can be omitted
from `ciSup_le_iff`.  -/
ciSup_le_iff' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α},
  BddAbove (Set.range f) → ∀ {a : α}, ⨆ i, f i ≤ a ↔ ∀ (i : ι), f i ≤ a
-- Mathlib.Data.List.Permutation
List.count_permutations'Aux_self : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α),
  List.count (x :: l) (List.permutations'Aux x l) = (List.takeWhile (fun x_1 => decide (x = x_1)) l).length + 1
-- Mathlib.Data.Nat.Cast.Order.Ring
/-- Specialisation of `Nat.ofNat_pos'`, which seems to be easier for Lean to use.  -/
Nat.ofNat_pos : ∀ {α : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [Nontrivial α] {n : ℕ}
  [inst_4 : n.AtLeastTwo], 0 < OfNat.ofNat n
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn : {n : ℕ} →
  Array Std.Tactic.BVDecide.LRAT.Internal.Assignment →
    Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Array Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
/-- The first leg of a cospan to define `sectionsObj` as a pullback in `C`.  -/
CategoryTheory.curryRightUnitorHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (I : C) → [inst_2 : CategoryTheory.Closed I] → CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ I ⟹ I
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isMatch_sliceTo_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos p : s.Pos}
  {h : pos ≤ p}, String.Slice.Pattern.Model.IsMatch pat (p.sliceTo pos h) ↔ String.Slice.Pattern.Model.IsMatch pat pos
-- Std.Time.Date.Unit.Weekday
/-- Check if it's a weekend.
 -/
Std.Time.Weekday.isWeekend : Std.Time.Weekday → Bool
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Over.instHasTerminalTopOfContainsIdentities : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T)
  [P.ContainsIdentities], CategoryTheory.Limits.HasTerminal (P.Over ⊤ X)
-- Mathlib.RingTheory.Adjoin.Polynomial.Basic
Algebra.adjoin_mem_exists_aeval : ∀ (R : Type u) {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A) {a : A},
  a ∈ R[x] → ∃ p, (Polynomial.aeval x) p = a
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.«grind_filterGen>=_» : Lean.ParserDescr
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_succ_Icc : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.succ (Finset.Icc i j) = Finset.Icc i.succ j.succ
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Icc_div : ∀ {M : Type u_4} {m n : ℕ} [inst : CommGroup M],
  m ≤ n → ∀ (f : ℕ → M), ∏ i ∈ Finset.Icc m n, f (i + 1) / f i = f (n + 1) / f m
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_zero : LinearGrowth.linearGrowthSup 0 = 0
-- Lean.Compiler.InlineAttrs
Lean.Compiler.instBEqInlineAttributeKind.beq : Lean.Compiler.InlineAttributeKind → Lean.Compiler.InlineAttributeKind → Bool
-- Init.Data.Slice.Array.Lemmas
Array.start_mkSlice_rci : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ}, (Std.Rci.Sliceable.mkSlice xs lo...*).start = min lo xs.size
-- Std.Tactic.BVDecide.LRAT.Internal.CNF
Std.Tactic.BVDecide.LRAT.Internal.Clause.entails_of_entails_delete : ∀ {α : Type u_1} {β : Type u_2} [DecidableEq α] [inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] {p : α → Bool}
  {c : β} {l : Std.Sat.Literal α},
  Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p (Std.Tactic.BVDecide.LRAT.Internal.Clause.delete c l) →
    Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofBddAugment_rankFinite : ∀ {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E),
  (IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).matroid.RankFinite
-- Aesop.Percent
Aesop.instInhabitedPercent : Inhabited Aesop.Percent
-- Mathlib.Order.Filter.SmallSets
Filter.smallSets_comap : ∀ {α : Type u_1} {β : Type u_2} (l : Filter β) (f : α → β),
  (Filter.comap f l).smallSets = l.lift' (Set.powerset ∘ Set.preimage f)
-- Init.System.IO
/-- Flushes the stream's output buffers.
 -/
IO.FS.Stream.flush : IO.FS.Stream → IO Unit
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∩ t₂).getKey? k = none
-- Mathlib.Data.Bool.Basic
Bool.decide_congr : ∀ {p q : Prop} [inst : Decidable p] [inst_1 : Decidable q], (p ↔ q) → decide p = decide q
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsImmersion f]
  [AlgebraicGeometry.IsImmersion g], AlgebraicGeometry.IsImmersion (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.ofList_toList : ∀ {α : Type u_1} (xs : FreeMonoid α), FreeMonoid.ofList (FreeMonoid.toList xs) = xs
-- Mathlib.Data.Set.Image
EquivLike.range_comp : ∀ {ι : Sort u_1} {ι' : Sort u_2} {E : Type u_3} [inst : EquivLike E ι ι'] {α : Type u_4} (f : ι' → α) (e : E),
  Set.range (f ∘ ⇑e) = Set.range f
-- Mathlib.Topology.Constructions
Pi.indiscreteTopology : ∀ {ι : Type u_5} {Y : ι → Type v} [inst : (i : ι) → TopologicalSpace (Y i)] [h : ∀ (i : ι), IndiscreteTopology (Y i)],
  IndiscreteTopology ((i : ι) → Y i)
-- Mathlib.FieldTheory.SeparableClosure
/-- If `K / E / F` is a field extension tower, such that `K / E` has no non-trivial separable
subextensions (when `K / E` is algebraic, this means that it is purely inseparable),
then the image of `separableClosure F E` in `K` is equal to `separableClosure F K`.  -/
separableClosure.map_eq_of_separableClosure_eq_bot : ∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
  separableClosure E K = ⊥ →
    IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E) = separableClosure F K
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.coe_toCoalgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B), ⇑↑e = ⇑e
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- **Alias** of the forward direction of `hasFDerivWithinAt_iff_isLittleOTVS`. -/
HasFDerivWithinAt.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} {s : Set E},
  HasFDerivWithinAt f f' s x → (fun x' => f x' - f x - f' (x' - x)) =o[𝕜; nhdsWithin x s] fun x' => x' - x
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.next_π₁ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂)
  (c₁₂ : ComplexShape I₁₂) [inst : TotalComplexShape c₁ c₂ c₁₂] {i₁ i₁' : I₁},
  c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)) = c₁.π c₂ c₁₂ (i₁', i₂)
-- Mathlib.MeasureTheory.OuterMeasure.Basic
/-- If `s : ℕ → Set α` is a monotone sequence of sets such that `∑' k, m (s (k + 1) \ s k) ≠ ∞`,
then `m (⋃ n, s n) = ⨆ n, m (s n)`.  -/
MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top : ∀ {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α},
  (∀ (n : ℕ), s n ⊆ s (n + 1)) → ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤ → m (⋃ n, s n) = ⨆ n, m (s n)
-- Lean.Compiler.IR.Basic
Lean.IR.IndexRenaming : Type
-- Init.Data.Array.Find
Array.findIdx?_push : ∀ {α : Type u_1} {xs : Array α} {a : α} {p : α → Bool},
  Array.findIdx? p (xs.push a) = (Array.findIdx? p xs).or (if p a = true then some xs.size else none)
-- Mathlib.Algebra.GroupWithZero.Associated
associated_iff_eq : ∀ {M : Type u_1} [inst : Monoid M] [Subsingleton Mˣ] {x y : M}, Associated x y ↔ x = y
-- Std.Time.DateTime
/-- Subtract `Millisecond.Offset` from a `DateTime`.
 -/
Std.Time.DateTime.subMilliseconds : Std.Time.DateTime → Std.Time.Millisecond.Offset → Std.Time.DateTime
-- Mathlib.CategoryTheory.Galois.EssSurj
/-- If `X` is a finite discrete `G`-set, it can be written as the finite disjoint union
of quotients of the form `G ⧸ Uᵢ` for open subgroups `(Uᵢ)`. Note that this
is simply the decomposition into orbits.  -/
CategoryTheory.PreGaloisCategory.has_decomp_quotients : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : CompactSpace G] (X : Action FintypeCat G) [inst_4 : TopologicalSpace X.V.obj] [DiscreteTopology X.V.obj]
  [ContinuousSMul G X.V.obj],
  ∃ ι, ∃ (x : Finite ι), ∃ f, Nonempty ((∐ fun i => Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ X)
-- Std.Time.Format.Modifier
Std.Time.instInhabitedOffsetX : Inhabited Std.Time.OffsetX