mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.instPreservesFiniteLimitsFunctorOppositeSheafTransportAndSheafify : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse]
  [inst_4 : CategoryTheory.HasSheafify K A],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Equivalence.transportAndSheafify J K e A)
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- The **Sequential Banach-Alaoglu theorem**: closed balls of the dual of a separable
normed space `V` are sequentially compact in the weak-\* topology.  -/
WeakDual.isSeqCompact_closedBall : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [TopologicalSpace.SeparableSpace E] [ProperSpace 𝕜] (x' : StrongDual 𝕜 E) (r : ℝ),
  IsSeqCompact (⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall x' r)
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minEntry.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β)
  (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1).isEmpty =
                              false) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            h),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x with
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_1 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      h_3 => h_2 size k v l size_1 k_1 v_1 l_1 r h r_1 h_3) =
    h_1 size k v r x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α]
  {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKeyD k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l)
        fallback =
      ((Std.Internal.List.getKey? k l).pfilter fun x h => (f x (Std.Internal.List.getValueCast x l ⋯)).isSome).getD
        fallback
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.classifyStandaloneWeekdayNumberText : ℕ → Option (Std.Time.Number ⊕ Std.Time.Text)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.of.sizeOf_spec : ∀ (R : Type u) [inst : CommRing R] [inst_1 : SizeOf R] (X : Type v) [commRing : CommRing X]
  [hopfAlgebra : HopfAlgebra R X],
  sizeOf { X := X, commRing := commRing, hopfAlgebra := hopfAlgebra } =
    1 + sizeOf X + sizeOf commRing + sizeOf hopfAlgebra
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopic.symm : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] ⦃f g : C(X, Y)⦄,
  f.Homotopic g → g.Homotopic f
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBaseNat.atom.injEq : ∀ {e : Q(ℕ)} (id id_1 : ℕ),
  (Mathlib.Tactic.Ring.Common.ExBaseNat.atom id = Mathlib.Tactic.Ring.Common.ExBaseNat.atom id_1) = (id = id_1)
-- Mathlib.RingTheory.Ideal.Cotangent
/-- The quotient ring of `I ⧸ I ^ 2` is `R ⧸ I`.  -/
Ideal.quotCotangent : {R : Type u} → [inst : CommRing R] → (I : Ideal R) → (R ⧸ I ^ 2) ⧸ I.cotangentIdeal ≃+* R ⧸ I
-- Mathlib.Data.Set.Finite.Basic
Set.Infinite.preimage' : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β}, (s ∩ Set.range f).Infinite → (f ⁻¹' s).Infinite
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.lmfdbIdParser.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Vector.MapIdx
Vector.mapIdx_reverse : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : ℕ → α → β},
  Vector.mapIdx f xs.reverse = (Vector.mapIdx (fun i => f (n - 1 - i)) xs).reverse
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.const_comp' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure γ) (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsMarkovKernel κ], (ProbabilityTheory.Kernel.const β μ).comp κ = ProbabilityTheory.Kernel.const α μ
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.dist_eq_one_of_head : ∀ {α : Type u_1} {s t : Stream'.Seq α}, s.head ≠ t.head → dist s t = 1
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.locallySmall_of_faithful : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) [F.Faithful] [CategoryTheory.LocallySmall.{w, v', u'} D],
  CategoryTheory.LocallySmall.{w, v, u} C
-- Mathlib.Topology.UniformSpace.Matrix
Matrix.instCompleteSpace : ∀ (m : Type u_1) (n : Type u_2) (𝕜 : Type u_3) [inst : UniformSpace 𝕜] [CompleteSpace 𝕜], CompleteSpace (Matrix m n 𝕜)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMap.toNNReal_neg_algebraMap : ∀ {X : Type u_1} [inst : TopologicalSpace X] (r : NNReal), (-(algebraMap ℝ C(X, ℝ)) ↑r).toNNReal = 0
-- Plausible.Testable
/-- Test a universal property about propositions  -/
Plausible.Testable.propVarTestable : {var : String} →
  {β : Prop → Prop} →
    [(b : Bool) → Plausible.Testable (β (b = true))] →
      Plausible.Testable (Plausible.NamedBinder var (∀ (p : Prop), β p))
-- Init.Classical
Classical.indefiniteDescription : {α : Sort u} → (p : α → Prop) → (∃ x, p x) → { x // p x }
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Functor.toUnder_map_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} S]
  (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → X ⟶ F.obj Y)
  (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) {X_1 Y : S} (g : X_1 ⟶ Y),
  ((F.toUnder X f h).map g).right = F.map g
-- Mathlib.Geometry.Euclidean.NinePointCircle
/-- The 3(n+1)-point sphere of a simplex. Due to the lack of a better name and to avoid numbers in the
identifier, we still use the name "nine-point circle" even for higher dimensions. The center
$N$ is defined on the Euler line, collinear with circumcenter $O$ and centroid $G$, in the order of
$O$, $G$, and $N$, with $OG : GN = n : 1$. The radius is $1/n$ of the circumradius.
 -/
Affine.Simplex.ninePointCircle : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] → {n : ℕ} → Affine.Simplex ℝ P n → EuclideanGeometry.Sphere P
-- Mathlib.Data.PNat.Factors
PrimeMultiset.card_ofPrime : ∀ (p : Nat.Primes), Multiset.card (PrimeMultiset.ofPrime p) = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- Paste two pullback squares "horizontally" to obtain another pullback square.

The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
|            |            |
v₁₁          v₁₂          v₁₃
↓            ↓            ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
```
 -/
CategoryTheory.IsPullback.paste_horiz : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃},
  CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁ →
    CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂ →
      CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃
        (CategoryTheory.CategoryStruct.comp h₂₁ h₂₂)
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.stronglyAdapted`. -/
MeasureTheory.ProgMeasurable.stronglyAdapted : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : MeasurableSpace ι],
  MeasureTheory.IsStronglyProgressive f u → MeasureTheory.StronglyAdapted f u
-- Mathlib.Order.Monotone.Defs
instDecidableMonotoneOfForallForallForallLe : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → {f : α → β} → [i : Decidable (∀ (a b : α), a ≤ b → f a ≤ f b)] → Decidable (Monotone f)
-- Mathlib.RingTheory.FiniteType
/-- An algebra over a commutative semiring is of `FiniteType` if it is finitely generated
over the base ring as algebra.  -/
Algebra.FiniteType : (R : Type uR) → (A : Type uA) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Prop
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
/-- Lift a quasi-compact `P`-cover of a `u`-scheme in an arbitrary universe to universe `u`.
This is again quasi-compact.  -/
AlgebraicGeometry.Scheme.Cover.qculift : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S) →
      [AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover] →
        AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
/-- The opposite of a left fraction.  -/
CategoryTheory.MorphismProperty.LeftFraction.neg : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] →
      {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction X Y → W.LeftFraction X Y
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.instSliceableRciSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.instSliceableRciSlice._auto_1) →
      Std.Rci.Sliceable (Std.TreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.Const.RciSlice α β)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
/-- Type representing a sign of the first non-zero exponent, returned by `sign`.  -/
Tactic.ComputeAsymptotics.UnitMonomial.Sign : Type
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.coeff_toMvPowerSeries_symm : ∀ {R : Type u_2} [inst : Semiring R] {σ : Type u_3} [inst_1 : Finite σ] {f : MvPowerSeries σ R} {n : σ →₀ ℕ},
  (HahnSeries.toMvPowerSeries.symm f).coeff n = (MvPowerSeries.coeff n) f
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.brecOn_2.eq : ∀ {motive_1 : Lean.Widget.MsgEmbed → Sort u} {motive_2 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed → Sort u}
  {motive_3 :
    Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
        (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) →
      Sort u}
  {motive_4 : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u}
  {motive_5 : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u}
  (t :
    Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
      (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren))
  (F_1 : (t : Lean.Widget.MsgEmbed) → t.below → motive_1 t)
  (F_2 : (t : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Lean.Widget.MsgEmbed.below_1 t → motive_2 t)
  (F_3 :
    (t :
        Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
          (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)) →
      Lean.Widget.MsgEmbed.below_2 t → motive_3 t)
  (F_4 : (t : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) → Lean.Widget.MsgEmbed.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) → Lean.Widget.MsgEmbed.below_4 t → motive_5 t),
  Lean.Widget.MsgEmbed.brecOn_2 t F_1 F_2 F_3 F_4 F_5 = F_3 t (Lean.Widget.MsgEmbed.brecOn_2.go t F_1 F_2 F_3 F_4 F_5).2
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.instCoeHeadTSyntaxConsSyntaxNodeKindNilSuggestionText : {kind : Lean.SyntaxNodeKind} → CoeHead (Lean.TSyntax kind) Lean.Meta.Tactic.TryThis.SuggestionText
-- Mathlib.Data.Set.Lattice
Set.disjoint_iUnion₂_left : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : Set α},
  Disjoint (⋃ i, ⋃ j, s i j) t ↔ ∀ (i : ι) (j : κ i), Disjoint (s i j) t
-- Mathlib.Order.Filter.Defs
/-- The monadic bind operation on filter is defined the usual way in terms of `map` and `join`.

Unfortunately, this `bind` does not result in the expected applicative. See `Filter.seq` for the
applicative instance.  -/
Filter.bind : {α : Type u_1} → {β : Type u_2} → Filter α → (α → Filter β) → Filter β
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
/-- Any integrable function can be approximated by bounded continuous functions,
version in terms of `∫`.  -/
MeasureTheory.Integrable.exists_boundedContinuous_integral_sub_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {E : Type u_2}
  [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [μ.WeaklyRegular] {f : α → E},
  MeasureTheory.Integrable f μ → ∀ {ε : ℝ}, 0 < ε → ∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ MeasureTheory.Integrable (⇑g) μ
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree.eq_1 : ∀ {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R),
  m.degree f = m.toSyn.symm (f.support.sup ⇑m.toSyn)
-- Mathlib.Combinatorics.Young.SemistandardTableau
/-- `entry i j` is value of the `(i, j)` entry of the SSYT `μ`.  -/
SemistandardYoungTableau.entry : {μ : YoungDiagram} → SemistandardYoungTableau μ → ℕ → ℕ → ℕ
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.NatTrans.IsMonoidal.id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F₁ : CategoryTheory.Functor C D} [inst_4 : F₁.LaxMonoidal],
  CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.CategoryStruct.id F₁)
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.parentD_findAux : ∀ {i : ℕ} {self : Batteries.UnionFind} {x : Fin self.size},
  Batteries.UnionFind.parentD (self.findAux x).s i =
    if i = ↑x then self.rootD ↑x else Batteries.UnionFind.parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.norm_mul_coe_unitary : ∀ {E : Type u_2} [inst : NormedRing E] [inst_1 : StarRing E] [CStarRing E] (A : E) (U : ↥(unitary E)), ‖A * ↑U‖ = ‖A‖
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.rangeS_algebraMap : ∀ {R : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A), (algebraMap (↥S) A).rangeS = S.toSubsemiring
-- Mathlib.CategoryTheory.Abelian.Transfer
/-- No point making this an instance, as it requires `i` and `adj`.  -/
CategoryTheory.AbelianOfAdjunction.hasCokernels : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D C) [G.PreservesZeroMorphisms] (i : F.comp G ≅ CategoryTheory.Functor.id C)
  (adj : G ⊣ F), CategoryTheory.Limits.HasCokernels C
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- If the angle between two vectors is 0, the norm of their difference equals
the absolute value of the difference of their norms.  -/
InnerProductGeometry.norm_sub_eq_abs_sub_norm_of_angle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  InnerProductGeometry.angle x y = 0 → ‖x - y‖ = |‖x‖ - ‖y‖|
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.inv_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] (f : X ≃ₜ X) (x : X), f⁻¹ x = f.symm x
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.Hom.cover.congr_simp : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X S : AlgebraicGeometry.Scheme} (f f_1 : X ⟶ S)
  (e_f : f = f_1) (hf : P f) [inst : AlgebraicGeometry.Surjective f],
  AlgebraicGeometry.Scheme.Hom.cover f hf = AlgebraicGeometry.Scheme.Hom.cover f_1 ⋯
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.CallHierarchy.children : Lean.Lsp.Ipc.CallHierarchy → Array Lean.Lsp.Ipc.CallHierarchy
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.core.inj : ∀ {a b : Lean.Expr} {ra rb : Lean.Grind.CommRing.Expr} {a_1 b_1 : Lean.Expr} {ra_1 rb_1 : Lean.Grind.CommRing.Expr},
  Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.core a b ra rb =
      Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.core a_1 b_1 ra_1 rb_1 →
    a = a_1 ∧ b = b_1 ∧ ra = ra_1 ∧ rb = rb_1
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- **Alias** of `PointedCone.subset_hull`. -/
PointedCone.subset_span : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] {s : Set E}, s ⊆ ↑(PointedCone.hull R s)
-- Mathlib.Algebra.DirectSum.Internal
/-- The canonical ring isomorphism between `⨁ i, A i` and `R`  -/
DirectSum.coeRingHom_of : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddMonoid ι] [inst_5 : SetLike.GradedMonoid A] (i : ι)
  (x : ↥(A i)), (DirectSum.coeRingHom A) ((DirectSum.of (fun i => ↥(A i)) i) x) = ↑x
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Id for `OfCommSemiring.Q`  -/
Lean.Meta.Grind.Arith.CommRing.CommSemiring.ringId : Lean.Meta.Grind.Arith.CommRing.CommSemiring → ℕ
-- Mathlib.Data.Vector.MapLemmas
/-- If `f` takes a pair of states, but always returns the same value for both elements of the
pair, then we can simplify to just a single element of state.
 -/
List.Vector.mapAccumr_redundant_pair : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_5} {n : ℕ} {s : σ} {xs : List.Vector α n} (f : α → σ × σ → (σ × σ) × β),
  (∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2) →
    (List.Vector.mapAccumr f xs (s, s)).2 =
      (List.Vector.mapAccumr (fun x s => ((f x (s, s)).1.1, (f x (s, s)).2)) xs s).2
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
DFinsupp.coeFnAddMonoidHom.eq_1 : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)],
  DFinsupp.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.exists_isCircuit : ∀ {α : Type u_1} {M : Matroid α} [M✶.RankPos], ∃ C, M.IsCircuit C
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.map_comp_comul : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (self : A →ₗc[R] B),
  TensorProduct.map self.toLinearMap self.toLinearMap ∘ₗ CoalgebraStruct.comul =
    CoalgebraStruct.comul ∘ₗ self.toLinearMap
-- Mathlib.Data.Int.Bitwise
_private.Mathlib.Data.Int.Bitwise.0.Int.div2.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.negSucc n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_2 n
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.mk_ordinal : Cardinal.mk Ordinal.{u} = Cardinal.univ.{u, u + 1}
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isLE_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : CochainComplex C ℤ} (e : K ≅ L) (n : ℤ) [K.IsLE n], L.IsLE n
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given `AddCommMonoid`s `M, P`, Localization maps `f : M →+ N, k : P →+ Q` for AddSubmonoids
`S, T` respectively, and `g : M →+ P` such that `g(S) ⊆ T`, `f x = f y`
implies `k (g x) = k (g y)`.  -/
AddSubmonoid.LocalizationMap.comp_eq_of_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} {Q : Type u_4}
  [inst_3 : AddCommMonoid Q],
  (∀ (y : ↥S), g ↑y ∈ T) → ∀ (k : T.LocalizationMap Q) {x y : M}, f x = f y → k (g x) = k (g y)
-- Mathlib.Data.Finset.Filter
Finset.mem_filter : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α} {a : α}, a ∈ Finset.filter p s ↔ a ∈ s ∧ p a
-- Mathlib.RingTheory.WittVector.Defs
WittVector.instNatCast : {p : ℕ} → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [CommRing R] → NatCast (WittVector p R)
-- Mathlib.Data.Finsupp.Pointwise
/-- The product of `f g : α →₀ β` is the finitely supported function
whose value at `a` is `f a * g a`.  -/
Finsupp.instMul : {α : Type u₁} → {β : Type u₂} → [inst : MulZeroClass β] → Mul (α →₀ β)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Fréchet derivative of `compContinuousLinearMap f g` with respect to `g`.
The derivative with respect to `f` is given by `compContinuousLinearMapL`.  -/
ContinuousMultilinearMap.fderivCompContinuousLinearMap : {𝕜 : Type u} →
  {ι : Type v} →
    {E : ι → Type wE} →
      {E₁ : ι → Type wE₁} →
        {G : Type wG} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
              [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
                [inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)] →
                  [inst_4 : (i : ι) → NormedSpace 𝕜 (E₁ i)] →
                    [inst_5 : SeminormedAddCommGroup G] →
                      [inst_6 : NormedSpace 𝕜 G] →
                        [Fintype ι] →
                          [DecidableEq ι] →
                            ContinuousMultilinearMap 𝕜 E₁ G →
                              ((i : ι) → E i →L[𝕜] E₁ i) →
                                ((i : ι) → E i →L[𝕜] E₁ i) →L[𝕜] ContinuousMultilinearMap 𝕜 E G
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.map_of : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (f : G →* H) (x : G),
  (Abelianization.map f) (Abelianization.of x) = Abelianization.of (f x)
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.CongrInfo.fixedPrefix.inj : ∀ {prefixSize suffixSize prefixSize_1 suffixSize_1 : ℕ},
  Lean.Meta.Sym.CongrInfo.fixedPrefix prefixSize suffixSize =
      Lean.Meta.Sym.CongrInfo.fixedPrefix prefixSize_1 suffixSize_1 →
    prefixSize = prefixSize_1 ∧ suffixSize = suffixSize_1