mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Constructions.SumProd
Filter.HasBasis.prod_nhds' : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {ιX : Type u_5} {ιY : Type u_6}
  {pX : ιX → Prop} {pY : ιY → Prop} {sx : ιX → Set X} {sy : ιY → Set Y} {p : X × Y},
  (nhds p.1).HasBasis pX sx →
    (nhds p.2).HasBasis pY sy → (nhds p).HasBasis (fun i => pX i.1 ∧ pY i.2) fun i => sx i.1 ×ˢ sy i.2
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.up_length_toListRev_eq_count : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  (fun x => { down := x.length }) <$> it.toListRev = it.length
-- Mathlib.Analysis.Convex.Gauge
/-- Any seminorm arises as the gauge of its unit ball.  -/
Seminorm.gauge_ball : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (p : Seminorm ℝ E), gauge (p.ball 0 1) = ⇑p
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsCoseparating.mono_productTo : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  P.IsCoseparating →
    ∀ (X : C) [inst_1 : CategoryTheory.Limits.HasProduct (P.productToFamily X)], CategoryTheory.Mono (P.productTo X)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Clean.State.next : Lean.Meta.Grind.Clean.State → Lean.PHashMap Lean.Name ℕ
-- Mathlib.Algebra.Module.RingHom
/-- Compose a `Module` with a `RingHom`, with action `f s • m`.

See note [reducible non-instances].  -/
Module.compHom : {R : Type u_1} →
  {S : Type u_2} →
    (M : Type u_3) →
      [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → [inst_3 : Semiring S] → (S →+* R) → Module S M
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.nontrivial_iff_exists_ne_one : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 1
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.toPreAbstractSimplicialComplex : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : Ring 𝕜] →
      [inst_1 : PartialOrder 𝕜] →
        [inst_2 : AddCommGroup E] →
          [inst_3 : Module 𝕜 E] → Geometry.SimplicialComplex 𝕜 E → PreAbstractSimplicialComplex E
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.div : ∀ {α : Type u_2} [inst : CommMonoid α] {A : Set α} {n : ℕ} {β : Type u_5} [inst_1 : DivisionCommMonoid β]
  {B₁ B₂ : Set β} {f₁ f₂ : α → β},
  IsMulFreimanHom n A B₁ f₁ → IsMulFreimanHom n A B₂ f₂ → IsMulFreimanHom n A (B₁ / B₂) (f₁ / f₂)
-- Mathlib.Algebra.Tropical.BigOperators
List.trop_minimum : ∀ {R : Type u_1} [inst : LinearOrder R] (l : List R),
  Tropical.trop l.minimum = (List.map (Tropical.trop ∘ WithTop.some) l).sum
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Generalized loop from a loop by uncurrying $I → (I^{N\setminus\{j\}} → X)$ into $I^N → X$.  -/
GenLoop.fromLoop : {N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {x : X} → [DecidableEq N] → (i : N) → LoopSpace (↑(GenLoop { j // j ≠ i } X x)) GenLoop.const → ↑(GenLoop N X x)
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBumpBase.mk : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      (toFun : ℝ → E → ℝ) →
        (∀ (R : ℝ) (x : E), toFun R x ∈ Set.Icc 0 1) →
          (∀ (R : ℝ) (x : E), toFun R (-x) = toFun R x) →
            ContDiffOn ℝ (↑⊤) (Function.uncurry toFun) (Set.Ioi 1 ×ˢ Set.univ) →
              (∀ (R : ℝ), 1 < R → ∀ (x : E), ‖x‖ ≤ 1 → toFun R x = 1) →
                (∀ (R : ℝ), 1 < R → Function.support (toFun R) = Metric.ball 0 R) → ContDiffBumpBase E
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm is nonarchimedean: the norm of `p + q` is at most the max of the norm of `p`
and the norm of `q`.  -/
padicNorm.nonarchimedean : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ}, padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
-- Mathlib.Algebra.Regular.Defs
/-- A regular element `c` is right-regular  -/
IsRegular.right : ∀ {R : Type u_1} [inst : Mul R] {c : R}, IsRegular c → IsRightRegular c
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.forIn_map : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {n : Type w → Type w''} {β₂ : Type w} [inst_1 : Monad n] [LawfulMonad n]
  [Std.Iterators.Finite α Id] [inst_4 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {it : Std.Iter β}
  {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)},
  forIn (Std.Iter.map f it) init g = forIn it init fun out acc => g (f out) acc
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullback.hom_eq_lift : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → objs j ⟶ B) [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C}
  (g : X ⟶ CategoryTheory.Limits.widePullback B objs arrows),
  g =
    CategoryTheory.Limits.WidePullback.lift
      (CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.WidePullback.base arrows))
      (fun j => CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.WidePullback.π arrows j)) ⋯
-- Mathlib.Analysis.LocallyConvex.PointwiseConvergence
/-- The family of seminorms that induce the topology of pointwise convergence, namely `‖A x‖` for
all `x : E`.  -/
PointwiseConvergenceCLM.seminormFamily : {𝕜₁ : Type u_3} →
  {𝕜₂ : Type u_4} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          (E : Type u_7) →
            (F : Type u_8) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : NormedAddCommGroup F] → [inst_6 : NormedSpace 𝕜₂ F] → SeminormFamily 𝕜₂ (E →SLₚₜ[σ] F) E
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_insert`. -/
EMetric.diam_insert : ∀ {X : Type u_2} {s : Set X} {x : X} [inst : PseudoEMetricSpace X],
  Metric.ediam (insert x s) = max (⨆ y ∈ s, edist x y) (Metric.ediam s)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- The natural map from `SkewMonoidAlgebra k G` to `G →₀ k`.  -/
SkewMonoidAlgebra.coeff : {k : Type u_1} → {G : Type u_2} → [inst : Zero k] → SkewMonoidAlgebra k G → G →₀ k
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.modByMonicHom.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f), h.modByMonicHom = { toFun := fun x => h.repr x %ₘ f, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.eq_singularPart : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] {ξ : ProbabilityTheory.Kernel α γ} {f : α → γ → ENNReal}
  [inst : ProbabilityTheory.IsFiniteKernel η] [inst_1 : ProbabilityTheory.IsFiniteKernel κ],
  κ = η.withDensity f + ξ →
    Measurable (Function.uncurry f) → ∀ (a : α), (ξ a).MutuallySingular (η a) → ξ a = (κ.singularPart η) a
-- Mathlib.GroupTheory.GroupAction.Primitive
AddAction.isPreprimitive_congr : ∀ {M : Type u_3} [inst : AddGroup M] {α : Type u_4} [inst_1 : AddAction M α] {N : Type u_5} {β : Type u_6}
  [inst_2 : AddGroup N] [inst_3 : AddAction N β] {φ : M → N} {f : α →ₑ[φ] β},
  Function.Surjective φ → Function.Bijective ⇑f → (AddAction.IsPreprimitive M α ↔ AddAction.IsPreprimitive N β)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsCodetecting.isCoseparating : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.Limits.HasCoequalizers C], P.IsCodetecting → P.IsCoseparating
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.package.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.package = 1
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.eq_of_comp_left_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y},
  (∀ {Z : C} (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) → f = g
-- Mathlib.Tactic.GCongr.Core
/-- `rel [h₁, ..., hₙ]` uses "generalized congruence" rules to solve a goal of form
`⊢ R (f a₁ ... aₙ) (f b₁ ... bₙ)` by substituting with the terms `hᵢ : Rᵢ aᵢ bᵢ`. The relations
`R`, `Rᵢ` can be any two-argument relation, including `· → ·`.

This tactic is extensible: to add a "generalized congruence" rule, tag a theorem with the attribute
`@[gcongr]`.

If a "generalized congruence" lemma has a side goal, `rel` will try to discharge it using
`gcongr_discharger`, which is an extensible tactic based on `positivity`. If side goals cannot be
discharged, or the terms `h₁`, ..., `hₙ` cannot solve the goals, the tactic fails.

Examples:
```
example {a b x c d : ℝ} (h1 : a ≤ b) (h2 : c ≤ d) :
    x ^ 2 * a + c ≤ x ^ 2 * b + d := by
  rel [h1, h2]
-- In this example we "substitute" the hypotheses `a ≤ b` and `c ≤ d` into the LHS `x ^ 2 * a + c`
-- of the goal and obtain the RHS `x ^ 2 * b + d`, thus proving the goal.
-- This constructs the proof term:
--   add_le_add (mul_le_mul_of_nonneg_left h1 (pow_bit0_nonneg x 1)) h2
-- using the generalized congruence lemmas `add_le_add` and `mul_le_mul_of_nonneg_left`.
```
 -/
Mathlib.Tactic.GCongr.«tacticRel[_]» : Lean.ParserDescr
-- Mathlib.Data.Nat.Log
Nat.log_lt_iff_lt_pow : ∀ {b : ℕ}, 1 < b → ∀ {x y : ℕ}, y ≠ 0 → (Nat.log b y < x ↔ y < b ^ x)
-- Init.Data.UInt.Lemmas
Fin.mk_uInt8ToNat : ∀ (n : UInt8), ⟨n.toNat, ⋯⟩ = n.toFin
-- Mathlib.Geometry.Convex.Cone.Basic
/-- Every submodule is trivially a convex cone.  -/
Submodule.toConvexCone : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : Module R M] → Submodule R M → ConvexCone R M
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If two functions agree in a punctured neighborhood, then their trailing coefficients agree.
 -/
meromorphicTrailingCoeffAt_congr_nhdsNE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E},
  f₁ =ᶠ[nhdsWithin x {x}ᶜ] f₂ → meromorphicTrailingCoeffAt f₁ x = meromorphicTrailingCoeffAt f₂ x
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.verify₃ : UInt8 → UInt8 → UInt8 → Bool
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.adjunctionOfEquivRight_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G_obj : D → C} (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
  (he :
    ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
      (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g))
  (X : C),
  (CategoryTheory.Adjunction.adjunctionOfEquivRight e he).unit.app X =
    (e X (F.obj X)) (CategoryTheory.CategoryStruct.id (F.obj X))
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.ringEquivOfRingEquiv_trans : ∀ {R : Type u_5} {S : Type u_6} (K : Type u_7) (L : Type u_8) [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CommRing S] [inst_3 : IsDomain S] [inst_4 : CommRing K] [inst_5 : CommRing L] [inst_6 : Algebra R K]
  [inst_7 : Algebra S L] [inst_8 : IsFractionRing R K] [inst_9 : IsFractionRing S L] {T : Type u_9}
  [inst_10 : CommRing T] [inst_11 : IsDomain T] (M : Type u_10) [inst_12 : CommRing M] [inst_13 : Algebra T M]
  [inst_14 : IsFractionRing T M] (f : R ≃+* S) (g : S ≃+* T),
  FractionalIdeal.ringEquivOfRingEquiv K M (f.trans g) =
    (FractionalIdeal.ringEquivOfRingEquiv K L f).trans (FractionalIdeal.ringEquivOfRingEquiv L M g)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.counitIso.hom.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.symm_comp_self : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (e : M ≃ₜ* N), ⇑e.symm ∘ ⇑e = id
-- Mathlib.Analysis.InnerProductSpace.Calculus
OpenPartialHomeomorph.contDiff_unitBallBall_symm : ∀ {n : ℕ∞} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {c : E} {r : ℝ} (hr : 0 < r),
  ContDiff ℝ ↑n ↑(OpenPartialHomeomorph.unitBallBall c r hr).symm
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.valueGroupOrderIso₀_apply : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [inst_1 : Ring R] (v : Valuation R Γ₀)
  (a : WithZero ↥(MonoidWithZeroHom.ofClass Valued.v).valueGroup),
  (WithVal.valueGroupOrderIso₀ v) a = (WithZero.map' ↑(WithVal.valueGroupEquiv v)) a
-- Mathlib.Data.Num.Prime
Num.minFac_to_nat : ∀ (n : Num), ↑n.minFac = (↑n).minFac
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightShift_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ₁ γ₂ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n' + a = n),
  (γ₁ + γ₂).rightShift a n' hn' = γ₁.rightShift a n' hn' + γ₂.rightShift a n' hn'
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.instDecidablePredMemSetFixedByAddOfDecidableEq.eq_1 : ∀ {M : Type u} [inst : AddMonoid M] {β : Type u_1} [inst_1 : AddAction M β] (m : M) [inst_2 : DecidableEq β] (b : β),
  AddAction.instDecidablePredMemSetFixedByAddOfDecidableEq m b = ⋯.mpr inferInstance
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
  (h₂₁ : p₂ = p₁) (h₂₃ : p₂ = p₃),
  CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₁).inv (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq ⋯).hom
-- Mathlib.Order.Category.CompleteLat
CompleteLat.str : (self : CompleteLat) → CompleteLattice ↑self
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.comp_holderOnWith : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y]
  [inst_2 : PseudoEMetricSpace Z] {Cg rg : NNReal} {g : Y → Z},
  HolderWith Cg rg g →
    ∀ {Cf rf : NNReal} {f : X → Y} {s : Set X},
      HolderOnWith Cf rf f s → HolderOnWith (Cg * Cf ^ ↑rg) (rg * rf) (g ∘ f) s
-- Mathlib.Order.Fin.Basic
Fin.succAbove_inj : ∀ {n : ℕ} {p : Fin (n + 1)} {i j : Fin n}, p.succAbove i = p.succAbove j ↔ i = j
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetAux'.eq_1 : ∀ {α : Type u_1} (l : List α), Multiset.powersetAux' l = List.map Multiset.ofList l.sublists'
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_append : ∀ {α : Type u_1} {n m : ℕ} {β : Type u_2} {xs : Vector α n} {ys : Vector α m} {f : (i : ℕ) → α → i < n + m → β},
  (xs ++ ys).mapFinIdx f = (xs.mapFinIdx fun i a h => f i a ⋯) ++ ys.mapFinIdx fun i a h => f (i + n) a ⋯
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.mem_map_of_mem : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {x : P₁} {s : AffineSubspace k P₁},
  x ∈ s → f x ∈ AffineSubspace.map f s
-- Mathlib.Order.SuccPred.Tree
IsPredArchimedean.findAtom.congr_simp : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] [inst_3 : OrderBot α]
  [inst_4 : DecidableEq α] (r r_1 : α), r = r_1 → IsPredArchimedean.findAtom r = IsPredArchimedean.findAtom r_1
-- Std.Data.DHashMap.Raw
/-- Updates the values of the hash map by applying the given function to all mappings.  -/
Std.DHashMap.Raw.map : {α : Type u} → {β : α → Type v} → {γ : α → Type w} → ((a : α) → β a → γ a) → Std.DHashMap.Raw α β → Std.DHashMap.Raw α γ
-- Mathlib.Algebra.Category.CommAlgCat.Basic
/-- The underlying type.  -/
CommAlgCat.carrier : {R : Type u} → [inst : CommRing R] → CommAlgCat R → Type v
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.eq_bot_of_card_eq : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), Nat.card ↥H = 1 → H = ⊥
-- Mathlib.Analysis.Convex.Strict
StrictConvex.smul : ∀ {𝕜 : Type u_1} {𝕝 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : TopologicalSpace E] [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : Field 𝕝] [inst_6 : Module 𝕝 E]
  [ContinuousConstSMul 𝕝 E] [LinearMap.CompatibleSMul E E 𝕜 𝕝] {s : Set E},
  StrictConvex 𝕜 s → ∀ (c : 𝕝), StrictConvex 𝕜 (c • s)
-- Mathlib.Algebra.Algebra.Prod
AlgEquiv.prodUnique_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Unique B] (self : A × B), AlgEquiv.prodUnique self = self.1
-- Init.Data.Char.Ordinal
Char.coe_ordinal : ∀ {c : Char}, ↑c.ordinal = if c.val < 55296 then c.val.toNat else c.val.toNat - Char.numSurrogates
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂_toLinearMap₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] [inst_7 : Fintype n] [inst_8 : Fintype m]
  [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂)
  (M : Matrix n m N₂), (LinearMap.toMatrix₂ b₁ b₂) ((Matrix.toLinearMap₂ b₁ b₂) M) = M
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
FDerivMeasurableAux.D.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  (K : Set (E →L[𝕜] F)),
  FDerivMeasurableAux.D f K =
    ⋂ e,
      ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), FDerivMeasurableAux.B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insert k v},
  (m.insert k v)[a] = if h₂ : (k == a) = true then v else m[a]
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.NoRepetition.right_of_append : ∀ {α : Type u} {a : α} {l m : List α}, NoRepetition✝ a (l ++ m) → NoRepetition✝ a m
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.nil : {V : Type u} → {G : SimpleGraph V} → {u : V} → G.Walk u u
-- Mathlib.MeasureTheory.Integral.Average
/-- Average value of a function `f` w.r.t. the standard measure.

It is equal to `(volume.real univ)⁻¹ * ∫ x, f x`, so it takes value zero if `f` is not integrable
or if the space has infinite measure. In a probability space, the average of any function is equal
to its integral.

For the average on a set, use `⨍ x in s, f x`, defined as `⨍ x, f x ∂(volume.restrict s)`.  -/
MeasureTheory.«term⨍_,_» : Lean.ParserDescr
-- Mathlib.Analysis.Analytic.Constructions
/-- **Alias** of `AnalyticOnNhd.curry_right`.

---

Analytic functions on products are analytic in the second coordinate  -/
AnalyticOnNhd.along_snd : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {x : E} {s : Set (E × F)},
  AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 (fun y => f (x, y)) {y | (x, y) ∈ s}
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.nilpotencyClass_quotient_le`.

---

The nilpotency class of a quotient of `G` is less or equal the nilpotency class of `G`.  -/
nilpotencyClass_quotient_le : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.Normal] [_h : Group.IsNilpotent G],
  Group.nilpotencyClass (G ⧸ H) ≤ Group.nilpotencyClass G
-- Mathlib.Data.Fin.Tuple.Basic
Fin.val_find : ∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] (h : ∃ k, p k), ↑(Fin.find p h) = Nat.find ⋯
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toSignedMeasure_zero : ∀ {α : Type u_1} {m : MeasurableSpace α}, MeasureTheory.Measure.toSignedMeasure 0 = 0
-- Lean.Elab.BuiltinNotation
_private.Lean.Elab.BuiltinNotation.0.Lean.Elab.Term.elabRunElab.unsafe_3 : Lean.TSyntax `term → Lean.Elab.TermElabM (Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr)
-- Mathlib.RingTheory.Etale.Basic
Algebra.formallyEtale_iff : ∀ (R : Type u) (A : Type v) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.FormallyEtale R A ↔ Subsingleton Ω[A⁄R] ∧ Subsingleton (Algebra.H1Cotangent R A)
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.instLocallyOfFiniteTypeFstScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.LocallyOfFiniteType g],
  AlgebraicGeometry.LocallyOfFiniteType (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zag.of_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j₁ j₂ : J} (f : j₁ ⟶ j₂), CategoryTheory.Zag j₁ j₂
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.pow.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k.succ),
  (k = 0 → False) →
    (match k.succ with
      | 0 => h_1 ()
      | 1 => h_2 ()
      | k.succ => h_3 k) =
      h_3 k
-- Init.Data.UInt.Lemmas
UInt64.ne_iff_toBitVec_ne : ∀ {a b : UInt64}, a ≠ b ↔ a.toBitVec ≠ b.toBitVec
-- Mathlib.Algebra.Group.Commute.Defs
/-- Two elements commute if `a * b = b * a`.  -/
Commute : {S : Type u_3} → [Mul S] → S → S → Prop
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.id_natTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (x : CategoryTheory.MonoidalCategory.DayFunctor C V),
  (CategoryTheory.CategoryStruct.id x).natTrans = CategoryTheory.CategoryStruct.id x.functor
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.prod_smul_empty : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (w : HNNExtension.NormalWord d),
  HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord • HNNExtension.NormalWord.empty = w
-- Mathlib.FieldTheory.Perfect
/-- The Frobenius automorphism for a perfect ring.  -/
frobeniusEquiv : (R : Type u_1) → (p : ℕ) → [inst : CommSemiring R] → [ExpChar R p] → [PerfectRing R p] → R ≃+* R
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.seq1 : Lean.Parser.Parser
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.closure_setOfPred_lt_re`. -/
Complex.closure_setOf_lt_re : ∀ (a : ℝ), closure {z | a < z.re} = {z | a ≤ z.re}
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.pOpcycles_extendOpcyclesIso_hom : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'],
  CategoryTheory.CategoryStruct.comp ((K.extend e).pOpcycles j') (K.extendOpcyclesIso e hj').hom =
    CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom (K.pOpcycles j)