mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.mk_add : ∀ {R : Type u_1} {M : Type u_2} {x y : M} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (p : Submodule R M), Submodule.Quotient.mk (x + y) = Submodule.Quotient.mk x + Submodule.Quotient.mk y
-- Mathlib.RingTheory.Spectrum.Maximal.Defs
MaximalSpectrum.ext : ∀ {R : Type u_1} {inst : CommSemiring R} {x y : MaximalSpectrum R}, x.asIdeal = y.asIdeal → x = y
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.forIn_eq_forIn_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ},
  (forIn t init fun a d => f a.fst d) = forIn t.keysArray init f
-- Mathlib.Algebra.Group.Shrink
Shrink.instSemigroup.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Semigroup α], Shrink.instSemigroup = (equivShrink α).symm.semigroup
-- Mathlib.CategoryTheory.Category.Bipointed
/-- The functor from `Pointed` to `Bipointed` which bipoints the point.  -/
pointedToBipointed : CategoryTheory.Functor Pointed Bipointed
-- Mathlib.Topology.Closure
Filter.le_lift'_closure : ∀ {X : Type u} [inst : TopologicalSpace X] (l : Filter X), l ≤ l.lift' closure
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).size =
        if k ∈ t ∧ (f (Std.DTreeMap.Raw.Const.get? t k)).isNone = true then t.size - 1
        else if k ∉ t ∧ (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true then t.size + 1 else t.size
-- Lean.Meta.Basic
/-- `withTrackingZetaDelta x` executes `x` while tracking zeta-delta reductions performed by `whnf`.
Furthermore, the `zetaDeltaFVarIds` set is temporarily cleared,
and also the cache is temporarily reset so that reductions are accurately tracked.

Any zeta-delta reductions recorded while executing `x` will *not* persist when leaving `withTrackingZetaDelta`.
 -/
Lean.Meta.withTrackingZetaDelta : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Mathlib.Data.Finmap
/-- **Alias** of the reverse direction of `Multiset.nodup_keys`. -/
Multiset.NodupKeys.nodup_keys : ∀ {α : Type u} {β : α → Type v} {m : Multiset ((a : α) × β a)}, m.NodupKeys → m.keys.Nodup
-- Mathlib.Topology.UniformSpace.Basic
/-- A version of `UniformContinuous.inf_dom_left` for binary functions  -/
uniformContinuous_inf_dom_left₂ : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : α → β → γ} {ua1 ua2 : UniformSpace α} {ub1 ub2 : UniformSpace β}
  {uc1 : UniformSpace γ}, (UniformContinuous fun p => f p.1 p.2) → UniformContinuous fun p => f p.1 p.2
-- Mathlib.RingTheory.Localization.Integer
/-- Each element `a : S` has an `M`-multiple which is an integer.

This version multiplies `a` on the right, matching the argument order in `LocalizationMap.surj`.
 -/
IsLocalization.exists_integer_multiple' : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (a : S), ∃ b, IsLocalization.IsInteger R (a * (algebraMap R S) ↑b)
-- Init.Prelude
/-- Like `node`, but also declares that the body can be matched using an antiquotation
with name `name`. For example, `def $id:declId := 1` uses an antiquotation with
name `declId` in the place where a `declId` is expected.  -/
Lean.ParserDescr.nodeWithAntiquot : String → Lean.SyntaxNodeKind → Lean.ParserDescr → Lean.ParserDescr
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- A finite sum of functions antitone on `u` is antitone on `u`.  -/
AntitoneOn.finsetSum : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {s : Finset ι} [AddLeftMono N]
  {γ : Type u_9} [inst_3 : Preorder γ] {u : Set γ} {f : ι → γ → N},
  (∀ i ∈ s, AntitoneOn (f i) u) → AntitoneOn (fun x => ∑ i ∈ s, f i x) u
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
/-- The natural isomorphism `M.exteriorPower 1 ≅ M`.  -/
ModuleCat.exteriorPower.natIso₁ : (R : Type u) → [inst : CommRing R] → ModuleCat.exteriorPower.functor R 1 ≅ CategoryTheory.Functor.id (ModuleCat R)
-- Mathlib.Order.LiminfLimsup
Filter.limsSup_le_limsSup_of_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f g : Filter α},
  f ≤ g →
    autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f) Filter.limsSup_le_limsSup_of_le._auto_1 →
      autoParam (Filter.IsBounded (fun x1 x2 => x1 ≤ x2) g) Filter.limsSup_le_limsSup_of_le._auto_3 →
        f.limsSup ≤ g.limsSup
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Projection
EuclideanGeometry.two_zsmul_oangle_self_orthogonalProjection : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)] (p : P)
  {p' : P} {s : AffineSubspace ℝ P} [inst_5 : s.direction.HasOrthogonalProjection],
  p ∉ s →
    ∀ (h : p' ∈ s),
      p' ≠ ↑((EuclideanGeometry.orthogonalProjection s) p) →
        2 • EuclideanGeometry.oangle p (↑((EuclideanGeometry.orthogonalProjection s) p)) p' = ↑Real.pi
-- Mathlib.RingTheory.Ideal.Operations
Ideal.range_finsuppTotal : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommGroup M] {R : Type u_3} [inst_1 : CommRing R] [inst_2 : Module R M]
  (I : Ideal R) {v : ι → M}, (Ideal.finsuppTotal ι M I v).range = I • Submodule.span R (Set.range v)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.add_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  (E : J.ZeroHypercover S) {T : C} (f : T ⟶ S) (hf : E.presieve₀ ⊔ CategoryTheory.Presieve.singleton f ∈ J.coverings S),
  (E.add f hf).toPreZeroHypercover = E.add f
-- Mathlib.Algebra.Star.Basic
star_mul_star : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] (x y : R), star (x * star y) = y * star x
-- Lean.DocString.Syntax
/-- Metadata for the preceding header.
 -/
Lean.Doc.Syntax.metadata_block : Lean.ParserDescr
-- Init.Data.String.Lemmas.Pattern.Split.Basic
String.Slice.Pattern.Model.split_eq_of_isLongestMatchAt : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {firstRejected start stop : s.Pos}
  {hle : firstRejected ≤ start},
  String.Slice.Pattern.Model.IsLongestMatchAt pat start stop →
    String.Slice.Pattern.Model.split pat firstRejected start hle =
      s.subslice firstRejected start hle :: String.Slice.Pattern.Model.split pat stop stop ⋯
-- Lean.Parser.Term
Lean.Parser.Term.let_fun.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Prelude
/-- `a <<< b` computes `a` shifted to the left by `b` places.
The meaning of this notation is type-dependent.
* On `Nat`, this is equivalent to `a * 2 ^ b`.
* On `UInt8` and other fixed width unsigned types, this is the same but
  truncated to the bit width. 

Conventions for notations in identifiers:

 * The recommended spelling of `<<<` in identifiers is `shiftLeft`. -/
HShiftLeft.hShiftLeft : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HShiftLeft α β γ] → α → β → γ
-- Mathlib.Algebra.Algebra.Unitization
Unitization.fst_add : ∀ {R : Type u_3} {A : Type u_4} [inst : Add R] [inst_1 : Add A] (x₁ x₂ : Unitization R A),
  (x₁ + x₂).toProd.1 = x₁.toProd.1 + x₂.toProd.1
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.scalarRestriction`.

---

When `M` is a `B`-module in `D` and `f : A ⟶ B` is a morphism of internal
monoid objects, `M` inherits an `A`-module structure via
"restriction of scalars", i.e `γ[A, M] = f ⊵ₗ M ≫ γ[B, M]`.  -/
CategoryTheory.Mod_.scalarRestriction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A B : C} →
              [inst_4 : CategoryTheory.MonObj A] →
                [inst_5 : CategoryTheory.MonObj B] →
                  (f : A ⟶ B) →
                    [CategoryTheory.IsMonHom f] → (M : D) → [CategoryTheory.ModObj B M] → CategoryTheory.ModObj A M
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.map_add : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x y : E), f (x + y) = f x + f y
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.left_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  [inst_2 : CategoryTheory.MonoidalCoherence X Y],
  CategoryTheory.MonoidalCoherence.iso =
    CategoryTheory.MonoidalCategoryStruct.leftUnitor X ≪≫ CategoryTheory.MonoidalCoherence.iso
-- Mathlib.Order.Interval.Set.Basic
/-- **Alias** of `Set.Ico_sdiff_left`. -/
Set.Ico_diff_left : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Ico a b \ {a} = Set.Ioo a b
-- Mathlib.Order.RelIso.Basic
/-- An increasing function is injective  -/
injective_of_increasing : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Trichotomous r] [Std.Irrefl s] (f : α → β),
  (∀ {x y : α}, r x y → s (f x) (f y)) → Function.Injective f
-- Mathlib.Algebra.Module.Bimodule
Subbimodule.coe_baseChange : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Module A M] [inst_6 : Module B M]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M]
  [inst_11 : SMulCommClass A B M] (S : Type u_5) [inst_12 : CommSemiring S] [inst_13 : Module S M]
  [inst_14 : Algebra S A] [inst_15 : Algebra S B] [inst_16 : IsScalarTower S A M] [inst_17 : IsScalarTower S B M]
  (p : Submodule (TensorProduct R A B) M), ↑(Subbimodule.baseChange S p) = ↑p
-- Mathlib.RingTheory.WittVector.StructurePolynomial
wittStructureRat_existsUnique : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℚ),
  ∃! φ,
    ∀ (n : ℕ),
      (MvPolynomial.bind₁ φ) (wittPolynomial p ℚ n) =
        (MvPolynomial.bind₁ fun i => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p ℚ n)) Φ
-- Mathlib.Analysis.SpecialFunctions.Arcosh
/-- `arcosh` is the right inverse of `cosh` over $[1, ∞)$.  -/
Real.cosh_arcosh : ∀ {x : ℝ}, 1 ≤ x → Real.cosh (Real.arcosh x) = x
-- Mathlib.Condensed.Discrete.Characterization
LightCondSet.mem_locallyConstant_essImage_of_isColimit_mapCocone : ∀ (X : LightCondSet)
  (h :
    (S : LightProfinite) →
      CategoryTheory.Limits.IsColimit (X.obj.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))),
  LightCondSet.LocallyConstant.functor.essImage X
-- Mathlib.Control.ULiftable
ULiftable.up_down : ∀ {f : Type u₀ → Type u₁} {g : Type (max u₀ v₀) → Type v₁} [inst : ULiftable f g] {α : Type u₀}
  (x : g (ULift.{v₀, u₀} α)), ULiftable.up (ULiftable.down x) = x
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.whiskering_obj_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u_1) [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (H : CategoryTheory.Functor C D) (F : CategoryTheory.Functor SimplexCategoryᵒᵖ C) (X : SimplexCategoryᵒᵖ),
  (((CategoryTheory.SimplicialObject.whiskering C D).obj H).obj F).obj X = H.obj (F.obj X)
-- Lean.Elab.Term.TermElabM
/-- For testing `TermElabM` methods. The #eval command will sign the error.  -/
Lean.Elab.Term.throwErrorIfErrors : Lean.Elab.TermElabM Unit
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.zero_lt_log_iff : ∀ {x : ENNReal}, 0 < x.log ↔ 1 < x
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- The equalizer of two non-unital star `R`-algebra homomorphisms  -/
NonUnitalStarAlgHom.equalizer : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : Module R A] →
              [inst_3 : Star A] →
                [inst_4 : NonUnitalNonAssocSemiring B] →
                  [inst_5 : Module R B] →
                    [inst_6 : Star B] →
                      [inst_7 : FunLike F A B] →
                        [NonUnitalAlgHomClass F R A B] → [StarHomClass F A B] → F → F → NonUnitalStarSubalgebra R A
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.incl_range : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  I.incl.range = LieIdeal.toLieSubalgebra R L I
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessResult.cacheKeyType : Lean.Meta.PreprocessResult✝ → Lean.Expr
-- Lean.Meta.Tactic.SolveByElim
/-- `applyFirst lemmas goal` applies the first of the `lemmas`
which can be successfully applied to `goal`, and fails if none apply.

We use this in `apply_rules` and `apply_assumption` where backtracking is not needed.
 -/
Lean.Meta.SolveByElim.applyFirst : optParam Lean.Meta.ApplyConfig { } →
  optParam Lean.Meta.TransparencyMode Lean.Meta.TransparencyMode.default →
    List Lean.Expr → Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.all_get : ∀ {α : Type u} {p : α → Prop} {s : Stream'.Seq α}, (∀ x ∈ s, p x) → ∀ {n : ℕ} {x : α}, s.get? n = some x → p x
-- Mathlib.NumberTheory.EulerProduct.Basic
tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [T0Space α]
  {f : ℕ → α},
  Multipliable f →
    Function.mulSupport f ⊆ {n | IsPrimePow n} → ∏' (n : ℕ), f n = ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 1))
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.getElem?_zipWithAll.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (a? : Option α) (b? : Option β)
  (h_1 : Unit → motive none none) (h_2 : (a? : Option α) → (b? : Option β) → motive a? b?),
  (a? = none → b? = none → False) →
    (match a?, b? with
      | none, none => h_1 ()
      | a?, b? => h_2 a? b?) =
      h_2 a? b?
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
SSet.stdSimplex.objMk₁_apply : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)), (SSet.stdSimplex.objMk₁ i) j = if j.castSucc < i then 0 else 1
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.faceSingletonComplIso_inv_ι : ∀ {n : ℕ} (i j : Fin (n + 2)) (hij : j ≠ i),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso j).inv (SSet.horn.ι i j hij) =
    SSet.horn.faceι i j hij
-- Mathlib.Analysis.Convex.Between
/-- Lift a `Sbtw` predicate from one ring to another along a scalar tower.  -/
Sbtw.lift : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [ZeroLEOneClass R] {R' : Type u_6} [inst_6 : Ring R']
  [inst_7 : PartialOrder R'] [inst_8 : Module R' V] [inst_9 : Module R' R] [IsScalarTower R' R V] [SMulPosMono R' R]
  {x y z : P}, Sbtw R' x y z → Sbtw R x y z
-- Mathlib.Algebra.Group.Shrink
Shrink.mulEquiv.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Mul α], Shrink.mulEquiv = (equivShrink α).symm.mulEquiv
-- Mathlib.Data.List.Lookmap
List.lookmap_cons : ∀ {α : Type u_1} (f : α → Option α) {a : α} {l : List α},
  List.lookmap f (a :: l) =
    match f a with
    | none => a :: List.lookmap f l
    | some b => b :: l
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.instInfSet : {K : Type u} → [inst : DivisionRing K] → InfSet (Subfield K)
-- Lean.Data.DeclarationRange
Lean.DeclarationLocation.mk.injEq : ∀ (module : Lean.Name) (range : Lean.DeclarationRange) (module_1 : Lean.Name) (range_1 : Lean.DeclarationRange),
  ({ module := module, range := range } = { module := module_1, range := range_1 }) =
    (module = module_1 ∧ range = range_1)
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderConjugate.lt_top_iff_one_lt : ∀ (p q : ENNReal) [p.HolderConjugate q], p < ⊤ ↔ 1 < q
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_vecMulVec : ∀ {K m n : Type u} [inst : CommRing K] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (w : m → K) (v : n → K),
  (Matrix.toLin' (Matrix.vecMulVec w v)).rank ≤ 1
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_le_linearGrowthSup : ∀ {R : Type u_1} [inst : ConditionallyCompleteLattice R] [inst_1 : Div R] [inst_2 : NatCast R] {u : ℕ → R},
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atTop fun n => u n / ↑n)
      LinearGrowth.linearGrowthInf_le_linearGrowthSup._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) Filter.atTop fun n => u n / ↑n)
        LinearGrowth.linearGrowthInf_le_linearGrowthSup._auto_3 →
      LinearGrowth.linearGrowthInf u ≤ LinearGrowth.linearGrowthSup u
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Group.mulLeftReflectLT_of_mulLeftStrictMono : ∀ {N : Type u_2} [inst : Group N] [inst_1 : LT N] [MulLeftStrictMono N], MulLeftReflectLT N
-- Lean.Meta.Basic
/-- Parameter information cache.  -/
Lean.Meta.FunInfo.paramInfo : Lean.Meta.FunInfo → Array Lean.Meta.ParamInfo
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.derivative_bernoulli : ∀ (k : ℕ), Polynomial.derivative (Polynomial.bernoulli k) = ↑k * Polynomial.bernoulli (k - 1)
-- Lean.Util.LeanOptions
Lean.instInhabitedLeanOption.default : Lean.LeanOption
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.mult_pos : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K}, 0 < w.mult
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.interSnd_toHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  (F : CategoryTheory.PreOneHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)]
  [inst_2 :
    ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
      CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
        (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))],
  (E.interSnd F).toHom = E.interSnd F.toPreZeroHypercover
-- Mathlib.Data.Setoid.Partition
IndexedPartition.range_piecewise_subset : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {β : Type u_3} (f : ι → α → β),
  Set.range (hs.piecewise f) ⊆ ⋃ i, Set.range (f i)
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.Integrable.comp_div : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] {g : ℝ → F},
  MeasureTheory.Integrable g MeasureTheory.volume →
    ∀ {R : ℝ}, R ≠ 0 → MeasureTheory.Integrable (fun x => g (x / R)) MeasureTheory.volume
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_insert_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {k : α} {fallback v : β}, Std.DHashMap.Internal.Raw₀.Const.getD (m.insert k v) k fallback = v
-- Init.Data.List.Basic
List.instLT : {α : Type u} → [LT α] → LT (List α)
-- Mathlib.RepresentationTheory.Character
Representation.char_mul_comm : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Field k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g h : G), ρ.character (h * g) = ρ.character (g * h)
-- Mathlib.Algebra.Order.Field.Basic
div_lt_div_of_neg_of_lt : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α},
  c < 0 → b < a → a / c < b / c
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_inter_subset : ∀ {α : Type u_2} [inst : Mul α] {s t₁ t₂ : Set α}, s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.inr'_eval : ∀ (x y : SimplexCategory) (i : Fin (y.len + 1)),
  (SimplexCategory.Hom.toOrderHom (AugmentedSimplexCategory.inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.right_inv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  {x : Y}, x ∈ e.target → ↑e (↑e.symm x) = x
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Return the results from matching the pattern `[.star]` or `[.labelledStar 0]`.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.matchTreeRootStar : {α : Type} →
  Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex →
    Lean.Meta.RefinedDiscrTree.TreeM✝ α (Lean.Meta.RefinedDiscrTree.MatchResult α)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prodComparisonNatIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasBinaryProducts C]
  [inst_3 : CategoryTheory.Limits.HasBinaryProducts D] (A : C)
  [inst_4 : ∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)],
  (CategoryTheory.Limits.prodComparisonNatIso F A).inv =
    (CategoryTheory.asIso { app := fun B => CategoryTheory.Limits.prodComparison F A B, naturality := ⋯ }).inv
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_atTop_atTop_iff_of_monotone : ∀ {α : Type u_3} {β : Type u_4} [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] {f : α → β} [inst_2 : Preorder β],
  Monotone f → (Filter.Tendsto f Filter.atTop Filter.atTop ↔ ∀ (b : β), ∃ a, b ≤ f a)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.Hom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {G : CategoryTheory.Comonad C} →
      {A B : G.Coalgebra} →
        (f : A.A ⟶ B.A) →
          autoParam (CategoryTheory.CategoryStruct.comp A.a (G.map f) = CategoryTheory.CategoryStruct.comp f B.a)
              CategoryTheory.Comonad.Coalgebra.Hom.h._autoParam →
            A.Hom B
-- Init.Data.UInt.Bitwise
USize.toFin_and : ∀ (a b : USize), (a &&& b).toFin = a.toFin &&& b.toFin
-- Lean.Meta.Tactic.Grind.ProveEq
/-- Executes `x` in a context where the number of binders have been increased.  -/
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.withIncOffset : {α : Type} → Lean.Meta.Grind.AbstractM✝ α → Lean.Meta.Grind.AbstractM✝ α
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Array
/-- Simplification procedure for `#[...][n]` for `n` a `Nat` literal.  -/
Array.reduceGetElem : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Polynomial.Derivation
Polynomial.mkDerivationEquiv_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (Polynomial R) A] [inst_4 : IsScalarTower R (Polynomial R) A] (a : A),
  (Polynomial.mkDerivationEquiv R) a = (Polynomial.mkDerivation R) a
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- **Alias** of `aeconst_of_dense_setOfPred_preimage_vadd_eq`. -/
aeconst_of_dense_setOf_preimage_vadd_eq : ∀ {M : Type u_1} [inst : TopologicalSpace M] {X : Type u_2} [inst_1 : TopologicalSpace X] [R1Space X]
  [inst_3 : MeasurableSpace X] [BorelSpace X] [inst_5 : VAdd M X] [ContinuousVAdd M X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd M X μ] {s : Set X},
  MeasureTheory.NullMeasurableSet s μ →
    Dense {g | (fun x => g +ᵥ x) ⁻¹' s = s} → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Init.Data.SInt.Lemmas
Int16.mul_succ : ∀ {a b : Int16}, a * (b + 1) = a * b + a
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.neg_bind : ∀ {α β : Type u} (f : α → FreeAbelianGroup β) (x : FreeAbelianGroup α), -x >>= f = -(x >>= f)
-- Mathlib.Algebra.Group.Int.Even
Int.two_dvd_ne_zero : ∀ {n : ℤ}, ¬2 ∣ n ↔ n % 2 = 1