mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddMemClass.subtype_injective : ∀ {M : Type u_1} {A : Type u_3} [inst : Add M] [inst_1 : SetLike A M] [hA : AddMemClass A M] (S' : A),
  Function.Injective ⇑(AddMemClass.subtype S')
-- Std.Http.Data.Request
/-- Adds a single header to the request being built.
Returns `none` if the header name or value is invalid.
 -/
Std.Http.Request.Builder.header? : Std.Http.Request.Builder → String → String → Option Std.Http.Request.Builder
-- Mathlib.Order.Interval.Set.ProjIcc
Set.OrdConnected.domRestrict : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α},
  s.OrdConnected → {x | t.domRestrict (fun x => x ∈ s) x}.OrdConnected
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.ofClass.eq_1 : ∀ {S : Type u_3} {M : Type u_4} [inst : AddMonoid M] [inst_1 : SetLike S M] [inst_2 : AddSubmonoidClass S M] (s : S),
  AddSubmonoid.ofClass s = { carrier := ↑s, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Data.Multiset.Count
Multiset.count_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (a b : α), Multiset.count a {b} = if a = b then 1 else 0
-- Init.Data.Ord.Vector
Vector.instTransCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] {n : ℕ}, Std.TransCmp (Vector.compareLex cmp)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_of_mem_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {f : α → Bool} {k : α},
  k ∈ Std.ExtTreeSet.filter f t → k ∈ t
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.map_restriction : ∀ {R : Type u} [inst : CommRing R] (p : Polynomial R),
  Polynomial.map (algebraMap (↥(Subring.closure ↑p.coeffs)) R) p.restriction = p
-- Mathlib.Order.Filter.CountablyGenerated
Filter.IsCountableBasis.mk : ∀ {α : Type u_1} {ι : Type u_4} {p : ι → Prop} {s : ι → Set α},
  Filter.IsBasis p s → (Set.ofPred p).Countable → Filter.IsCountableBasis p s
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.sumIDeriv_eq_self_add : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R),
  Polynomial.sumIDeriv p = p + Polynomial.derivative (Polynomial.sumIDeriv p)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_div_pos : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}, 0 < 1 / a ↔ 0 < a
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- Interpret a linear equivalence between modules as an affine equivalence.  -/
LinearEquiv.toAffineEquiv : {k : Type u_1} →
  {V₁ : Type u_6} →
    {V₂ : Type u_7} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] →
          [inst_2 : AddCommGroup V₂] → [inst_3 : Module k V₁] → [inst_4 : Module k V₂] → (V₁ ≃ₗ[k] V₂) → V₁ ≃ᵃ[k] V₂
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MkEval.toMkEvalComp : {m : Type → Type} → [self : Mathlib.Tactic.BicategoryLike.MkEval m] → Mathlib.Tactic.BicategoryLike.MkEvalComp m
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.leftAdjointUniq_hom_app_counit : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : D),
  CategoryTheory.CategoryStruct.comp ((adj1.leftAdjointUniq adj2).hom.app (G.obj x)) (adj2.counit.app x) =
    adj1.counit.app x
-- Mathlib.Data.Erased
Erased.instInhabitedOfNonempty : {α : Sort u_1} → [h : Nonempty α] → Inhabited (Erased α)
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.toLinearMap_comp : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup P] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : LieRingModule L M] [inst_9 : LieRingModule L N]
  [inst_10 : LieRingModule L P] (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N), ↑(f.comp g) = ↑f ∘ₗ ↑g
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncate_lift : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {S : Type u_2} [inst_2 : Semiring S]
  {f : (k : ℕ) → S →+* TruncatedWittVector p k R}
  (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁) (s : S),
  (WittVector.truncate n) ((WittVector.lift f f_compat) s) = (f n) s
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.instIsOverMapHomCommRingCatResidueFieldCongr : ∀ {X : AlgebraicGeometry.Scheme} {x y : ↥X} (h : x = y),
  AlgebraicGeometry.Scheme.Hom.IsOver (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.residueFieldCongr h).hom) X
-- Mathlib.Algebra.Order.Group.Abs
abs_sub_le : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] (a b c : G),
  |a - c| ≤ |a - b| + |b - c|
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.instLT : {M : Type u_1} → [AddGroup M] → [Lattice M] → LT (ArchimedeanOrder M)
-- Mathlib.GroupTheory.GroupAction.FixedPoints
AddAction.fixedBy_subset_fixedBy_zsmul : ∀ (α : Type u_1) {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G) (j : ℤ),
  AddAction.fixedBy α g ⊆ AddAction.fixedBy α (j • g)
-- Mathlib.Data.NNReal.Defs
NNReal.instCommSemiring : CommSemiring NNReal
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_congr : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f g : α → M} {s t : Set α},
  s = t → (∀ x ∈ t, f x = g x) → ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), g i
-- Mathlib.Tactic.Linarith.Frontend
/-- `linarith?` behaves like `linarith` but, on success, it prints a suggestion of
the form `linarith only [...]` listing a minimized set of hypotheses used in the
final proof.  Use `linarith?!` for the higher-reducibility variant and set the
`minimize` flag in the configuration to control whether greedy minimization is
performed.
 -/
Mathlib.Tactic.linarith? : Lean.ParserDescr
-- Mathlib.Algebra.Order.Group.Synonym
isRegular_toLex : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, IsRegular (toLex a) ↔ IsRegular a
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.Lan.CommuteWith.mk : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} {h : c ⟶ x},
  Nonempty ((CategoryTheory.Bicategory.lanLeftExtension f g).whisker h).IsKan →
    CategoryTheory.Bicategory.Lan.CommuteWith f g h
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.withDensity_rnDeriv_le : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α), ν.withDensity (μ.rnDeriv ν) ≤ μ
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_closure_of_mem : ∀ {R : Type u} [inst : NonAssocRing R] {s : Set R} {x : R}, x ∈ s → x ∈ Subring.closure s
-- Mathlib.Algebra.GroupWithZero.Semiconj
SemiconjBy.inv_right₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a x y : G₀}, SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ioc_castAdd : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n),
  ∑ i ∈ Finset.Ioc (Fin.castAdd m a) (Fin.castAdd m b), f i = ∑ i ∈ Finset.Ioc a b, f (Fin.castAdd m i)
-- Mathlib.Data.List.Chain
List.isChain_attachWith : ∀ {α : Type u_1} {l : List α} {p : α → Prop} (h : ∀ x ∈ l, p x) {r : { a // p a } → { a // p a } → Prop},
  List.IsChain r (l.attachWith p h) ↔ List.IsChain (fun a b => ∃ (ha : p a) (hb : p b), r ⟨a, ha⟩ ⟨b, hb⟩) l
-- Lean.Widget.UserWidget
/-- Hash of the JS module to retrieve.  -/
Lean.Widget.GetWidgetSourceParams.hash : Lean.Widget.GetWidgetSourceParams → UInt64
-- Mathlib.Order.WithBot
WithTop.decidableLT.eq_1 : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] (b : WithTop α), WithTop.decidableLT none b = isFalse ⋯
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Continuous.fourierPowSMulRight : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E},
  Continuous f → ∀ (n : ℕ), Continuous fun v => VectorFourier.fourierPowSMulRight L f v n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_obj_iso_hom : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (x : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).obj S).obj
          x).iso.hom =
    S.iso.hom.app x
-- Mathlib.Data.Finset.Image
Subtype.impEmbedding.eq_1 : ∀ {α : Type u_1} (p q : α → Prop) (h : ∀ (x : α), p x → q x),
  Subtype.impEmbedding p q h = { toFun := fun x => ⟨↑x, ⋯⟩, inj' := ⋯ }
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
InformationTheory.leftDeriv_klFun_one : derivWithin InformationTheory.klFun (Set.Iio 1) 1 = 0
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.insertEntryIfNew : {α : Type u} → {β : α → Type v} → [BEq α] → (k : α) → β k → List ((a : α) × β a) → List ((a : α) × β a)
-- Mathlib.Algebra.Group.Action.Pi
Pi.isScalarTower'' : ∀ {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {γ : ι → Type u_6} [inst : (i : ι) → SMul (α i) (β i)]
  [inst_1 : (i : ι) → SMul (β i) (γ i)] [inst_2 : (i : ι) → SMul (α i) (γ i)]
  [∀ (i : ι), IsScalarTower (α i) (β i) (γ i)], IsScalarTower ((i : ι) → α i) ((i : ι) → β i) ((i : ι) → γ i)
-- Std.Async.Select
Std.Async.Selector.mk.injEq : ∀ {α : Type} (tryFn : Std.Async.Async (Option α)) (registerFn : Std.Async.Waiter α → Std.Async.Async Unit)
  (unregisterFn : Std.Async.Async Unit) (tryFn_1 : Std.Async.Async (Option α))
  (registerFn_1 : Std.Async.Waiter α → Std.Async.Async Unit) (unregisterFn_1 : Std.Async.Async Unit),
  ({ tryFn := tryFn, registerFn := registerFn, unregisterFn := unregisterFn } =
      { tryFn := tryFn_1, registerFn := registerFn_1, unregisterFn := unregisterFn_1 }) =
    (tryFn = tryFn_1 ∧ registerFn = registerFn_1 ∧ unregisterFn = unregisterFn_1)
-- Mathlib.Algebra.FiveLemma
/-- The five lemma in terms of groups. For a diagram explaining the variables,
see the module docstring.  -/
MonoidHom.bijective_of_surjective_of_bijective_of_bijective_of_injective : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {M₄ : Type u_4} {M₅ : Type u_5} {N₁ : Type u_6} {N₂ : Type u_7}
  {N₃ : Type u_8} {N₄ : Type u_9} {N₅ : Type u_10} [inst : Group M₁] [inst_1 : Group M₂] [inst_2 : Group M₃]
  [inst_3 : Group M₄] [inst_4 : Group M₅] [inst_5 : Group N₁] [inst_6 : Group N₂] [inst_7 : Group N₃]
  [inst_8 : Group N₄] [inst_9 : Group N₅] (f₁ : M₁ →* M₂) (f₂ : M₂ →* M₃) (f₃ : M₃ →* M₄) (f₄ : M₄ →* M₅)
  (g₁ : N₁ →* N₂) (g₂ : N₂ →* N₃) (g₃ : N₃ →* N₄) (g₄ : N₄ →* N₅) (i₁ : M₁ →* N₁) (i₂ : M₂ →* N₂) (i₃ : M₃ →* N₃)
  (i₄ : M₄ →* N₄) (i₅ : M₅ →* N₅),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      g₃.comp i₃ = i₄.comp f₃ →
        g₄.comp i₄ = i₅.comp f₄ →
          Function.MulExact ⇑f₁ ⇑f₂ →
            Function.MulExact ⇑f₂ ⇑f₃ →
              Function.MulExact ⇑f₃ ⇑f₄ →
                Function.MulExact ⇑g₁ ⇑g₂ →
                  Function.MulExact ⇑g₂ ⇑g₃ →
                    Function.MulExact ⇑g₃ ⇑g₄ →
                      Function.Surjective ⇑i₁ →
                        Function.Bijective ⇑i₂ →
                          Function.Bijective ⇑i₄ → Function.Injective ⇑i₅ → Function.Bijective ⇑i₃
-- Mathlib.Analysis.Calculus.Deriv.ZPow
deriv_zpow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (m : ℤ) (x : 𝕜), deriv (fun x => x ^ m) x = ↑m * x ^ (m - 1)
-- Mathlib.Order.Bounds.Image
bddAbove_range_prod : ∀ {ι : Sort x} {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {F : ι → α × β},
  BddAbove (Set.range F) ↔ BddAbove (Set.range (Prod.fst ∘ F)) ∧ BddAbove (Set.range (Prod.snd ∘ F))
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.iIndepFun.cgf_sum₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X : ι → Ω → ℝ},
  ProbabilityTheory.iIndepFun X μ →
    (∀ (i : ι), AEMeasurable (X i) μ) →
      ∀ {s : Finset ι},
        (∀ i ∈ s, MeasureTheory.Integrable (fun ω => Real.exp (t * X i ω)) μ) →
          ProbabilityTheory.cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, ProbabilityTheory.cgf (X i) μ t
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_alter_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β} {f : Option β → Option β},
  m.WF → (m.alter k f).getD k fallback = (f m[k]?).getD fallback
-- Lean.AuxRecursor
_private.Lean.AuxRecursor.0.Lean.sparseCasesOnExt : Lean.TagDeclarationExtension
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_le_coe_add_dist : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α} {f g : BoundedContinuousFunction α ℝ}, f x ≤ g x + dist f g
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.hom_ext : ∀ {M N : AddMagmaCat} {f g : M ⟶ N}, AddMagmaCat.Hom.hom f = AddMagmaCat.Hom.hom g → f = g
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.CompatibleSMul.units : ∀ {M : Type u_8} {M₂ : Type u_10} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] {R : Type u_14} {S : Type u_15}
  [inst_2 : Monoid R] [inst_3 : MulAction R M] [inst_4 : MulAction R M₂] [inst_5 : Semiring S] [inst_6 : Module S M]
  [inst_7 : Module S M₂] [LinearMap.CompatibleSMul M M₂ R S], LinearMap.CompatibleSMul M M₂ Rˣ S
-- Mathlib.Data.ZMod.Basic
/-- Equivalence between `ℕ` and `ZMod N × ℕ`, sending `n` to `(n mod N, n / N)`.  -/
Nat.residueClassesEquiv : (N : ℕ) → [NeZero N] → ℕ ≃ ZMod N × ℕ
-- Std.Data.HashMap.Lemmas
Std.HashMap.insertManyIfNewUnit_list_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} {k : α},
  m.insertManyIfNewUnit [k] = m.insertIfNew k ()
-- Std.Http.Protocol.H1.Parser
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.parseQuotedString.loop : ℕ → ByteArray → ℕ → Std.Internal.Parsec.ByteArray.Parser ByteArray
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_eq_of_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [inst_2 : LawfulBEq α], (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → ∀ {k : α}, m₁.get? k = m₂.get? k
-- Std.Time.Format.Modifier
Std.Time.DayPeriod.noon.sizeOf_spec : sizeOf Std.Time.DayPeriod.noon = 1
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
MvPowerSeries.lexOrder_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder σ] [inst_2 : WellFoundedGT σ],
  MvPowerSeries.lexOrder 0 = ⊤
-- Qq.Commands
/-- `run_tacq` is the Qq analogue to `run_tac` which allows executing arbitrary `TacticM` code.
In contrast to `run_tac`, the local context of the main goal can be directly accessed as quoted
expressions. Optionally, the annotated goal can also be saved using the syntax `run_tacq $g =>`.
Example:
```
example (a b : Nat) (h : a = b) : True := by
  run_tacq goal =>
    let p : Q(Prop) := q($a = $b)
    let t ← Lean.Meta.inferType h
    Lean.logInfo p
    Lean.logInfo <| toString (← Lean.Meta.isDefEq t p)
    Lean.logInfo <| toString (← Lean.Meta.isDefEq h.ty p)
    Lean.logInfo goal
    Lean.logInfo goal.ty
  trivial
```
See also: `by_elabq`.
 -/
Qq.«tacticRun_tacq_=>_» : Lean.ParserDescr
-- Mathlib.Topology.PartialHomeomorph.Defs
/-- Coercion of a partial homeomorphisms to a function. We don't use `e.toFun` because it is
actually `e.toPartialEquiv.toFun`, so `simp` will apply lemmas about `toPartialEquiv`.  -/
PartialHomeomorph.toFun' : {X : Type u_1} →
  {Y : Type u_3} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → PartialHomeomorph X Y → X → Y
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsCompatibleWithShiftTrWIntOfIsStableUnderShift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderShift ℤ], P.trW.IsCompatibleWithShift ℤ
-- Mathlib.Logic.Encodable.Basic
Fin.encodable : (n : ℕ) → Encodable (Fin n)
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHSubOffset_4 : HSub Std.Time.Timestamp Std.Time.Second.Offset Std.Time.Timestamp
-- Mathlib.Data.Finset.CastCard
/-- $\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$.
This result is casted to any additive group with 1,
so that we don't have to work with `ℕ`-subtraction.  -/
Finset.cast_card_erase_of_mem : ∀ {α : Type u_1} {R : Type u_2} {s : Finset α} {a : α} [inst : DecidableEq α] [inst_1 : AddGroupWithOne R],
  a ∈ s → ↑(s.erase a).card = ↑s.card - 1
-- Init.Data.List.Basic
List.replicate_eq_replicateTR : @List.replicate = @List.replicateTR
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
SheafOfModules.conjugateEquiv_pullbackComp_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {D' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D'] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat}
  {R : CategoryTheory.Sheaf K RingCat} [inst_3 : F.IsContinuous J K]
  (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) [inst_4 : (SheafOfModules.pushforward φ).IsRightAdjoint]
  {K' : CategoryTheory.GrothendieckTopology D'} {G : CategoryTheory.Functor D D'} {R' : CategoryTheory.Sheaf K' RingCat}
  [inst_5 : G.IsContinuous K K'] [inst_6 : (F.comp G).IsContinuous J K']
  (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R') [inst_7 : (SheafOfModules.pushforward ψ).IsRightAdjoint],
  (CategoryTheory.conjugateEquiv
        ((SheafOfModules.pullbackPushforwardAdjunction φ).comp (SheafOfModules.pullbackPushforwardAdjunction ψ))
        (SheafOfModules.pullbackPushforwardAdjunction
          (CategoryTheory.CategoryStruct.comp φ ((F.sheafPushforwardContinuous RingCat J K).map ψ))))
      (SheafOfModules.pullbackComp φ ψ).inv =
    (SheafOfModules.pushforwardComp φ ψ).hom
-- Mathlib.Topology.Order
/-- If `s` equals the collection of open sets in the topology it generates, then `s` defines a
topology.  -/
TopologicalSpace.mkOfClosure : {α : Type u} → (s : Set (Set α)) → {u | TopologicalSpace.GenerateOpen s u} = s → TopologicalSpace α
-- Init.Meta.Defs
/-- Controls which new mvars are turned in to goals by the `apply` tactic.
- `nonDependentFirst`  mvars that don't depend on other goals appear first in the goal list.
- `nonDependentOnly` only mvars that don't depend on other goals are added to goal list.
- `all` all unassigned mvars are added to the goal list.
 -/
Lean.Meta.ApplyNewGoals : Type
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
/-- A version of `measurable_const` that assumes `f x = f y` for all `x, y`. This version works
for functions between empty types.  -/
measurable_const' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : β → α},
  (∀ (x y : β), f x = f y) → Measurable f
-- Mathlib.ModelTheory.Skolem
FirstOrder.Language.card_functions_sum_skolem₁ : ∀ {L : FirstOrder.Language},
  Cardinal.mk ((n : ℕ) × (L.sum L.skolem₁).Functions n) = Cardinal.mk ((n : ℕ) × L.BoundedFormula Empty (n + 1))
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.unop_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ),
  CategoryTheory.NatTrans.unop (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.unop
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.lift_inj : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F : IntermediateField K L}
  (E E' : IntermediateField K ↥F), IntermediateField.lift E = IntermediateField.lift E' ↔ E = E'
-- Mathlib.Algebra.Homology.Embedding.TruncLE
ComplexShape.Embedding.ιTruncLENatTrans_app : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [inst : e.IsTruncLE]
  (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.CategoryWithHomology C]
  (K : HomologicalComplex C c'), (e.ιTruncLENatTrans C).app K = K.ιTruncLE e
-- Mathlib.Analysis.Normed.Operator.Mul
/-- Simultaneous left- and right-multiplication in a non-unital normed algebra, considered as a
continuous trilinear map. This is akin to its non-continuous version `LinearMap.mulLeftRight`,
but there is a minor difference: `LinearMap.mulLeftRight` is uncurried.  -/
ContinuousLinearMap.mulLeftRight : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (R : Type u_3) →
      [inst_1 : NonUnitalSeminormedRing R] →
        [inst_2 : NormedSpace 𝕜 R] → [IsScalarTower 𝕜 R R] → [SMulCommClass 𝕜 R R] → R →L[𝕜] R →L[𝕜] R →L[𝕜] R
-- Mathlib.CategoryTheory.Core
CategoryTheory.CoreHom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : CategoryTheory.Core C} → (X.of ≅ Y.of) → CategoryTheory.CoreHom X Y
-- Init.Data.Range.Polymorphic.PRange
Std.Rco.HasRcoIntersection.mk : {α : Type w} → (Std.Rco α → Std.Rco α → Std.Rco α) → Std.Rco.HasRcoIntersection α
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.compactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace X] (h : X ≃ₜ Y),
  CompactSpace Y
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.mk.sizeOf_spec : ∀ {α : Type u} [inst : UniformSpace α] [inst_1 : SizeOf α] (space : Type v) (coe : α → space)
  (uniformStruct : UniformSpace space) (complete : CompleteSpace space) (separation : T0Space space)
  (isUniformInducing : IsUniformInducing coe) (dense : DenseRange coe),
  sizeOf
      { space := space, coe := coe, uniformStruct := uniformStruct, complete := complete, separation := separation,
        isUniformInducing := isUniformInducing, dense := dense } =
    1 + sizeOf space + sizeOf uniformStruct + sizeOf complete + sizeOf separation + sizeOf isUniformInducing
-- Mathlib.Algebra.QuadraticAlgebra.Defs
/-- The natural function `R → QuadraticAlgebra R a b`.

Note that, if `R` is a ring, you should use `algebraMap` instead of `C`.  -/
QuadraticAlgebra.C : {R : Type u_1} → {a b : R} → [Zero R] → R → QuadraticAlgebra R a b
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.pred_eq_of_isSuccPrelimit : ∀ {o : Ordinal.{u_4}}, Order.IsSuccPrelimit o → o.pred = o
-- Init.Data.List.Find
List.lookup_replicate : ∀ {α : Type u_2} [inst : BEq α] {n : ℕ} {a : α} {α_1 : Type u_1} {b : α_1} {k : α},
  List.lookup k (List.replicate n (a, b)) = if n = 0 then none else if (k == a) = true then some b else none
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.upper : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LE α] (s : ClopenUpperSet α), IsUpperSet ↑s
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instCommGroup : {G : Type u_1} →
  [inst : TopologicalSpace G] → [inst_1 : CommGroup G] → [IsTopologicalGroup G] → CommGroup (SeparationQuotient G)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.mul_minus_one_getConst_eq : ∀ (p : Int.Internal.Linear.Poly), (p.mul (-1)).getConst = -p.getConst
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet_id : ∀ {Ω : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (h : CategoryTheory.CoreSmallCategoryOfSet Ω C)
  (X : ↑h.obj), h.smallCategoryOfSet.id X = h.homEquiv.symm (CategoryTheory.CategoryStruct.id (h.objEquiv X))