mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`.  -/
ContinuousAddEquiv.apply_symm_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (e : M ≃ₜ+ N) (y : N), e (e.symm y) = y
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.assignUnassignedLevelMVars.match_1.eq_1 : ∀ (motive : Lean.Expr × Array Lean.Expr → Sort u_1) (c₂ : Lean.Expr) (cs₂ : Array Lean.Expr)
  (h_1 : (c₂ : Lean.Expr) → (cs₂ : Array Lean.Expr) → motive (c₂, cs₂)),
  (match (c₂, cs₂) with
    | (c₂, cs₂) => h_1 c₂ cs₂) =
    h_1 c₂ cs₂
-- Mathlib.Topology.Algebra.FilterBasis
/-- If a group is endowed with a topological structure coming from a group filter basis then, it's a
topological group.  -/
GroupFilterBasis.isTopologicalGroup : ∀ {G : Type u} [inst : Group G] (B : GroupFilterBasis G), IsTopologicalGroup G
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- Postcomposing `f` with `Prod.snd` is `C^n` at `x`  -/
ContDiffAt.snd : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F × G} {x : E},
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n (fun x => (f x).2) x
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.minimizeGlobalIdentifierInContext : Lean.Name → List Lean.OpenDecl → Lean.Name → Lean.Name
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.martingale_of_condExp_sub_eq_zero_nat : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝒢 : MeasureTheory.Filtration ℕ m0} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ]
  {f : ℕ → Ω → E},
  MeasureTheory.StronglyAdapted 𝒢 f →
    (∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
      (∀ (i : ℕ), μ[f (i + 1) - f i | ↑𝒢 i] =ᵐ[μ] 0) → MeasureTheory.Martingale f 𝒢 μ
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.errorName.injEq : ∀ (stx partialId stx_1 partialId_1 : Lean.Syntax),
  (Lean.Elab.CompletionInfo.errorName stx partialId = Lean.Elab.CompletionInfo.errorName stx_1 partialId_1) =
    (stx = stx_1 ∧ partialId = partialId_1)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.weekdayOfIndex : ℕ → Std.Time.Weekday
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.invFun_monomial : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (n : ℕ) (a : A),
  PolyEquivTensor.invFun R A ((Polynomial.monomial n) a) = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] Polynomial.X ^ n
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x : C) {y z : D} (f : y ≅ z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f.hom)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f.inv) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x y)
-- Mathlib.Algebra.GroupWithZero.Associated
/-- The canonical quotient map from a monoid `M` into the `Associates` of `M`  -/
Associates.mk : {M : Type u_2} → [inst : Monoid M] → M → Associates M
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instIsRightCancelMul : ∀ {α : Type u_1} [inst : Mul α] [IsRightCancelMul α], IsRightCancelMul (Colex α)
-- Lean.Data.PersistentHashMap
_private.Lean.Data.PersistentHashMap.0.Lean.PersistentHashMap.insertAux.traverse : {α : Type u_1} →
  {β : Type u_2} →
    [BEq α] →
      [Hashable α] →
        USize →
          (keys : Array α) →
            (vals : Array β) →
              keys.size = vals.size → ℕ → Lean.PersistentHashMap.Node α β → Lean.PersistentHashMap.Node α β
-- Mathlib.Order.Heyting.Hom
BiheytingHom.coe_id : ∀ (α : Type u_2) [inst : BiheytingAlgebra α], ⇑(BiheytingHom.id α) = id
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctorStruct.mk.injEq : ∀ {B : Type u₁} [inst : Quiver B] [inst_1 : (a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [inst_2 : Quiver C]
  [inst_3 : (a b : C) → Quiver (a ⟶ b)] (toPrefunctor : B ⥤q C)
  (map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (toPrefunctor.map f ⟶ toPrefunctor.map g)) (toPrefunctor_1 : B ⥤q C)
  (map₂_1 : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (toPrefunctor_1.map f ⟶ toPrefunctor_1.map g)),
  ({ toPrefunctor := toPrefunctor, map₂ := map₂ } = { toPrefunctor := toPrefunctor_1, map₂ := map₂_1 }) =
    (toPrefunctor = toPrefunctor_1 ∧ map₂ ≍ map₂_1)
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.univUnitBall_apply_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E], ↑OpenPartialHomeomorph.univUnitBall 0 = 0
-- Mathlib.Data.Nat.Sqrt
Nat.eq_sqrt' : ∀ {n a : ℕ}, a = n.sqrt ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2
-- Mathlib.Algebra.Regular.Defs
IsAddLeftRegular.eq_1 : ∀ {R : Type u_1} [inst : Add R] (c : R), IsAddLeftRegular c = Function.Injective fun x => c + x
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `DifferentiableWithinAt.fun_finsetProd`. -/
DifferentiableWithinAt.fun_finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} {𝔸' : Type u_3}
  [inst_1 : NormedCommRing 𝔸'] [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) → DifferentiableWithinAt 𝕜 (fun x => ∏ i ∈ u, f i x) s x
-- Mathlib.RingTheory.FiniteType
RingHom.FiniteType.comp_surjective : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  {f : A →+* B} {g : B →+* C}, f.FiniteType → Function.Surjective ⇑g → (g.comp f).FiniteType
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.quotQuotUliftAddEquiv.eq_1 : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : DecidableEq J],
  AddCommGrpCat.Colimits.quotQuotUliftAddEquiv F =
    { toFun := ⇑(AddCommGrpCat.Colimits.quotToQuotUlift F), invFun := ⇑(AddCommGrpCat.Colimits.quotUliftToQuot F),
      left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateIsoEquiv_apply_hom : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (α : L₂ ≅ L₁), ((CategoryTheory.conjugateIsoEquiv adj₁ adj₂) α).hom = (CategoryTheory.conjugateEquiv adj₁ adj₂) α.hom
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.rootMultiplicity_mul : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {p q : Polynomial R} {x : R},
  p * q ≠ 0 → Polynomial.rootMultiplicity x (p * q) = Polynomial.rootMultiplicity x p + Polynomial.rootMultiplicity x q
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instFromJsonDiagnosticCode : Lean.FromJson Lean.Lsp.DiagnosticCode
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.ofIsoSelf_inv : ∀ {R : Type u} [inst : CommRing R] (A : CommHopfAlgCat R), A.ofIsoSelf.inv = CategoryTheory.CategoryStruct.id A
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.map_Ψ₃ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) (f : R →+* S),
  (W.map f).Ψ₃ = Polynomial.map f W.Ψ₃
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_mul_iff_isBigO_div : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {f g h : α → 𝕜},
  (∀ᶠ (x : α) in l, f x ≠ 0) → ((fun x => f x * g x) =O[l] h ↔ g =O[l] fun x => h x / f x)
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.imp_inf : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ θ : L.BoundedFormula α n},
  T.Imp φ ψ → T.Imp φ θ → T.Imp φ (ψ ⊓ θ)
-- Mathlib.Topology.Instances.Rat
Rat.uniformContinuous_neg : UniformContinuous Neg.neg
-- Mathlib.Order.BooleanAlgebra.Set
Set.inter_sdiff_distrib_left : ∀ {α : Type u_1} (s t u : Set α), s ∩ (t \ u) = (s ∩ t) \ (s ∩ u)
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.lt_def : ∀ {E : Type u_3} [inst : AddGroup E] {p q : NonarchAddGroupSeminorm E}, p < q ↔ ⇑p < ⇑q
-- Batteries.Data.List.Pairwise
List.pwFilter_cons_of_neg : ∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] {a : α} {l : List α},
  (¬∀ b ∈ List.pwFilter R l, R a b) → List.pwFilter R (a :: l) = List.pwFilter R l
-- Mathlib.Data.EReal.Basic
EReal.coe_strictMono : StrictMono Real.toEReal
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instInhabitedPreDiscrTree.default : {α : Type} → Lean.Meta.LazyDiscrTree.PreDiscrTree α
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.instIsNoetherianCotangentOfSubtypeMem : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [IsNoetherian R ↥I], IsNoetherian R I.Cotangent
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.transpose.eq_1 : ∀ (μ : YoungDiagram), μ.transpose = { cells := (Equiv.prodComm ℕ ℕ).finsetCongr μ.cells, isLowerSet := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.variableChange_a₃ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R),
  (C • W).a₃ = ↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)
-- Init.SimpLemmas
false_iff : ∀ (p : Prop), (False ↔ p) = ¬p
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.Eqv.add_comm : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x y : FreeAddMonoid (M × N)),
  TensorProduct.Eqv R M N (x + y) (y + x)
-- Mathlib.Algebra.Group.Defs
NPow.ofPow.eq_1 : ∀ {M : Type u_2} [inst : Pow M ℕ], NPow.ofPow = { npow := fun n x => Pow.pow x n }
-- Mathlib.Analysis.Normed.Group.HomCompletion
/-- The normed group hom induced between completions.  -/
NormedAddGroupHom.completion : {G : Type u_1} →
  [inst : SeminormedAddCommGroup G] →
    {H : Type u_2} →
      [inst_1 : SeminormedAddCommGroup H] →
        NormedAddGroupHom G H → NormedAddGroupHom (UniformSpace.Completion G) (UniformSpace.Completion H)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- Being filtered is preserved by equivalence of categories.  -/
CategoryTheory.IsFiltered.of_equivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (h : C ≌ D), CategoryTheory.IsFiltered D
-- Mathlib.Geometry.Manifold.StructureGroupoid
instInhabitedStructureGroupoid : {H : Type u_1} → [inst : TopologicalSpace H] → Inhabited (StructureGroupoid H)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_eq : ∀ (z : ℂ), Complex.cos z = Complex.cos ↑z.re * Complex.cosh ↑z.im - Complex.sin ↑z.re * Complex.sinh ↑z.im * Complex.I
-- Mathlib.Algebra.Group.Prod
Prod.instSubtractionMonoid : {G : Type u_1} → {H : Type u_2} → [SubtractionMonoid G] → [SubtractionMonoid H] → SubtractionMonoid (G × H)
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.CommSq.shortComplex'_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄}
  (sq : CategoryTheory.CommSq fst snd f g), sq.shortComplex'.g = CategoryTheory.Limits.biprod.desc f (-g)
-- Mathlib.Topology.Algebra.InfiniteSum.Field
Multipliable.norm_tprod : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedCommRing E] [NormMulClass E] [NormOneClass E] {f : α → E},
  Multipliable f → ‖∏' (i : α), f i‖ = ∏' (i : α), ‖f i‖
-- Mathlib.RingTheory.Etale.Basic
Algebra.Etale.finitePresentation : ∀ {R : Type u} {A : Type v} {inst : CommRing R} {inst_1 : CommRing A} {inst_2 : Algebra R A} [self : Algebra.Etale R A],
  Algebra.FinitePresentation R A
-- Mathlib.Analysis.Convex.Gauge
setOfPred_gauge_lt_one_eq_interior : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], Convex ℝ s → s ∈ nhds 0 → {x | gauge s x < 1} = interior s
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.preimage_le : ∀ {G : GrpCat} {P : ProfiniteGrp.{u}} {f : G ⟶ GrpCat.of ↑P.toProfinite.toTop}
  {H K : OpenNormalSubgroup ↑P.toProfinite.toTop},
  H ≤ K → ProfiniteGrp.ProfiniteCompletion.preimage f H ≤ ProfiniteGrp.ProfiniteCompletion.preimage f K
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_eq_some_getD : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {fallback : β},
  a ∈ m → Std.ExtDHashMap.Const.get? m a = some (Std.ExtDHashMap.Const.getD m a fallback)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.tmul_one_mul_coe_tmul : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] {i₂ : ι} (a₁ : A) (a₂ : ↥(𝒜 i₂)) (b₂ : B),
  a₁ ᵍ⊗ₜ[R] 1 * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] b₂
-- Init.Omega.IntList
/-- The sum of the entries of an `IntList`.  -/
Lean.Omega.IntList.sum : Lean.Omega.IntList → ℤ
-- Mathlib.Algebra.Lie.Free
_private.Mathlib.Algebra.Lie.Free.0.«termLib.lift_comp_of» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instInitiallySmallElementsFiberOfIsCofiltered : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] [CategoryTheory.IsCofiltered N],
  CategoryTheory.InitiallySmall (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber p).Elements
-- Mathlib.Topology.Algebra.ConstMulAction
isClosed_setOfPred_map_smul : ∀ {M : Type u_1} {N : Type u_4} (α : Type u_5) (β : Type u_6) [inst : SMul M α] [inst_1 : SMul N β]
  [inst_2 : TopologicalSpace β] [T2Space β] [ContinuousConstSMul N β] (σ : M → N),
  IsClosed {f | ∀ (c : M) (x : α), f (c • x) = σ c • f x}
-- Mathlib.Algebra.Lie.Basic
sub_lie : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x y : L) (m : M),
  ⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Subgroup.subgroupOfContinuousMulEquivOfLe_toMulEquiv : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {H K : Subgroup G} (hHK : H ≤ K),
  ↑(Subgroup.subgroupOfContinuousMulEquivOfLe hHK) = Subgroup.subgroupOfEquivOfLe hHK
-- Mathlib.FieldTheory.Minpoly.Field
/-- A minimal polynomial is prime.  -/
minpoly.prime : ∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [IsDomain B] [inst_3 : Algebra A B] {x : B},
  IsIntegral A x → Prime (minpoly A x)
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.State.writingBodyFixed.injEq : ∀ (n n_1 : ℕ),
  (Std.Http.Protocol.H1.Writer.State.writingBodyFixed n = Std.Http.Protocol.H1.Writer.State.writingBodyFixed n_1) =
    (n = n_1)
-- Mathlib.Order.Basic
not_lt_of_subsingleton : ∀ {α : Type u_2} [inst : Preorder α] {a b : α} [Subsingleton α], ¬a < b
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.isVonNBounded_iff_seminorm_bddAbove : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [inst_3 : TopologicalSpace E] {s : Set E},
  WithSeminorms p → (Bornology.IsVonNBounded 𝕜 s ↔ ∀ (i : ι), BddAbove (⇑(p i) '' s))
-- Init.Data.Array.Int
Array.min_mul_length_le_sum_int : ∀ {xs : Array ℤ} (h : xs ≠ #[]), xs.min h * ↑xs.size ≤ xs.sum
-- Init.Data.List.Sublist
List.reverse_subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse ⊆ l₂ ↔ l₁ ⊆ l₂
-- Mathlib.Topology.Maps.OpenQuotient
Topology.IsInducing.isOpenQuotientMap_of_surjective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsInducing f → Function.Surjective f → IsOpenQuotientMap f
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for strict reverse monotonicity of multiplication on the left,
namely `a * b₁ < a * b₂ → b₁ < b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedMonoid`.  -/
MulLeftReflectLT : (M : Type u_1) → [Mul M] → [LT M] → Prop
-- Mathlib.CategoryTheory.Triangulated.Adjunction
CategoryTheory.Adjunction.IsTriangulated.commShift : ∀ {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} {inst_2 : CategoryTheory.Limits.HasZeroObject C}
  {inst_3 : CategoryTheory.Limits.HasZeroObject D} {inst_4 : CategoryTheory.Preadditive C}
  {inst_5 : CategoryTheory.Preadditive D} {inst_6 : CategoryTheory.HasShift C ℤ} {inst_7 : CategoryTheory.HasShift D ℤ}
  {inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive}
  {inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive} {inst_10 : CategoryTheory.Pretriangulated C}
  {inst_11 : CategoryTheory.Pretriangulated D} {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {adj : F ⊣ G} {inst_12 : F.CommShift ℤ} {inst_13 : G.CommShift ℤ} [self : adj.IsTriangulated], adj.CommShift ℤ
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Copy of an oplax monoidal structure on a functor `F` with new `η` and `δ` fields equal to the
old ones.

This is useful to fix definitional equalities.  -/
CategoryTheory.Functor.OplaxMonoidal.copy : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (hF : F.OplaxMonoidal) →
                (η' :
                    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
                      CategoryTheory.MonoidalCategoryStruct.tensorUnit D) →
                  (δ' :
                      (X Y : C) →
                        F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶
                          CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) →
                    autoParam (η' = CategoryTheory.Functor.OplaxMonoidal.η F)
                        CategoryTheory.Functor.OplaxMonoidal.copy._auto_1 →
                      autoParam (δ' = CategoryTheory.Functor.OplaxMonoidal.δ F)
                          CategoryTheory.Functor.OplaxMonoidal.copy._auto_3 →
                        F.OplaxMonoidal
-- Mathlib.Topology.Order.Hom.Esakia
instCoeTCEsakiaHomOfEsakiaHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : TopologicalSpace α] →
          [inst_2 : Preorder α] →
            [inst_3 : TopologicalSpace β] → [inst_4 : Preorder β] → [EsakiaHomClass F α β] → CoeTC F (EsakiaHom α β)
-- Mathlib.Probability.Independence.CharacteristicFunction
/-- Two random variables are independent if and only if their joint characteristic function is equal
to the product of the characteristic functions. This is `indepFun_iff_charFunDual_prod` for
`WithLp`. See `indepFun_iff_charFun_prod` for the Hilbert space version.  -/
ProbabilityTheory.indepFun_iff_charFunDual_prod' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (p : ENNReal) [inst : Fact (1 ≤ p)]
  [MeasureTheory.IsFiniteMeasure P] {E : Type u_2} {F : Type u_3} {mE : MeasurableSpace E}
  [inst_2 : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {mF : MeasurableSpace F}
  [inst_5 : NormedAddCommGroup F] [CompleteSpace F] [BorelSpace F] [SecondCountableTopology F] {X : Ω → E} {Y : Ω → F}
  [inst_9 : NormedSpace ℝ E] [inst_10 : NormedSpace ℝ F] [CompleteSpace E],
  AEMeasurable X P →
    AEMeasurable Y P →
      (ProbabilityTheory.IndepFun X Y P ↔
        ∀ (L : StrongDual ℝ (WithLp p (E × F))),
          MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun ω => WithLp.toLp p (X ω, Y ω)) P) L =
            MeasureTheory.charFunDual (MeasureTheory.Measure.map X P)
                (L ∘SL ↑(WithLp.prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inl ℝ E F) *
              MeasureTheory.charFunDual (MeasureTheory.Measure.map Y P)
                (L ∘SL ↑(WithLp.prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inr ℝ E F))
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.Pivot.listTransvecCol_getElem : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) {i : ℕ}
  (h : i < (Matrix.Pivot.listTransvecCol M).length),
  (Matrix.Pivot.listTransvecCol M)[i] =
    Matrix.transvection (Sum.inl ⟨i, ⋯⟩) (Sum.inr ()) (-M (Sum.inl ⟨i, ⋯⟩) (Sum.inr ()) / M (Sum.inr ()) (Sum.inr ()))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.lift_fst_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd =
    CategoryTheory.CategoryStruct.id (X ⨯ Y)
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- A closed ball centred at the origin in a valued ring is open.  -/
Valued.isOpen_closedBall : ∀ (R : Type u) [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀]
  {r : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀}, r ≠ 0 → IsOpen {x | Valued.v.restrict x ≤ r}
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E / F` is an algebraic extension, then the separable closure of `F` in `E` is
equal to `F` if and only if `E / F` is purely inseparable.  -/
separableClosure.eq_bot_iff : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E],
  separableClosure F E = ⊥ ↔ IsPurelyInseparable F E
-- Init.NotationExtra
Lean.expandBracketedBinders : Lean.Name → Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
MvPolynomial.algebraicIndependent_X : ∀ (σ : Type u_3) (R : Type u_4) [inst : CommRing R], AlgebraicIndependent R MvPolynomial.X
-- Mathlib.Algebra.Category.Grp.Limits
/-- The flat sections of a functor into `AddGrpCat` form an additive subgroup of all sections.  -/
AddGrpCat.sectionsAddSubgroup : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddGrpCat) → AddSubgroup ((j : J) → ↑(F.obj j))
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_add_of_add_pos : ∀ {x : ENNReal}, x ≠ ⊤ → ∀ (y z : ℝ), 0 < y + z → x ^ (y + z) = x ^ y * x ^ z
-- Mathlib.Algebra.Notation.Defs
/-- Type class for the `+ᵥ` notation.  -/
VAdd : Type u → Type v → Type (max u v)
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_restrictScalars : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_3} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {B : Type u_4}
  [inst_3 : Ring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R B] [inst_6 : Algebra S B]
  [inst_7 : IsScalarTower R S B] {C : Type u_5} [inst_8 : Ring C] [inst_9 : TopologicalSpace C] [inst_10 : Algebra R C]
  [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C] (f : B →A[S] C),
  ↑(ContinuousAlgHom.restrictScalars R f) = AlgHom.restrictScalars R ↑f