mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.coe_smul_addMonoidHom : ∀ {A : Type u_5} {B : Type u_6} {M : Type u_7} [inst : AddMonoid A] [inst_1 : DistribSMul M A] [inst_2 : AddZeroClass B]
  (c : Mᵈᵐᵃ) (f : A →+ B), ⇑(c • f) = c • ⇑f
-- Init.Data.BitVec.Lemmas
BitVec.ofNat_mul_ofNat : ∀ {n : ℕ} (x y : ℕ), BitVec.ofNat n x * BitVec.ofNat n y = BitVec.ofNat n (x * y)
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.fromLeftInv_eq_inv : ∀ {M : Type u_1} [inst : Group M] (S : Submonoid M) (x : ↥S.leftInv), ↑(S.fromLeftInv x) = (↑x)⁻¹
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The adjunction `Γ ⊣ Spec` from `CommRingᵒᵖ` to `LocallyRingedSpace`.  -/
AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction : AlgebraicGeometry.LocallyRingedSpace.Γ.rightOp ⊣ AlgebraicGeometry.Spec.toLocallyRingedSpace
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.mem_horn_iff_notMem_range : ∀ {n d : ℕ} (s : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := d })) (i : Fin (n + 1)),
  s ∈ (SSet.horn n i).obj (Opposite.op { len := d }) ↔ ∃ j, ∃ (_ : j ≠ i), j ∉ Set.range ⇑s
-- Mathlib.Order.Monotone.Basic
/-- If `α` is a preorder with no maximal elements, then there exists a strictly monotone function
`ℕ → α` with any prescribed value of `f 0`.  -/
Nat.exists_strictMono' : ∀ {α : Type u} [inst : Preorder α] [NoMaxOrder α] (a : α), ∃ f, StrictMono f ∧ f 0 = a
-- Mathlib.AlgebraicGeometry.Geometrically.Basic
AlgebraicGeometry.geometrically_inf : ∀ (P Q : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme),
  AlgebraicGeometry.geometrically (P ⊓ Q) = AlgebraicGeometry.geometrically P ⊓ AlgebraicGeometry.geometrically Q
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterMap.match_1.splitter : {β' : Type u_1} →
  (motive : Option β' → Sort u_2) →
    (x : Option β') → (x = none → motive none) → ((out' : β') → x = some out' → motive (some out')) → motive x
-- Init.Data.UInt.Lemmas
USize.toUInt64_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < USize.size), (USize.ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯
-- Lean.Environment
/-- Opaque persistent environment extension entry.  -/
Lean.EnvExtensionEntrySpec : NonemptyType
-- Mathlib.Algebra.Lie.TensorProduct
TensorProduct.LieModule.map_tmul : ∀ {R : Type u} [inst : CommRing R] {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} {Q : Type w₃}
  [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N]
  [inst_9 : LieRingModule L N] [inst_10 : LieModule R L N] [inst_11 : AddCommGroup P] [inst_12 : Module R P]
  [inst_13 : LieRingModule L P] [inst_14 : LieModule R L P] [inst_15 : AddCommGroup Q] [inst_16 : Module R Q]
  [inst_17 : LieRingModule L Q] [inst_18 : LieModule R L Q] (f : M →ₗ⁅R,L⁆ P) (g : N →ₗ⁅R,L⁆ Q) (m : M) (n : N),
  (TensorProduct.LieModule.map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
-- Mathlib.FieldTheory.Relrank
Subfield.lift_relrank_comap_comap_eq_lift_relrank_inf : ∀ {E : Type v} [inst : Field E] {L : Type w} [inst_1 : Field L] (A B : Subfield E) (f : L →+* E),
  Cardinal.lift.{v, w} ((Subfield.comap f A).relrank (Subfield.comap f B)) =
    Cardinal.lift.{w, v} (A.relrank (B ⊓ f.fieldRange))
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.log_eq_iff : ∀ {b x : Ordinal.{u_1}}, 1 < b → x ≠ 0 → ∀ (y : Ordinal.{u_1}), Ordinal.log b x = y ↔ b ^ y ≤ x ∧ x < b ^ (y + 1)
-- Mathlib.Algebra.Ring.Basic
succ_ne_self : ∀ {α : Type u_3} [inst : NonAssocRing α] [Nontrivial α] (a : α), a + 1 ≠ a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
/-- Given a walk `p` and a node in the support, there exists a natural `n`, such that given node
is the `n`-th node (zero-indexed) in the walk. In addition, `n` is at most the length of the walk.
Due to the definition of `getVert` it would otherwise be legal to return a larger `n` for the last
node.  -/
SimpleGraph.Walk.mem_support_iff_exists_getVert : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk v w}, u ∈ p.support ↔ ∃ n, p.getVert n = u ∧ n ≤ p.length
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Min α] [inst_1 : Min β] [inst_2 : Top α] [inst_3 : Top β] [inst_4 : SizeOf α]
  [inst_5 : SizeOf β] (toInfHom : InfHom α β) (map_top' : toInfHom.toFun ⊤ = ⊤),
  sizeOf { toInfHom := toInfHom, map_top' := map_top' } = 1 + sizeOf toInfHom + sizeOf map_top'
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- If a multilinear map in finitely many variables on seminormed spaces
sends vectors with a component of norm zero to vectors of norm zero
and satisfies the inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖` on a shell `ε i / ‖c i‖ < ‖m i‖ < ε i`
for some positive numbers `ε i` and elements `c i : 𝕜`, `1 < ‖c i‖`,
then it satisfies this inequality for all `m`.

The first assumption is automatically satisfied on normed spaces, see `bound_of_shell` below.
For seminormed spaces, it follows from continuity of `f`, see next lemma,
see `bound_of_shell_of_continuous` below.  -/
MultilinearMap.bound_of_shell_of_norm_map_coord_zero : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] (f : MultilinearMap 𝕜 E G),
  (∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0) →
    ∀ {ε : ι → ℝ} {C : ℝ},
      (∀ (i : ι), 0 < ε i) →
        ∀ {c : ι → 𝕜},
          (∀ (i : ι), 1 < ‖c i‖) →
            (∀ (m : (i : ι) → E i),
                (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖) →
              ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
-- Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
IsTranscendenceBasis.lift_rank_eq_max_lift : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Type w} {x : ι → E}
  [Nonempty ι],
  IsTranscendenceBasis F x →
    Cardinal.lift.{max u w, v} (Module.rank F E) =
      max (max (Cardinal.lift.{max v w, u} (Cardinal.mk F)) (Cardinal.lift.{max u v, w} (Cardinal.mk ι)))
        Cardinal.aleph0
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.mk'_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : HomotopicalAlgebra.IsFibrant X] [inst_3 : HomotopicalAlgebra.IsFibrant Y]
  (h :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C)
      (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))),
  (HomotopicalAlgebra.FibrantBrownFactorization.mk' f h).i = h.i
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.map_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D), (sq.map F).X₃ = F.obj sq.X₃
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Array.length_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} [LawfulMonad m] {array : Array β},
  (array.iterM m).length = pure { down := array.size }
-- Mathlib.Order.WithBot
WithTop.forall_le_coe_iff_le : ∀ {α : Type u_1} [inst : Preorder α] {x y : WithTop α} [NoTopOrder α], (∀ (a : α), x ≤ ↑a → y ≤ ↑a) ↔ y ≤ x
-- Mathlib.CategoryTheory.Opposites
/-- `Functor.rightOp` sends identity functors to the canonical isomorphism `opOp`.  -/
CategoryTheory.Functor.rightOpId : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (CategoryTheory.Functor.id Cᵒᵖ).rightOp ≅ CategoryTheory.opOp C
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
continuousAt_extChartAt_symm'' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x : M} {y : E},
  y ∈ (extChartAt I x).target → ContinuousAt (↑(extChartAt I x).symm) y
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexFuel : ℕ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Ordering
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_lt_zero : ∀ {α : Type u} [inst : Zero α] {a : α} [inst_1 : LT α], ↑a < 0 ↔ a < 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentColorParams.mk.injEq : ∀ (toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams) (toPartialResultParams : Lean.Lsp.PartialResultParams)
  (textDocument : Lean.Lsp.TextDocumentIdentifier) (toWorkDoneProgressParams_1 : Lean.Lsp.WorkDoneProgressParams)
  (toPartialResultParams_1 : Lean.Lsp.PartialResultParams) (textDocument_1 : Lean.Lsp.TextDocumentIdentifier),
  ({ toWorkDoneProgressParams := toWorkDoneProgressParams, toPartialResultParams := toPartialResultParams,
        textDocument := textDocument } =
      { toWorkDoneProgressParams := toWorkDoneProgressParams_1, toPartialResultParams := toPartialResultParams_1,
        textDocument := textDocument_1 }) =
    (toWorkDoneProgressParams = toWorkDoneProgressParams_1 ∧
      toPartialResultParams = toPartialResultParams_1 ∧ textDocument = textDocument_1)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry?_eq_minEntry? : ∀ {α : Type u} {β : Type v} [Ord α] {l : Std.DTreeMap.Internal.Impl α fun x => β},
  Std.DTreeMap.Internal.Impl.Const.minEntry? l = Option.map (fun x => (x.fst, x.snd)) l.minEntry?
-- Mathlib.Order.Category.BddOrd
BddOrd.hasForgetToPartOrd : CategoryTheory.HasForget₂ BddOrd PartOrd
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.ι_ne_zero : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] [Nontrivial R] (x : X), FreeAlgebra.ι R x ≠ 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic.0.termZ : Lean.ParserDescr
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_algebraMap : ∀ {K : Type u} [inst : Field K] (p : Polynomial K), ((algebraMap (Polynomial K) (RatFunc K)) p).num = p
-- Mathlib.RingTheory.Valuation.Basic
Valuation.one_apply_of_ne_zero : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [inst_2 : Nontrivial R]
  [inst_3 : NoZeroDivisors R] [inst_4 : DecidablePred fun x => x = 0] {x : R}, x ≠ 0 → 1 x = 1
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.const.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (a : Bool), sizeOf (Std.Tactic.BVDecide.BoolExpr.const a) = 1 + sizeOf a
-- Std.Http.Protocol.H1
/-- If the connection will be kept alive after the message.
 -/
Std.Http.Protocol.H1.Machine.keepAlive : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Mathlib.Logic.Function.Basic
Option.rec_update : ∀ {α : Type u_1} {β : Option α → Sort u_2} [inst : DecidableEq α] (f : β none) (g : (a : α) → β (some a)) (a : α)
  (x : β (some a)),
  (fun t => Option.rec f (Function.update g a x) t) = Function.update (fun t => Option.rec f g t) (some a) x
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
Std.IterM.length_uLift : ∀ {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [inst : Std.Iterator α m β]
  [inst_1 : Monad m] [inst_2 : Monad n] {it : Std.IterM m β} [inst_3 : MonadLiftT m (Std.Iterators.ULiftT n)]
  [Std.Iterators.Finite α m] [inst_5 : Std.IteratorLoop α m m] [LawfulMonad m] [LawfulMonad n]
  [Std.LawfulIteratorLoop α m m] [LawfulMonadLiftT m (Std.Iterators.ULiftT n)],
  (it.uLift n).length = (fun x => { down := x.down.down }) <$> (monadLift it.length).run
-- Mathlib.Order.Category.Frm
Frm.instConcreteCategoryFrameHomCarrier : CategoryTheory.ConcreteCategory Frm fun x1 x2 => FrameHom ↑x1 ↑x2
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.lowerThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.mk_whiskerLeft : ∀ {C : Type u} (X : CategoryTheory.FreeMonoidalCategory C) {Y₁ Y₂ : CategoryTheory.FreeMonoidalCategory C}
  (f : Y₁.Hom Y₂),
  ⟦CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f⟧ = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X ⟦f⟧
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.commute_of_mem_adjoin_singleton_of_commute : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {a b c : A},
  c ∈ NonUnitalStarAlgebra.adjoin R {b} → Commute a b → Commute a (star b) → Commute a c
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedResponseError.default : {α : Type u} → Lean.JsonRpc.ResponseError α
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Nat.Partition.countRestricted.eq_1 : ∀ (n m : ℕ), Nat.Partition.countRestricted n m = {x | ∀ i ∈ x.parts, Multiset.count i x.parts < m}
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp] {a : α} {f : β a → β a}
  {t : Std.DTreeMap.Raw α β cmp}, t.WF → (t.modify a f).WF
-- Mathlib.Analysis.Normed.Ring.Units
/-- The formula
`Ring.inverse (x + t) =
  (∑ i ∈ Finset.range n, (- x⁻¹ * t) ^ i) * x⁻¹ + (- x⁻¹ * t) ^ n * Ring.inverse (x + t)`
holds for `t` sufficiently small.  -/
NormedRing.inverse_add_nth_order : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (x : Rˣ) (n : ℕ),
  ∀ᶠ (t : R) in nhds 0,
    Ring.inverse (↑x + t) = (∑ i ∈ Finset.range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * Ring.inverse (↑x + t)
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- A normed division ring is a topological division ring.  -/
NormedDivisionRing.to_isTopologicalDivisionRing : ∀ {α : Type u_1} [inst : NormedDivisionRing α], IsTopologicalDivisionRing α
-- Std.Time.Time.PlainTime
/-- Converts a `PlainTime` value to the total number of minutes.
 -/
Std.Time.PlainTime.toMinutes : Std.Time.PlainTime → Std.Time.Minute.Offset
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.hasDerivAt_arcosh : ∀ {x : ℝ}, x ∈ Set.Ioi 1 → HasDerivAt Real.arcosh (√(x ^ 2 - 1))⁻¹ x
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.edit.inj : ∀ {a a_1 : Lean.Lsp.TextDocumentEdit}, Lean.Lsp.DocumentChange.edit a = Lean.Lsp.DocumentChange.edit a_1 → a = a_1
-- Aesop.Search.Queue
Aesop.LIFOQueue.goals : Aesop.LIFOQueue → Array Aesop.GoalRef
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- Lifting to over `Y` and pulling back along `X ⟶ Y` is the same as lifting to over `X`.  -/
CategoryTheory.Over.starPullbackIsoStar : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        {X Y : C} →
          (f : X ⟶ Y) → (CategoryTheory.Over.star Y).comp (CategoryTheory.Over.pullback f) ≅ CategoryTheory.Over.star X
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.mk'_eq_div : ∀ {A : Type u_4} [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] {r : A} (s : ↥(nonZeroDivisors A)),
  IsLocalization.mk' K r s = (algebraMap A K) r / (algebraMap A K) ↑s
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k : α}, (Std.ExtTreeSet.ofList l cmp).contains k = l.contains k
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsUniformAddGroup : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsUniformAddGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.iSupLift_of_mem : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : IsScalarTower R A A]
  [inst_6 : SMulCommClass R A A] {ι : Sort u_1} [inst_7 : Nonempty ι] {K : ι → NonUnitalSubalgebra R A}
  {dir : Directed (fun x1 x2 => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₙₐ[R] B}
  {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A}
  {hT : T = iSup K} {i : ι} (x : ↥T) (hx : ↑x ∈ K i), (NonUnitalSubalgebra.iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.toCLM.eq_1 : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A],
  CStarMatrix.toCLM =
    {
      toFun := fun M =>
        { toFun := ⇑(WithCStarModule.equivL ℂ).symm ∘ (fun v => Matrix.vecMul v M) ∘ ⇑(WithCStarModule.equivL ℂ),
          map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Algebra.CharZero.Defs
OfNat.ofNat_ne_one : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ) [inst_2 : n.AtLeastTwo], OfNat.ofNat n ≠ 1
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If a `E ⋙ F` has a limit, and `E` is an equivalence, we can construct a limit of `F`.
 -/
CategoryTheory.Limits.hasLimit_of_equivalence_comp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} (e : K ≌ J)
  [CategoryTheory.Limits.HasLimit (e.functor.comp F)], CategoryTheory.Limits.HasLimit F
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.complete : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [CauSeq.IsComplete β abv] (s : CauSeq β abv),
  ∃ b, s ≈ CauSeq.const abv b
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.single_eq_zero_iff : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] {i : ι} {a : 𝕜},
  EuclideanSpace.single i a = 0 ↔ a = 0
-- Lean.Parser.Term
/-- The `sorry` term is a temporary placeholder for a missing proof or value.

The syntax is intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton.
Lean will give a warning whenever a declaration uses `sorry`, so you aren't likely to miss it,
but you can double check if a declaration depends on `sorry` by looking for `sorryAx` in the output
of the `#print axioms my_thm` command, the axiom used by the implementation of `sorry`.

"Go to definition" on `sorry` in the Infoview will go to the source position where it was introduced, if such information is available.

Each `sorry` is guaranteed to be unique, so for example the following fails:
```lean
example : (sorry : Nat) = sorry := rfl -- fails
```

See also the `sorry` tactic, which is short for `exact sorry`.
 -/
Lean.Parser.Term.sorry : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.Ray
/-- Nonzero vectors, as used to define rays. This type depends on an unused argument `R` so that
`RayVector.Setoid` can be an instance.  -/
RayVector : Type u_1 → (M : Type u_2) → [Zero M] → Type (max 0 u_2)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The variant of `chaar_self` for `haarContent`  -/
MeasureTheory.Measure.haar.haarContent_self : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G}, (MeasureTheory.Measure.haar.haarContent K₀) K₀.toCompacts = 1
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.distortion_disjUnion : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I} [inst : Fintype ι]
  (h : Disjoint π₁.iUnion π₂.iUnion), (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion
-- Init.Data.List.OfFn
List.ofFnM_succ_last : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α},
  List.ofFnM f = do
    let as ← List.ofFnM fun i => f i.castSucc
    let a ← f (Fin.last n)
    pure (as ++ [a])
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).ι =
    CategoryTheory.CategoryStruct.id c.pt
-- Mathlib.Topology.Order
TopologicalSpace.tendsto_nhds_generateFrom_iff : ∀ {α : Type u} {β : Type u_1} {m : α → β} {f : Filter α} {g : Set (Set β)} {b : β},
  Filter.Tendsto m f (nhds b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.coe_pair : ∀ (x y : ZFSet.{u}), ↑(x.pair y) = {{x}, {x, y}}
-- Init.System.IO
/-- Returns `true` if a stream refers to a Windows console or Unix terminal.  -/
IO.FS.Stream.isTty : IO.FS.Stream → BaseIO Bool
-- Mathlib.Data.Finset.Image
Finset.image_ssubset_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s t : Finset α},
  Function.Injective f → (Finset.image f s ⊂ Finset.image f t ↔ s ⊂ t)
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.ofHom_smul : ∀ {k : Type u} {G : Type v} {X Y : Type w} [inst : TopologicalSpace k] [inst_1 : CommRing k] [inst_2 : Monoid G]
  [inst_3 : AddCommGroup X] [inst_4 : Module k X] [inst_5 : TopologicalSpace X] [inst_6 : IsTopologicalAddGroup X]
  [inst_7 : ContinuousSMul k X] [inst_8 : AddCommGroup Y] [inst_9 : Module k Y] [inst_10 : TopologicalSpace Y]
  [inst_11 : IsTopologicalAddGroup Y] [inst_12 : ContinuousSMul k Y] {ρ : ContRepresentation k G X}
  {σ : ContRepresentation k G Y} (r : k) (f : ContIntertwiningMap ρ σ), TopRep.ofHom (r • f) = r • TopRep.ofHom f
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.biprod.mapBiprod_inv_map_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] (X Y : C)
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_6 : CategoryTheory.Limits.PreservesBinaryBiproduct X Y F] {W : C} (f : X ⟶ W) (g : Y ⟶ W),
  CategoryTheory.CategoryStruct.comp (F.mapBiprod X Y).inv (F.map (CategoryTheory.Limits.biprod.desc f g)) =
    CategoryTheory.Limits.biprod.desc (F.map f) (F.map g)
-- Mathlib.Topology.Algebra.Group.Basic
/-- If `f → a` and `g → b` along a nontrivial filter on the domain, valued in a
Hausdorff topological group, then `f / g → 1` if and only if `a = b`.  -/
tendsto_div_nhds_one_iff_eq : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {α : Type u_1} {l : Filter α}
  [l.NeBot] [T2Space G] {f g : α → G} {a b : G},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto g l (nhds b) → (Filter.Tendsto (fun x => f x / g x) l (nhds 1) ↔ a = b)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_inter_Ioc_of_left_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α},
  b₁ ≤ b₂ → Set.Ioo a₁ b₁ ∩ Set.Ioc a₂ b₂ = Set.Ioo (max a₁ a₂) b₁
-- Init.Control.Lawful.MonadLift.Instances
_private.Init.Control.Lawful.MonadLift.Instances.0.Except.map.match_1.eq_2 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (v : α) (h_1 : (err : ε) → motive (Except.error err))
  (h_2 : (v : α) → motive (Except.ok v)),
  (match Except.ok v with
    | Except.error err => h_1 err
    | Except.ok v => h_2 v) =
    h_2 v