mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Separation.CompletelyRegular
completelyRegularSpace_iff_isInducing_stoneCechUnit : ∀ {X : Type u} [inst : TopologicalSpace X], CompletelyRegularSpace X ↔ Topology.IsInducing stoneCechUnit
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- One can reformulate being `C^n` on a set as continuity on this set, and being `C^n` in any
extended chart.  -/
contMDiffOn_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n M'],
  ContMDiffOn I I' n f s ↔
    ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.insert : {α : Type u_1} →
  {β : Type u_2} → (cmp : α → α → Ordering) → Lean.PrefixTreeNode α β cmp → List α → β → Lean.PrefixTreeNode α β cmp
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.IsBasis'.cardinalMk_sdiff_comm : ∀ {α : Type u} {M : Matroid α} {I J X : Set α} [M.InvariantCardinalRank],
  M.IsBasis' I X → M.IsBasis' J X → Cardinal.mk ↑(I \ J) = Cardinal.mk ↑(J \ I)
-- Init.GrindInstances.Ring.Rat
Lean.Grind.instLawfulOfScientificRat : Lean.Grind.LawfulOfScientific ℚ
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.mul_def : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (a b : WithTop α),
  a * b = if a = 0 ∨ b = 0 then 0 else WithTop.map₂ (fun x1 x2 => x1 * x2) a b
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₄_of_isCharTwoJNeZeroNF_of_char_two : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] [CharP R 2], W.c₄ = 1
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inl_mul : ∀ {R : Type u_1} (A : Type u_2) [inst : Mul R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : SMulZeroClass R A]
  (r₁ r₂ : R), Unitization.inl (r₁ * r₂) = Unitization.inl r₁ * Unitization.inl r₂
-- Mathlib.Data.Finset.Lattice.Fold
Multiset.count_finset_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] (s : Finset α) (f : α → Multiset β) (b : β),
  Multiset.count b (s.sup f) = s.sup fun a => Multiset.count b (f a)
-- Lean.Parser.Extension
Lean.Parser.ensureUnaryParserAlias : Lean.Name → IO Unit
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeInductiveDecl.mk.injEq : ∀ (decl : Lean.Declaration) (indFvars : Array Lean.Expr) (numParams : ℤ)
  (rs : Array Lean.Elab.Command.PreElabHeaderResult) (decl_1 : Lean.Declaration) (indFvars_1 : Array Lean.Expr)
  (numParams_1 : ℤ) (rs_1 : Array Lean.Elab.Command.PreElabHeaderResult),
  ({ decl := decl, indFvars := indFvars, numParams := numParams, rs := rs } =
      { decl := decl_1, indFvars := indFvars_1, numParams := numParams_1, rs := rs_1 }) =
    (decl = decl_1 ∧ indFvars = indFvars_1 ∧ numParams = numParams_1 ∧ rs = rs_1)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.appendCore.loop.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (i' : ℕ) (h_1 : Unit → motive 0) (h_2 : (i' : ℕ) → motive i'.succ),
  (match i'.succ with
    | 0 => h_1 ()
    | i'.succ => h_2 i') =
    h_2 i'
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.CommGrp C),
  (CategoryTheory.Functor.mapCommGrpIdIso.hom.app X).hom.hom.hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Data.Real.Pointwise
Real.iSup_mul_of_nonpos : ∀ {ι : Sort u_1} {r : ℝ}, r ≤ 0 → ∀ (f : ι → ℝ), (⨆ i, f i) * r = ⨅ i, f i * r
-- Mathlib.Algebra.Category.ModuleCat.Localization
ModuleCat.instAdditiveLocalizationLocalizedModuleFunctor : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (S : Submonoid R),
  (ModuleCat.localizedModuleFunctor S).Additive
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.sub_right_inj_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a b c : α}, a ≠ ⊤ → (a - b = a - c ↔ b = c)
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], DerivedCategory.Qh.IsLocalization (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- From a functor `F : J ⥤ C`, given a terminal object of `J` and that the morphisms in the
diagram are isomorphisms, show the cone `coneOfDiagramTerminal` is a limit.  -/
CategoryTheory.Limits.limitOfDiagramTerminal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {X : J} →
          (hX : CategoryTheory.Limits.IsTerminal X) →
            (F : CategoryTheory.Functor J C) →
              [inst_2 : ∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfDiagramTerminal hX F)
-- Init.Data.List.Basic
List.Perm.below : {α : Type u} → {motive : (a a_1 : List α) → a.Perm a_1 → Prop} → {a a_1 : List α} → a.Perm a_1 → Prop
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
OnePoint.isBoundedAt_iff_forall_SL2Z : ∀ {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ},
  IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range →
    (c.IsBoundedAt f k ↔
      ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ),
        (Matrix.SpecialLinearGroup.mapGL ℝ) γ • OnePoint.infty = c →
          UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map k γ f))
-- Lean.DocString.Extension
Lean.instInhabitedVersoModuleDocs : Inhabited Lean.VersoModuleDocs
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_eq_getD_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {fallback : β}, m.getD a fallback = m[a]?.getD fallback
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.bot_prod_bot : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N], ⊥.prod ⊥ = ⊥
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.disjoint_smallBall_logSizeBallSeq : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] (hJ : J.Nonempty)
  {i j : ℕ},
  i ≠ j →
    Disjoint ((PairReduction.logSizeBallSeq J hJ a c i).smallBall c)
      ((PairReduction.logSizeBallSeq J hJ a c j).smallBall c)
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Composing on the left by a uniformly continuous function preserves uniform convergence  -/
UniformContinuous.comp_tendstoUniformly : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β}
  {p : Filter ι} [inst_1 : UniformSpace γ] {g : β → γ},
  UniformContinuous g → TendstoUniformly F f p → TendstoUniformly (fun i => g ∘ F i) (g ∘ f) p
-- Mathlib.RingTheory.HahnSeries.Lex
/-- `HahnSeries.embDomain` as an `OrderEmbedding`.  -/
HahnSeries.embDomainOrderEmbedding : {Γ : Type u_1} →
  {R : Type u_2} →
    [inst : LinearOrder Γ] →
      [inst_1 : PartialOrder R] →
        {Γ' : Type u_3} →
          [inst_2 : LinearOrder Γ'] → Γ ↪o Γ' → [inst_3 : Zero R] → Lex (HahnSeries Γ R) ↪o Lex (HahnSeries Γ' R)
-- Mathlib.Data.Multiset.UnionInter
Multiset.filter_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (p : α → Prop) [inst_1 : DecidablePred p] (s t : Multiset α),
  Multiset.filter p (s ∩ t) = Multiset.filter p s ∩ Multiset.filter p t
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.withSeminorms_iff_nhds_eq_iInf : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [t : TopologicalSpace E] [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι),
  WithSeminorms p ↔ nhds 0 = ⨅ i, Filter.comap (⇑(p i)) (nhds 0)
-- Mathlib.Algebra.Group.Defs
pow_add : ∀ {M : Type u_2} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
/-- If `L` is an algebraic extension of `K = Frac(A)` and `L` has no zero smul divisors by `A`,
then `L` is the localization of the integral closure `C` of `A` in `L` at `A⁰`.  -/
IsIntegralClosure.isLocalization : ∀ (A : Type u_1) (K : Type u_2) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  (L : Type u_3) [inst_4 : Field L] (C : Type u_4) [inst_5 : CommRing C] [inst_6 : Algebra K L] [inst_7 : Algebra A L]
  [IsScalarTower A K L] [inst_9 : Algebra C L] [IsIntegralClosure C A L] [inst_11 : Algebra A C] [IsScalarTower A C L]
  [IsDomain A] [Algebra.IsAlgebraic K L], IsLocalization (Algebra.algebraMapSubmonoid C (nonZeroDivisors A)) L
-- Mathlib.Order.Defs.Unbundled
/-- The carrier of a `RelLowerSet` is a lower set relative to `P`.

Do NOT use directly. Please use `RelLowerSet.isRelLowerSet` instead.  -/
RelLowerSet.isRelLowerSet' : ∀ {α : Type u_1} [inst : LE α] {P : α → Prop} (self : RelLowerSet P), IsRelLowerSet self.carrier P
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `wbtw_const_vadd_iff`. -/
Wbtw.const_vadd : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} (v : V), Wbtw R x y z → Wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M`, if a `CommMonoid` map
`g : M →* P` induces a map `f.lift hg : N →* P` then for all `z : N, v w : P`, we have
`f.lift hg z * w = v ↔ g x * w = g y * v`, where `x : M, y ∈ S` are such that
`z * f y = f x`.  -/
Submonoid.LocalizationMap.lift_spec_mul : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (z : N) (w v : P),
  (f.lift hg) z * w = v ↔ g (f.sec z).1 * w = g ↑(f.sec z).2 * v
-- Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
CategoryTheory.Limits.pointwiseBinaryBiproductData_bicone : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u_2} [inst_3 : CategoryTheory.Category.{v_2, u_2} D]
  (F G : CategoryTheory.Functor D C),
  (CategoryTheory.Limits.pointwiseBinaryBiproductData F G).bicone = CategoryTheory.Limits.pointwiseBinaryBicone F G
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.symm_comp : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B), (↑e.symm).comp ↑e = BialgHom.id R A
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
Profinite.NobelingProof.fin_comap_jointlySurjective : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I],
  IsClosed C →
    ∀ (f : LocallyConstant ↑C ℤ),
      ∃ s g,
        f =
          LocallyConstant.comap
            { toFun := Profinite.NobelingProof.ProjRestrict C fun x => x ∈ s, continuous_toFun := ⋯ } g
-- Mathlib.RingTheory.Coalgebra.Quotient
Coalgebra.Quotient.comul_mk : ∀ {R : Type u_1} {C : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup C] [inst_2 : Module R C]
  [inst_3 : CoalgebraStruct R C] (I : Submodule R C) [inst_4 : I.IsCoideal] (x : C),
  CoalgebraStruct.comul (Submodule.Quotient.mk x) = (TensorProduct.map I.mkQ I.mkQ) (CoalgebraStruct.comul x)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
EuclideanGeometry.continuousAt_angle : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {x : P × P × P},
  x.1 ≠ x.2.1 → x.2.2 ≠ x.2.1 → ContinuousAt (fun y => EuclideanGeometry.angle y.1 y.2.1 y.2.2) x
-- Aesop.EMap
Aesop.EMap.map : {α β : Type} → (Lean.Expr → α → β) → Aesop.EMap α → Aesop.EMap β
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- The ideals of a discrete valuation ring are exactly the powers of the maximal ideal.  -/
IsDiscreteValuationRing.idealOrderIsoENat : (R : Type u_1) → [inst : CommRing R] → [inst_1 : IsDomain R] → [IsDiscreteValuationRing R] → Ideal R ≃o ℕ∞ᵒᵈ
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.nonempty_ordConnectedComponent : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α}, (s.ordConnectedComponent x).Nonempty ↔ x ∈ s
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.isUniformAddGroup : ∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α],
  IsUniformAddGroup (UniformSpace.Completion α)
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.subset_vonNeumann_self : ∀ (x : ZFSet.{u_1}), x ⊆ ZFSet.vonNeumann x.rank
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.comm_trans_rTensorBot : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  (A : Subalgebra R S), (Algebra.TensorProduct.comm R ↥⊥ ↥A).trans A.rTensorBot = A.lTensorBot
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addXYZ_of_Z_eq_zero_right : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  W'.Equation Q → Q 2 = 0 → W'.addXYZ P Q = -(Q 0 * P 2) • P
-- Mathlib.Data.List.Cycle
/-- As a function from a relation to a predicate, `chain` is monotonic.  -/
Cycle.chain_mono : ∀ {α : Type u_1}, Monotone Cycle.Chain
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.zag_of_zag_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J K) [F.Full] {j₁ j₂ : J},
  CategoryTheory.Zag (F.obj j₁) (F.obj j₂) → CategoryTheory.Zag j₁ j₂
-- Init.Data.BitVec.Lemmas
BitVec.getElem_zero_ofBool : ∀ (b : Bool), (BitVec.ofBool b)[0] = b
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrable_congr : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f g : X → ε} {μ : MeasureTheory.Measure X},
  f =ᵐ[μ] g → (MeasureTheory.LocallyIntegrable f μ ↔ MeasureTheory.LocallyIntegrable g μ)
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.mk.injEq : ∀ {α : Type u} [inst : AddGroup α] (toTopologicalSpace : TopologicalSpace α)
  (toIsTopologicalAddGroup : IsTopologicalAddGroup α) (toTopologicalSpace_1 : TopologicalSpace α)
  (toIsTopologicalAddGroup_1 : IsTopologicalAddGroup α),
  ({ toTopologicalSpace := toTopologicalSpace, toIsTopologicalAddGroup := toIsTopologicalAddGroup } =
      { toTopologicalSpace := toTopologicalSpace_1, toIsTopologicalAddGroup := toIsTopologicalAddGroup_1 }) =
    (toTopologicalSpace = toTopologicalSpace_1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α},
  (m.erase k).get? k = none
-- Mathlib.Algebra.Group.Prod
MonoidHom.prodMap_def : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] {M' : Type u_6} {N' : Type u_7}
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (f : M →* M') (g : N →* N'),
  f.prodMap g = (f.comp (MonoidHom.fst M N)).prod (g.comp (MonoidHom.snd M N))
-- Init.PropLemmas
ite_else_self : ∀ {p q : Prop} [h : Decidable p], (if p then q else p) ↔ p ∧ q
-- Lean.Attributes
Lean.AttributeApplicationTime.noConfusionType : Sort v✝ → Lean.AttributeApplicationTime → Lean.AttributeApplicationTime → Sort v✝
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.eval_rootOfSplits : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} (hf : f.Splits) (hfd : f.degree ≠ 0),
  Polynomial.eval (Polynomial.rootOfSplits hf hfd) f = 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.cosimplicialSimplicialEquiv_inverse_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Functor SimplexCategoryᵒᵖ Cᵒᵖ}
  (α : X ⟶ Y),
  (CategoryTheory.cosimplicialSimplicialEquiv C).inverse.map α =
    Quiver.Hom.op { app := fun X_1 => (α.app (Opposite.op X_1)).unop, naturality := ⋯ }
-- Mathlib.Analysis.RCLike.Extend
/-- **Alias** of `StrongDual.extendRCLike`.

---

Extend `fr : StrongDual ℝ F` to `StrongDual 𝕜 F`.

Norm properties of this extension can be found in
`Mathlib/Analysis/Normed/Module/RCLike/Extend.lean`.  -/
ContinuousLinearMap.extendTo𝕜 : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {F : Type u_2} →
      [inst_1 : TopologicalSpace F] →
        [inst_2 : AddCommGroup F] →
          [inst_3 : Module 𝕜 F] →
            [ContinuousConstSMul 𝕜 F] → [inst_5 : Module ℝ F] → [IsScalarTower ℝ 𝕜 F] → StrongDual ℝ F → StrongDual 𝕜 F
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivAt.const_sub : ∀ {𝕜 : 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}
  {f' : E →L[𝕜] F} {x : E}, HasFDerivAt f f' x → ∀ (c : F), HasFDerivAt (fun x => c - f x) (-f') x
-- Mathlib.Data.Multiset.Sort
Multiset.sort_eq : ∀ {α : Type u_1} (s : Multiset α) (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], ↑(s.sort r) = s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.any_eq_false_iff_forall_mem_getKey_getElem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulHashable α]
  [EquivBEq α] {p : α → β → Bool}, m.WF → (m.any p = false ↔ ∀ (a : α) (h : a ∈ m), p (m.getKey a h) m[a] = false)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_f : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (i : data.I₀),
  data.toPreOneHypercover.f i = data.f i
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.role.nonBracketed : Lean.Doc.Parser.InlineCtxt → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.subAt_nil : ∀ {A : Type u_1} (T : ↥(Descriptive.tree A)), Descriptive.Tree.subAt T [] = T
-- Init.Prelude
HXor.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → HXor α β γ
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasAntitoneBasis.iInf_principal : ∀ {α : Type u_1} {ι : Type u_7} [inst : Preorder ι] [Nonempty ι] [IsDirectedOrder ι] {s : ι → Set α},
  Antitone s → (⨅ i, Filter.principal (s i)).HasAntitoneBasis s
-- Init.Tactics
/-- If true, use `try?` as a discharger for subgoals that cannot be closed
by `solve_by_elim` alone.  -/
Lean.Parser.Tactic.LibrarySearchConfig.try? : Lean.Parser.Tactic.LibrarySearchConfig → Bool
-- Mathlib.Order.Hom.Lattice
SupHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Max β] (f : SupHom α β), (SupHom.id β).comp f = f
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- A Coxeter matrix can be coerced to a matrix.  -/
CoxeterMatrix.instCoeFunMatrixNat : {B : Type u_1} → CoeFun (CoxeterMatrix B) fun x => Matrix B B ℕ
-- Mathlib.Order.Comparable
/-- **Alias** of `incompRel_of_antisymmRel_of_incompRel`. -/
AntisymmRel.trans_incompRel : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → IncompRel (fun x1 x2 => x1 ≤ x2) b c → IncompRel (fun x1 x2 => x1 ≤ x2) a c
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelAddMonoid.toAddRightReflectLT : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α], AddRightReflectLT α
-- Mathlib.Order.Monotone.Union
/-- If `f` is antitone both on `s` and `t`, with `s` to the left of `t` and the center
point belonging to both `s` and `t`, then `f` is antitone on `s ∪ t`  -/
AntitoneOn.union_right : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α} {c : α},
  AntitoneOn f s → AntitoneOn f t → IsGreatest s c → IsLeast t c → AntitoneOn f (s ∪ t)
-- Mathlib.Order.Bounds.Basic
lt_isLUB_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {a b : α}, IsLUB s a → (b < a ↔ ∃ c ∈ s, b < c)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_empty : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X}, ∫ (x : X) in ∅, f x ∂μ = 0
-- Mathlib.Tactic.TryThis
/-- Produces the text `Try this: <tac>` with the given tactic, and then executes it.  -/
Mathlib.Tactic.tacticTry_this__ : Lean.ParserDescr
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.instInhabited : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C : HomologicalComplex V c} → Inhabited (HomotopyEquiv C C)
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.coeff_update_same : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M),
  (f.update a b).coeff a = b
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
/-- The full subcategory of `C ⥤ D` consisting of functors inverting morphisms in `W`  -/
CategoryTheory.MorphismProperty.FunctorsInverting : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C →
      (D : Type u_1) → [CategoryTheory.Category.{v_1, u_1} D] → Type (max (max (max u u_1) v) v_1)
-- Init.Data.BitVec.Lemmas
/-- Negating `x` and then extracting [start..start+len) is the same as extracting and then negating,
as long as the range [start..start+len) is in bounds.
See that if the index is out-of-bounds, then `extractLsb` will return `false`,
which makes the operation not commute.
 -/
BitVec.extractLsb'_not_of_lt : ∀ {w : ℕ} {x : BitVec w} {start len : ℕ},
  start + len < w → BitVec.extractLsb' start len (~~~x) = ~~~BitVec.extractLsb' start len x
-- Aesop.Builder.Basic
Aesop.RuleBuilderOptions.mk.injEq : ∀ (immediatePremises? : Option (Array Lean.Name)) (indexingMode? : Option Aesop.IndexingMode)
  (casesPatterns? : Option (Array Aesop.CasesPattern)) (pattern? : Option Lean.Term)
  (transparency? indexTransparency? : Option Lean.Meta.TransparencyMode)
  (immediatePremises?_1 : Option (Array Lean.Name)) (indexingMode?_1 : Option Aesop.IndexingMode)
  (casesPatterns?_1 : Option (Array Aesop.CasesPattern)) (pattern?_1 : Option Lean.Term)
  (transparency?_1 indexTransparency?_1 : Option Lean.Meta.TransparencyMode),
  ({ immediatePremises? := immediatePremises?, indexingMode? := indexingMode?, casesPatterns? := casesPatterns?,
        pattern? := pattern?, transparency? := transparency?, indexTransparency? := indexTransparency? } =
      { immediatePremises? := immediatePremises?_1, indexingMode? := indexingMode?_1,
        casesPatterns? := casesPatterns?_1, pattern? := pattern?_1, transparency? := transparency?_1,
        indexTransparency? := indexTransparency?_1 }) =
    (immediatePremises? = immediatePremises?_1 ∧
      indexingMode? = indexingMode?_1 ∧
        casesPatterns? = casesPatterns?_1 ∧
          pattern? = pattern?_1 ∧ transparency? = transparency?_1 ∧ indexTransparency? = indexTransparency?_1)