mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_lt_div_iff_of_pos_right : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  0 < c → (a / c < b / c ↔ a < b)
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (a b n : ℤ) (h : a + b = n) (a' : ℤ) (ha' : a' = a + x) (n' : ℤ) (hn' : n' = n + x) {Z : C}
  (h_1 :
    ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).obj (K.total (ComplexShape.up ℤ))).X n ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).ιTotal (ComplexShape.up ℤ) a b n h)
      (CategoryTheory.CategoryStruct.comp ((K.totalShift₁Iso x).hom.f n) h_1) =
    CategoryTheory.CategoryStruct.comp (K.shiftFunctor₁XXIso a x a' ha' b).hom
      (CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a' b n' ⋯)
        (CategoryTheory.CategoryStruct.comp
          (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) x n n' hn').inv h_1))
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.parser.go : Std.Time.FormatConfig →
  Std.Time.Awareness →
    Std.Time.GenericFormat.DateBuilder✝ → Std.Time.FormatString → Std.Internal.Parsec.String.Parser Std.Time.DateTime
-- Mathlib.RingTheory.Valuation.LocalSubring
/-- [Stacks Tag 052K](https://stacks.math.columbia.edu/tag/052K) -/
ValuationSubring.isMax_toLocalSubring : ∀ {K : Type u_3} [inst : Field K] (R : ValuationSubring K), IsMax R.toLocalSubring
-- Mathlib.Data.Setoid.Partition
/-- Defining `≤` on partitions as the `≤` defined on their induced equivalence relations.  -/
Setoid.Partition.le : {α : Type u_1} → LE (Setoid.Partitions α)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mem_top : ∀ {M : Type u_1} [inst : MulOneClass M] (x : M), x ∈ ⊤
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k₁ k₂ : α}
  (h' : cmp k₁ k₂ = Ordering.eq) (h₁ : k₁ ∈ t), t.getKey k₁ h₁ = t.getKey k₂ ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α},
  t.WF → (k ∈ Std.DTreeMap.Raw.filter f t ↔ Option.any (f k) (t.get? k) = true)
-- Lean.Meta.Tactic.TryThis
/-- Add an `exact e` or `refine e` suggestion.

The parameters are:
* `ref`: the span of the widget diagnostic
* `e`: the replacement expression
* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
  If not provided it defaults to `ref`.
* `addSubgoalsMsg`: if true (default false), any remaining subgoals will be shown after
  `Remaining subgoals:`
* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
  suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
* `checkState?`: if passed, the tactic state in which the generated tactic will be validated,
  inserting `expose_names` if necessary.
* `tacticErrorAsInfo`: if true (default false), if a generated tactic is invalid (e.g., due to a
   pretty-printing issue), the resulting error message will be logged as an info message instead of
   being thrown as an error. Has no effect if `checkState?` is `none`.
 -/
Lean.Meta.Tactic.TryThis.addExactSuggestion : Lean.Syntax →
  Lean.Expr →
    optParam (Option Lean.Syntax) none →
      optParam Bool false →
        optParam (Option String) none →
          optParam (Option Lean.Elab.Tactic.SavedState) none → optParam Bool false → Lean.Elab.Tactic.TacticM Unit
-- Aesop.Script.SpecificTactics
Aesop.tryExactFVarS : Lean.MVarId → Lean.FVarId → Lean.Meta.TransparencyMode → Aesop.ScriptM Bool
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_functor_obj_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D),
  (CategoryTheory.WithTerminal.equivComma.functor.obj F).right = F.obj CategoryTheory.WithTerminal.star
-- Mathlib.Algebra.CubicDiscriminant
Cubic.ne_zero_of_a_ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a ≠ 0 → P.toPoly ≠ 0
-- Mathlib.Logic.Equiv.Prod
Equiv.Perm.eq_of_prodExtendRight_ne : ∀ {α₁ : Type u_9} {β₁ : Type u_10} [inst : DecidableEq α₁] {e : Equiv.Perm β₁} {a a' : α₁} {b : β₁},
  (Equiv.Perm.prodExtendRight a e) (a', b) ≠ (a', b) → a' = a
-- Mathlib.FieldTheory.Finite.Basic
/-- The **Fermat-Euler totient theorem**. `ZMod.pow_totient` is an alternative statement
of the same theorem.  -/
Nat.ModEq.pow_totient : ∀ {x n : ℕ}, x.Coprime n → x ^ n.totient ≡ 1 [MOD n]
-- Mathlib.CategoryTheory.Limits.Final
/-- When `F : C ⥤ D` is initial, and `t : Cone G` for some `G : D ⥤ E`,
`t.whisker F` is a limit cone exactly when `t` is.
 -/
CategoryTheory.Functor.Initial.isLimitWhiskerEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.Initial] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {G : CategoryTheory.Functor D E} →
                  (t : CategoryTheory.Limits.Cone G) →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Cone.whisker F t) ≃
                      CategoryTheory.Limits.IsLimit t
-- Lean.Elab.Quotation
/-- compute compatibility of pattern with given head check  -/
Lean.Elab.Term.Quotation.HeadInfo.onMatch : Lean.Elab.Term.Quotation.HeadInfo → Lean.Elab.Term.Quotation.HeadCheck → Lean.Elab.Term.Quotation.MatchResult
-- Mathlib.Algebra.BigOperators.Associated
Associated.prod : ∀ {M : Type u_4} [inst : CommMonoid M] {ι : Type u_5} (s : Finset ι) (f g : ι → M),
  (∀ i ∈ s, Associated (f i) (g i)) → Associated (∏ i ∈ s, f i) (∏ i ∈ s, g i)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nsmul_subset_nsmul_add_of_sq_subset_add : ∀ {α : Type u_2} [inst : AddMonoid α] {s t : Set α} {n : ℕ}, 2 • s ⊆ t + s → n ≠ 0 → n • s ⊆ (n - 1) • t + s
-- Mathlib.Condensed.Discrete.Module
CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete : ∀ (R : Type (u + 1)) [inst : Ring R], (Condensed.discrete (ModuleCat R)).Faithful
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.ofEq : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Lean.Expr
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- Every Fredholm operator admits a `FredholmPackage`.

This is the primary way to get a `FredholmPackage` if you don't need control of the decompositions.
If you do, see `IsFredholm.fredholmPackage`.  -/
ContinuousLinearMap.IsFredholm.nonempty_fredholmPackage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] [CompleteSpace 𝕜] [IsTopologicalAddGroup E] [IsTopologicalAddGroup F]
  [ContinuousSMul 𝕜 F] {u : E →L[𝕜] F}, u.IsFredholm → Nonempty u.FredholmPackage
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnits_mono : ∀ {M : Type u_1} [inst : Monoid M], Monotone Subgroup.ofUnits
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
trivializationAt_model_space_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  (p : TangentBundle I H) (x : H), ↑(trivializationAt E (TangentSpace I) x) p = (p.proj, p.snd)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_pos : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}
  [ZeroLEOneClass G₀], 0 < a → ∀ (n : ℤ), 0 < a ^ n
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toOuterMeasure_caratheodory : ∀ {α : Type u_1} (p : PMF α), p.toOuterMeasure.caratheodory = ⊤
-- Lean.DocString.Extension
Lean.VersoDocString.mk.injEq : ∀ (text : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))
  (subsections : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty))
  (text_1 : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))
  (subsections_1 : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)),
  ({ text := text, subsections := subsections } = { text := text_1, subsections := subsections_1 }) =
    (text = text_1 ∧ subsections = subsections_1)
-- Mathlib.RingTheory.AdjoinRoot
PowerBasis.quotientEquivQuotientMinpolyMap_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (pb : PowerBasis R S)
  (I : Ideal R) (a : S ⧸ Ideal.map (algebraMap R S) I),
  (pb.quotientEquivQuotientMinpolyMap I) a =
    (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I (minpoly R pb.gen))
      ((Ideal.quotientMap (Ideal.map (AdjoinRoot.of (minpoly R pb.gen)) I)
          ↑{ toEquiv := ↑(AdjoinRoot.equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm, map_mul' := ⋯, map_add' := ⋯ } ⋯)
        a)
-- Mathlib.Order.Preorder.Chain
/-- By definition, a flag is a maximal chain  -/
Flag.max_chain' : ∀ {α : Type u_4} [inst : LE α] (self : Flag α) ⦃s : Set α⦄,
  IsChain (fun x1 x2 => x1 ≤ x2) s → self.carrier ⊆ s → self.carrier = s
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
EReal.expOrderIso_symm : EReal.expOrderIso.symm = ENNReal.logOrderIso
-- Mathlib.Algebra.Lie.OfAssociative
/-- A subalgebra of an associative algebra is a Lie subalgebra of the associated Lie algebra.  -/
lieSubalgebraOfSubalgebra : (R : Type u) →
  [inst : CommRing R] → (A : Type v) → [inst_1 : Ring A] → [inst_2 : Algebra R A] → Subalgebra R A → LieSubalgebra R A
-- Init.Data.Vector.Algebra
Vector.instAdd : {α : Type u_1} → {n : ℕ} → [Add α] → Add (Vector α n)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_eq_cfcL : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} {f : R → R}
  (ha : p a) (hf : ContinuousOn f (spectrum R a)),
  cfc f a = (cfcL ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }
-- Lean.Meta.Sym.ExprPtr
/-- Key for the `ENodeMap`, `ParentMap`, and other maps and sets.
We use pointer addresses and rely on the fact all internalized expressions
have been hash-consed, i.e., we have applied `shareCommon`.
 -/
Lean.Meta.Sym.ExprPtr : Type
-- Mathlib.Tactic.Sat.FromLRAT
/-- Reification of a single clause formula.  -/
Sat.Fmla.reify_one : ∀ {v : Sat.Valuation} {c : Sat.Clause} {a : Prop}, Sat.Clause.reify v c a → Sat.Fmla.reify v (Sat.Fmla.one c) a
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.MorphismProperty.le_isLocal_isLocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C),
  W ≤ W.isLocal.isLocal
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDual_ker : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M), b.toDual.ker = ⊥
-- Std.Data.ExtHashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtHashMap.getKey? : {α : Type u} →
  {β : Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → α → Option α
-- Mathlib.RingTheory.PowerSeries.Basic
/-- The natural inclusion from polynomials into formal power series.  -/
Polynomial.toPowerSeries : {R : Type u_1} → [inst : Semiring R] → Polynomial R → PowerSeries R
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.liftAddHom_symm_apply : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (F : (α →₀ M) →+ N)
  (x : α), Finsupp.liftAddHom.symm F x = F.comp (Finsupp.singleAddHom x)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
deriv_norm_ofReal_cpow : ∀ (c : ℂ) {t : ℝ}, 0 < t → deriv (fun x => ‖↑x ^ c‖) t = c.re * t ^ (c.re - 1)
-- Init.Data.Array.Lemmas
Array.map_eq_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {b : β}, Array.map f xs = #[b] ↔ ∃ a, xs = #[a] ∧ f a = b
-- Mathlib.Algebra.Group.Equiv.TypeTags
MulEquiv.piMultiplicative_apply : ∀ {ι : Type u_1} (K : ι → Type u_4) [inst : (i : ι) → Add (K i)] (x : Multiplicative ((i : ι) → K i)) (i : ι),
  (MulEquiv.piMultiplicative K) x i = Multiplicative.ofAdd (Multiplicative.toAdd x i)
-- Mathlib.Algebra.Order.Module.Defs
/-- Scalar multiplication on the right by a positive element preserves strict monotonicity.  -/
StrictMono.smul_const : ∀ {α : Type u_1} {β : Type u_2} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β]
  [SMulPosStrictMono α β] {γ : Type u_3} [inst_5 : Preorder γ] {f : γ → α},
  StrictMono f → 0 < b → StrictMono fun x => f x • b
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.instBEqPoly.beq.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Sort u_1) (a : ℤ) (a_1 : Lean.Grind.CommRing.Mon)
  (a_2 : Lean.Grind.CommRing.Poly) (b : ℤ) (b_1 : Lean.Grind.CommRing.Mon) (b_2 : Lean.Grind.CommRing.Poly)
  (h_1 : (a b : ℤ) → motive (Lean.Grind.CommRing.Poly.num a) (Lean.Grind.CommRing.Poly.num b))
  (h_2 :
    (a : ℤ) →
      (a_3 : Lean.Grind.CommRing.Mon) →
        (a_4 : Lean.Grind.CommRing.Poly) →
          (b : ℤ) →
            (b_3 : Lean.Grind.CommRing.Mon) →
              (b_4 : Lean.Grind.CommRing.Poly) →
                motive (Lean.Grind.CommRing.Poly.add a a_3 a_4) (Lean.Grind.CommRing.Poly.add b b_3 b_4))
  (h_3 : (x x_1 : Lean.Grind.CommRing.Poly) → motive x x_1),
  (match Lean.Grind.CommRing.Poly.add a a_1 a_2, Lean.Grind.CommRing.Poly.add b b_1 b_2 with
    | Lean.Grind.CommRing.Poly.num a, Lean.Grind.CommRing.Poly.num b => h_1 a b
    | Lean.Grind.CommRing.Poly.add a a_3 a_4, Lean.Grind.CommRing.Poly.add b b_3 b_4 => h_2 a a_3 a_4 b b_3 b_4
    | x, x_1 => h_3 x x_1) =
    h_2 a a_1 a_2 b b_1 b_2
-- Mathlib.Algebra.Ring.Ext
NonUnitalNonAssocCommRing.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : NonUnitalNonAssocCommRing R⦄,
  HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_nat_mod : ∀ {ι : Type u_1} (s : Finset ι) (n : ℕ) (f : ι → ℕ), (∏ i ∈ s, f i) % n = (∏ i ∈ s, f i % n) % n
-- Mathlib.Topology.MetricSpace.Algebra
TendstoLocallyUniformly.mul₀_of_isBoundedUnder : ∀ {X : Type u_3} {M : Type u_4} {ι : Type u_5} [inst : TopologicalSpace X] [inst_1 : PseudoMetricSpace M]
  [inst_2 : Zero M] [inst_3 : Mul M] [IsBoundedSMul M M] {F G : ι → X → M} {f g : X → M} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    TendstoLocallyUniformly G g l →
      (∀ (x : X), Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x) fun y => dist (f y) 0) →
        (∀ (x : X), Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x) fun y => dist (g y) 0) →
          TendstoLocallyUniformly (F * G) (f * g) l
-- Mathlib.Data.Set.MemPartition
_private.Mathlib.Data.Set.MemPartition.0.memPartition.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.instSimpleSimpleSubobject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} [inst_3 : CategoryTheory.IsArtinianObject X]
  (h : ¬CategoryTheory.Limits.IsZero X), CategoryTheory.Simple (CategoryTheory.simpleSubobject h)
-- Init.Data.List.Nat.Modify
List.eraseIdx_modifyHead_zero : ∀ {α : Type u_1} {f : α → α} {l : List α}, (List.modifyHead f l).eraseIdx 0 = l.eraseIdx 0
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodyLTFactor_ne_zero : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], NumberField.mixedEmbedding.convexBodyLTFactor K ≠ 0
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Finpartition.card_filter_equitabilise_big : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {m a b : ℕ} (P : Finpartition s)
  (h : a * m + b * (m + 1) = s.card), {u ∈ (Finpartition.equitabilise h).parts | u.card = m + 1}.card = b
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- Two matrices agree if their rows agree.  -/
Matrix.ext_row : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {A B : Matrix m n α}, (∀ (i : m), A.row i = B.row i) → A = B
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_toDual : ∀ {α : Type u_1} [inst : Preorder α] {a b : α},
  Set.Icc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Icc b a
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.lineDerivOp_apply_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F] (f : TemperedDistribution E F) (g : SchwartzMap E ℂ) (m : E),
  (LineDeriv.lineDerivOp m f) g = f (-LineDeriv.lineDerivOp m g)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.r_zpow : ∀ {n : ℕ} (i : ZMod n) (k : ℤ), DihedralGroup.r i ^ k = DihedralGroup.r (i * ↑k)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateRow_smul : ∀ {m : Type u_2} {R : Type u_5} {α : Type v} {ι : Type u_6} [inst : SMul R α] (x : R) (v : m → α),
  Matrix.replicateRow ι (x • v) = x • Matrix.replicateRow ι v
-- Aesop.Stats.Basic
Aesop.GoalStats.mk : ℕ → Aesop.GoalKind → ℕ → ℕ → Aesop.ForwardStateStats → Aesop.GoalStats
-- Mathlib.Algebra.Algebra.Pi
Pi.evalAlgHom_apply : ∀ {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] (i : ι) (f : (i : ι) → A i), (Pi.evalAlgHom R A i) f = f i
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.split.eq_def : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} (firstRejected curr : s.Pos)
  (hle : firstRejected ≤ curr),
  String.Slice.Pattern.Model.split pat firstRejected curr hle =
    if h : curr = s.endPos then [s.subslice firstRejected curr hle]
    else
      match hd : String.Slice.Pattern.Model.matchAt? pat curr with
      | some pos =>
        have this := ⋯;
        s.subslice firstRejected curr hle :: String.Slice.Pattern.Model.split pat pos pos ⋯
      | none => String.Slice.Pattern.Model.split pat firstRejected (curr.next h) ⋯
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasPushouts : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  {inst_1 : Fact κ.IsRegular} {inst_2 : OrderBot κ.ord.ToType} [self : I.IsCardinalForSmallObjectArgument κ],
  CategoryTheory.Limits.HasPushouts C
-- Mathlib.Data.Rat.Cast.CharZero
NNRat.cast_add : ∀ {α : Type u_3} [inst : DivisionSemiring α] [CharZero α] (p q : ℚ≥0), ↑(p + q) = ↑p + ↑q
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
AlgebraicGeometry.residueFieldIsoBase.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [inst_1 : IsAlgClosed K]
  (f f_1 : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) (e_f : f = f_1)
  [inst_2 : AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}),
  AlgebraicGeometry.residueFieldIsoBase f x hx = AlgebraicGeometry.residueFieldIsoBase f_1 x hx
-- Lean.Parser.Do
Lean.Parser.Term.elseIf.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Fin.Basic
/-- Use the ordering on `Fin n` for checking recursive definitions.

For example, the following definition is not accepted by the termination checker,
unless we declare the `WellFoundedRelation` instance:
```lean
def factorial {n : ℕ} : Fin n → ℕ
  | ⟨0, _⟩ := 1
  | ⟨i + 1, hi⟩ := (i + 1) * factorial ⟨i, i.lt_succ_self.trans hi⟩
```
 -/
Fin.instWellFoundedRelation_mathlib : {n : ℕ} → WellFoundedRelation (Fin n)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.instRelCWComplex : {X : Type u_1} → [inst : TopologicalSpace X] → (C : Set X) → [Topology.CWComplex C] → Topology.RelCWComplex C ∅
-- Mathlib.CategoryTheory.Sites.LocalSite
CategoryTheory.GrothendieckTopology.IsLocalSite.instFullSheafCoconstantSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_2 : J.IsLocalSite] (A : Type u')
  [inst_3 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  [inst_5 : CategoryTheory.Limits.HasProducts A] [CategoryTheory.HasWeakSheafify J A],
  (CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A).Full
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.ext_indep_iff : ∀ {α : Type u_1} {M₁ M₂ : Matroid α}, M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- `E` acts on `N` by conjugation.  -/
GroupExtension.conjAct : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} → [inst : Group N] → [inst_1 : Group E] → [inst_2 : Group G] → GroupExtension N E G → E →* MulAut N
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.natCast_add_omega0 : ∀ (n : ℕ), ↑n + Ordinal.omega0 = Ordinal.omega0
-- Init.Data.Array.Lex.Lemmas
Array.ltIrrefl : ∀ {α : Type u_1} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2], Std.Irrefl fun x1 x2 => x1 < x2
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.compCreatesLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [ℰ : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor D E) →
                [CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] →
                  [CategoryTheory.CreatesLimitsOfSize.{w, w', v₂, v₃, u₂, u₃} G] →
                    CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₃, u₁, u₃} (F.comp G)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
DifferentiableAt.sin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → DifferentiableAt ℝ (fun x => Real.sin (f x)) x
-- Init.Prelude
/-- `m • a : α` denotes the product of `m : M` and `a : α`. The meaning of this notation is type-dependent,
but it is intended to be used for left actions.  -/
SMul.smul : {M : Type u} → {α : Type v} → [self : SMul M α] → M → α → α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k fallback : α},
      (List.map Prod.fst l).contains k = false → (t.insertMany l).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.one_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), 1 x = x