mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Echelon.Basic
/-- `A` is in row echelon form: for rows `i₁ < i₂`, if the higher row `i₁` is zero at every
column strictly left of `j₂`, then the lower row `i₂` is zero at `j₂`.  -/
Matrix.IsRowEchelon : {m : Type u_1} → {n : Type u_2} → {R : Type v} → [Zero R] → [LT m] → [LT n] → Matrix m n R → Prop
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
PreQuasiregular.mk : {R : Type u_1} → R → PreQuasiregular R
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_union_add_inter' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ∀ (t : Set α), μ (s ∪ t) + μ (s ∩ t) = μ s + μ t
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
AddGroup.covariant_swap_iff_contravariant_swap : ∀ {N : Type u_2} {r : N → N → Prop} [inst : AddGroup N],
  Covariant N N (Function.swap fun x1 x2 => x1 + x2) r ↔ Contravariant N N (Function.swap fun x1 x2 => x1 + x2) r
-- Mathlib.Data.List.Cycle
List.prev_ne_cons_cons : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x y z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y),
  x ≠ z → (y :: z :: l).prev x h = (z :: l).prev x ⋯
-- Mathlib.Logic.Equiv.Set
/-- A singleton set is equivalent to a `PUnit` type.  -/
Equiv.Set.singleton : {α : Type u_3} → (a : α) → ↑{a} ≃ PUnit.{u}
-- Mathlib.Analysis.Real.Pi.Leibniz
/-- **Leibniz's series for `π`**. The alternating sum of odd number reciprocals is `π / 4`,
proved by using Abel's limit theorem to extend the Maclaurin series of `arctan` to 1.  -/
Real.tendsto_sum_pi_div_four : Filter.Tendsto (fun k => ∑ i ∈ Finset.range k, (-1) ^ i / (2 * ↑i + 1)) Filter.atTop (nhds (Real.pi / 4))
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.alterₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α] (k : α)
  (f : Option (β k) → Option (β k)) (t : Std.DTreeMap.Internal.Impl α β) (h : t.Balanced),
  Std.DTreeMap.Internal.Impl.alterₘ k f t h =
    (Std.DTreeMap.Internal.Impl.updateCell k (fun x => Std.DTreeMap.Internal.Cell.alter f x) t h).impl
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Ico_sub : ∀ {M : Type u_4} (f : ℕ → M) {m n : ℕ} [inst : AddCommGroup M],
  m ≤ n → ∑ i ∈ Finset.Ico m n, (f (i + 1) - f i) = f n - f m
-- Mathlib.Algebra.Lie.Semisimple.Basic
/-- A simple Lie algebra is semisimple.  -/
LieAlgebra.IsSimple.instIsSemisimple : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsSimple R L], LieAlgebra.IsSemisimple R L
-- Mathlib.Data.FP.Basic
FP.emax.eq_1 : ∀ [C : FP.FloatCfg], FP.emax = FP.FloatCfg.emax
-- Mathlib.MeasureTheory.Measure.OpenPos
IsClosed.ae_eq_univ_iff_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure]
  {F : Set X}, IsClosed F → (F =ᵐ[μ] Set.univ ↔ F = Set.univ)
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.AwaitRefreshParams.state : ProofWidgets.RefreshComponent.AwaitRefreshParams → Lean.Server.WithRpcRef ProofWidgets.RefreshComponent.RefreshRef
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitConst : Lean.Expr → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsLoop.of_isRestriction : ∀ {α : Type u_1} {M N : Matroid α} {e : α}, N.IsLoop e → N.IsRestriction M → M.IsLoop e
-- Mathlib.Logic.Basic
exists_apply_eq_apply' : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) (a' : α), ∃ a, f a' = f a
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.instMax : {E : Type u_3} → [inst : AddGroup E] → Max (NonarchAddGroupSeminorm E)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linearHom_apply : ∀ {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₁] (self : P₁ ≃ᵃ[k] P₁), AffineEquiv.linearHom self = self.linear
-- Mathlib.Algebra.Group.Basic
ite_add_zero : ∀ {M : Type u_4} [inst : AddZeroClass M] {P : Prop} [inst_1 : Decidable P] {a b : M},
  (if P then a + b else 0) = (if P then a else 0) + if P then b else 0
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} [inst_2 : SizeOf α]
  (toFun : ↥g.cycleFactorsFinset → α) (mem_support_self' : ∀ (c : ↥g.cycleFactorsFinset), toFun c ∈ (↑c).support),
  sizeOf { toFun := toFun, mem_support_self' := mem_support_self' } = 1
-- Std.Data.HashMap.Basic
/-- Checks if any element satisfies the predicate, short-circuiting if a predicate succeeds.  -/
Std.HashMap.any : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → (α → β → Bool) → Bool
-- Mathlib.Order.CompleteBooleanAlgebra
OrderDual.instCoframe : {α : Type u} → [Order.Frame α] → Order.Coframe αᵒᵈ
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.range_mk : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α}, Set.range QuotientAddGroup.mk = Set.univ
-- Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
MeasureTheory.IsZeroOneMeasure.measure_inter_eq_prod : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsZeroOneMeasure μ]
  {s t : Set α}, MeasurableSet s → MeasurableSet t → μ (s ∩ t) = μ s * μ t
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- A line through `p` is tangent to the sphere at `p` if and only if the angle between the line and
the radius at `p` equals `π / 2`.  -/
EuclideanGeometry.Sphere.IsTangentAt_iff_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P},
  p ∈ s → (s.IsTangentAt p line[ℝ, p, q] ↔ EuclideanGeometry.angle q p s.center = Real.pi / 2)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonShowDocumentClientCapabilities : Lean.ToJson Lean.Lsp.ShowDocumentClientCapabilities
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_updateCell : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α}
  {f : Std.DTreeMap.Internal.Cell α β (compare k) → Std.DTreeMap.Internal.Cell α β (compare k)}
  {l : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced),
  l.Ordered →
    (Std.DTreeMap.Internal.Impl.updateCell k f l hlb).impl.toListModel =
      List.filter (fun x => compare k x.fst == Ordering.gt) l.toListModel ++
          (f (Std.DTreeMap.Internal.List.findCell l.toListModel (compare k))).inner.toList ++
        List.filter (fun x => compare k x.fst == Ordering.lt) l.toListModel
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.mul_const_lt : ∀ {α : Type u_1} {b c : α} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α],
  b < c → ∀ {a : α}, 0 < a → a * b < a * c
-- Mathlib.Analysis.Normed.Operator.Banach
/-- Upgrade a `LinearMap` to a `ContinuousLinearMap` using a variation on the
**closed graph theorem**.  -/
ContinuousLinearMap.ofSeqClosedGraph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [CompleteSpace E] →
            {F : Type u_5} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [CompleteSpace F] →
                    {g : E →ₗ[𝕜] F} →
                      (∀ (u : ℕ → E) (x : E) (y : F),
                          Filter.Tendsto u Filter.atTop (nhds x) →
                            Filter.Tendsto (⇑g ∘ u) Filter.atTop (nhds y) → y = g x) →
                        E →L[𝕜] F
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_sum_le : ∀ {R : Type u} [inst : Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R),
  (∑ i ∈ s, f i).degree ≤ s.sup fun b => (f b).degree
-- Mathlib.Topology.Irreducible
/-- [Stacks Tag 004W](https://stacks.math.columbia.edu/tag/004W) ((3)) -/
exists_mem_irreducibleComponents_subset_of_isIrreducible : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X), IsIrreducible s → ∃ u ∈ irreducibleComponents X, s ⊆ u
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.cancel_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {g : β →ᵈ γ} {f₁ f₂ : α →ᵈ β},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.mk : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Module.Projective A Ω[A⁄R] → Subsingleton (Algebra.H1Cotangent R A) → Algebra.FormallySmooth R A
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
_private.Mathlib.NumberTheory.LSeries.HurwitzZetaValues.0.HurwitzZeta.hurwitzZeta_one_sub_two_mul_nat : ∀ {k : ℕ} {x : ℝ},
  k ≠ 0 →
    x ∈ Set.Icc 0 1 →
      HurwitzZeta.hurwitzZeta (↑x) (1 - 2 * ↑k) =
        -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
-- Mathlib.Analysis.Meromorphic.Order
/-- The order multiplies by `n` when taking a meromorphic function to its `n`th power.  -/
meromorphicOrderAt_zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {x : 𝕜},
  MeromorphicAt f x → ∀ {n : ℤ}, meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Asserts that a given `IteratorLoop` instance is equal to `IteratorLoop.defaultImplementation`.
(Even though equal, the given instance might be vastly more efficient.)
 -/
Std.LawfulIteratorLoop : {β : Type w} →
  (α : Type w) →
    (m : Type w → Type w') →
      (n : Type x → Type x') → [Monad m] → [Monad n] → [inst : Std.Iterator α m β] → [i : Std.IteratorLoop α m n] → Prop
-- Lean.Declaration
Lean.ConstantInfo.quotInfo.injEq : ∀ (val val_1 : Lean.QuotVal), (Lean.ConstantInfo.quotInfo val = Lean.ConstantInfo.quotInfo val_1) = (val = val_1)
-- Init.Meta
/-- `erw [rules]` is a shorthand for `rw (transparency := .default) [rules]`.
This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
which only unfolds `@[reducible]` definitions).  -/
Lean.Parser.Tactic.tacticErw___ : Lean.ParserDescr
-- Mathlib.Algebra.Order.Pi
Pi.mulSingle_le_mulSingle : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : DecidableEq ι] [inst_1 : (i : ι) → One (α i)]
  [inst_2 : (i : ι) → Preorder (α i)] {i : ι} {a b : α i}, Pi.mulSingle i a ≤ Pi.mulSingle i b ↔ a ≤ b
-- Mathlib.Algebra.Lie.Basic
LieEquiv.apply_symm_apply : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) (x : L₂), e (e.symm x) = x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_half_eq_sqrt : ∀ {x : ℝ}, 0 ≤ x → x ≤ 2 * Real.pi → Real.sin (x / 2) = √((1 - Real.cos x) / 2)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_bool : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (f : Bool → MeasureTheory.Measure α),
  MeasureTheory.Measure.sum f = f true + f false
-- Batteries.Data.List.Lemmas
List.getElem_zero_findIdxs_eq_findIdx : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} (h : 0 < (List.findIdxs p xs).length),
  (List.findIdxs p xs)[0] = List.findIdx p xs
-- Lean.Environment
Lean.EnvExtension.asyncMode : {σ : Type} → Lean.EnvExtension σ → Lean.EnvExtension.AsyncMode
-- Init.Data.Vector.Basic
/-- Append two vectors.  -/
Vector.append : {α : Type u_1} → {n m : ℕ} → Vector α n → Vector α m → Vector α (n + m)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.next?_toList : ∀ {α : Type u_1} {s : RBTree.RBNode.Stream α},
  Option.map
      (fun x =>
        match x with
        | (a, b) => (a, b.toList))
      s.next? =
    s.toList.next?
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂_eqToHom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {x y : B} (f g : x ⟶ y) (hfg : f = g),
  F.map₂ (CategoryTheory.eqToHom hfg) = CategoryTheory.eqToHom ⋯
-- Init.Data.Array.Sort.Basic
_private.Init.Data.Array.Sort.Basic.0.Array.MergeSort.Internal.merge.go.eq_def : ∀ {α : Type u_1} (le : α → α → Bool) (xs ys : Subarray α) (hxs : 0 < Std.Slice.size xs) (hys : 0 < Std.Slice.size ys)
  (acc : Array α),
  Array.MergeSort.Internal.merge.go✝ le xs ys hxs hys acc =
    have x := xs[0];
    have y := ys[0];
    if le x y = true then
      if hi : 1 < Std.Slice.size xs then Array.MergeSort.Internal.merge.go✝ le (xs.drop 1) ys ⋯ hys (acc.push x)
      else Std.Slice.foldl (fun acc y => acc.push y) (acc.push x) ys
    else
      if hj : 1 < Std.Slice.size ys then Array.MergeSort.Internal.merge.go✝ le xs (ys.drop 1) hxs ⋯ (acc.push y)
      else Std.Slice.foldl (fun acc x => acc.push x) (acc.push y) xs
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
/-- The inverse of a linear change of variables given by matrix inversion.  -/
WeierstrassCurve.VariableChange.inv_def : ∀ {R : Type u} [inst : CommRing R] (C : WeierstrassCurve.VariableChange R),
  C⁻¹ = { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }
-- Mathlib.Algebra.Group.Equiv.Opposite
MulEquiv.inv'_symm_apply : ∀ (G : Type u_3) [inst : DivisionMonoid G], ⇑(MulEquiv.inv' G).symm = Inv.inv ∘ MulOpposite.unop
-- Mathlib.Data.Finsupp.Multiset
Finsupp.coe_orderIsoMultiset_symm : ∀ {ι : Type u_3} [inst : DecidableEq ι], ⇑Finsupp.orderIsoMultiset.symm = ⇑Multiset.toFinsupp
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.dist_eq_two_inv_pow : ∀ {α : Type u_1} {s t : Stream'.Seq α}, s ≠ t → ∃ n, dist s t = 2⁻¹ ^ n
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mk.inj : ∀ {numVarsSucc : ℕ} {clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc))}
  {rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc))}
  {assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment}
  {clauses_1 : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc))}
  {rupUnits_1 ratUnits_1 : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc))}
  {assignments_1 : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment},
  { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =
      { clauses := clauses_1, rupUnits := rupUnits_1, ratUnits := ratUnits_1, assignments := assignments_1 } →
    clauses = clauses_1 ∧ rupUnits = rupUnits_1 ∧ ratUnits = ratUnits_1 ∧ assignments = assignments_1
-- Batteries.Data.List.Basic
List.rotate'.eq_2 : ∀ {α : Type u_1} (x : List α), (x = [] → False) → x.rotate' 0 = x
-- Lean.Environment
Lean.Kernel.Exception.declHasMVars.inj : ∀ {env : Lean.Kernel.Environment} {name : Lean.Name} {expr : Lean.Expr} {env_1 : Lean.Kernel.Environment}
  {name_1 : Lean.Name} {expr_1 : Lean.Expr},
  Lean.Kernel.Exception.declHasMVars env name expr = Lean.Kernel.Exception.declHasMVars env_1 name_1 expr_1 →
    env = env_1 ∧ name = name_1 ∧ expr = expr_1
-- Mathlib.RingTheory.IsPrimary
Submodule.IsPrimary.isPrime_radical_colon : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {S : Submodule R M}, S.IsPrimary → (S.colon Set.univ).radical.IsPrime
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.finsetSum_apply' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (I : Finset ι)
  (κ : ι → ProbabilityTheory.Kernel α β) (a : α) (s : Set β), ((∑ i ∈ I, κ i) a) s = ∑ i ∈ I, ((κ i) a) s
-- Init.Data.SInt.Lemmas
Int16.toInt64_le : ∀ {a b : Int16}, a.toInt64 ≤ b.toInt64 ↔ a ≤ b
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
cfcₙL_integrable : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NonUnitalNormedRing A] [inst_3 : StarRing A] [inst_4 : NormedSpace 𝕜 A]
  [inst_5 : IsScalarTower 𝕜 A A] [inst_6 : SMulCommClass 𝕜 A A] [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p]
  [inst_8 : CompleteSpace A] (a : A) (f : X → ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜),
  MeasureTheory.Integrable f μ →
    ∀ (ha : autoParam (p a) cfcₙL_integrable._auto_1), MeasureTheory.Integrable (fun x => (cfcₙL ha) (f x)) μ
-- Lean.Parser.Command
/-- `#where` gives a description of the state of the current scope scope.
This includes the current namespace, `open` namespaces, `universe` and `variable` commands,
and options set with `set_option`.
 -/
Lean.Parser.Command.where : Lean.Parser.Parser
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Bundle.ContMDiffRiemannianMetric.mk.sizeOf_spec : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  [inst_3 : TopologicalSpace B] [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℝ F] {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_8 : (b : B) → TopologicalSpace (E b)] [inst_9 : (b : B) → AddCommGroup (E b)]
  [inst_10 : (b : B) → Module ℝ (E b)] [inst_11 : FiberBundle F E] [inst_12 : VectorBundle ℝ F E] [inst_13 : SizeOf EB]
  [inst_14 : SizeOf HB] [inst_15 : SizeOf B] [inst_16 : SizeOf F] [inst_17 : (a : B) → SizeOf (E a)]
  (inner : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ) (symm : ∀ (b : B) (v w : E b), ((inner b) v) w = ((inner b) w) v)
  (pos : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner b) v) v)
  (isVonNBounded : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1})
  (contMDiff : ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n fun b => ⟨b, inner b⟩),
  sizeOf { inner := inner, symm := symm, pos := pos, isVonNBounded := isVonNBounded, contMDiff := contMDiff } = 1
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
span_le_span_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  {s t u : Set M}, LinearIndependent R Subtype.val → s ⊆ u → t ⊆ u → (Submodule.span R s ≤ Submodule.span R t ↔ s ⊆ t)
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_add : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (n m a a' a'' : M) (ha' : n + a = a')
  (ha'' : m + a' = a''),
  F.shiftIso (m + n) a a'' ⋯ =
    CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n) (F.shift a) ≪≫
      (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n) (F.shift a) ≪≫
        (CategoryTheory.shiftFunctor C m).isoWhiskerLeft (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
-- Mathlib.Algebra.Order.Star.Basic
Nat.instStarOrderedRing : StarOrderedRing ℕ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_succ_succ : ∀ {m n : ℕ}, ((m + 1)<...=n + 1).toList = List.map (fun x => x + 1) (m<...=n).toList
-- Init.Data.Slice.List.Lemmas
ListSlice.mkSlice_ric_eq_mkSlice_rcc : ∀ {α : Type u_1} {xs : ListSlice α} {hi : ℕ},
  (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rcc.Sliceable.mkSlice xs 0...=hi
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.dec.inj : ∀ {h h_1 : Lean.FVarId},
  Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.dec h = Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.dec h_1 → h = h_1
-- Mathlib.Data.Multiset.Defs
Multiset.card_attach : ∀ {α : Type u_1} {m : Multiset α}, m.attach.card = m.card
-- Init.Data.BitVec.Lemmas
BitVec.toInt_umod_of_msb : ∀ {w : ℕ} {x y : BitVec w}, x.msb = false → (x % y).toInt = x.toInt % ↑y.toNat
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.tan_sub : ∀ {x y : ℝ},
  (((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * Real.pi / 2) ∨
      (∃ k, x = (2 * ↑k + 1) * Real.pi / 2) ∧ ∃ l, y = (2 * ↑l + 1) * Real.pi / 2) →
    Real.tan (x - y) = (Real.tan x - Real.tan y) / (1 + Real.tan x * Real.tan y)
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.filter_snd_eq_antidiagonal : ∀ {A : Type u_1} [inst : AddCommMonoid A] [inst_1 : PartialOrder A] [CanonicallyOrderedAdd A] [inst_3 : Sub A]
  [OrderedSub A] [AddLeftReflectLE A] [inst_6 : Finset.HasAntidiagonal A] (n m : A)
  [inst_7 : DecidablePred fun x => x = m] [inst_8 : Decidable (m ≤ n)],
  {x ∈ Finset.HasAntidiagonal.antidiagonal n | x.2 = m} = if m ≤ n then {(n - m, m)} else ∅
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.sound : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R} {t s : ↥(ValuativeRel.posSubmonoid R)},
  x * ↑s ≤ᵥ y * ↑t → y * ↑t ≤ᵥ x * ↑s → ValuativeRel.ValueGroupWithZero.mk x t = ValuativeRel.ValueGroupWithZero.mk y s
-- Batteries.Data.List.Lemmas
List.idxsOf_append : ∀ {α : Type u_1} {xs ys : List α} {x : α} {s : ℕ} [inst : BEq α],
  List.idxsOf x (xs ++ ys) s = List.idxsOf x xs s ++ List.idxsOf x ys (s + xs.length)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
List.sum_toFinset_count_eq_length : ∀ {ι : Type u_1} [inst : DecidableEq ι] (l : List ι), ∑ a ∈ l.toFinset, List.count a l = l.length
-- Mathlib.Data.Set.Countable
Set.countable_iff_nonempty_encodable : ∀ {α : Type u} {s : Set α}, s.Countable ↔ Nonempty (Encodable ↑s)
-- Std.Data.DTreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise `none`.
The key in the returned pair will be `BEq` to the input `a`.
 -/
Std.DTreeMap.getEntry? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Option ((a : α) × β a)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.inter_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)],
  E.inter F =
    (E.bind fun i => CategoryTheory.PreZeroHypercover.pullback₁ (E.f i) F).reindex (Equiv.sigmaEquivProd E.I₀ F.1).symm
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.instInhabitedQuotientUnitUnit : Inhabited (Path.Homotopic.Quotient () ())
-- Batteries.CodeAction.Match
/-- Filter for the info-nodes to find the match-nodes.  -/
Batteries.CodeAction.isMatchTerm : Lean.Elab.Info → Bool
-- Init.Data.UInt.Lemmas
USize.toUSize_toUInt16 : ∀ (n : USize), n.toUInt16.toUSize = n % 65536
-- Mathlib.Topology.Algebra.UniformConvergence
instNegUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [Neg β] → Neg (UniformOnFun α β 𝔖)
-- Batteries.Util.ProofWanted
/-- Parses the surface syntax of `theorem_wanted` and forwards to the shared `elabWanted`.  -/
elabTheoremWanted : Lean.Elab.Command.CommandElab
-- Mathlib.Algebra.Ring.Int.Parity
Int.not_even_iff_odd : ∀ {n : ℤ}, ¬Even n ↔ Odd n
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- A partial map as a rational map.  -/
AlgebraicGeometry.Scheme.PartialMap.toRationalMap : {X Y : AlgebraicGeometry.Scheme} → X.PartialMap Y → X.RationalMap Y
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Path.zoom_del.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (x : RBTree.RBNode α)
  (h_1 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r))
  (h_2 : (x : RBTree.RBNode α) → motive x),
  (∀ (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α), x = RBTree.RBNode.node c l v r → False) →
    (match x with
      | RBTree.RBNode.node c l v r => h_1 c l v r
      | x => h_2 x) =
      h_2 x
-- Mathlib.Computability.Reduce
toNat_manyOneReducible : ∀ {α : Type u} [inst : Primcodable α] [inst_1 : Inhabited α] {p : Set α}, toNat p ≤₀ p