mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.constantCoeff_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a →
    ∀ (f : MvPowerSeries σ R),
      MvPowerSeries.constantCoeff (MvPowerSeries.subst a f) =
        ∑ᶠ (d : σ →₀ ℕ), (MvPowerSeries.coeff d) f • MvPowerSeries.constantCoeff (d.prod fun s e => a s ^ e)
-- Lean.Language.Basic
/-- Use given range.  -/
Lean.Language.SnapshotTask.ReportingRange.some : Lean.Syntax.Range → Lean.Language.SnapshotTask.ReportingRange
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- **Alias** of `AlgebraicGeometry.SmoothOfRelativeDimension`.

---

A morphism of schemes `f : X ⟶ Y` is smooth of relative dimension `n` if for each `x : X` there
exists an affine open neighborhood `V` of `x` and an affine open neighborhood `U` of
`f.base x` with `V ≤ f ⁻¹ᵁ U` such that the induced map `Γ(Y, U) ⟶ Γ(X, V)` is
standard smooth of relative dimension `n`.
 -/
AlgebraicGeometry.IsSmoothOfRelativeDimension : ℕ → {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.eulerMascheroniSeq'_one : Real.eulerMascheroniSeq' 1 = 1
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.intercalateTR.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → List (List α) → Array α → Sort u_2) →
    (x : List α) →
      (x_1 : List (List α)) →
        (x_2 : Array α) →
          ((x : List α) → (acc : Array α) → motive x [] acc) →
            ((x y : List α) → (xs : List (List α)) → (acc : Array α) → motive x (y :: xs) acc) → motive x x_1 x_2
-- Mathlib.Order.Notation
Bot.mk : {α : Type u_1} → α → Bot α
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.ediam_univ : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
  Metric.ediam Set.univ = Metric.ediam Set.univ
-- Lean.Meta.Tactic.SolveByElim
/-- Elaborate a list of lemmas and local context.
See `mkAssumptionSet` for an explanation of why this is needed.
 -/
Lean.Meta.SolveByElim.elabContextLemmas : Lean.Meta.SolveByElim.SolveByElimConfig →
  Lean.MVarId →
    List (Lean.Elab.TermElabM Lean.Expr) →
      (Lean.Meta.SolveByElim.SolveByElimConfig → Lean.Elab.TermElabM (List Lean.Expr)) → Lean.MetaM (List Lean.Expr)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.smul_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ} (k : R)
  (z : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + n = q), (k • z).v p q hpq = k • z.v p q hpq
-- Batteries.Data.Vector.Lemmas
Vector.scanr_eq_scanrM : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {init : β} {f : α → β → β} {as : Vector α n},
  Vector.scanr f init as = (Vector.scanrM (fun x1 x2 => pure (f x1 x2)) init as).run
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.isIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y), CategoryTheory.IsIso e.inv
-- Mathlib.Analysis.Fourier.Notation
/-- A `FourierInvPair` is a pair of spaces `E` and `F` such that `𝓕 ∘ 𝓕⁻ = id` on `E`.  -/
FourierInvPair : (E : Type u_5) → (F : Type u_6) → [FourierTransform F E] → [FourierTransformInv E F] → Prop
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_filterMap : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : (↑m).WF)
  {h' : (Std.DHashMap.Internal.Raw₀.filterMap f m).contains k = true},
  (Std.DHashMap.Internal.Raw₀.filterMap f m).get k h' = (f k (m.get k ⋯)).get ⋯
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.TrySuggestionEntry.mk.inj : ∀ {name : Lean.Name} {prio : ℕ} {name_1 : Lean.Name} {prio_1 : ℕ},
  { name := name, prio := prio } = { name := name_1, prio := prio_1 } → name = name_1 ∧ prio = prio_1
-- Mathlib.Tactic.Ring.Basic
/-- `CSLift α β` is a typeclass used by `ring` for lifting operations from `α`
(which is not a commutative semiring) into a commutative semiring `β` by using an injective map
`lift : α → β`.  -/
Mathlib.Tactic.Ring.CSLift : Type u → outParam (Type u) → Type u
-- Mathlib.Analysis.InnerProductSpace.Basic
nnnorm_inner_le_nnnorm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), ‖inner 𝕜 x y‖₊ ≤ ‖x‖₊ * ‖y‖₊
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_eq_some : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k : α}, k ∈ m → m.get? k = some k
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
/-- By definition, a separable measure admits a countable and measure-dense family of sets.  -/
MeasureTheory.exists_countable_measureDense : ∀ {X : Type u_1} [m : MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsSeparable μ],
  ∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜
-- Mathlib.Order.Lattice
Prod.instDistribLattice : (α : Type u) → (β : Type v) → [DistribLattice α] → [DistribLattice β] → DistribLattice (α × β)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_inv_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T)
  (n : SimplexCategoryᵒᵖ) (i : CategoryTheory.ToType (Opposite.unop n)) {Z : CategoryTheory.Limits.FormalCoproduct C}
  (h : U ⟶ Z),
  CategoryTheory.CategoryStruct.comp (U.cechIsoCechNerveApp hT n).inv
      (CategoryTheory.CategoryStruct.comp (U.powerπ i) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.WidePullback.π
        (fun x => (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U) i)
      h
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_sub_ratCast : ∀ (q : ℚ) {x : ℝ}, Irrational (x - ↑q) → Irrational x
-- Mathlib.Analysis.BoxIntegral.DivergenceTheorem
BoxIntegral.BoxAdditiveMap.restrict.congr_simp : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)}
  (f f_1 : BoxIntegral.BoxAdditiveMap ι M I₀),
  f = f_1 → ∀ (I : WithTop (BoxIntegral.Box ι)) (hI : I ≤ I₀), f.restrict I hI = f_1.restrict I hI
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
/-- The normed group homomorphism of considering a bounded continuous function on a finite-measure
space as an element of `Lp`.  -/
BoundedContinuousFunction.toLpHom : {α : Type u_1} →
  {E : Type u_2} →
    {m0 : MeasurableSpace α} →
      (p : ENNReal) →
        (μ : MeasureTheory.Measure α) →
          [inst : TopologicalSpace α] →
            [BorelSpace α] →
              [inst_2 : NormedAddCommGroup E] →
                [SecondCountableTopologyEither α E] →
                  [MeasureTheory.IsFiniteMeasure μ] →
                    [inst_5 : Fact (1 ≤ p)] →
                      NormedAddGroupHom (BoundedContinuousFunction α E) ↥(MeasureTheory.Lp E p μ)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∉ t₁ → (t₁ ∪ t₂).getKeyD k fallback = t₂.getKeyD k fallback
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
OrthonormalBasis.measurePreserving_repr_symm : ∀ {ι : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F]
  [inst_2 : MeasurableSpace F] [inst_3 : BorelSpace F] [inst_4 : Fintype ι] [inst_5 : FiniteDimensional ℝ F]
  (b : OrthonormalBasis ι ℝ F), MeasureTheory.MeasurePreserving (⇑b.repr.symm) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.Tactic.Ring.RingNF
_private.Mathlib.Tactic.Ring.RingNF.0.Mathlib.Tactic.RingNF.instEvalExprBehaviorIfUnchanged.evalExpr : Lean.Expr → Lean.MetaM Mathlib.Tactic.BehaviorIfUnchanged
-- Mathlib.Data.Nat.PSub
/-- Same as `psub`, but with a more efficient implementation.  -/
Nat.psub' : ℕ → ℕ → Option ℕ
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {toHom : E.Hom F.toPreZeroHypercover}
  {s₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHom.s₀ i) (toHom.s₀ j)}
  {h₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (s₁ k)}
  {w₁₁ :
    autoParam
      (∀ {i j : E.I₀} (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k) (F.p₁ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (toHom.h₀ i))
      CategoryTheory.PreOneHypercover.Hom.w₁₁._autoParam}
  {w₁₂ :
    autoParam
      (∀ {i j : E.I₀} (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k) (F.p₂ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (toHom.h₀ j))
      CategoryTheory.PreOneHypercover.Hom.w₁₂._autoParam}
  {toHom_1 : E.Hom F.toPreZeroHypercover} {s₁_1 : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHom_1.s₀ i) (toHom_1.s₀ j)}
  {h₁_1 : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (s₁_1 k)}
  {w₁₁_1 :
    autoParam
      (∀ {i j : E.I₀} (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁_1 k) (F.p₁ (s₁_1 k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (toHom_1.h₀ i))
      CategoryTheory.PreOneHypercover.Hom.w₁₁._autoParam}
  {w₁₂_1 :
    autoParam
      (∀ {i j : E.I₀} (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁_1 k) (F.p₂ (s₁_1 k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (toHom_1.h₀ j))
      CategoryTheory.PreOneHypercover.Hom.w₁₂._autoParam},
  { toHom := toHom, s₁ := s₁, h₁ := h₁, w₁₁ := w₁₁, w₁₂ := w₁₂ } =
      { toHom := toHom_1, s₁ := s₁_1, h₁ := h₁_1, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 } →
    toHom = toHom_1 ∧ s₁ ≍ s₁_1 ∧ h₁ ≍ h₁_1
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_natCast : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (n : ℕ), F⟮↑n⟯ = ⊥
-- Mathlib.Topology.Category.TopCat.Opens
/-- The inclusion map from an open subset to the whole space, as a morphism in `TopCat`.
 -/
TopologicalSpace.Opens.inclusion' : {X : TopCat} → (U : TopologicalSpace.Opens ↑X) → (TopologicalSpace.Opens.toTopCat X).obj U ⟶ X
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.iInf₂ : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] {κ : Sort u_4}
  {κ' : κ → Sort u_5} {f : (i : κ) → κ' i → Ideal A},
  (∀ (i : κ) (j : κ' i), Ideal.IsHomogeneous 𝒜 (f i j)) → Ideal.IsHomogeneous 𝒜 (⨅ i, ⨅ j, f i j)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_id : ∀ {L : FirstOrder.Language} {P : Type u_2} [inst : L.Structure P] (S : L.Substructure P),
  FirstOrder.Language.Substructure.comap (FirstOrder.Language.Hom.id L P) S = S
-- Lean.Meta.MatchUtil
Lean.Meta.matchNot? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeriesOfIdeal_le_self : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (k : ℕ), LieAlgebra.derivedSeriesOfIdeal R L k I ≤ I
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.AlternatingFaceMapComplex.obj.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C),
  AlgebraicTopology.AlternatingFaceMapComplex.obj X =
    ChainComplex.of (fun n => X.obj (Opposite.op { len := n })) (AlgebraicTopology.AlternatingFaceMapComplex.objD X) ⋯
-- Mathlib.Algebra.Order.Ring.GeomSum
Nat.geom_sum_Ico_le : ∀ {b : ℕ}, 2 ≤ b → ∀ (a n : ℕ), ∑ i ∈ Finset.Ico 1 n, a / b ^ i ≤ a / (b - 1)
-- Lean.Util.Trace
_private.Lean.Util.Trace.0.Lean.withTraceNode.postCallback : {α : Type} →
  {m : Type → Type} →
    [Monad m] →
      [Lean.MonadTrace m] →
        [Lean.MonadRef m] →
          [Lean.AddMessageContext m] →
            {ε : Type} →
              [always : Lean.MonadAlwaysExcept ε m] →
                [Lean.ExceptToTraceResult ε α] →
                  Lean.Name →
                    Bool →
                      String →
                        Lean.Options →
                          Bool →
                            Lean.PersistentArray Lean.TraceElem →
                              (Except ε α → m Lean.MessageData) → Except ε α × Float × Float → m α
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- An abbreviation for `HasLimit (Discrete.functor f)`.  -/
CategoryTheory.Limits.HasProduct : {β : Type w} → {C : Type u} → [CategoryTheory.Category.{v, u} C] → (β → C) → Prop
-- Mathlib.Data.PNat.Notation
instReprPNat : Repr ℕ+
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_erase_eq_of_not_compare_eq_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, ¬cmp k (t.maxKey ⋯) = Ordering.eq → (t.erase k).maxKey he = t.maxKey ⋯
-- Mathlib.Data.Set.Sigma
Set.sigma_insert : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {a : (i : ι) → α i},
  (s.sigma fun i => insert (a i) (t i)) = (fun i => ⟨i, a i⟩) '' s ∪ s.sigma t
-- Mathlib.Analysis.Normed.Module.Basic
instSeminormedRingRestrictScalars : {𝕜 : Type u_1} → {𝕜' : Type u_2} → {E : Type u_3} → [I : SeminormedRing E] → SeminormedRing (RestrictScalars 𝕜 𝕜' E)
-- Aesop.Tree.RunMetaM
Aesop.Goal.runMetaMModifyingParentState : {m : Type → Type} → [Monad m] → [MonadLiftT Lean.MetaM m] → [MonadFinally m] → {α : Type} → m α → Aesop.Goal → m α
-- Mathlib.Data.List.Cycle
List.nextOr_self_cons_cons : ∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α) (x y d : α), (x :: y :: xs).nextOr x d = y
-- Mathlib.GroupTheory.Congruence.Hom
/-- Homomorphisms on the quotient of an `AddMonoid` by an additive congruence relation
are equal if they are equal on elements that are coercions from the `AddMonoid`.  -/
AddCon.lift_funext : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M}
  (f g : c.Quotient →+ P), (∀ (a : M), f ↑a = g ↑a) → f = g
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Given `f ∣ x`, this is the map `A_{(f)} → A_f → A_x`. We will lift this to a map
`A_{(f)} → A_{(x)}` in `awayMap`.  -/
_private.Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization.0.HomogeneousLocalization.awayMapAux : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                (𝒜 : ι → σ) →
                  [inst_5 : GradedRing 𝒜] → {f x : A} → f ∣ x → HomogeneousLocalization.Away 𝒜 f →+* Localization.Away x
-- Mathlib.Order.Interval.Set.Image
StrictMono.image_Ioi_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  StrictMono f → f '' Set.Ioi a ⊆ Set.Ioi (f a)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ideal_top : ∀ {X : AlgebraicGeometry.Scheme}, ⊤.ideal = ⊤
-- Mathlib.Analysis.Distribution.TestFunction
/-- The natural inclusion `𝓓^{n}_{K}(E, F) → 𝓓^{n}(Ω, F)`, when `K ⊆ Ω`, as a continuous
linear map.  -/
TestFunction.ofSupportedInCLM : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace ℝ E] →
          {Ω : TopologicalSpace.Opens E} →
            {F : Type u_4} →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace ℝ F] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    {n : ℕ∞} →
                      [inst_6 : SMulCommClass ℝ 𝕜 F] →
                        {K : TopologicalSpace.Compacts E} →
                          ↑K ⊆ ↑Ω → ContDiffMapSupportedIn E F n K →L[𝕜] TestFunction Ω F n
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.finish_v : ∀ (u : PNat.XgcdType), u.r = 0 → u.finish.v = u.v
-- Init.Data.Vector.Perm
Vector.Perm.toList : ∀ {α : Type u_1} {n : ℕ} {as bs : Vector α n}, as.Perm bs → as.toList.Perm bs.toList
-- Init.Core
/-- An trichotomous relation `r` satisfies `¬ r a b → ¬ r b a → a = b`.  -/
Std.Trichotomous.trichotomous : ∀ {α : Sort u} {r : α → α → Prop} [self : Std.Trichotomous r] (a b : α), ¬r a b → ¬r b a → a = b
-- Mathlib.Data.Num.Lemmas
PosNum.cmp_to_nat_lemma : ∀ {m n : PosNum}, ↑m < ↑n → ↑m.bit1 < ↑n.bit0
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.ofQuotientStabilizer_mk : ∀ (G : Type u) {X : Type v} [inst : Group G] [inst_1 : MulAction G X] (x : X) (g : G),
  MulAction.ofQuotientStabilizer G x ↑g = g • x
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.lift_lt_omega_ofNat : ∀ {o : Ordinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Ordinal.lift.{v, u} o < Ordinal.omega (OfNat.ofNat n) ↔ o < Ordinal.omega (OfNat.ofNat n)
-- Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent
AlgebraicGeometry.instDescendsAlongSchemeLocallyOfFinitePresentationMinMorphismPropertySurjectiveFlatQuasiCompact : CategoryTheory.MorphismProperty.DescendsAlong (@AlgebraicGeometry.LocallyOfFinitePresentation)
  (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.instInhabitedK'.default : Turing.PartrecToTM2.K'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofIsInitialLeft_ι : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂)
  [inst_3 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.flip.obj X₂)]
  [inst_4 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.flip.obj Y₂)]
  (h : CategoryTheory.Limits.IsInitial X₁),
  (CategoryTheory.Functor.PushoutObjObj.ofIsInitialLeft F f₁ f₂ h).ι = (F.obj Y₁).map f₂
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.completeBipartiteGraphCongr_apply : ∀ {V₁ : Type u_5} {V₂ : Type u_6} {W₁ : Type u_7} {W₂ : Type u_8} (hV : V₁ ≃ V₂) (hW : W₁ ≃ W₂) (a : V₁ ⊕ W₁),
  (SimpleGraph.completeBipartiteGraphCongr hV hW) a = Sum.map (⇑hV) (⇑hW) a
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
_private.Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization.0.Int.castDef.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.negSucc n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_2 n
-- Mathlib.MeasureTheory.Function.EssSup
ENNReal.essSup_add_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f g : α → ENNReal),
  essSup (f + g) μ ≤ essSup f μ + essSup g μ
-- Lean.LocalContext
Lean.LocalContext.size : Lean.LocalContext → ℕ
-- Mathlib.NumberTheory.LSeries.ZMod
/-- The `LFunction` of the function `x ↦ e (j * x)`, where `e : ZMod N → ℂ` is the standard additive
character, is `expZeta (j / N)`.

Note this is not at all obvious from the definitions, and we prove it by analytic continuation
from the convergence range.
 -/
ZMod.LFunction_stdAddChar_eq_expZeta : ∀ {N : ℕ} [inst : NeZero N] (j : ZMod N) (s : ℂ),
  j ≠ 0 ∨ s ≠ 1 → ZMod.LFunction (fun k => ZMod.stdAddChar (j * k)) s = HurwitzZeta.expZeta (ZMod.toAddCircle j) s
-- Mathlib.Order.Filter.Bases.Basic
Filter.basis_sets : ∀ {α : Type u_1} (l : Filter α), l.HasBasis (fun s => s ∈ l) id
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.coprod_inl_rightDistrib_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalRightDistrib C]
  {X Y Z Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (Y ⨿ Z) X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.CategoryStruct.comp (∂R X Y Z).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inl X) h
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- The canonical map from the quotient of the stabilizer to the set.  -/
MulAction.ofQuotientStabilizer : (G : Type u) → {X : Type v} → [inst : Group G] → [inst_1 : MulAction G X] → (x : X) → G ⧸ MulAction.stabilizer G x → X
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCStarAlgebra.toSMulCommClass : ∀ {A : Type u_1} [self : NonUnitalCStarAlgebra A], SMulCommClass ℂ A A
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
SkewMonoidAlgebra.support_mul_single : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : Semiring k] [inst_2 : MulSemiringAction G k]
  (f : SkewMonoidAlgebra k G) [inst_3 : IsRightCancelMul G] (r : k) (x : G),
  (∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0) →
    (f * SkewMonoidAlgebra.single x r).support = Finset.map (mulRightEmbedding x) f.support
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_lt_of_translationNumber_lt_int : ∀ (f : CircleDeg1Lift) {n : ℤ}, f.translationNumber < ↑n → ∀ (x : ℝ), f x < x + ↑n
-- Mathlib.Order.Interval.Set.LinearOrder
Set.compl_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, (Set.Ici a)ᶜ = Set.Iio a
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.mk : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      {d : HNNExtension.NormalWord.TransversalPair G A B} →
        (toReducedWord : HNNExtension.NormalWord.ReducedWord G A B) →
          (∀ (u : ℤˣ) (g : G), (u, g) ∈ toReducedWord.toList → g ∈ d.set u) → HNNExtension.NormalWord d
-- Mathlib.Algebra.PresentedMonoid.Basic
/-- The quotient map from the free monoid on `α` to the presented monoid with the same generators
and the given relations `rels`.  -/
PresentedMonoid.mk : {α : Type u_1} → (rels : FreeMonoid α → FreeMonoid α → Prop) → FreeMonoid α →* PresentedMonoid rels
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get_getKey? : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {a : α} {h' : (m.getKey? a).isSome = true}, (m.getKey? a).get h' = m.getKey a ⋯
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.map_add₂ : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (x₁ x₂ : M) (y : N), (f (x₁ + x₂)) y = (f x₁) y + (f x₂) y
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.symmDiff_congr : ∀ {α : Type u} {s t u : Set α}, (symmDiff s t).Finite → ((symmDiff s u).Finite ↔ (symmDiff t u).Finite)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.mkIso_hom_fst : ∀ {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 y : CategoryTheory.Limits.CategoricalPullback F G} (eₗ : x.fst ≅ y.fst) (eᵣ : x.snd ≅ y.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map eₗ.hom) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (G.map eᵣ.hom))
      CategoryTheory.Limits.CategoricalPullback.mkIso._auto_1),
  (CategoryTheory.Limits.CategoricalPullback.mkIso eₗ eᵣ w).hom.fst = eₗ.hom