mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
/-- If `a.card ≤ b.card`, then the hypergeometric series has infinite convergence radius.  -/
Complex.radius_regularizedHGFunSeries_eq_top : ∀ {a b : Multiset ℂ}, a.card ≤ b.card → (Complex.regularizedHGFunSeries a b).radius = ⊤
-- Mathlib.Order.WellFoundedSet
Set.WellFoundedOn.insert : ∀ {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α},
  s.WellFoundedOn r → ∀ (a : α), (insert a s).WellFoundedOn r
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_actionHomRight : ∀ {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.MonoidalRightAction C D] (x : D) {y z : C} (f : y ⟶ z)
  [inst_4 : CategoryTheory.IsIso f],
  CategoryTheory.inv (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f) =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x (CategoryTheory.inv f)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft' : ∀ {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.MonoidalRightAction C D] {x y : D} (f : x ⟶ y)
  [inst_4 : CategoryTheory.IsIso f] (z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f z)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (CategoryTheory.inv f) z) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj x z)
-- Std.Http.Protocol.H1.Parser
/-- Parses fixed-size data that can be incomplete.
 -/
Std.Http.Protocol.H1.parseFixedSizeData : ℕ → Std.Internal.Parsec.ByteArray.Parser Std.Http.Protocol.H1.TakeResult
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_le_of_le_ofReal : ∀ {a : ENNReal} {b : ℝ}, 0 ≤ b → a ≤ ENNReal.ofReal b → a.toReal ≤ b
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsZeroOrMarkovKernel κ] (f : β → γ),
  ProbabilityTheory.IsZeroOrMarkovKernel (κ.map f)
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.RealizeValueResult.mk.inj : ∀ {res? : Except Lean.Exception Dynamic} {snap? : Option Lean.Language.SnapshotTree}
  {res?_1 : Except Lean.Exception Dynamic} {snap?_1 : Option Lean.Language.SnapshotTree},
  { res? := res?, snap? := snap? } = { res? := res?_1, snap? := snap?_1 } → res? = res?_1 ∧ snap? = snap?_1
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_two_pow : ∀ {n m : ℕ}, (2 ^ n).testBit m = decide (n = m)
-- Mathlib.Order.InitialSeg
/-- For any principal segment `r ≺i s`, there is a `Subrel` of `s` order isomorphic to `r`.  -/
PrincipalSeg.subrelIso : {α : Type u_1} →
  {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → (f : PrincipalSeg r s) → (Subrel s fun x => s x f.top) ≃r r
-- Std.Time.Date.PlainDate
Std.Time.instOrdPlainDate : Ord Std.Time.PlainDate
-- Mathlib.Logic.Function.Defs
Function.prod_inj : ∀ {ι : Sort u_3} {α : ι → Type u_1} {β : ι → Type u_2} {f f' : (i : ι) → α i} {g g' : (i : ι) → β i},
  Function.prod f g = Function.prod f' g' ↔ f = f' ∧ g = g'
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.one.injEq : ∀ (name name_1 : Lean.TSyntax `Lean.binderIdent),
  (Lean.Parser.Tactic.MRefinePat.one name = Lean.Parser.Tactic.MRefinePat.one name_1) = (name = name_1)
-- Lean.Parser.Do
/-- `break` exits the surrounding `for` loop.  -/
Lean.Parser.Term.doBreak : Lean.Parser.Parser
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioo_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Ioo a b)), Subtype.val '' Set.Iio c = Set.Ioo a ↑c
-- Mathlib.Order.Basic
Ne.not_le_or_not_ge : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≠ b → ¬a ≤ b ∨ ¬b ≤ a
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.homOfEq_map_homOfEq : ∀ {V W : Type u} [inst : Quiver V] [inst_1 : Quiver W] (e : V ≃ W) (he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)) {X Y : V}
  (f : X ⟶ Y) {X' Y' : V} (hX : X = X') (hY : Y = Y') {X'' Y'' : W} (hX' : e X' = X'') (hY' : e Y' = Y''),
  Quiver.homOfEq ((he X' Y') (Quiver.homOfEq f hX hY)) hX' hY' = Quiver.homOfEq ((he X Y) f) ⋯ ⋯
-- Init.Data.Vector.Count
Vector.count_singleton_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α}, Vector.count a #v[a] = 1
-- Mathlib.Data.Num.ZNum
ZNum.of_natCast : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (n : ℕ), ↑↑n = ↑n
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_bot : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : Bot β], ↑⊥ = ⊥
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.lift.eq_1 : ∀ {α : Type u} [inst : Add α] {β : Type v} [inst_1 : AddSemigroup β],
  AddMagma.FreeAddSemigroup.lift =
    { toFun := fun f => { toFun := fun x => Quot.liftOn x ⇑f ⋯, map_add' := ⋯ },
      invFun := fun f => f.comp AddMagma.FreeAddSemigroup.of, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Topology.Gluing
TopCat.GlueData.rel_equiv : ∀ (D : TopCat.GlueData), Equivalence D.Rel
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.sub_add_cancel : ∀ {M : Type u} [inst : Lean.Grind.AddCommGroup M] {a b : M}, a - b + b = a
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.mk_eq_zero : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M)
  {x : M} (h : x ∈ p), ⟨x, h⟩ = 0 ↔ x = 0
-- Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions
/-- The main result, *Legendre's Theorem* on rational approximation:
if `ξ` is a real number and `q` is a rational number such that `|ξ - q| < 1/(2*q.den^2)`,
then `q` is a convergent of the continued fraction expansion of `ξ`.
This is the version using `GenContFract.convs`.  -/
Real.exists_convs_eq_rat : ∀ {ξ : ℝ} {q : ℚ}, |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2) → ∃ n, (GenContFract.of ξ).convs n = ↑q
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mergeAll?.match_1.splitter : (motive : Option (Lean.TSyntax `tactic) → Sort u_1) →
  (x : Option (Lean.TSyntax `tactic)) →
    ((tac' : Lean.TSyntax `tactic) → motive (some tac')) →
      ((x : Option (Lean.TSyntax `tactic)) → (∀ (tac' : Lean.TSyntax `tactic), x = some tac' → False) → motive x) →
        motive x
-- Mathlib.CategoryTheory.Monoidal.Linear
CategoryTheory.MonoidalLinear.smul_whiskerRight : ∀ {R : Type u_1} {inst : Semiring R} {C : Type u_2} {inst_1 : CategoryTheory.Category.{v_1, u_2} C}
  {inst_2 : CategoryTheory.Preadditive C} {inst_3 : CategoryTheory.Linear R C}
  {inst_4 : CategoryTheory.MonoidalCategory C} {inst_5 : CategoryTheory.MonoidalPreadditive C}
  [self : CategoryTheory.MonoidalLinear R C] (r : R) {Y Z : C} (f : Y ⟶ Z) (X : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (r • f) X =
    r • CategoryTheory.MonoidalCategoryStruct.whiskerRight f X
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiffUnion : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C)
  (hI : ↑I ⊆ C), (↑(hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.roots_X_pow_card_sub_X : ∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K],
  (Polynomial.X ^ Fintype.card K - Polynomial.X).roots = Finset.univ.val
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ofCoeff_eq_one : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddMonoidWithOne k] {a : G →₀ k},
  { coeff := a } = 1 ↔ a = fun₀ | 1 => 1
-- Mathlib.Logic.Equiv.Defs
/-- `PLift α` is equivalent to `α`.  -/
Equiv.plift : {α : Sort u} → PLift α ≃ α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)], k ∉ m₂ → (m₁ ∩ m₂).get! k = default
-- Aesop.Rule.Name
Aesop.instInhabitedDisplayRuleName : Inhabited Aesop.DisplayRuleName
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_mono : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {g : M → M'}
  {s t : Set M} {x : M},
  (∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x) →
    ChartedSpace.LiftPropWithinAt P g s x → t ⊆ s → ChartedSpace.LiftPropWithinAt P g t x
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_X_pow_succ : ∀ {R : Type u} [inst : Semiring R] (n : ℕ),
  Polynomial.derivative (Polynomial.X ^ (n + 1)) = Polynomial.C (↑n + 1) * Polynomial.X ^ n
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.isDetpBalanced_iff_sub_mul_det_eq_zero : ∀ {n : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_4} [inst_2 : CommRing R] {A : Matrix n n R}
  {a b : R}, A.IsDetpBalanced a b ↔ (a - b) * A.det = 0
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
polarCoord_source : polarCoord.source = {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
-- Init.Core
/-- `HasEquiv α` is the typeclass which supports the notation `x ≈ y` where `x y : α`. -/
HasEquiv : Sort u → Sort (max u (v + 1))
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instAddCommMonoidCoeOfAddSubmonoidClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → AddCommMonoid (R i)] [inst_2 : ∀ (i : ι), AddSubmonoidClass (S i) (R i)],
  RestrictedProduct.instAddCommMonoidCoeOfAddSubmonoidClass R = Function.Injective.addCommMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Vertex.HVertexOperator
/-- Given a coefficient function valued in linear maps satisfying a partially well-ordered support
condition, we produce a heterogeneous vertex operator.  -/
HVertexOperator.of_coeff : {Γ : Type u_1} →
  [inst : PartialOrder Γ] →
    {R : Type u_2} →
      {V : Type u_3} →
        {W : Type u_4} →
          [inst_1 : CommRing R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : Module R V] →
                [inst_4 : AddCommGroup W] →
                  [inst_5 : Module R W] →
                    (f : Γ → V →ₗ[R] W) →
                      (∀ (x : V), (Function.support fun x_1 => (f x_1) x).IsPWO) → HVertexOperator Γ R V W
-- Mathlib.Algebra.MvPolynomial.Degrees
/-- The submodule of multivariate polynomials of degrees bounded by a monomial `s`.  -/
MvPolynomial.degreesLE : (R : Type u) → (σ : Type u_1) → [inst : CommSemiring R] → Multiset σ → Submodule R (MvPolynomial σ R)
-- Aesop.Builder.Basic
/-- Options for the builders. Most options are only relevant for certain builders.
 -/
Aesop.RuleBuilderOptions : Type
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.imp_top : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n), T.Imp φ ⊤
-- Lean.Linter.Deprecated
Lean.Linter.instInhabitedDeprecationEntry : Inhabited Lean.Linter.DeprecationEntry
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.reindex_toGenerators : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Presentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ),
  (P.reindex e f).toGenerators = P.reindex e
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsMonHom.instNormalOfIsCommMonObjOfMono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H] {φ : H ⟶ G}
  [inst_4 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommMonObj G] [CategoryTheory.IsMonHom φ]
  [CategoryTheory.Mono φ], CategoryTheory.IsMonHom.Normal φ
-- Mathlib.Topology.Algebra.IsUniformGroup.Order
/-- If a sequence of functions converges uniformly on a set to a function `g` which is bounded above
by a value `u`, then the sequence is strictly bounded by any `v` such that `u < v`.  -/
TendstoUniformlyOn.eventually_forall_lt : ∀ {α : Type u_1} {ι : Type u_2} {β : Type u_3} [inst : UniformSpace β] [inst_1 : AddGroup β] [IsUniformAddGroup β]
  [inst_3 : PartialOrder β] [OrderTopology β] [AddLeftMono β] [AddRightMono β] {f : ι → α → β} {g : α → β} {K : Set α}
  {p : Filter ι} {u v : β},
  u < v → TendstoUniformlyOn f g p K → (∀ x ∈ K, g x ≤ u) → ∀ᶠ (i : ι) in p, ∀ x ∈ K, f i x < v
-- Mathlib.LinearAlgebra.TensorProduct.Associator
LinearMap.rTensor_lTensor_comp_assoc_symm : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R Q] [inst_8 : Module R P] (x : M →ₗ[R] N),
  LinearMap.rTensor Q (LinearMap.lTensor P x) ∘ₗ ↑(TensorProduct.assoc R P M Q).symm =
    ↑(TensorProduct.assoc R P N Q).symm ∘ₗ LinearMap.lTensor P (LinearMap.rTensor Q x)
-- Std.Http.Server.Config
/-- Maximum length of header field name (default: 256 bytes)
 -/
Std.Http.Config.maxHeaderNameLength : Std.Http.Config → ℕ
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trNormal.eq_6 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (dec : List.Vector Bool n → Γ),
  Turing.TM1to1.trNormal dec Turing.TM1.Stmt.halt = Turing.TM1.Stmt.halt
-- Mathlib.FieldTheory.SeparableDegree
/-- The separable degree of a non-zero polynomial is equal to its degree if and only if
it is separable.  -/
Polynomial.natSepDegree_eq_natDegree_iff : ∀ {F : Type u} [inst : Field F] (f : Polynomial F), f ≠ 0 → (f.natSepDegree = f.natDegree ↔ f.Separable)
-- Init.Data.List.MinMaxOn
List.maxOn_cons : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {x : α} {xs : List α}
  {f : α → β}, List.maxOn f (x :: xs) ⋯ = if h : xs = [] then x else maxOn f x (List.maxOn f xs h)
-- Batteries.Lean.LawfulMonadLift
instLawfulMonadLiftTTermElabMTacticM_batteries : LawfulMonadLiftT Lean.Elab.TermElabM Lean.Elab.Tactic.TacticM
-- Mathlib.RingTheory.Ideal.UFD
/-- Let `R` be a Noetherian domain, `x ∈ R` be a prime element. Then `R` is a UFD if and only if
`Rₓ` is a UFD.  -/
UniqueFactorizationMonoid.iff_localizationAway_of_prime : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsNoetherianRing R] {x : R},
  Prime x → (UniqueFactorizationMonoid R ↔ UniqueFactorizationMonoid (Localization.Away x))
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instInhabitedFunctionTheorem.default : Mathlib.Meta.FunProp.FunctionTheorem
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousOn_neg_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β], UpperSemicontinuousOn (-f) s ↔ LowerSemicontinuousOn f s
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- **Alias** of `PeriodPair.isOpen_compl_lattice_sdiff`. -/
PeriodPair.isOpen_compl_lattice_diff : ∀ (L : PeriodPair) {s : Set ℂ}, IsOpen (↑L.lattice \ s)ᶜ
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_le_subst_nonneg_cert.eq_1 : ∀ (x : Int.Internal.Linear.Var) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_le_subst_nonneg_cert x p₁ p₂ p₃ =
    (Int.ble' 0 (p₁.coeff x)).and' (p₃.beq' (Int.Internal.Linear.Poly.combine_mul_k (p₁.coeff x) (-p₂.coeff x) p₂ p₁))
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- **Alias** of the forward direction of `locallyLipschitzOn_iff_restrict`. -/
LocallyLipschitzOn.restrict : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {s : Set α} {f : α → β},
  LocallyLipschitzOn s f → LocallyLipschitz (s.domRestrict f)
-- Mathlib.CategoryTheory.Square
/-- The functor `Square C ⥤ Arrow (Arrow C)` which sends a
commutative square `sq` to the obvious arrow from the left morphism of `sq`
to the right morphism of `sq`.  -/
CategoryTheory.Square.toArrowArrowFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.Square C) (CategoryTheory.Arrow (CategoryTheory.Arrow C))
-- Mathlib.Topology.Algebra.Module.LinearPMap
LinearPMap.closure.eq_1 : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] (f : E →ₗ.[R] F), f.closure = if hf : f.IsClosable then Exists.choose hf else f
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.imageMonoidHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] [inst_4 : FunLike F α β] [inst_5 : MonoidHomClass F α β] (f : F) (a : Finset α),
  (Finset.imageMonoidHom f) a = (Finset.imageMulHom f).toFun a
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.CofixA.brecOn.eq : ∀ {F : PFunctor.{uA, uB}} {motive : (a : ℕ) → PFunctor.Approx.CofixA F a → Sort u} {a : ℕ}
  (t : PFunctor.Approx.CofixA F a)
  (F_1 : (a : ℕ) → (t : PFunctor.Approx.CofixA F a) → PFunctor.Approx.CofixA.below t → motive a t),
  PFunctor.Approx.CofixA.brecOn t F_1 = F_1 a t (PFunctor.Approx.CofixA.brecOn.go t F_1).2
-- Init.Data.Vector.Lemmas
Vector.forM_mk : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} [inst : Monad m] {f : α → m PUnit.{u_1 + 1}} {xs : Array α}
  (h : xs.size = n), forM (Vector.mk xs h) f = forM xs f
-- Lean.Parser.Command
Lean.Parser.Command.tactic_extension.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_eq_iSup_addOrderOf' : ∀ {G : Type u} [inst : AddCommMonoid G], AddMonoid.exponent G = if ∃ g, addOrderOf g = 0 then 0 else ⨆ g, addOrderOf g
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
/-- **Alias** of `le_add_of_le_right`. -/
le_add_left : ∀ {α : Type u} [inst : Add α] [inst_1 : Preorder α] [CanonicallyOrderedAdd α] {a b c : α}, a ≤ c → a ≤ b + c
-- Mathlib.Algebra.Group.Defs
AddLeftCancelMonoid.toIsLeftCancelAdd : ∀ {M : Type u} [self : AddLeftCancelMonoid M], IsLeftCancelAdd M
-- Mathlib.Topology.Hom.Open
/-- The type of continuous open maps from `α` to `β`, aka Priestley homomorphisms.  -/
ContinuousOpenMap : (α : Type u_6) → (β : Type u_7) → [TopologicalSpace α] → [TopologicalSpace β] → Type (max u_6 u_7)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.opNorm_pi : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_3 : Fintype ι]
  {ι' : Type v'} [inst_4 : Fintype ι'] {E' : ι' → Type wE'} [inst_5 : (i' : ι') → SeminormedAddCommGroup (E' i')]
  [inst_6 : (i' : ι') → NormedSpace 𝕜 (E' i')] (f : (i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')),
  ‖ContinuousMultilinearMap.pi f‖ = ‖f‖
-- Mathlib.Data.Finset.Basic
Finset.univ_finset_eq_singleton_empty_iff : ∀ {α : Type u_4}, Set.univ = {∅} ↔ IsEmpty α
-- Mathlib.LinearAlgebra.TensorPower.Basic
_private.Mathlib.LinearAlgebra.TensorPower.Basic.0.TensorPower.termₜ1 : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPushout.inl_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G]
  [inst_3 : CategoryTheory.Limits.HasPushout f g] [inst_4 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (G.map f) (G.map g))
      (CategoryTheory.Limits.PreservesPushout.iso G f g).hom =
    G.map (CategoryTheory.Limits.pushout.inl f g)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Eq
Std.Tactic.BVDecide.BVPred.mkEq.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (pair : aig.BinaryRefVec w),
  Std.Tactic.BVDecide.BVPred.mkEq aig pair =
    Std.Sat.AIG.RefVec.fold (Std.Sat.AIG.RefVec.zip aig pair Std.Sat.AIG.mkBEqCached).aig
      (Std.Sat.AIG.RefVec.zip aig pair Std.Sat.AIG.mkBEqCached).vec Std.Sat.AIG.mkAndCached
-- Mathlib.Algebra.Order.Quantale
sSup_mul_distrib : ∀ {α : Type u_1} {x : α} {s : Set α} [inst : Semigroup α] [inst_1 : CompleteLattice α] [IsQuantale α],
  sSup s * x = ⨆ y ∈ s, y * x
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along row 0.  -/
Matrix.det_succ_row_zero : ∀ {R : Type v} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R),
  A.det = ∑ j, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det
-- Mathlib.Data.Set.Defs
/-- `𝒫 s` is the set of all subsets of `s`.  -/
Set.term𝒫_ : Lean.ParserDescr
-- Mathlib.SetTheory.ZFC.Rank
ZFSet.rank_le_iff : ∀ {x : ZFSet.{u}} {o : Ordinal.{u}}, x.rank ≤ o ↔ ∀ ⦃y : ZFSet.{u}⦄, y ∈ x → y.rank < o
-- Mathlib.Algebra.Group.Defs
/-- A mixin for cancellative multiplication.  -/
IsCancelMul : (G : Type u) → [Mul G] → Prop
-- Mathlib.Order.SupIndep
/-- Bind operation for `SupIndep`.  -/
Finset.SupIndep.biUnion : ∀ {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [inst : Lattice α] [IsModularLattice α] [inst_2 : OrderBot α]
  [inst_3 : DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α},
  (s.SupIndep fun i => (g i).sup f) → (∀ i' ∈ s, (g i').SupIndep f) → (s.biUnion g).SupIndep f
-- Mathlib.Data.Multiset.MapFold
Multiset.foldr_induction' : ∀ {α : Type u_1} {β : Type v} (f : α → β → β) [inst : LeftCommutative f] (x : β) (q : α → Prop) (p : β → Prop)
  (s : Multiset α), (∀ (a : α) (b : β), q a → p b → p (f a b)) → p x → (∀ a ∈ s, q a) → p (Multiset.foldr f x s)
-- Mathlib.Order.Hom.Bounded
TopHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Top α] [inst_1 : Top β] (toFun : α → β) (map_top' : toFun ⊤ = ⊤)
  (toFun_1 : α → β) (map_top'_1 : toFun_1 ⊤ = ⊤),
  ({ toFun := toFun, map_top' := map_top' } = { toFun := toFun_1, map_top' := map_top'_1 }) = (toFun = toFun_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.IsColimit.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} {K : CategoryTheory.Limits.Multicofork I}
  (hK : CategoryTheory.Limits.IsColimit K) {T : C} {f g : K.pt ⟶ T},
  (∀ (a : J.R), CategoryTheory.CategoryStruct.comp (K.π a) f = CategoryTheory.CategoryStruct.comp (K.π a) g) → f = g
-- Mathlib.Order.Atoms
IsAtom.bot_lt : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, IsAtom a → ⊥ < a
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.sepByIndentSemicolon.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.id_mapId_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (a : B),
  ((CategoryTheory.StrictPseudofunctor.id B).mapId a).inv =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)