mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {inst_2 : CategoryTheory.Limits.HasZeroObject C} {inst_3 : CategoryTheory.HasShift C ℤ}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_5 : CategoryTheory.Pretriangulated C}
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {m₁ : Z₁₂ ⟶ Z₁₃} {m₃ : Z₁₃ ⟶ Z₂₃} {comm₁ : CategoryTheory.CategoryStruct.comp m₁ v₁₃ = v₁₂}
  {comm₂ :
    CategoryTheory.CategoryStruct.comp w₁₂ ((CategoryTheory.shiftFunctor C 1).map m₁) =
      CategoryTheory.CategoryStruct.comp u₂₃ w₁₃}
  {comm₃ : CategoryTheory.CategoryStruct.comp w₁₃ ((CategoryTheory.shiftFunctor C 1).map m₃) = w₂₃}
  {comm₄ : CategoryTheory.CategoryStruct.comp m₃ v₂₃ = CategoryTheory.CategoryStruct.comp v₁₃ u₁₂}
  {mem :
    CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃ (CategoryTheory.CategoryStruct.comp v₂₃ w₁₂) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles}
  {m₁_1 : Z₁₂ ⟶ Z₁₃} {m₃_1 : Z₁₃ ⟶ Z₂₃} {comm₁_1 : CategoryTheory.CategoryStruct.comp m₁_1 v₁₃ = v₁₂}
  {comm₂_1 :
    CategoryTheory.CategoryStruct.comp w₁₂ ((CategoryTheory.shiftFunctor C 1).map m₁_1) =
      CategoryTheory.CategoryStruct.comp u₂₃ w₁₃}
  {comm₃_1 : CategoryTheory.CategoryStruct.comp w₁₃ ((CategoryTheory.shiftFunctor C 1).map m₃_1) = w₂₃}
  {comm₄_1 : CategoryTheory.CategoryStruct.comp m₃_1 v₂₃ = CategoryTheory.CategoryStruct.comp v₁₃ u₁₂}
  {mem_1 :
    CategoryTheory.Pretriangulated.Triangle.mk m₁_1 m₃_1 (CategoryTheory.CategoryStruct.comp v₂₃ w₁₂) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles},
  { m₁ := m₁, m₃ := m₃, comm₁ := comm₁, comm₂ := comm₂, comm₃ := comm₃, comm₄ := comm₄, mem := mem } =
      { m₁ := m₁_1, m₃ := m₃_1, comm₁ := comm₁_1, comm₂ := comm₂_1, comm₃ := comm₃_1, comm₄ := comm₄_1, mem := mem_1 } →
    m₁ = m₁_1 ∧ m₃ = m₃_1
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.map_bernoulliMeasure : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] [inst_1 : MeasurableSpace Y] [MeasurableSingletonClass X]
  [MeasurableSingletonClass Y] (x y : X) (f : X → Y) (p : ↑unitInterval),
  MeasureTheory.Measure.map f (ProbabilityTheory.bernoulliMeasure x y p) =
    ProbabilityTheory.bernoulliMeasure (f x) (f y) p
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.instCoeOutHom : {T : Type u} → [inst : CategoryTheory.Category.{v, u} T] → {X Y : T} → CoeOut (X ⟶ Y) (CategoryTheory.Arrow T)
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_X₁ : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).X₁ = F.comp CategoryTheory.ShortComplex.π₁
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Bot.isCyclic : ∀ {α : Type u_1} [inst : Group α], IsCyclic ↥⊥
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.finSnoc : ∀ {α : Type u_1} [inst : TopologicalSpace α] {n : ℕ} {X : Fin (n + 1) → Type u_5}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (X i)] {f : α → (j : Fin n) → X j.castSucc} {g : α → X (Fin.last n)}
  {a : α} {s : Set α},
  ContinuousWithinAt f s a → ContinuousWithinAt g s a → ContinuousWithinAt (fun a => Fin.snoc (f a) (g a)) s a
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.indepFun_mul_right : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β} [inst_2 : Mul β]
  [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.CondIndepFun m' hm' (f i) (f j * f k) μ
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.prod_map_comap_prod' : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {M' : Type u_5} {N' : Type u_6} [inst_2 : Mul M']
  [inst_3 : Mul N'] (f : M →ₙ* N) (g : M' →ₙ* N') (S : Subsemigroup N) (S' : Subsemigroup N'),
  Subsemigroup.comap (f.prodMap g) (S.prod S') = (Subsemigroup.comap f S).prod (Subsemigroup.comap g S')
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.prodProdProdComm_toLinearEquiv : ∀ (R : Type u_8) (M₁ : Type u_9) (M₂ : Type u_10) (M₃ : Type u_11) (M₄ : Type u_12) [inst : Semiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄]
  [inst_9 : TopologicalSpace M₁] [inst_10 : TopologicalSpace M₂] [inst_11 : TopologicalSpace M₃]
  [inst_12 : TopologicalSpace M₄],
  ↑(ContinuousLinearEquiv.prodProdProdComm R M₁ M₂ M₃ M₄) = LinearEquiv.prodProdProdComm R M₁ M₂ M₃ M₄
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.zpow_eq_empty : ∀ {α : Type u_2} [inst : DivisionMonoid α] {s : Set α} {n : ℤ}, s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0
-- Mathlib.Data.Int.Interval
Int.card_uIcc : ∀ (a b : ℤ), (Finset.uIcc a b).card = (b - a).natAbs + 1
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- `Matrix.mulVec M` as a linear map.

Note this is a special case of `Matrix.mulVecBilin`.  -/
Matrix.mulVecLin : {R : Type u_1} →
  [inst : CommSemiring R] → {m : Type u_4} → {n : Type u_5} → [Fintype n] → Matrix m n R → (n → R) →ₗ[R] m → R
-- Mathlib.Data.Real.Embedding
/-- `ratLt` as a set of real numbers.  -/
Archimedean.ratLt' : {M : Type u_1} → [AddCommGroup M] → [LinearOrder M] → [One M] → M → Set ℝ
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.subtractionMonoid : {α : Type u} → [DivisionMonoid α] → SubtractionMonoid (Additive α)
-- Mathlib.FieldTheory.Separable
/-- Transfer `Algebra.IsSeparable` across an `AlgEquiv`.  -/
AlgEquiv.Algebra.isSeparable : ∀ {F : Type u_1} {K : Type u_3} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K] {E : Type u_4}
  [inst_3 : Ring E] [inst_4 : Algebra F E] (e : K ≃ₐ[F] E) [Algebra.IsSeparable F K], Algebra.IsSeparable F E
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.exists_prime_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α),
  a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a
-- Mathlib.Data.Nat.Multiplicity
/-- **Legendre's Theorem**

The multiplicity of a prime in `n!` is the sum of the quotients `n / p ^ i`. This sum is expressed
over the finset `Ico 1 b` where `b` is any bound greater than `log p n`.  -/
Nat.Prime.emultiplicity_factorial : ∀ {p : ℕ}, Nat.Prime p → ∀ {n b : ℕ}, Nat.log p n < b → emultiplicity p n.factorial = ↑(∑ i ∈ Finset.Ico 1 b, n / p ^ i)
-- Mathlib.Topology.Continuous
continuous_of_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  (∀ (x y : X), f x = f y) → Continuous f
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₂₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₂₄ = CategoryTheory.Arrow.Hom.right f.hom
-- Std.Http.Protocol.H1
/-- Completes a message whose body is intentionally omitted from wire output
(`HEAD`/bodyless status handling).
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.completeOmittedBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- Transport a `NormalEpi` structure via an isomorphism of arrows.  -/
CategoryTheory.NormalEpi.ofArrowIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          CategoryTheory.NormalEpi f →
            {X' Y' : C} →
              {f' : X' ⟶ Y'} → (CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') → CategoryTheory.NormalEpi f'
-- Init.Data.List.Lemmas
List.head?_append : ∀ {α : Type u_1} {l' l : List α}, (l ++ l').head? = l.head?.or l'.head?
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.IsStrictCut.mk : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} [toIsCut : RBTree.RBNode.IsCut cmp cut],
  (∀ {x y : α} [Std.TransCmp cmp], cut x = Ordering.eq → cmp x y = cut y) → RBTree.RBNode.IsStrictCut cmp cut
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- Assume that a measure `μ` is `IsMulLeftInvariant`, that the action of `Γ` on `G` has a
measurable fundamental domain `s` with positive finite volume, and that there is a single measurable
set `V ⊆ G ⧸ Γ` along which the pullback of `μ` and `ν` agree (so the scaling is right). Then
`μ` satisfies `QuotientMeasureEqMeasurePreimage`. The main tool of the proof is the uniqueness of
left invariant measures, if normalized by a single positive finite-measured set.  -/
MeasureTheory.Measure.IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] [PolishSpace G] {Γ : Subgroup G} [inst_6 : Γ.Normal] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} (ν : MeasureTheory.Measure G)
  [ν.IsMulLeftInvariant] [Countable ↥Γ] [ν.IsMulRightInvariant] [MeasureTheory.SigmaFinite ν] [μ.IsMulLeftInvariant]
  [MeasureTheory.SigmaFinite μ] {s : Set G},
  MeasureTheory.IsFundamentalDomain (↥Γ.op) s ν →
    ∀ {V : Set (G ⧸ Γ)},
      MeasurableSet V →
        μ V ≠ 0 → μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s) → μ V ≠ ⊤ → MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.forget_η : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Mon.forget C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (braiding braiding_1 :
    (X Y : C) →
      CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X)
  (e_braiding : braiding = braiding_1)
  (braiding_naturality_right :
    ∀ (X : C) {Y Z : C} (f : Y ⟶ Z),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (braiding X Z).hom =
        CategoryTheory.CategoryStruct.comp (braiding X Y).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
  (braiding_naturality_left :
    ∀ {X Y : C} (f : X ⟶ Y) (Z : C),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (braiding Y Z).hom =
        CategoryTheory.CategoryStruct.comp (braiding X Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f))
  (hexagon_forward :
    ∀ (X Y Z : C),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
          (CategoryTheory.CategoryStruct.comp (braiding X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
            (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (braiding X Y).hom Z)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (braiding X Z).hom)))
  (hexagon_reverse :
    ∀ (X Y Z : C),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
          (CategoryTheory.CategoryStruct.comp (braiding (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
            (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (braiding Y Z).hom)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (braiding X Z).hom Y))),
  { braiding := braiding, braiding_naturality_right := braiding_naturality_right,
      braiding_naturality_left := braiding_naturality_left, hexagon_forward := hexagon_forward,
      hexagon_reverse := hexagon_reverse } =
    { braiding := braiding_1, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯, hexagon_forward := ⋯,
      hexagon_reverse := ⋯ }
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.coe_toSubsemigroup_apply : ∀ {A : Type u_5} [inst : Add A] (S : AddSubsemigroup A),
  ↑(AddSubsemigroup.toSubsemigroup S) = ⇑Multiplicative.toAdd ⁻¹' ↑S
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.Hom.mk.sizeOf_spec : ∀ {X : UniformSpaceCat} {Y : UniformSpaceCat} (hom' : { f // UniformContinuous f }),
  sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.overMapUnitIso_hom_val_app_hom_apply : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D}
  {R : CategoryTheory.Sheaf K RingCat} {X Y : D} (f : X ⟶ Y) (x : (CategoryTheory.Over X)ᵒᵖ)
  (x_1 : ↑(((SheafOfModules.overMap R f).obj (SheafOfModules.unit (R.over Y))).val.obj x)),
  (ModuleCat.Hom.hom ((SheafOfModules.overMapUnitIso f).hom.val.app x)) x_1 = x_1
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- **Alias** of `WithAbs.norm_toAbs_eq`. -/
WithAbs.norm_eq_abv' : ∀ {R : Type u_1} [inst : Ring R] (v : AbsoluteValue R ℝ) (x : R), ‖WithAbs.toAbs v x‖ = v x
-- Mathlib.Algebra.Ring.TransferInstance
Equiv.ringEquiv_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : Add β] [inst_1 : Mul β] (b : β),
  (RingEquiv.symm e.ringEquiv) b = e.symm b
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A]
  {X Y W : CategoryTheory.Sheaf J A} (f : W ⟶ X) (g : W ⟶ Y),
  (CategoryTheory.CartesianMonoidalCategory.lift f g).hom = CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom
-- Mathlib.Topology.Defs.Basic
/-- Delaborator for `Continuous[_, _]`.  -/
Topology.delabContinuous : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.weightMap_mul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (x y : P.Hom P),
  (x * y).weightMap = x.weightMap ∘ₗ y.weightMap
-- Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
CategoryTheory.MonoidalClosed.enrichedCategorySelf_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] (X Y : C), (X ⟶[C] Y) = (X ⟹ Y)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans_refl_restr : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set β),
  e.trans ((PartialEquiv.refl β).restr s) = e.restr (↑e ⁻¹' s)
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity holds iff pairwise distances are proportional with a positive ratio.  -/
similar_iff_exists_pos_pairwise_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  Similar v₁ v₂ ↔ ∃ r, 0 < r ∧ Pairwise fun i₁ i₂ => dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
-- Mathlib.Data.Set.Card
Set.ncard_sdiff_singleton_le : ∀ {α : Type u_1} (s : Set α) (a : α), (s \ {a}).ncard ≤ s.ncard
-- Init.Data.Option.Lemmas
Option.idempotentOp_merge : ∀ {α : Type u_1} (f : α → α → α) [Std.IdempotentOp f], Std.IdempotentOp (Option.merge f)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_apply_eq_zero : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet t → ((μ.restrict s) t = 0 ↔ μ (t ∩ s) = 0)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.forget₂_obj : ∀ (R : Type u) [inst : Ring R] (X : ModuleCat R),
  (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj X = AddCommGrpCat.of ↑X
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.Result.ofNat : ℕ → Std.Tactic.BVDecide.LRAT.Internal.Result
-- Mathlib.Data.Fintype.EquivFin
instInfiniteOption : ∀ {α : Type u_1} [Infinite α], Infinite (Option α)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.eq_succMany?_of_toList_eq_append_cons : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff),
  cur = (Std.PRange.least?.bind (Std.PRange.succMany? pref.length)).get ⋯
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mem_addSubgroup_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a : M}
  {s : UpperSet (ArchimedeanClass M)}, s ≠ ⊤ → (a ∈ ArchimedeanClass.addSubgroup s ↔ ArchimedeanClass.mk a ∈ s)
-- Mathlib.Data.List.Perm.Basic
List.getElem_cons_eraseIdx_perm : ∀ {α : Type u_1} {l : List α} {n : ℕ} (h : n < l.length), (l[n] :: l.eraseIdx n).Perm l
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.lt.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          ((val : β) → motive none (some val)) →
            ((x : α) → (y : β) → motive (some x) (some y)) →
              ((x : Option α) →
                  (x_2 : Option β) →
                    (∀ (val : β), x = none → x_2 = some val → False) →
                      (∀ (x_4 : α) (y : β), x = some x_4 → x_2 = some y → False) → motive x x_2) →
                motive x x_1
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.of.inj : ∀ {carrier : Type u_1} {str : GroupWithZero carrier} {carrier_1 : Type u_1} {str_1 : GroupWithZero carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.GroupTheory.GroupAction.Pointwise
smul_preimage_set_subset : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : SMul M α] [inst_1 : SMul M β]
  [inst_2 : FunLike F α β] [MulActionHomClass F M α β] (f : F) (c : M) (t : Set β), c • ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (c • t)
-- Mathlib.LinearAlgebra.Finsupp.LSum
Submodule.finsuppSum_mem : ∀ (R : Type u_1) {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_4}
  {β : Type u_5} [inst_3 : Zero β] (S : Submodule R M) (f : ι →₀ β) (g : ι → β → M),
  (∀ (c : ι), f c ≠ 0 → g c (f c) ∈ S) → f.sum g ∈ S
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_g : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  (CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).g = T.mor₂
-- Mathlib.Util.Superscript
Mathlib.Tactic.Superscript.Mapping.mk : Std.HashMap Char Char → Std.HashMap Char Char → Mathlib.Tactic.Superscript.Mapping
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.map_comap_eq : ∀ {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M₂] [inst_7 : LieRingModule L M₂] (N₂ : LieSubmodule R L M₂) (f : M →ₗ⁅R,L⁆ M₂),
  N₂ ≤ f.range → LieSubmodule.map f (LieSubmodule.comap f N₂) = N₂
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- The volume form on an oriented real inner product space can be evaluated as the determinant with
respect to any orthonormal basis of the space compatible with the orientation.  -/
Orientation.volumeForm_robust_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) (b : OrthonormalBasis (Fin n) ℝ E),
  b.toBasis.orientation ≠ o → o.volumeForm = -b.toBasis.det
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_le_eRank : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.eRk X ≤ M.eRank
-- Mathlib.Topology.Baire.Lemmas
/-- Baire theorem: if countably many closed sets cover the whole space, then their interiors
are dense. Formulated here with an index set which is a countable set in any type.  -/
dense_biUnion_interior_of_closed : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [BaireSpace X] {S : Set α} {f : α → Set X},
  (∀ s ∈ S, IsClosed (f s)) → S.Countable → ⋃ s ∈ S, f s = Set.univ → Dense (⋃ s ∈ S, interior (f s))
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.PosNum.divMod.match_3.eq_1 : ∀ (motive : PosNum → Sort u_1) (n : PosNum) (h_1 : (n : PosNum) → motive n.bit0) (h_2 : (n : PosNum) → motive n.bit1)
  (h_3 : Unit → motive PosNum.one),
  (match n.bit0 with
    | n.bit0 => h_1 n
    | n.bit1 => h_2 n
    | PosNum.one => h_3 ()) =
    h_1 n
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Presieve.IsSheaf.isSheafFor_of_mem_precoverage : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {J : CategoryTheory.Precoverage C}
  {P : CategoryTheory.Functor Cᵒᵖ (Type u_1)},
  CategoryTheory.Presieve.IsSheaf J.toGrothendieck P →
    ∀ {S : C} {R : CategoryTheory.Presieve S}, R ∈ J.coverings S → CategoryTheory.Presieve.IsSheafFor P R
-- Mathlib.Algebra.Notation.Defs
VAdd.ext : ∀ {G : Type u} {P : Type v} {x y : VAdd G P}, VAdd.vadd = VAdd.vadd → x = y
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Given a morphism property `P` on a category `T` and an object `X : T`, this is the
subcategory of `Under X` defined by `P` where morphisms satisfy `Q`.  -/
CategoryTheory.MorphismProperty.Under : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    CategoryTheory.MorphismProperty T → CategoryTheory.MorphismProperty T → T → Type (max v_1 u_1)
-- Init.Prelude
Substring.Raw.mk : String → String.Pos.Raw → String.Pos.Raw → Substring.Raw
-- Mathlib.Order.RelSeries
RelSeries.append_cons : ∀ {α : Type u_1} {r : SetRel α α} {p q : RelSeries r} {x : α} (hx : (x, p.head) ∈ r) (hq : (p.last, q.head) ∈ r),
  (p.cons x hx).append q ⋯ = (p.append q hq).cons x ⋯
-- Mathlib.Order.CompleteLattice.Lemmas
inf_iInf_nat_succ : ∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α), u 0 ⊓ ⨅ i, u (i + 1) = ⨅ i, u i