mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- Every square matrix over a field can be brought, by left and right multiplication by
invertible matrices, into the block form `fromBlocks 1 0 0 0`, where the identity block has size
equal to the rank of the matrix.  -/
Matrix.exists_rank_normal_form : ∀ {m : Type um} {R : Type uR} [inst : Field R] [inst_1 : Fintype m] [inst_2 : DecidableEq m] (M : Matrix m m R),
  ∃ V U e, IsUnit V ∧ IsUnit U ∧ V * M * U = (Matrix.fromBlocks 1 0 0 0).submatrix ⇑e ⇑e
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- The restriction of a locally ringed space `X` to the top subspace is isomorphic to `X` itself.
 -/
AlgebraicGeometry.LocallyRingedSpace.restrictTopIso : (X : AlgebraicGeometry.LocallyRingedSpace) → X.restrict ⋯ ≅ X
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.integrable_approxOn : ∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  [inst_3 : BorelSpace E] {f : β → E} {μ : MeasureTheory.Measure β} (fmeas : Measurable f),
  MeasureTheory.Integrable f μ →
    ∀ {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s) [inst_4 : TopologicalSpace.SeparableSpace ↑s],
      MeasureTheory.Integrable (fun x => y₀) μ →
        ∀ (n : ℕ), MeasureTheory.Integrable (⇑(MeasureTheory.SimpleFunc.approxOn f fmeas s y₀ h₀ n)) μ
-- Mathlib.Order.Bounds.Defs
IsGreatest.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : Set α) (a : α), IsGreatest s a = (a ∈ s ∧ a ∈ upperBounds s)
-- Mathlib.Algebra.Opposites
MulOpposite.unop_comp_op : ∀ {α : Type u_1}, MulOpposite.unop ∘ MulOpposite.op = id
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.reverse_surjective : ∀ {T : Type u_1}, Function.Surjective ContextFreeGrammar.reverse
-- Mathlib.Combinatorics.Configuration
/-- Intersection of two lines  -/
Configuration.HasPoints.mkPoint : {P : Type u_1} →
  {L : Type u_2} → {inst : Membership P L} → [self : Configuration.HasPoints P L] → {l₁ l₂ : L} → l₁ ≠ l₂ → P
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- The proposition that a linear map is bounded between spaces with families of seminorms.  -/
Seminorm.IsBounded : {𝕜 : Type u_2} →
  {𝕜₂ : Type u_3} →
    {E : Type u_6} →
      {F : Type u_7} →
        {ι : Type u_9} →
          {ι' : Type u_10} →
            [inst : SeminormedRing 𝕜] →
              [inst_1 : AddCommGroup E] →
                [inst_2 : Module 𝕜 E] →
                  [inst_3 : SeminormedRing 𝕜₂] →
                    [inst_4 : AddCommGroup F] →
                      [inst_5 : Module 𝕜₂ F] →
                        {σ₁₂ : 𝕜 →+* 𝕜₂} →
                          [RingHomIsometric σ₁₂] → (ι → Seminorm 𝕜 E) → (ι' → Seminorm 𝕜₂ F) → (E →ₛₗ[σ₁₂] F) → Prop
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.FixedTermElabRef.toFixedTermElabImpl : Lean.Elab.Term.FixedTermElabRef → Lean.Elab.Term.FixedTermElab
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
/-- Given `w : TwoSquare T L R B`, one may obtain a 2-square `TwoSquare T' L R B'` if we
provide natural transformations `α : T ⟶ T'` and `β : B' ⟶ B`.  -/
CategoryTheory.TwoSquare.whiskerHorizontal : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_4} →
      {D₂ : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] →
                {T : CategoryTheory.Functor C₁ D₁} →
                  {L : CategoryTheory.Functor C₁ C₂} →
                    {R : CategoryTheory.Functor D₁ D₂} →
                      {B : CategoryTheory.Functor C₂ D₂} →
                        CategoryTheory.TwoSquare T L R B →
                          {T' : CategoryTheory.Functor C₁ D₁} →
                            {B' : CategoryTheory.Functor C₂ D₂} →
                              (T' ⟶ T) → (B ⟶ B') → CategoryTheory.TwoSquare T' L R B'
-- Mathlib.Data.Finsupp.Fin
Finsupp.cons_right_injective : ∀ {n : ℕ} {M : Type u_1} [inst : Zero M] (y : M), Function.Injective (Finsupp.cons y)
-- Std.Time.DateTime.Timestamp
/-- Returns the `Duration` represented by the `Timestamp` since the Unix epoch.
 -/
Std.Time.Timestamp.toDurationSinceUnixEpoch : Std.Time.Timestamp → Std.Time.Duration
-- Lean.Server.References
Lean.Server.RefInfo.mk.injEq : ∀ (definition : Option Lean.Server.Reference) (usages : Array Lean.Server.Reference)
  (definition_1 : Option Lean.Server.Reference) (usages_1 : Array Lean.Server.Reference),
  ({ definition := definition, usages := usages } = { definition := definition_1, usages := usages_1 }) =
    (definition = definition_1 ∧ usages = usages_1)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.absolutelyContinuous : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] (μ : MeasureTheory.VectorMeasure X V), μ.AbsolutelyContinuous μ.ennrealVariation
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- Two subsemigroups are equal if they have the same elements.  -/
Subsemigroup.ext : ∀ {M : Type u_1} [inst : Mul M] {S T : Subsemigroup M}, (∀ (x : M), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
/-- Noncomputably determines the multiset of prime factors.  -/
UniqueFactorizationMonoid.factors : {α : Type u_1} → [inst : CommMonoidWithZero α] → [UniqueFactorizationMonoid α] → α → Multiset α
-- Mathlib.Algebra.Category.ModuleCat.Basic
LinearMap.comp_id_moduleCat : ∀ {R : Type u_1} [inst : Ring R] {G : ModuleCat R} {H : Type u} [inst_1 : AddCommGroup H] [inst_2 : Module R H]
  (f : ↑G →ₗ[R] H), f ∘ₗ ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id G) = f
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.isSome_get?_eq_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α},
  (m.get? a).isSome = m.contains a
-- Lean.Meta.Tactic.Intro
_private.Lean.Meta.Tactic.Intro.0.Lean.Meta.introNImp : {σ : Type} →
  Lean.MVarId →
    ℕ →
      (Lean.LocalContext → Lean.Name → Bool → σ → Lean.MetaM (Lean.Name × σ)) →
        σ → Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- Mathlib.Order.Set
WithBot.range_eq : ∀ {α : Type u_1} {β : Type u_2} (f : WithBot α → β), Set.range f = insert (f ⊥) (Set.range (f ∘ WithBot.some))
-- Mathlib.NumberTheory.LegendreSymbol.Basic
legendreSym.eq_neg_one_iff_not_one : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {a : ℤ}, ↑a ≠ 0 → (legendreSym p a = -1 ↔ ¬legendreSym p a = 1)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
StrictMono.neg : ∀ {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α]
  [inst_4 : Preorder β] {f : β → α}, StrictMono f → StrictAnti fun x => -f x
-- Mathlib.Algebra.Group.Commute.Defs
Commute.mul_inv_cancel_assoc : ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → a * (b * a⁻¹) = b
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.exists_norm_lt_one : ∀ (K : Type u_1) [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K], ∃ x, 0 < ‖x‖ ∧ ‖x‖ < 1
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
MeasureTheory.memLp_piLp_iff : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {p q : ENNReal} [inst : Fact (1 ≤ q)]
  {ι : Type u_2} [inst_1 : Fintype ι] {E : ι → Type u_3} [inst_2 : (i : ι) → NormedAddCommGroup (E i)]
  {f : X → PiLp q E}, MeasureTheory.MemLp f p μ ↔ ∀ (i : ι), MeasureTheory.MemLp (fun x => (f x).ofLp i) p μ
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.equivOfIsClopenOfIsConnected_mk : ∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} {U : ι → Set α} (hclopen : ∀ (i : ι), IsClopen (U i))
  (hdisj : Pairwise (Function.onFun Disjoint U)) (hunion : ⋃ i, U i = Set.univ) (hconn : ∀ (i : ι), IsConnected (U i))
  {i : ι},
  ∀ x ∈ U i,
    (ConnectedComponents.equivOfIsClopenOfIsConnected hclopen hdisj hunion hconn) (ConnectedComponents.mk x) = i
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- A matroid as defined by a ground set and an independence predicate.
This definition is an implementation detail whose purpose is to organize the multiple
different versions of the independence axioms;
usually, terms of type `IndepMatroid` should either be directly piped into `IndepMatroid.matroid`,
or should be constructed as a private definition
which is then converted into a matroid via `IndepMatroid.matroid`.

To define a `Matroid α` from a known independence predicate
`MyIndep : Set α → Prop` and ground set `E : Set α`, one can either write
```
def myMatroid (…) : Matroid α :=
  IndepMatroid.matroid <| IndepMatroid.ofFoo E MyIndep _ _ … _
```
or, slightly more indirectly,
```
private def myIndepMatroid (…) : IndepMatroid α := IndepMatroid.ofFoo E MyIndep _ _ … _

def myMatroid (…) : Matroid α := (myIndepMatroid …).matroid
```
In both cases, `IndepMatroid.ofFoo` is either `IndepMatroid.mk`,
or one of the several other available constructors for `IndepMatroid`,
and the `_` represent the proofs that this constructor requires.

After such a definition is made, the facts that `myMatroid.Indep = myIndep` and `myMatroid.E = E`
are true by either `rfl` or `simp [myMatroid]`, and can be made directly into @[simp] lemmas.
 -/
IndepMatroid : Type u_2 → Type u_2
-- Mathlib.RingTheory.WittVector.Defs
WittVector.hasNatPow : {p : ℕ} → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [CommRing R] → Pow (WittVector p R) ℕ
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.isHashSelf_reinsertAux : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  (data : { d // 0 < d.size }) (a : α) (b : β a),
  Std.DHashMap.Internal.IsHashSelf ↑data →
    Std.DHashMap.Internal.IsHashSelf ↑(Std.DHashMap.Internal.Raw₀.reinsertAux hash data a b)
-- Mathlib.Data.Set.Prod
/-- The diagonal map $\Delta: X \to X \times_Y X$.  -/
toPullbackDiag : {X : Type u_1} → {Y : Sort u_2} → (f : X → Y) → X → Function.Pullback f f
-- Init.Data.UInt.Bitwise
USize.toUInt16_shiftLeft_mod : ∀ (a b : USize), (a <<< (b % 16)).toUInt16 = a.toUInt16 <<< b.toUInt16
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Order.cof_ord_cof : ∀ (α : Type u_1) [inst : LinearOrder α] [WellFoundedLT α], (Order.cof α).ord.cof = Order.cof α
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom : ∀ {R : Type u} [inst : CommRing R] {X Y : AlgCat R} (f : X ⟶ Y),
  (ModuleCat.MonModuleEquivalenceAlgebra.inverse.map f).hom = ModuleCat.ofHom (AlgCat.Hom.hom f).toLinearMap
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.EncodedQueryString.mk.inj : ∀ {r : UInt8 → Bool} {toByteArray : ByteArray} {valid : Std.Http.URI.IsAllowedEncodedQueryChars r toByteArray}
  {toByteArray_1 : ByteArray} {valid_1 : Std.Http.URI.IsAllowedEncodedQueryChars r toByteArray_1},
  { toByteArray := toByteArray, valid := valid } = { toByteArray := toByteArray_1, valid := valid_1 } →
    toByteArray = toByteArray_1
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) (R₀ : Type u_5)
  [inst_4 : CommRing R₀] [inst_5 : Algebra R₀ R] [inst_6 : Algebra R₀ S] [inst_7 : IsScalarTower R₀ R S]
  [inst_8 : P.HasCoeffs R₀], (MvPolynomial.aeval P.val) (P.invJacobianOfHasCoeffs R₀) = ↑⋯.unit⁻¹
-- Mathlib.Topology.Algebra.Group.GroupTopology
/-- Given `f : α → β` and a topology on `α`, the coinduced group topology on `β` is the finest
topology such that `f` is continuous and `β` is a topological group.  -/
GroupTopology.coinduced : {α : Type u_1} → {β : Type u_2} → [t : TopologicalSpace α] → [inst : Group β] → (α → β) → GroupTopology β
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_filterMap : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF)
  {h' : k ∈ (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl},
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.get k h' = (f k (t.get k ⋯)).get ⋯
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.union : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, M.IsRkFinite X → M.IsRkFinite Y → M.IsRkFinite (X ∪ Y)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The oriented angle between two vectors equals the unoriented angle if the sign is positive.  -/
Orientation.oangle_eq_angle_of_sign_eq_one : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, (o.oangle x y).sign = 1 → o.oangle x y = ↑(InnerProductGeometry.angle x y)
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.coe_of_map_sub : ∀ {G : Type u_5} [inst : AddGroup G] {H : Type u_8} [inst_1 : AddGroup H] (f : G → H)
  (hf : ∀ (x y : G), f (x - y) = f x - f y), ⇑(AddMonoidHom.ofMapSub f hf) = f
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- Every split epi `f` with a kernel induces a binary bicone with `f` as its `snd` and
the kernel map as its `inl`.
We will show in `isBilimitBinaryBiconeOfIsSplitEpiOfKernel` that this binary bicone is in fact
already a biproduct.  -/
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          [CategoryTheory.IsSplitEpi f] →
            {c : CategoryTheory.Limits.KernelFork f} →
              CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.BinaryBicone c.pt Y
-- Mathlib.RingTheory.Regular.IsSMulRegular
IsSMulRegular.rTensor : ∀ {R : Type u_1} (M : Type u_3) {M' : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
  [inst_3 : Module R M] [inst_4 : Module R M'] [Module.Flat R M] {r : R},
  IsSMulRegular M' r → IsSMulRegular (TensorProduct R M' M) r
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.seminorm_fderivLM_top : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {K : TopologicalSpace.Compacts E} {i : ℕ} (f : ContDiffMapSupportedIn E F ⊤ K),
  (ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) ⊤ K i) ((ContDiffMapSupportedIn.fderivLM 𝕜 ⊤ ⊤) f) =
    (ContDiffMapSupportedIn.seminorm 𝕜 E F ⊤ K (i + 1)) f
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instPow_1 : {α : Type u_1} → {β : Type u_2} → [Pow α β] → Pow α (Colex β)
-- Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp
/-- The `ι`-ary tensor product distributes over `κ i`-ary finitely supported functions.  -/
PiTensorProduct.ofDFinsuppEquiv : {R : Type u_1} →
  {ι : Type u_2} →
    {κ : ι → Type u_3} →
      {M : (i : ι) → κ i → Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)] →
            [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)] →
              [Fintype ι] →
                [DecidableEq ι] →
                  [(i : ι) → DecidableEq (κ i)] →
                    (PiTensorProduct R fun i => Π₀ (j : κ i), M i j) ≃ₗ[R]
                      Π₀ (p : (i : ι) → κ i), PiTensorProduct R fun i => M i (p i)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.limitConeOfComp_cone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone (F.comp G)),
  (CategoryTheory.Functor.Initial.limitConeOfComp F t).cone = CategoryTheory.Functor.Initial.extendCone.obj t.cone
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.instToExprLinearCombo : Lean.ToExpr Lean.Omega.LinearCombo
-- Std.Time.Duration
Std.Time.Duration.instHMulInt_1 : HMul Std.Time.Duration ℤ Std.Time.Duration
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The real part of the Riemann zeta function is positive for real arguments greater than 1.  -/
riemannZeta_re_pos_of_one_lt : ∀ {x : ℝ}, 1 < x → 0 < (riemannZeta ↑x).re
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.one_le_rpow_of_pos_of_le_one_of_nonpos : ∀ {x z : ℝ}, 0 < x → x ≤ 1 → z ≤ 0 → 1 ≤ x ^ z
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.Hom.ext : ∀ {A B : AddGrpCat} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_strictMono_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Injective ⇑f → StrictMono (Subsemigroup.map f)
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.enumOrd_univ : Ordinal.enumOrd Set.univ = id
-- Mathlib.RingTheory.PicardGroup
/-- If there is an `R`-isomorphism between `M ⊗[R] N` and `R`,
the induced map `M → Nᵛ` is an isomorphism.  -/
Module.Invertible.bijective_curry : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] (e : TensorProduct R M N ≃ₗ[R] R),
  Function.Bijective ⇑(TensorProduct.curry ↑e)
-- Mathlib.Algebra.Field.Subfield.Basic
RingHom.rangeRestrictFieldEquiv_apply_symm_apply : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L) (x : ↥f.fieldRange),
  f (f.rangeRestrictFieldEquiv.symm x) = ↑x
-- Init.Data.Int.DivMod.Lemmas
Int.mul_lt_mul_right_of_neg : ∀ {a b c : ℤ}, a < 0 → (b * a < c * a ↔ c < b)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.TreeSet.ofList l cmp).get? k' = some k
-- Mathlib.Order.Hom.Basic
OrderEmbedding.coe_ofMapLEIff : ∀ {α : Type u_6} {β : Type u_7} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β}
  (h : ∀ (a b : α), f a ≤ f b ↔ a ≤ b), ⇑(OrderEmbedding.ofMapLEIff f h) = f
-- ProofWidgets.Compat
ProofWidgets.ExprWithCtx.ci : ProofWidgets.ExprWithCtx → Lean.Elab.ContextInfo
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.resRec.match_3.splitter : {w : ℕ} →
  (motive : (s : ℕ) → s < w → 0 < s → Sort u_1) →
    (s : ℕ) →
      (hs : s < w) →
        (hslt : 0 < s) →
          ((hs : 0 < w) → (hslt : 0 < 0) → s = 0 → motive 0 hs hslt) →
            ((s' : ℕ) → (hs : s' + 1 < w) → (hslt : 0 < s' + 1) → s = s'.succ → motive s'.succ hs hslt) →
              motive s hs hslt
-- Mathlib.Algebra.BigOperators.Finprod
finsum_congr_Prop : ∀ {M : Type u_2} [inst : AddCommMonoid M] {p q : Prop} {f : p → M} {g : q → M} (hpq : p = q),
  (∀ (h : q), f ⋯ = g h) → finsum f = finsum g
-- Mathlib.Algebra.Ring.Rat
/-- The characteristic of `ℚ` is 0.  -/
Rat.instCharZero : CharZero ℚ
-- Mathlib.Analysis.Normed.Module.Connected
Metric.contractibleSpace_eball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal},
  0 < r → ContractibleSpace ↑(Metric.eball x r)
-- Std.Data.HashSet.Basic
/-- Folds the given function over the elements of the hash set in some order.  -/
Std.HashSet.fold : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → (β → α → β) → β → Std.HashSet α → β
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] (h : t.WF)
  {l : List α} {k : α}
  {h' : Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯) = true}
  (contains : k ∈ t), (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).getKey k h' = t.getKey k contains
-- Lean.Elab.ConfigEval.DeriveEvalTerm
_private.Lean.Elab.ConfigEval.DeriveEvalTerm.0.Lean.Elab.ConfigEval.ensureEvalTerm.extraDeps : Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM (Array Lean.Expr)
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instFreeInt : ∀ (K : Type u_1) [inst : Field K] [NumberField K], Module.Free ℤ (NumberField.RingOfIntegers K)
-- Mathlib.Data.TypeVec
/-- constructor for `prod`  -/
TypeVec.prod.mk : {n : ℕ} → {α β : TypeVec.{u} n} → (i : Fin2 n) → α i → β i → α.prod β i
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.instIsMultiplicativeSchemeIsAffineHom : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsAffineHom
-- Mathlib.Order.Hom.Basic
OrderEmbedding.isWellOrder : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [IsWellOrder β fun x1 x2 => x1 < x2]
  (f : α ↪o β), IsWellOrder α fun x1 x2 => x1 < x2
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.val_step_filterMap.match_3.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.toMultilinearMapLinear_apply : ∀ {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {R' : Type u_1} {A : Type u_2} [inst : Semiring R']
  [inst_1 : Semiring A] [inst_2 : (i : ι) → AddCommMonoid (M₁ i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : (i : ι) → TopologicalSpace (M₁ i)] [inst_5 : TopologicalSpace M₂] [inst_6 : ContinuousAdd M₂]
  [inst_7 : (i : ι) → Module A (M₁ i)] [inst_8 : Module A M₂] [inst_9 : Module R' M₂]
  [inst_10 : ContinuousConstSMul R' M₂] [inst_11 : SMulCommClass A R' M₂] (self : ContinuousMultilinearMap A M₁ M₂),
  ContinuousMultilinearMap.toMultilinearMapLinear self = self.toMultilinearMap
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωScottContinuous.of_apply₂ : ∀ {α : Type u_2} {γ : Type u_4} {β : α → Type u_6} [inst : (x : α) → OmegaCompletePartialOrder (β x)]
  [inst_1 : OmegaCompletePartialOrder γ] {f : γ → (x : α) → β x},
  (∀ (a : α), OmegaCompletePartialOrder.ωScottContinuous fun x => f x a) → OmegaCompletePartialOrder.ωScottContinuous f
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instMin.eq_1 : ∀ (M : Type u_1) [inst : AddZeroClass M],
  SaturatedAddSubmonoid.instMin M =
    {
      min := fun s₁ s₂ =>
        let __src := s₁.toAddSubmonoid ⊓ s₂.toAddSubmonoid;
        { toAddSubmonoid := __src, addSaturated := ⋯ } }
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- The map `p ↦ v +ᵥ p` as a continuous affine automorphism of an affine space
on which addition is continuous.  -/
ContinuousAffineEquiv.constVAdd : (k : Type u_1) →
  (P₁ : Type u_2) →
    {V₁ : Type u_6} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] →
          [inst_2 : Module k V₁] →
            [inst_3 : AddTorsor V₁ P₁] → [inst_4 : TopologicalSpace P₁] → [ContinuousConstVAdd V₁ P₁] → V₁ → P₁ ≃ᴬ[k] P₁
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_filter_add_sum_filter_not : ∀ {M : Type u_5} [inst : AddCommMonoid M] {s : Multiset M} (p : M → Prop) [inst_1 : DecidablePred p],
  (Multiset.filter p s).sum + (Multiset.filter (fun a => ¬p a) s).sum = s.sum
-- Mathlib.RingTheory.Perfection
/-- Given monoids `M` and `N`, with `M` being perfect,
any homomorphism `M →+* N` can be lifted uniquely to a homomorphism `M →* Perfection N p`.  -/
Perfection.liftMonoidHom : (p : ℕ) →
  (M : Type u_2) →
    [inst : CommMonoid M] →
      [PerfectRing M p] → (N : Type u_3) → [inst_2 : CommMonoid N] → (M →* N) ≃* (M →* Perfection N p)