mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_erase_eq_iff_not_compare_eq_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, (t.erase k).min he = t.min ⋯ ↔ ¬cmp k (t.min ⋯) = Ordering.eq
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.instIsPrimeVanishingIdealSingletonForallSet : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3} {x : σ → K},
  (MvPolynomial.vanishingIdeal k {x}).IsPrime
-- Mathlib.Topology.Category.Born
Born.instCoeSortType : CoeSort Born (Type u_1)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.contMDiffWithinAt_comp_diffeomorph_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {G : Type u_7} [inst_9 : TopologicalSpace G]
  {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9}
  [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H M] {M' : Type u_10} [inst_12 : TopologicalSpace M']
  [inst_13 : ChartedSpace H' M'] {N : Type u_11} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n m : WithTop ℕ∞} (h : Diffeomorph I J M N n) {f : N → M'} {s : Set M} {x : M},
  m ≤ n → (ContMDiffWithinAt I I' m (f ∘ ⇑h) s x ↔ ContMDiffWithinAt J I' m f (⇑h.symm ⁻¹' s) (h x))
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  [inst_1 : SizeOf C]
  (h : {n : ℕ} → Fin (n + 1) → (X.obj (Opposite.op { len := n }) ⟶ Y.obj (Opposite.op { len := n + 1 })))
  (h_zero_comp_δ_zero : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (h 0) (Y.δ 0) = g.app (Opposite.op { len := n }))
  (h_last_comp_δ_last :
    ∀ (n : ℕ),
      CategoryTheory.CategoryStruct.comp (h (Fin.last n)) (Y.δ (Fin.last (n + 1))) = f.app (Opposite.op { len := n }))
  (h_succ_comp_δ_castSucc_of_lt :
    ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
      i ≤ j.castSucc →
        CategoryTheory.CategoryStruct.comp (h j.succ) (Y.δ i.castSucc) =
          CategoryTheory.CategoryStruct.comp (X.δ i) (h j))
  (h_succ_comp_δ_castSucc_succ :
    ∀ {n : ℕ} (j : Fin (n + 1)),
      CategoryTheory.CategoryStruct.comp (h j.succ) (Y.δ j.castSucc.succ) =
        CategoryTheory.CategoryStruct.comp (h j.castSucc) (Y.δ j.castSucc.succ))
  (h_castSucc_comp_δ_succ_of_lt :
    ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
      j.castSucc < i →
        CategoryTheory.CategoryStruct.comp (h j.castSucc) (Y.δ i.succ) =
          CategoryTheory.CategoryStruct.comp (X.δ i) (h j))
  (h_comp_σ_castSucc_of_le :
    ∀ {n : ℕ} (i j : Fin (n + 1)),
      i ≤ j →
        CategoryTheory.CategoryStruct.comp (h j) (Y.σ i.castSucc) =
          CategoryTheory.CategoryStruct.comp (X.σ i) (h j.succ))
  (h_comp_σ_succ_of_lt :
    ∀ {n : ℕ} (i j : Fin (n + 1)),
      j ≤ i →
        CategoryTheory.CategoryStruct.comp (h j) (Y.σ i.succ) =
          CategoryTheory.CategoryStruct.comp (X.σ i) (h j.castSucc)),
  sizeOf
      { h := h, h_zero_comp_δ_zero := h_zero_comp_δ_zero, h_last_comp_δ_last := h_last_comp_δ_last,
        h_succ_comp_δ_castSucc_of_lt := h_succ_comp_δ_castSucc_of_lt,
        h_succ_comp_δ_castSucc_succ := h_succ_comp_δ_castSucc_succ,
        h_castSucc_comp_δ_succ_of_lt := h_castSucc_comp_δ_succ_of_lt,
        h_comp_σ_castSucc_of_le := h_comp_σ_castSucc_of_le, h_comp_σ_succ_of_lt := h_comp_σ_succ_of_lt } =
    1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_modify : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : β → β},
  m.WF → (m.modify k f).getKey? k' = if (k == k') = true then if k ∈ m then some k else none else m.getKey? k'
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.lt_top_of_sum_ne_top : ∀ {α : Type u_1} {s : Finset α} {f : α → ENNReal}, ∑ x ∈ s, f x ≠ ⊤ → ∀ {a : α}, a ∈ s → f a < ⊤
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.comapMkQOrderEmbedding_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  (p' : Submodule R (M ⧸ p)), p.comapMkQOrderEmbedding p' = Submodule.comap p.mkQ p'
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The seminorm on a `SeminormedRing`, as a `RingSeminorm`.  -/
SeminormedRing.toRingSeminorm : (R : Type u_2) → [inst : SeminormedRing R] → RingSeminorm R
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.collect.pushNewArg : Bool →
  Lean.Elab.Term.CollectPatternVars.Context →
    Lean.Elab.Term.Arg → Lean.Elab.Term.CollectPatternVars.M Lean.Elab.Term.CollectPatternVars.Context
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (I : Type w) (X : I → C)
  (coversTop : J.CoversTop X) (presentation : (i : I) → (M.over (X i)).Presentation) (I_1 : Type w) (X_1 : I_1 → C)
  (coversTop_1 : J.CoversTop X_1) (presentation_1 : (i : I_1) → (M.over (X_1 i)).Presentation),
  ({ I := I, X := X, coversTop := coversTop, presentation := presentation } =
      { I := I_1, X := X_1, coversTop := coversTop_1, presentation := presentation_1 }) =
    (I = I_1 ∧ X ≍ X_1 ∧ presentation ≍ presentation_1)
-- Init.Data.SInt.Bitwise
instCommutativeInt16HAnd : Std.Commutative fun x1 x2 => x1 &&& x2
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.postcompose₂_map_right : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor H D')
  {X Y :
    CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)}
  (φ : X ⟶ Y),
  ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).map φ).right = CategoryTheory.CategoryStruct.id X.right
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentIdentifier.mk.injEq : ∀ (uri uri_1 : Lean.Lsp.DocumentUri), ({ uri := uri } = { uri := uri_1 }) = (uri = uri_1)
-- Mathlib.Algebra.Homology.Augment
/-- Truncating an augmented chain complex is isomorphic (with components the identity)
to the original complex.
 -/
ChainComplex.truncateAugment : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (C : ChainComplex V ℕ) →
        {X : V} →
          (f : C.X 0 ⟶ X) →
            (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) → ChainComplex.truncate.obj (C.augment f w) ≅ C
-- Lean.SubExpr
Lean.SubExpr.instToJsonGoalLocation : Lean.ToJson Lean.SubExpr.GoalLocation
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_same_else' : ∀ (c t e : Bool), (e == bif c then t else e) = (!c || t == e)
-- Mathlib.Order.Disjoint
Complementeds.mk_sup_mk : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {a b : α} (ha : IsComplemented a)
  (hb : IsComplemented b), ⟨a, ha⟩ ⊔ ⟨b, hb⟩ = ⟨a ⊔ b, ⋯⟩
-- Init.Data.Int.DivMod.Bootstrap
Int.mul_ediv_cancel_of_emod_eq_zero : ∀ {a b : ℤ}, a % b = 0 → b * (a / b) = a
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.changeInverse_unitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : C),
  (e.changeInverse iso).unitIso.hom.app X =
    CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (iso.hom.app (e.functor.obj X))
-- Mathlib.CategoryTheory.Localization.Construction
/-- The canonical bijection between objects in a category and its
localization with respect to a `MorphismProperty` `W`  -/
CategoryTheory.Localization.Construction.objEquiv : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] → (W : CategoryTheory.MorphismProperty C) → C ≃ W.Localization
-- Mathlib.Topology.Instances.Rat
Rat.instNoncompactSpace : NoncompactSpace ℚ
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorHom_def' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X₁ Y₁ X₂ Y₂ : C}
  (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ g)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y₂)
-- Init.Data.Nat.Dvd
Nat.emod_pos_of_not_dvd : ∀ {a b : ℕ}, ¬a ∣ b → 0 < b % a
-- Mathlib.Topology.Algebra.Module.Cardinality
/-- A complete nontrivially normed field has cardinality at least continuum.  -/
continuum_le_cardinal_of_nontriviallyNormedField : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜], Cardinal.continuum ≤ Cardinal.mk 𝕜
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addDysonETransform_fst : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.addDysonETransform e x).1 = x.1 ∪ (e +ᵥ x.2)
-- Std.Data.Iterators.Consumers.Monadic.Set
/-- Traverses the given iterator and stores the emitted values in a `ExtTreeSet`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.toExtTreeSet`.
 -/
Std.IterM.Total.toExtTreeSet : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.Iterators.Finite α m] →
          [Std.IteratorLoop α m m] →
            Std.IterM.Total m β →
              (cmp : autoParam (β → β → Ordering) Std.IterM.Total.toExtTreeSet._auto_1) →
                [Std.TransCmp cmp] → m (Std.ExtTreeSet β cmp)
-- Mathlib.Control.Bifunctor
LawfulBifunctor.const : LawfulBifunctor Functor.Const
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintInfo.mk.inj : ∀ {position : String.Pos.Raw} {label : Lean.Elab.InlayHintLabel} {kind? : Option Lean.Elab.InlayHintKind}
  {textEdits : Array Lean.Elab.InlayHintTextEdit} {tooltip? : Option String} {paddingLeft paddingRight : Bool}
  {position_1 : String.Pos.Raw} {label_1 : Lean.Elab.InlayHintLabel} {kind?_1 : Option Lean.Elab.InlayHintKind}
  {textEdits_1 : Array Lean.Elab.InlayHintTextEdit} {tooltip?_1 : Option String} {paddingLeft_1 paddingRight_1 : Bool},
  { position := position, label := label, kind? := kind?, textEdits := textEdits, tooltip? := tooltip?,
        paddingLeft := paddingLeft, paddingRight := paddingRight } =
      { position := position_1, label := label_1, kind? := kind?_1, textEdits := textEdits_1, tooltip? := tooltip?_1,
        paddingLeft := paddingLeft_1, paddingRight := paddingRight_1 } →
    position = position_1 ∧
      label = label_1 ∧
        kind? = kind?_1 ∧
          textEdits = textEdits_1 ∧ tooltip? = tooltip?_1 ∧ paddingLeft = paddingLeft_1 ∧ paddingRight = paddingRight_1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.maxD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {fallback : α},
  t₁.Equiv t₂ → t₁.maxD fallback = t₂.maxD fallback
-- Lean.Parser.Types
/-- Run `p` with a fresh cache, restore outer cache afterwards.
`p` may access the entire syntax stack.
 -/
Lean.Parser.withResetCacheFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.χ₀`.

---

The unique map to the terminal object.  -/
CategoryTheory.Classifier.SubobjectRepresentableBy.χ₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} →
        (h : CategoryTheory.SubobjectRepresentableBy Ω) → (U : C) → U ⟶ CategoryTheory.Subobject.underlying.obj h.Ω₀
-- Mathlib.Data.Nat.Nth
Nat.nth_eq_zero_mono : ∀ {p : ℕ → Prop}, ¬p 0 → ∀ {a b : ℕ}, a ≤ b → Nat.nth p a = 0 → Nat.nth p b = 0
-- Init.Data.UInt.Bitwise
UInt16.ofNat_shiftLeft : ∀ (a b : ℕ), b < 16 → UInt16.ofNat (a <<< b) = UInt16.ofNat a <<< UInt16.ofNat b
-- Mathlib.Order.Comparable
AntisymmRel.compRel_congr_right : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → (CompRel (fun x1 x2 => x1 ≤ x2) a b ↔ CompRel (fun x1 x2 => x1 ≤ x2) a c)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.posRealAction : MulAction { x // 0 < x } UpperHalfPlane
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {Q : QuadraticForm R M} → StarMul ↥(spinGroup Q)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatQuarterNumber : Std.Time.Month.Quarter → String
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- The product of `n` terms of the form `ι R m` is an alternating map.

This is a special case of `MultilinearMap.mkPiAlgebraFin`, and the exterior algebra version of
`TensorAlgebra.tprod`.  -/
ExteriorAlgebra.ιMulti : (R : Type u1) →
  [inst : CommRing R] →
    {M : Type u2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (n : ℕ) → M [⋀^Fin n]→ₗ[R] ExteriorAlgebra R M
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- `PolynomialModule.single` as a linear map.  -/
PolynomialModule.lsingle : (R : Type u_2) →
  {M : Type u_3} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → ℕ → M →ₗ[R] PolynomialModule R M
-- Mathlib.NumberTheory.MulChar.Basic
/-- Define a structure for multiplicative characters.
A multiplicative character from a commutative monoid `R` to a commutative monoid with zero `R'`
is a homomorphism of (multiplicative) monoids that sends non-units to zero.  -/
MulChar : (R : Type u_1) → [CommMonoid R] → (R' : Type u_2) → [CommMonoidWithZero R'] → Type (max u_1 u_2)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coe_add : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Add Y] (f g : LocallyConstant X Y),
  ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_ofFn : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin n → M), (List.ofFn f).prod = ∏ i, f i
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_union_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} (mem : k ∈ t₂),
  (t₁ ∪ t₂).get k ⋯ = t₂.get k mem
-- ProofWidgets.Data.Html
Lean.Parser.Category.proofWidgetsJsxChild : Lean.Parser.Category
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- The region between two measurable functions on a measurable set is measurable;
a version for the region together with the graphs of both functions.  -/
measurableSet_region_between_cc : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f g : α → ℝ} {s : Set α},
  Measurable f → Measurable g → MeasurableSet s → MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Icc (f p.1) (g p.1)}
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instSymmetricCategory : {k : Type u} →
  {G : Type v} → [inst : CommRing k] → [inst_1 : Monoid G] → CategoryTheory.SymmetricCategory (Rep.{u, u, v} k G)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.zipWithTR.go.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      (motive : List α → List β → Array γ → Sort u_4) →
        (x : List α) →
          (x_1 : List β) →
            (x_2 : Array γ) →
              ((a : α) → (as : List α) → (b : β) → (bs : List β) → (acc : Array γ) → motive (a :: as) (b :: bs) acc) →
                ((x : List α) →
                    (x_3 : List β) →
                      (acc : Array γ) →
                        (∀ (a : α) (as : List α) (b : β) (bs : List β), x = a :: as → x_3 = b :: bs → False) →
                          motive x x_3 acc) →
                  motive x x_1 x_2
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderCobaseChange] [Q.IsStableUnderCobaseChange], (P ⊓ Q).IsStableUnderCobaseChange
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.isSome_succMany?_of_lt_size_toArray : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α] {i : ℕ},
  i < r.toArray.size → (Std.PRange.least?.bind (Std.PRange.succMany? i)).isSome = true
-- Mathlib.Tactic.DepRewrite
/-- Which transparency level to use when cleaning up casts to decide if a cast is a refl-cast.  -/
Mathlib.Tactic.DepRewrite.Config.castTransparency : Mathlib.Tactic.DepRewrite.Config → Lean.Meta.TransparencyMode
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.natDegree_sub_lt : ∀ {R : Type u_1} [inst : Ring R] {p q : Polynomial R} {n : ℕ},
  n ≠ 0 → p.IsMonicOfDegree n → q.IsMonicOfDegree n → (p - q).natDegree < n
-- Std.Http.Data.Request
/-- The HTTP method (GET, POST, PUT, DELETE, etc.) for the request

Reference: https://httpwg.org/specs/rfc9112.html#rfc.section.3.1
 -/
Std.Http.Request.Head.method : Std.Http.Request.Head → Std.Http.Method
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.map_cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {basis_hd' : ℝ → ℝ}
  {basis_tl' : Tactic.ComputeAsymptotics.Basis} (f : ℝ → ℝ)
  (g :
    Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl → Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl')
  {exp : ℝ} {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.map f g
      (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl) =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons (f exp) (g coef)
      (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.map f g tl)
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.instSplitEpiCategoryType : CategoryTheory.SplitEpiCategory (Type u)
-- Mathlib.Logic.Equiv.Defs
Equiv.functionSwap_apply : ∀ (α : Sort u_1) (β : Sort u_2) (γ : α → β → Sort u_3), ⇑(Equiv.functionSwap α β γ) = Function.swap
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- `toIcoDiv` is continuous on the set of points that are not congruent to `a` modulo `p`.  -/
continuousOn_toIcoDiv : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜),
  ContinuousOn (toIcoDiv hp a) {x | ¬x ≡ a [PMOD p]}
-- Std.Data.Iterators.Combinators.TakeWhile
/-- Given an iterator `it` and a predicate `P`, `it.takeWhile P` is an iterator that outputs
the values emitted by `it` until one of those values is rejected by `P`.
If some emitted value is rejected by `P`, the value is dropped and the iterator terminates.

**Marble diagram:**

Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:

```text
it               ---a----b---c--d-e--⊥
it.takeWhile P   ---a----b---⊥

it               ---a----⊥
it.takeWhile P   ---a----⊥
```

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is productive

Depending on `P`, it is possible that `it.takeWhile P` is finite (or productive) although `it` is not.
In this case, the `Finite` (or `Productive`) instance needs to be proved manually.

**Performance:**

This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then
it terminates.
 -/
Std.Iter.takeWhile : {α β : Type w} → (P : β → Bool) → Std.Iter β → Std.Iter β
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_nonpos_of_nonneg_of_nonpos : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a b : G₀} [PosMulMono G₀],
  0 ≤ a → b ≤ 0 → a / b ≤ 0
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
/-- The fundamental property of the adjoint.  -/
LinearPMap.adjoint_isFormalAdjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F}
  [inst_5 : CompleteSpace E], Dense ↑T.domain → T.adjoint.IsFormalAdjoint T
-- Init.Data.List.Lemmas
List.flatten_eq_cons_iff : ∀ {α : Type u_1} {xss : List (List α)} {y : α} {ys : List α},
  xss.flatten = y :: ys ↔ ∃ as bs cs, xss = as ++ (y :: bs) :: cs ∧ (∀ l ∈ as, l = []) ∧ ys = bs ++ cs.flatten
-- Mathlib.Data.Finsupp.Basic
Rat.cast_finsupp_sum : ∀ {α : Type u_1} {M : Type u_5} {R : Type u_10} [inst : Zero M] (f : α →₀ M) [inst_1 : DivisionRing R] [CharZero R]
  (g : α → M → ℚ), ↑(f.sum g) = f.sum fun a b => ↑(g a b)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.to_hasBasis' : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
  {s' : ι' → Set α},
  l.HasBasis p s → (∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i) → (∀ (i' : ι'), p' i' → s' i' ∈ l) → l.HasBasis p' s'
-- Std.Http.Data.URI.Basic
/-- Returns the parent path by removing the last segment. If the path is empty, returns the path unchanged.
 -/
Std.Http.URI.Path.parent : Std.Http.URI.Path → Std.Http.URI.Path
-- Init.Grind.Lemmas
Lean.Grind.and_eq_of_eq_true_right : ∀ {a b : Prop}, b = True → (a ∧ b) = a
-- Init.Control.Except
ExceptT.instMonadLiftExcept : {ε : Type u} → {m : Type u → Type v} → [Monad m] → MonadLift (Except ε) (ExceptT ε m)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.mk'.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} (toN toN_1 : X.N) (e_toN : toN = toN_1)
  (notMem : toN.simplex ∉ A.obj (Opposite.op { len := toN.dim })),
  { toN := toN, notMem := notMem } = { toN := toN_1, notMem := ⋯ }
-- Mathlib.Tactic.DeriveTraversable
/-- Get the auxiliary local declaration corresponding to the current declaration. If there are
multiple declarations it will throw.  -/
Mathlib.Deriving.Traversable.getAuxDefOfDeclName : Lean.Elab.TermElabM Lean.FVarId
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.constr_comp : ∀ {M' : Type u_7} [inst : AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] (b : Module.Basis ι R M) [inst_4 : Module R M'] (S : Type u_13)
  [inst_5 : Semiring S] [inst_6 : Module S M'] [inst_7 : SMulCommClass R S M'] (f : M' →ₗ[R] M') (v : ι → M'),
  (b.constr S) (⇑f ∘ v) = f ∘ₗ (b.constr S) v
-- Mathlib.Algebra.FreeMonoid.Basic
/-- Define a multiplicative action of `FreeMonoid α` on `β`.  -/
FreeMonoid.mkMulAction : {α : Type u_1} → {β : Type u_2} → (α → β → β) → MulAction (FreeMonoid α) β
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termY₁ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Prod
MulEquiv.uniqueProd_symm_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Unique N] (a : M),
  MulEquiv.uniqueProd.symm a = (default, a)
-- Lean.Elab.Do.Switch
Lean.Elab.Term.expandTermTry : Lean.Macro