mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β]
  [inst_4 : Min γ] [inst_5 : Top γ] {g : InfTopHom β γ} {f₁ f₂ : InfTopHom α β},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Std.Do.PostCond
Std.Do.instInhabitedExceptConds : {ps : Std.Do.PostShape} → Inhabited (Std.Do.ExceptConds ps)
-- Mathlib.Data.Finset.Disjoint
List.disjoint_toFinset_iff_disjoint : ∀ {α : Type u_2} [inst : DecidableEq α] {l l' : List α}, Disjoint l.toFinset l'.toFinset ↔ l.Disjoint l'
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftMonoidWithZeroHom_apply : ∀ {K : Type u} [inst : Field K] {L : Type u_1} [inst_1 : CommGroupWithZero L] (φ : Polynomial K →*₀ L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (f : RatFunc K),
  (RatFunc.liftMonoidWithZeroHom φ hφ) f = φ f.num / φ f.denom
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.eq_neg_of_add_eq_zero_right : ∀ {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α}, a + ↑u = 0 → a = ↑(-u)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k a : α} {fallback : β a} {v : β k},
  (t.insert k v).getD a fallback = if h : cmp k a = Ordering.eq then cast ⋯ v else t.getD a fallback
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
/-- `c.carrier` is the set of conjugates represented by `c`.  -/
ConjRootClass.carrier : {K : Type u_1} →
  {L : Type u_2} → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → ConjRootClass K L → Set L
-- Mathlib.Algebra.Group.Submonoid.Support
Submonoid.mulSupport_toSubmonoid : ∀ {G : Type u_1} [inst : Group G] (M : Submonoid G), M.mulSupport.toSubmonoid = M ⊓ M⁻¹
-- Mathlib.NumberTheory.ZetaValues
continuous_bernoulliFun : ∀ (k : ℕ), Continuous (bernoulliFun k)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivWithinAt_inter' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s t : Set E},
  t ∈ nhdsWithin x s → (HasFDerivWithinAt f f' (s ∩ t) x ↔ HasFDerivWithinAt f f' s x)
-- Init.SimpLemmas
dite_congr : ∀ {b c : Prop} {α : Sort u_1} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
  (h₁ : b = c), (∀ (h : c), x_1 ⋯ = u h) → (∀ (h : ¬c), y ⋯ = v h) → dite b x_1 y = dite c u v
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- The negative of a harmonic function is harmonic.
 -/
InnerProductSpace.HarmonicAt.neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {x : E},
  InnerProductSpace.HarmonicAt f x → InnerProductSpace.HarmonicAt (-f) x
-- Std.Data.ByteSlice
/-- A region of some underlying byte array.

A byte slice contains a byte array together with the start and end indices of a region of interest.
Byte slices can be used to avoid copying or allocating space, while being more convenient than
tracking the bounds by hand. The region of interest consists of every index that is both greater
than or equal to `start` and strictly less than `stop`.
 -/
ByteSlice : Type
-- Mathlib.LinearAlgebra.Projection
LinearMap.ker_id_sub_eq_of_proj : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p : Submodule R E}
  {f : E →ₗ[R] ↥p}, (∀ (x : ↥p), f ↑x = x) → (LinearMap.id - p.subtype ∘ₗ f).ker = p
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.fromPreimage_ι_assoc : ∀ {X Y : SSet} (A : X.Subcomplex) (p : Y ⟶ X) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (A.fromPreimage p) (CategoryTheory.CategoryStruct.comp A.ι h) =
    CategoryTheory.CategoryStruct.comp (A.preimage p).ι (CategoryTheory.CategoryStruct.comp p h)
-- Init.Data.BitVec.Lemmas
BitVec.add_neg_eq_sub : ∀ {w : ℕ} {x y : BitVec w}, x + -y = x - y
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}, k ∈ t.insert k
-- Batteries.Lean.LawfulMonad
instLawfulMonadCommandElabM_batteries : LawfulMonad Lean.Elab.Command.CommandElabM
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.single_finsetSum : ∀ {α : Type u_1} {ι : Type u_2} {M : Type u_8} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → M) (a : α),
  (fun₀ | a => ∑ b ∈ s, f b) = ∑ b ∈ s, fun₀ | a => f b
-- Init.Data.Option.Lemmas
Option.not_isSome : ∀ {α : Type u_1} (a : Option α), (!a.isSome) = a.isNone
-- Std.Time.Format.DateFormat
/-- Narrow month names (12 elements, index 0 = J).
 -/
Std.Time.DateFormatSymbols.monthNarrow : Std.Time.DateFormatSymbols → Vector String 12
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- Replacing a vertex of a simplex by its centroid preserves affine independence.  -/
Affine.Simplex.affineIndependent_points_update_centroid : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  AffineIndependent k (Function.update s.points i s.centroid)
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.widget.sizeOf_spec : ∀ (wi : Lean.Widget.WidgetInstance) (alt : Lean.Widget.TaggedText Lean.Widget.MsgEmbed),
  sizeOf (Lean.Widget.MsgEmbed.widget wi alt) = 1 + sizeOf wi + sizeOf alt
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.range_subset : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A),
  Set.range ⇑(algebraMap R A) ⊆ ↑S
-- Mathlib.Order.RelIso.Basic
RelEmbedding.mk.sizeOf_spec : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} [inst : SizeOf α] [inst_1 : SizeOf β]
  [inst_2 : (a a_1 : α) → SizeOf (r a a_1)] [inst_3 : (a a_1 : β) → SizeOf (s a a_1)] (toEmbedding : α ↪ β)
  (map_rel_iff' : ∀ {a b : α}, s (toEmbedding a) (toEmbedding b) ↔ r a b),
  sizeOf { toEmbedding := toEmbedding, map_rel_iff' := map_rel_iff' } = 1 + sizeOf toEmbedding
-- Mathlib.Order.UpperLower.Basic
/-- **Alias** of the reverse direction of `isLowerSet_preimage_toDual_iff`. -/
IsUpperSet.ofDual : ∀ {α : Type u_1} [inst : LE α] {s : Set αᵒᵈ}, IsUpperSet s → IsLowerSet (⇑OrderDual.toDual ⁻¹' s)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof → Sort u} →
    (t : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr) →
      ((t : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr) → t.below → motive_1 t) →
        ((t : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof) → t.below → motive_2 t) → motive_1 t ×' t.below
-- Std.Internal.UV.System
Std.Internal.UV.System.GroupInfo.mk.sizeOf_spec : ∀ (groupname : String) (gid : UInt64) (members : Array String),
  sizeOf { groupname := groupname, gid := gid, members := members } = 1 + sizeOf groupname + sizeOf gid + sizeOf members
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalGroup.mulInvClosureNhd.nhds : ∀ {G : Type u_1} [inst : TopologicalSpace G] {T W : Set G} [inst_1 : Group G],
  IsTopologicalGroup.mulInvClosureNhd T W → T ∈ nhds 1
-- Lean.Elab.Do.Legacy
/-- Auxiliary datastructure for representing a `do` code block, and compiling "reassignments" (e.g., `x := x + 1`).
We convert `Code` into a `Syntax` term representing the:
- `do`-block, or
- the visitor argument for the `forIn` combinator.

We say the following constructors are terminals:
- `break`:    for interrupting a `for x in s`
- `continue`: for interrupting the current iteration of a `for x in s`
- `return e`: for returning `e` as the result for the whole `do` computation block
- `action a`: for executing action `a` as a terminal
- `ite`:      if-then-else
- `match`:    pattern matching
- `jmp`       a goto to a join-point

We say the terminals `break`, `continue`, `action`, and `return` are "exit points"

Note that, `return e` is not equivalent to `action (pure e)`. Here is an example:
```
def f (x : Nat) : IO Unit := do
if x == 0 then
   return ()
IO.println "hello"
```
Executing `#eval f 0` will not print "hello". Now, consider
```
def g (x : Nat) : IO Unit := do
if x == 0 then
   pure ()
IO.println "hello"
```
The `if` statement is essentially a noop, and "hello" is printed when we execute `g 0`.

- `decl` represents all declaration-like `doElem`s (e.g., `let`, `have`, `let rec`).
  The field `stx` is the actual `doElem`,
  `vars` is the array of variables declared by it, and `cont` is the next instruction in the `do` code block.
  `vars` is an array since we have declarations such as `let (a, b) := s`.

- `reassign` is an reassignment-like `doElem` (e.g., `x := x + 1`).

- `joinpoint` is a join point declaration: an auxiliary `let`-declaration used to represent the control-flow.

- `seq a k` executes action `a`, ignores its result, and then executes `k`.
  We also store the do-elements `dbg_trace` and `assert!` as actions in a `seq`.

A code block `C` is well-formed if
- For every `jmp ref j as` in `C`, there is a `joinpoint j ps b k` and `jmp ref j as` is in `k`, and
  `ps.size == as.size`  -/
Lean.Elab.Term.Do.Code : Type
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.strictMonoOn_one_sub_smoothingFn : StrictMonoOn (fun x => 1 - AkraBazziRecurrence.smoothingFn x) (Set.Ioi 1)
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond_one_right : ∀ (n : ℕ), (n + 1).stirlingSecond 1 = 1
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonWorkspaceClientCapabilities.fromJson : Lean.Json → Except String Lean.Lsp.WorkspaceClientCapabilities
-- Mathlib.Data.QPF.Multivariate.Constructions.Const
MvQPF.Const.get_mk : ∀ {n : ℕ} {A : Type u} {α : TypeVec.{u} n} (x : A), (MvQPF.Const.mk x).get = x
-- Mathlib.Order.Partition.Finpartition
Finpartition.existsUnique_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α}, a ∈ s → ∃! t, t ∈ P.parts ∧ a ∈ t
-- Mathlib.Algebra.Ring.GeomSum
dvd_pow_sub_one_of_dvd : ∀ {R : Type u_1} [inst : Ring R] {r : R} {a b : ℕ}, a ∣ b → r ^ a - 1 ∣ r ^ b - 1
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
max_sub_min_eq_abs' : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] [AddRightMono α] (a b : α),
  max a b - min a b = |a - b|
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types
CategoryTheory.Limits.instAB5Type : CategoryTheory.AB5 (Type v)
-- Mathlib.Algebra.Ring.BooleanRing
toBoolRing_ofBoolRing : ∀ {α : Type u_1} (a : AsBoolRing α), toBoolRing (ofBoolRing a) = a
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.comp_map : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.PreSubmersivePresentation S T ι' σ')
  (P : Algebra.PreSubmersivePresentation R S ι σ) (a : σ' ⊕ σ),
  (Q.comp P).map a = Sum.elim (fun rq => Sum.inl (Q.map rq)) (fun rp => Sum.inr (P.map rp)) a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_alter_of_not_compare_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k k' : α} {f : Option β → Option β}, ¬cmp k k' = Ordering.eq → (k' ∈ Std.ExtDTreeMap.Const.alter t k f ↔ k' ∈ t)
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₂_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (μ : CategoryTheory.MonoidalCategory.curriedTensorPre F ⟶ CategoryTheory.MonoidalCategory.curriedTensorPost F)
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₂ μ).app X₁).app X₂).app X₃ =
    (μ.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)).app X₃
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin_zero_fst : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a b : α),
  (F.intervalGapsWithin h a b 0).1 = a
-- Mathlib.GroupTheory.CosetCover
/-- If `H` is a subgroup of `G` and `G` is the union of a finite family of left cosets of `H`
then `H` has finite index.  -/
Subgroup.finiteIndex_of_leftCoset_cover_const : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {s : Finset ι} {H : Subgroup G} {g : ι → G},
  ⋃ i ∈ s, g i • ↑H = Set.univ → H.FiniteIndex
-- Init.Data.String.Basic
String.startPos_eq_endPos_iff : ∀ {b : String}, b.startPos = b.endPos ↔ b = ""
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.liftPath_zero : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) (γ : C(↑unitInterval, X)) (e : E) (γ_0 : γ 0 = p e), (cov.liftPath γ e γ_0) 0 = e
-- Init.Data.BitVec.Lemmas
BitVec.getElem_shiftLeft : ∀ {m i : ℕ} {x : BitVec m} {n : ℕ} (h : i < m), (x <<< n)[i] = (!decide (i < n) && x[i - n])
-- Lean.Elab.InfoTree.Types
Lean.Elab.TermInfo.lctx : Lean.Elab.TermInfo → Lean.LocalContext
-- Mathlib.Order.Interval.Set.Basic
Set.instNoMaxOrderElemIoi : ∀ {α : Type u_1} [inst : Preorder α] {a : α} [NoMaxOrder α], NoMaxOrder ↑(Set.Ioi a)
-- Lean.Level
Lean.Level.PP.Result.leaf.sizeOf_spec : ∀ (a : Lean.Name), sizeOf (Lean.Level.PP.Result.leaf a) = 1 + sizeOf a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)]
  (X : P.FullSubcategory),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.obj).hom
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.listEncode.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} (x : L.Term α),
  x.listEncode =
    match x with
    | FirstOrder.Language.var i => [Sum.inl i]
    | FirstOrder.Language.func f ts => Sum.inr ⟨l, f⟩ :: List.flatMap (fun i => (ts i).listEncode) (List.finRange l)
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.piUnique_symm_apply : ∀ {ι : Type u_16} (M : ι → Type u_17) [inst : (j : ι) → Mul (M j)] [inst_1 : Unique ι] (x : M default) (i : ι),
  (MulEquiv.piUnique M).symm x i = uniqueElim x i
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.QuasiMeasurePreserving.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {τ : MeasureTheory.Measure γ}
  {ω : Type u_4} {mω : MeasurableSpace ω} {υ : MeasureTheory.Measure ω} [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite τ] [MeasureTheory.SFinite υ] {f : α → β} {g : γ → ω},
  MeasureTheory.Measure.QuasiMeasurePreserving f μ ν →
    MeasureTheory.Measure.QuasiMeasurePreserving g τ υ →
      MeasureTheory.Measure.QuasiMeasurePreserving (Prod.map f g) (μ.prod τ) (ν.prod υ)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : ℝ≥0 → ℝ≥0` is continuous on a compact set `s` and `a : X → A` is continuous on
`t : Set X`, and `0 ≤ a x` and has spectrum contained in `s` for all `x ∈ t`, then
`fun x ↦ cfc f (a x)` is continuous on `t`.  -/
ContinuousOn.cfc_nnreal' : ∀ {X : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [inst_10 : TopologicalSpace X] {s : Set NNReal},
  IsCompact s →
    ∀ (f : NNReal → NNReal) {a : X → A} {t : Set X},
      ContinuousOn a t →
        (∀ x ∈ t, spectrum NNReal (a x) ⊆ s) →
          (∀ x ∈ t, 0 ≤ a x) →
            autoParam (ContinuousOn f s) ContinuousOn.cfc_nnreal'._auto_1 → ContinuousOn (fun x => cfc f (a x)) t
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.isEquivalence_left_of_isEquivalence_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.IsEquivalence], L.IsEquivalence
-- Mathlib.Data.Part
Part.sub_get_eq : ∀ {α : Type u_1} [inst : Sub α] (a b : Part α) (hab : (a - b).Dom), (a - b).get hab = a.get ⋯ - b.get ⋯
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.posDef_iff_dotProduct_mulVec : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [inst_3 : Fintype n]
  {M : Matrix n n R}, M.PosDef ↔ M.IsHermitian ∧ ∀ ⦃x : n → R⦄, x ≠ 0 → 0 < star x ⬝ᵥ M.mulVec x
-- Batteries.Recycling.RBTree.Basic
_private.Batteries.Recycling.RBTree.Basic.0.RBTree.RBNode.append.match_1.eq_4 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b c : RBTree.RBNode α) (y : α) (d : RBTree.RBNode α) (h_1 : (x : RBTree.RBNode α) → motive RBTree.RBNode.nil x)
  (h_2 : (x : RBTree.RBNode α) → motive x RBTree.RBNode.nil)
  (h_3 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.red c y d))
  (h_4 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.black a x b) (RBTree.RBNode.node RBTree.RBColor.black c y d))
  (h_5 :
    (a l : RBTree.RBNode α) →
      (v : α) →
        (r : RBTree.RBNode α) →
          a = RBTree.RBNode.node RBTree.RBColor.black l v r →
            (b : RBTree.RBNode α) →
              (x : α) →
                (c : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.black l v r) (RBTree.RBNode.node RBTree.RBColor.red b x c))
  (h_6 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c l : RBTree.RBNode α) →
          (v : α) →
            (r : RBTree.RBNode α) →
              c = RBTree.RBNode.node RBTree.RBColor.black l v r →
                motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.black l v r)),
  (match RBTree.RBNode.node RBTree.RBColor.black a x b, RBTree.RBNode.node RBTree.RBColor.black c y d with
    | RBTree.RBNode.nil, x => h_1 x
    | x, RBTree.RBNode.nil => h_2 x
    | RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.red c y d => h_3 a x b c y d
    | RBTree.RBNode.node RBTree.RBColor.black a x b, RBTree.RBNode.node RBTree.RBColor.black c y d => h_4 a x b c y d
    | a@h:(RBTree.RBNode.node RBTree.RBColor.black l v r), RBTree.RBNode.node RBTree.RBColor.red b x c =>
      h_5 a l v r h b x c
    | RBTree.RBNode.node RBTree.RBColor.red a x b, c@h:(RBTree.RBNode.node RBTree.RBColor.black l v r) =>
      h_6 a x b c l v r h) =
    h_4 a x b c y d
-- Mathlib.CategoryTheory.Localization.OfQuotient
CategoryTheory.Quotient.isLocalization_functor' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) [CategoryTheory.Congruence r]
  (W : CategoryTheory.MorphismProperty C),
  W.IsInvertedBy (CategoryTheory.Quotient.functor r) →
    (∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.ι) → (CategoryTheory.Quotient.functor r).IsLocalization W
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.State.minPrec : Lean.PrettyPrinter.Parenthesizer.State → Option ℕ
-- Batteries.Data.Nat.Bisect
Nat.avg_lt_right : ∀ {a b : ℕ}, a < b → a.avg b < b
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G], ContinuousLinearMap.lTensor G 0 = 0
-- Mathlib.RingTheory.FreeCommRing
FreeRing.coe_add : ∀ {α : Type u} (x y : FreeRing α), ↑(x + y) = ↑x + ↑y
-- Init.Data.List.Sublist
List.IsSuffix.filterMap : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) ⦃l₁ l₂ : List α⦄,
  l₁ <:+ l₂ → List.filterMap f l₁ <:+ List.filterMap f l₂
-- Mathlib.Data.PEquiv
/-- The inverse partial equivalence.  -/
PEquiv.symm : {α : Type u} → {β : Type v} → (α ≃. β) → β ≃. α
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.of_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {m n : WithTop ℕ∞},
  m ≤ n → ∀ [IsManifold I n M], IsManifold I m M
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the forward direction of the isomorphism
`PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂` w.r.t. the canonical maps to the colimit.  -/
CategoryTheory.Limits.PreservesColimit₂.map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv_assoc : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] (K₁ : CategoryTheory.Functor J₁ C₁)
  (K₂ : CategoryTheory.Functor J₂ C₂) (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G] [inst_6 : CategoryTheory.Limits.HasColimit K₁]
  [inst_7 : CategoryTheory.Limits.HasColimit K₂] (j : J₁ × J₂) {Z : C}
  (h :
    CategoryTheory.Limits.colimit
        (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp ((G.map (CategoryTheory.Limits.colimit.ι K₁ j.1)).app (K₂.obj j.2))
      (CategoryTheory.CategoryStruct.comp
        ((G.obj (CategoryTheory.Limits.colimit K₁)).map (CategoryTheory.Limits.colimit.ι K₂ j.2))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ K₁ K₂ G).inv h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι
        (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j)
      h
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsAffine Y]
  (𝒰 : X.OpenCover) [∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)],
  P f ↔
    ∀ (i : 𝒰.I₀),
      Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)))