mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.swapTrue_eq_true : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (x : I → Bool),
  Profinite.NobelingProof.SwapTrue o x (Profinite.NobelingProof.term I ho) = true
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight₁_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K], Height.mulHeight₁ 0 = 1
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.mulRight_one : ∀ (R : Type u_6) (A : Type u_7) [inst : Semiring R] [inst_1 : NonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A], LinearMap.mulRight R 1 = LinearMap.id
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.gcdCoeffs : Int.Internal.Linear.Poly → ℤ → ℤ
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
AlgebraicGeometry.HasAffineProperty.affineAnd_eq_of_propertyIsLocal : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  {P P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
  AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) →
    ∀ [AlgebraicGeometry.HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] => Q],
      P = @AlgebraicGeometry.IsAffineHom ⊓ P'
-- Init.GrindInstances.ToInt
Lean.Grind.instLEIntIi : Lean.Grind.ToInt.LE ℤ Lean.Grind.IntInterval.ii
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.monadMonEquiv_counitIso_hom_app_hom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.Mon (CategoryTheory.Functor C C)),
  ((CategoryTheory.Monad.monadMonEquiv C).counitIso.hom.app x).hom =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.Monad.monToMonad C).comp (CategoryTheory.Monad.monadToMon C)).obj x).X
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.dual_zero : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] {B : Type uB} [inst_2 : AddCommGroup B]
  [inst_3 : Module R A] [inst_4 : Module R B], CharacterModule.dual 0 = 0
-- Mathlib.NumberTheory.Height.MvPolynomial
Height.mulHeight_mul_mulHeight : ∀ {K : Type u_4} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {a b c d : K},
  ![a, b] ≠ 0 →
    ![c, d] ≠ 0 → Height.mulHeight ![a, b] * Height.mulHeight ![c, d] = Height.mulHeight ![a * c, a * d, b * c, b * d]
-- Mathlib.Geometry.Manifold.Diffeomorph
ContinuousLinearEquiv.contMDiffAt_transContinuousLinearEquiv_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M] {M' : Type u_10}
  [inst_11 : TopologicalSpace M'] [inst_12 : ChartedSpace H' M'] {n : WithTop ℕ∞} (e : E ≃L[𝕜] F) {f : M' → M} {x : M'},
  ContMDiffAt I' (I.transContinuousLinearEquiv e) n f x ↔ ContMDiffAt I' I n f x
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The ring homomorphism from the colimit commutative ring to the cone point of any other
cocone.  -/
CommRingCat.Colimits.descMorphism : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) →
      (s : CategoryTheory.Limits.Cocone F) → CommRingCat.Colimits.colimit F ⟶ s.pt
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceRErase.eq_7 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (rs : ℕ) (k_1 : α) (v_1 : β k_1)
  (l_1 r_2 : Std.DTreeMap.Internal.Impl α β) (hrb_2 : (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l_1 r_2).Balanced)
  (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β)
  (hlb_1 : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced)
  (hlr_3 :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
      (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l_1 r_2).size),
  Std.DTreeMap.Internal.Impl.balanceRErase k v (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l_1 r_2)
      (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) hrb_2 hlb_1 hlr_3 =
    if hrsd : ls > Std.DTreeMap.Internal.delta * rs then
      match ll, lr, hlb_1, hlr_3 with
      | Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr, Std.DTreeMap.Internal.Impl.inner rrs k_2 v_2 l r, hrb,
        hlr =>
        if rls < Std.DTreeMap.Internal.ratio * rrs then
          Std.DTreeMap.Internal.Impl.inner (1 + rs + ls) lk lv
            (Std.DTreeMap.Internal.Impl.inner (1 + rs + rls) k v (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l_1 r_2)
              ll)
            lr
        else
          Std.DTreeMap.Internal.Impl.inner (1 + rs + ls) rlk rlv
            (Std.DTreeMap.Internal.Impl.inner (1 + rs + rll.size) k v
              (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l_1 r_2) rll)
            (Std.DTreeMap.Internal.Impl.inner (1 + rrs + rlr.size) lk lv rlr lr)
      | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf, hrb, hlr => ⋯.elim
      | Std.DTreeMap.Internal.Impl.leaf, x, hrb, hlr => ⋯.elim
    else
      Std.DTreeMap.Internal.Impl.inner (1 + rs + ls) k v (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l_1 r_2)
        (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.constOfIsEmpty.congr_simp : ∀ (R : Type u) {ι : Type v} (M₁ : ι → Type w₁) {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  [inst_7 : IsEmpty ι] (m m_1 : M₂),
  m = m_1 → ContinuousMultilinearMap.constOfIsEmpty R M₁ m = ContinuousMultilinearMap.constOfIsEmpty R M₁ m_1
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- Promotes a bijective bialgebra homomorphism to a bialgebra equivalence.  -/
BialgEquiv.ofBijective : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Bialgebra R A] → [inst_4 : Bialgebra R B] → (f : A →ₐc[R] B) → Function.Bijective ⇑f → A ≃ₐc[R] B
-- Init.Data.String.Basic
String.offset_pos : ∀ {s : String} {off : String.Pos.Raw} {h : String.Pos.Raw.IsValid s off}, (s.pos off h).offset = off
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.comp.eq_3 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.WithTerminal C) (_X : C),
  CategoryTheory.WithTerminal.comp = fun f _g => PEmpty.elim f
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabDumpAsyncEnvState : Lean.Elab.Command.CommandElab
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.Const.insertMany t l) k' = v
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedOrderRingHom.eq_1 : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Field β] [inst_4 : ConditionallyCompleteLinearOrder β] [inst_5 : IsStrictOrderedRing β]
  [inst_6 : Archimedean α],
  ConditionallyCompleteLinearOrderedField.inducedOrderRingHom α β =
    { toRingHom := (ConditionallyCompleteLinearOrderedField.inducedAddHom α β).mkRingHomOfMulSelfOfTwoNeZero ⋯ ⋯ ⋯,
      monotone' := ⋯ }
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.LEquiv.addEmptyConstants.congr_simp : ∀ (L : FirstOrder.Language) (α : Type w') [ie : IsEmpty α],
  FirstOrder.Language.LEquiv.addEmptyConstants L α = FirstOrder.Language.LEquiv.addEmptyConstants L α
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_ofNat : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : NatCast α] (m : ℕ)
  [inst_3 : m.AtLeastTwo], (Matrix.diagonal fun x => OfNat.ofNat m) = OfNat.ofNat m
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- Get the common retraction for a coreflexive pair.  -/
CategoryTheory.commonRetraction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {A B : C} → (f g : A ⟶ B) → [CategoryTheory.IsCoreflexivePair f g] → B ⟶ A
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.isoMk_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom)
            (θ.naturality f).hom =
          CategoryTheory.CategoryStruct.comp (η.naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f)))
      CategoryTheory.Pseudofunctor.StrongTrans.isoMk._auto_1)
  (a : B), (CategoryTheory.Pseudofunctor.StrongTrans.isoMk app naturality).inv.as.app a = (app a).inv
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- The uniform bijection between two completions of the same uniform space.  -/
AbstractCompletion.compareEquiv : {α : Type uα} →
  [inst : UniformSpace α] →
    (pkg : AbstractCompletion.{vα, uα} α) → (pkg' : AbstractCompletion.{vα', uα} α) → pkg.space ≃ᵤ pkg'.space
-- Lean.Environment
Lean.instGetElem?ArrayModuleIdxLtNatToNatSize : {α : Type u_1} → GetElem? (Array α) Lean.ModuleIdx α fun a i => i.toNat < a.size
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.instGroupWithZero : (k : Type u) → [inst : Field k] → GroupWithZero (AlgebraicClosure k)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncOptions.save? : Lean.Lsp.TextDocumentSyncOptions → Option Lean.Lsp.SaveOptions
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- On a set of unique differentiability, the second derivative is obtained by taking the
derivative of the derivative.  -/
iteratedFDerivWithin_two_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  (f : E → F) {z : E},
  UniqueDiffOn 𝕜 s →
    z ∈ s →
      ∀ (m : Fin 2 → E), (iteratedFDerivWithin 𝕜 2 f s z) m = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z) (m 0)) (m 1)
-- Mathlib.Analysis.Convex.Function
ConcaveOn.left_lt_of_lt_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f → ∀ {x y z : E}, x ∈ s → y ∈ s → z ∈ openSegment 𝕜 x y → f z < f y → f x < f z
-- Mathlib.Analysis.ODE.Gronwall
/-- The Grönwall bound is monotone with respect to the time variable `x`.  -/
gronwallBound_mono : ∀ {δ K ε : ℝ}, 0 ≤ δ → 0 ≤ ε → 0 ≤ K → Monotone (gronwallBound δ K ε)
-- Mathlib.Tactic.Translate.Reorder
/-- Return the reorder that reverses the action of the given reorder.  -/
Mathlib.Tactic.Translate.ArgReorder.reverse : Mathlib.Tactic.Translate.ArgReorder → Mathlib.Tactic.Translate.ArgReorder
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
IsMIntegralCurveAt.comp_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {t₀ : ℝ},
  IsMIntegralCurveAt γ v t₀ → ∀ (dt : ℝ), IsMIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.not_mem_of_isEmpty : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a : α}, m.isEmpty = true → a ∉ m
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.copy_source : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (f : α → β) (hf : ↑e = f) (g : β → α) (hg : ↑e.symm = g)
  (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t), (e.copy f hf g hg s hs t ht).source = s
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.exists_mem_ofAddUnits_val_eq : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M}, x ∈ S.ofAddUnits → ∃ y ∈ S, ↑y = x
-- Init.Grind.Order
Lean.Grind.Order.eq_mp : ∀ {p q : Prop}, p = q → p → q
-- Mathlib.ModelTheory.Algebra.Field.Basic
_private.Mathlib.ModelTheory.Algebra.Field.Basic.0.FirstOrder.Field.FieldAxiom.toSentence.match_1.eq_4 : ∀ (motive : FirstOrder.Field.FieldAxiom → Sort u_1) (h_1 : Unit → motive FirstOrder.Field.FieldAxiom.addAssoc)
  (h_2 : Unit → motive FirstOrder.Field.FieldAxiom.zeroAdd)
  (h_3 : Unit → motive FirstOrder.Field.FieldAxiom.negAddCancel)
  (h_4 : Unit → motive FirstOrder.Field.FieldAxiom.mulAssoc) (h_5 : Unit → motive FirstOrder.Field.FieldAxiom.mulComm)
  (h_6 : Unit → motive FirstOrder.Field.FieldAxiom.oneMul) (h_7 : Unit → motive FirstOrder.Field.FieldAxiom.existsInv)
  (h_8 : Unit → motive FirstOrder.Field.FieldAxiom.leftDistrib)
  (h_9 : Unit → motive FirstOrder.Field.FieldAxiom.existsPairNE),
  (match FirstOrder.Field.FieldAxiom.mulAssoc with
    | FirstOrder.Field.FieldAxiom.addAssoc => h_1 ()
    | FirstOrder.Field.FieldAxiom.zeroAdd => h_2 ()
    | FirstOrder.Field.FieldAxiom.negAddCancel => h_3 ()
    | FirstOrder.Field.FieldAxiom.mulAssoc => h_4 ()
    | FirstOrder.Field.FieldAxiom.mulComm => h_5 ()
    | FirstOrder.Field.FieldAxiom.oneMul => h_6 ()
    | FirstOrder.Field.FieldAxiom.existsInv => h_7 ()
    | FirstOrder.Field.FieldAxiom.leftDistrib => h_8 ()
    | FirstOrder.Field.FieldAxiom.existsPairNE => h_9 ()) =
    h_4 ()
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.MonCat.Hom.mk.inj : ∀ {A B : MonCat} {hom' hom'_1 : ↑A →* ↑B}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Order.RelIso.Basic
RelEmbedding.irrefl : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [Std.Irrefl s], Std.Irrefl r
-- Mathlib.Data.Finsupp.Single
Finsupp.single_apply_left : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] {f : α → β},
  Function.Injective f → ∀ (x z : α) (y : M), (fun₀ | f x => y) (f z) = (fun₀ | x => y) z
-- Mathlib.Data.Sum.Basic
Sum.isSome_getRight?_iff_isRight : ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, x.getRight?.isSome = true ↔ x.isRight = true
-- Mathlib.Topology.UniformSpace.Cauchy
isComplete_iUnion_separated : ∀ {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {s : ι → Set α},
  (∀ (i : ι), IsComplete (s i)) →
    ∀ {U : SetRel α α},
      U ∈ uniformity α → (∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j) → IsComplete (⋃ i, s i)
-- Mathlib.Algebra.Order.Floor.Defs
/-- `Int.floor a` is the greatest integer `z` such that `z ≤ a`. It is denoted with `⌊a⌋`.  -/
Int.«term⌊_⌋» : Lean.ParserDescr
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.mk.congr_simp : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} (toFun toFun_1 : E → F)
  (e_toFun : toFun = toFun_1) (contDiff' : ContDiff ℝ (↑n) toFun) (hasCompactSupport' : HasCompactSupport toFun)
  (tsupport_subset' : tsupport toFun ⊆ ↑Ω),
  { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
      tsupport_subset' := tsupport_subset' } =
    { toFun := toFun_1, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
reduceIte : Lean.Meta.Simp.Simproc
-- Mathlib.Analysis.SpecificLimits.RCLike
RCLike.tendsto_ofReal_atBot_cobounded : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜], Filter.Tendsto RCLike.ofReal Filter.atBot (Bornology.cobounded 𝕜)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_pos : ∀ {x : ℝ}, 1 < x → 0 < Real.log x
-- Mathlib.Algebra.Module.Equiv.Defs
RingEquiv.symm_toSemilinearEquiv_symm_apply : ∀ {R : Type u_1} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* S) (x : R),
  f.symm.toSemilinearEquiv.symm x = f x
-- Mathlib.Topology.Algebra.Monoid
ContinuousMap.mulRight.eq_1 : ∀ {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : Mul X] [inst_2 : SeparatelyContinuousMul X] (x : X),
  ContinuousMap.mulRight x = { toFun := fun x_1 => x_1 * x, continuous_toFun := ⋯ }
-- Mathlib.Order.WellFoundedSet
Set.isPWO_of_finite : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α} [Finite α], s.IsPWO
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_getElem?_iff_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α},
  t[a]?.isSome = true ↔ a ∈ t
-- Mathlib.Analysis.Complex.RealDeriv
ContDiffAt.real_of_complex : ∀ {e : ℂ → ℂ} {z : ℝ} {n : WithTop ℕ∞}, ContDiffAt ℂ n e ↑z → ContDiffAt ℝ n (fun x => (e ↑x).re) z
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
/-- **Alias** of `CategoryTheory.MonoidalCategoryStruct.tensorUnit`. -/
CategoryTheory.Functor.chosenTerminal : (C : Type u) → {𝒞 : CategoryTheory.Category.{v, u} C} → [self : CategoryTheory.MonoidalCategoryStruct C] → C
-- Init.System.IO
IO.FS.SystemTime.mk : ℤ → UInt32 → IO.FS.SystemTime
-- Mathlib.Algebra.Algebra.Defs
/-- The canonical ring homomorphism `algebraMap R A : R →+* A` for any `R`-algebra `A`,
packaged as an `R`-linear map.
 -/
Algebra.linearMap : (R : Type u) → (A : Type w) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → R →ₗ[R] A
-- Std.Async.Timer
Std.Async.Sleep.native : Std.Async.Sleep → Std.Internal.UV.Timer
-- Std.Async.IO
Std.Async.IO.AsyncRead.read : {α β : Type} → [self : Std.Async.IO.AsyncRead α β] → α → Std.Async.Async β
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
_private.Std.Tactic.BVDecide.LRAT.Internal.Assignment.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.splitter : (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1) →
  (a : Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
    (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos) →
      (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg) →
        (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both) →
          (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned) → motive a
-- Mathlib.Order.Heyting.Hom
BiheytingHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : BiheytingAlgebra α] →
      [inst_1 : BiheytingAlgebra β] →
        (toLatticeHom : LatticeHom α β) →
          (∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b) →
            (∀ (a b : α), toLatticeHom.toFun (a \ b) = toLatticeHom.toFun a \ toLatticeHom.toFun b) → BiheytingHom α β
-- Mathlib.Combinatorics.Hall.Basic
/-- This is the version of **Hall's Marriage Theorem** in terms of indexed
families of finite sets `t : ι → Finset α`.  It states that there is a
set of distinct representatives if and only if every union of `k` of the
sets has at least `k` elements.

Recall that `s.biUnion t` is the union of all the sets `t i` for `i ∈ s`.

This theorem is bootstrapped from `Finset.all_card_le_biUnion_card_iff_exists_injective'`,
which has the additional constraint that `ι` is a `Fintype`.
 -/
Finset.all_card_le_biUnion_card_iff_exists_injective : ∀ {ι : Type u} {α : Type v} [inst : DecidableEq α] (t : ι → Finset α),
  (∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) ↔ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.ofHom_comp : ∀ {M N P : Type u} [inst : CommMonoid M] [inst_1 : CommMonoid N] [inst_2 : CommMonoid P] (f : M →* N) (g : N →* P),
  CommMonCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (CommMonCat.ofHom f) (CommMonCat.ofHom g)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.integral_eq_norm_posPart_sub : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : ↥(α →₁ₛ[μ] ℝ)),
  MeasureTheory.L1.SimpleFunc.integral f =
    ‖MeasureTheory.L1.SimpleFunc.posPart f‖ - ‖MeasureTheory.L1.SimpleFunc.negPart f‖
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_sum : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] {ι : Type u_3} (s : Finset ι)
  [inst_2 : AddCommMonoid R] [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R] (f : ι → BoundedContinuousFunction α R),
  ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instPowUInt32UintOfNatNat : Lean.Grind.ToInt.Pow UInt32 (Lean.Grind.IntInterval.uint 32)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- A morphism in the Grothendieck construction `∫ F` between two points `X Y : ∫ F` consists of
a morphism in the base category `base : X.base ⟶ Y.base` and
a morphism in a fiber `f.fiber : (F.map base).obj X.fiber ⟶ Y.fiber`.  -/
CategoryTheory.Pseudofunctor.Grothendieck.Hom : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} →
      F.Grothendieck → F.Grothendieck → Type (max v₁ v₂)
-- Mathlib.Topology.Algebra.OpenSubgroup
Ideal.isOpen_of_isOpen_subideal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] {U I : Ideal R},
  U ≤ I → IsOpen ↑U → IsOpen ↑I
-- Mathlib.Data.Finset.Sum
Finset.eq_disjSum_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {u : Finset (α ⊕ β)},
  u = s.disjSum t ↔ u.toLeft = s ∧ u.toRight = t
-- Mathlib.Data.LawfulXor.Equiv
Equiv.xor_symm : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [inst_2 : LawfulXor α] {a : α},
  Equiv.symm (Equiv.xor a) = Equiv.xor a
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α) (a b : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.Expr.denoteN ctx (a.sub b) = 0
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- Characterization of `C^n` sections within a set at a point of a vector bundle.  -/
Bundle.contMDiffWithinAt_section : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] {s : (x : B) → E x} {a : Set B}
  {x₀ : B},
  ContMDiffWithinAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) a x₀ ↔
    ContMDiffWithinAt IB (modelWithCornersSelf 𝕜 F) n (fun x => (↑(trivializationAt F E x₀) ⟨x, s x⟩).2) a x₀
-- Mathlib.Data.Finsupp.Option
Finsupp.some_update_none : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : Option α →₀ M) (a : M), (f.update none a).some = f.some
-- Init.Data.Vector.Basic
/-- Deletes the first `i` elements of a vector. If `i` is greater than or equal to the size of the
vector then the empty vector is returned.

We immediately simplify this to the `extract` operation, so there is no verification API for this function.
 -/
Vector.drop : {α : Type u_1} → {n : ℕ} → Vector α n → (i : ℕ) → Vector α (n - i)
-- Mathlib.SetTheory.ZFC.PSet
PSet.equiv_of_isEmpty : ∀ (x : PSet.{u_1}) (y : PSet.{u_2}) [IsEmpty x.Type] [IsEmpty y.Type], x.Equiv y