mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a : α}, ∅.get? a = none
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_const_mul_id : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} (c : 𝕜), deriv (fun y => c * y) x = c
-- Mathlib.Algebra.Order.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero : {A : Type u_1} →
  {B : Type u_2} →
    [inst : MonoidWithZero A] →
      [inst_1 : LinearOrderedCommGroupWithZero B] → {f : A →*₀ B} → LinearOrderedCommGroupWithZero f.ValueGroup₀
-- Mathlib.Analysis.Analytic.OfScalars
/-- This naming follows the convention of `NormedSpace.expSeries_apply_eq'`.  -/
FormalMultilinearSeries.ofScalars_apply_eq' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c : ℕ → 𝕜) (x : E),
  (fun n => (FormalMultilinearSeries.ofScalars E c n) fun x_1 => x) = fun n => c n • x ^ n
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.mem_pointwise_smul_iff_inv_smul_mem : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Group α] [inst_2 : MulDistribMulAction α G] {a : α}
  {S : Subgroup G} {x : G}, x ∈ a • S ↔ a⁻¹ • x ∈ S
-- Mathlib.Algebra.Group.Commute.Defs
Commute.all : ∀ {S : Type u_3} [inst : CommMagma S] (a b : S), Commute a b
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_lt_of_pred : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [PredOrder ι], MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a a_1 : α) (e_a : a = a_1) (l l_1 : List ((a : α) × β a))
  (e_l : l = l_1) (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getKey a l h = Std.Internal.List.getKey a_1 l_1 ⋯
-- Init.Data.Vector.Find
Vector.findFinIdx?_eq_bind_find?_finIdxOf? : ∀ {α : Type} {n : ℕ} [inst : BEq α] [LawfulBEq α] {xs : Vector α n} {p : α → Bool},
  Vector.findFinIdx? p xs = (Vector.find? p xs).bind fun x => xs.finIdxOf? x
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.continuousEvalConst : ∀ {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_7}
  {F : Type u_8} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜₁ E] [inst_8 : Module 𝕜₂ F],
  ContinuousEvalConst (E →SLₚₜ[σ] F) E F
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- The logarithmic counting function of the constant function zero is zero.
 -/
ValueDistribution.logCounting_const_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {e : WithTop E}, ValueDistribution.logCounting 0 e = 0
-- Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Polynomial.IsDistinguishedAt.map_eq_X_pow : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} {I : Ideal R},
  f.IsDistinguishedAt I → Polynomial.map (Ideal.Quotient.mk I) f = Polynomial.X ^ f.natDegree
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule : ∀ (R : Type u_2) [inst : Ring R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleRing R]
  [h : IsSimpleModule R M], ∃ I, Nonempty (M ≃ₗ[R] ↥I)
-- Mathlib.Algebra.GroupWithZero.Action.Hom
ZeroHom.instSMulWithZero : {M : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : Zero A] → [inst_1 : Zero B] → [inst_2 : Zero M] → [SMulWithZero M B] → SMulWithZero M (ZeroHom A B)
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyGT! : {α : Type u} → {β : α → Type v} → [Ord α] → [Inhabited α] → α → Std.DTreeMap.Internal.Impl α β → α
-- Mathlib.Data.Finset.Defs
Finset.ssubset_of_ssubset_of_subset : ∀ {α : Type u_1} {s₁ s₂ s₃ : Finset α}, s₁ ⊂ s₂ → s₂ ⊆ s₃ → s₁ ⊂ s₃
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
/-- If `f` has bounded variation on `uIcc a b`, then `f'` is interval integrable on `a..b`.  -/
BoundedVariationOn.intervalIntegrable_deriv : ∀ {f : ℝ → ℝ} {a b : ℝ}, BoundedVariationOn f (Set.uIcc a b) → IntervalIntegrable (deriv f) MeasureTheory.volume a b
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalize_naturality : ∀ {C : Type u} (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C)
  {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.FreeMonoidalCategory.inclusionObj n) f)
      (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C Y n).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C X n).hom
      (CategoryTheory.FreeMonoidalCategory.inclusion.map (CategoryTheory.eqToHom ⋯))
-- Lean.Server.CodeActions.Attr
_private.Lean.Server.CodeActions.Attr.0.Lean.CodeAction.mkCommandCodeAction.unsafe_1 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Lean.CodeAction.CommandCodeAction
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.trans : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.HashMap α β},
  m₁.Equiv m₂ → m₂.Equiv m₃ → m₁.Equiv m₃
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.neg_symm : ∀ (G : Type v) [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd G G]
  [inst_3 : IsIsometricVAdd Gᵃᵒᵖ G], (IsometryEquiv.neg G).symm = IsometryEquiv.neg G
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.eval_apply_injective : ∀ (K : Type uK) {V : Type uV} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V], Function.Injective ⇑(Module.Dual.eval K V)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  k ∈ t.insert k v
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∩ t₂).contains k = (t₁.contains k && t₂.contains k)
-- Mathlib.AlgebraicGeometry.SpreadingOut
AlgebraicGeometry.Scheme.IsGermInjectiveAt.cond : ∀ {X : AlgebraicGeometry.Scheme} {x : ↥X} [self : X.IsGermInjectiveAt x],
  ∃ U,
    ∃ (hx : x ∈ U),
      AlgebraicGeometry.IsAffineOpen U ∧
        Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx))
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Prequotient.brecOn.eq : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  {motive : MonCat.Colimits.Prequotient F → Sort u_1} (t : MonCat.Colimits.Prequotient F)
  (F_1 : (t : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Prequotient.below t → motive t),
  MonCat.Colimits.Prequotient.brecOn t F_1 = F_1 t (MonCat.Colimits.Prequotient.brecOn.go t F_1).2
-- Mathlib.Analysis.SpecialFunctions.JapaneseBracket
rpow_neg_one_add_norm_sq_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {r : ℝ} (x : E),
  0 < r → (1 + ‖x‖ ^ 2) ^ (-r / 2) ≤ 2 ^ (r / 2) * (1 + ‖x‖) ^ (-r)
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.IsocrystalEquiv.mk.sizeOf_spec : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {k : Type u_1} [inst_1 : CommRing k] [inst_2 : CharP k p]
  [inst_3 : PerfectRing k p] {V : Type u_2} [inst_4 : AddCommGroup V] [inst_5 : WittVector.Isocrystal p k V]
  {V₂ : Type u_3} [inst_6 : AddCommGroup V₂] [inst_7 : WittVector.Isocrystal p k V₂] [inst_8 : SizeOf k]
  [inst_9 : SizeOf V] [inst_10 : SizeOf V₂] (toLinearEquiv : V ≃ₗ[FractionRing (WittVector p k)] V₂)
  (frob_equivariant :
    ∀ (x : V),
      (WittVector.Isocrystal.frobenius p k) (toLinearEquiv x) =
        toLinearEquiv ((WittVector.Isocrystal.frobenius p k) x)),
  sizeOf { toLinearEquiv := toLinearEquiv, frob_equivariant := frob_equivariant } = 1 + sizeOf toLinearEquiv
-- Mathlib.Analysis.Normed.Ring.Int
Int.norm_coe_units : ∀ (e : ℤˣ), ‖↑e‖ = 1
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- The precomposition `Ext Y Z a →+ Ext X Z b` with `α : Ext X Y n` when `n + a = b`.  -/
CategoryTheory.Abelian.Ext.precomp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X Y : C} →
          {n : ℕ} →
            CategoryTheory.Abelian.Ext X Y n →
              (Z : C) → {a b : ℕ} → n + a = b → CategoryTheory.Abelian.Ext Y Z a →+ CategoryTheory.Abelian.Ext X Z b
-- Std.Do.PostCond
/-- A postcondition expressing total correctness.
That is, it expresses that the asserted computation finishes without throwing an exception
*and* the result satisfies the given predicate `p`.
 -/
Std.Do.«term_⇓_=>_» : Lean.ParserDescr
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.Exists.eq_2 : ∀ {α : Type u_1} (n : ℕ) (P : (Fin (n + 1) → α) → Prop),
  FinVec.Exists P = ∃ x, FinVec.Exists fun v => P (Matrix.vecCons x v)
-- Init.Core
/-- *Ex falso* for negation: from `¬a` and `a` anything follows. This is the same as `absurd` with
the arguments flipped, but it is in the `Not` namespace so that projection notation can be used.  -/
Not.elim : {a : Prop} → {α : Sort u_1} → ¬a → a → α
-- Mathlib.Computability.TuringMachine.Tape
Turing.BlankRel.eq_def : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (l₁ l₂ : List Γ),
  Turing.BlankRel l₁ l₂ = (Turing.BlankExtends l₁ l₂ ∨ Turing.BlankExtends l₂ l₁)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.mk : {Ω : Type u_1} →
  {ι : Type u_2} →
    [inst : Preorder ι] →
      {m : MeasurableSpace Ω} →
        (seq : ι → MeasurableSpace Ω) → Monotone seq → (∀ (i : ι), seq i ≤ m) → MeasureTheory.Filtration ι m
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.down_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C}
  (f : CategoryTheory.WithTerminal.of X ⟶ CategoryTheory.WithTerminal.of Y)
  (g : CategoryTheory.WithTerminal.of Y ⟶ CategoryTheory.WithTerminal.of Z),
  CategoryTheory.WithTerminal.down (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.WithTerminal.down f) (CategoryTheory.WithTerminal.down g)
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected_f : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected] [inst_2 : P.IsStableUnderBaseChange]
  [inst_3 : P.HasOfPostcompProperty P] (i j : 𝒰.I₀) (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)),
  (𝒰.intersectionOfLocallyDirected i j).f k = CategoryTheory.Limits.pullback.lift (𝒰.trans k.snd.1) (𝒰.trans k.snd.2) ⋯
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_left_mul_add : ∀ {α : Type u} [inst : CommRing α] (x y z : α), Ideal.span {x, x * z + y} = Ideal.span {x, y}
-- Mathlib.Data.Fin.Tuple.Reflection
/-- This can be used to prove
```lean
example (P : (Fin 2 → α) → Prop) : (∃ f, P f) ↔ ∃ a₀ a₁, P ![a₀, a₁] :=
  (exists_iff _).symm
```
 -/
FinVec.exists_iff : ∀ {α : Type u_1} {m : ℕ} (P : (Fin m → α) → Prop), FinVec.Exists P ↔ ∃ x, P x
-- Mathlib.Topology.Category.Profinite.CofilteredLimit
Profinite.exists_locallyConstant_finite_aux : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J]
  {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {α : Type u_1} [Finite α]
  (hC : CategoryTheory.Limits.IsLimit C) (f : LocallyConstant (↑C.pt.toTop) α),
  ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyι_descOpcycles_eq_zero_of_boundary : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} [inst_2 : S.HasHomology] (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A)
  (hx : k = CategoryTheory.CategoryStruct.comp S.g x),
  CategoryTheory.CategoryStruct.comp S.homologyι (S.descOpcycles k ⋯) = 0
-- Mathlib.RingTheory.TensorProduct.IsBaseChangePi
/-- Localization of modules commutes with binary products.  -/
IsLocalizedModule.prodMap : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_3} {N : Type u_4} {M' : Type u_5} {N' : Type u_6}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid M'] [inst_6 : AddCommMonoid N'] [inst_7 : Module R M'] [inst_8 : Module R N'] (f : M →ₗ[R] M')
  (g : N →ₗ[R] N') [IsLocalizedModule S f] [IsLocalizedModule S g], IsLocalizedModule S (f.prodMap g)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgHom.coe_codRestrict : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] (f : F)
  (S : NonUnitalStarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) (x : A),
  ↑((NonUnitalStarAlgHom.codRestrict f S hf) x) = f x
-- Mathlib.MeasureTheory.Category.MeasCat
MeasCat.str : (self : MeasCat) → MeasurableSpace self.carrier
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.nhds_eq_comap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (x : X),
  nhds x = Filter.comap (⇑h) (nhds (h x))
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverse_involutive : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, Function.Involutive ⇑CliffordAlgebra.reverse
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.equiv_iff_toArray_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ ↔ t₁.toArray = t₂.toArray
-- Mathlib.MeasureTheory.Measure.Map
MeasurableEquiv.map_ae : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : MeasurableSpace β] (f : α ≃ᵐ β)
  (μ : MeasureTheory.Measure α),
  Filter.map (⇑f) (MeasureTheory.ae μ) = MeasureTheory.ae (MeasureTheory.Measure.map (⇑f) μ)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.of_bound' : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  (∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖) → f =O[l] g
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- The zero-preserving homomorphism including a single value into a dependent family of values,
as functions supported at a point.

This is the `ZeroHom` version of `Pi.single`.  -/
ZeroHom.single : {I : Type u} →
  (f : I → Type v) → [DecidableEq I] → [inst : (i : I) → Zero (f i)] → (i : I) → ZeroHom (f i) ((i : I) → f i)
-- Lean.Structure
/-- The projection function associated to the field. For subobjects, this is the same as the `projFn` in its `fieldInfo` entry.  -/
Lean.StructureParentInfo.projFn : Lean.StructureParentInfo → Lean.Name
-- Lean.Data.Lsp.Internal
/-- Start character of selection range.  -/
Lean.Lsp.DeclInfo.selectionRangeStartPosCharacter : Lean.Lsp.DeclInfo → ℕ
-- Mathlib.CategoryTheory.Abelian.Basic
/-- The factorisation of a morphism through its abelian image.  -/
CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasKernels C] →
        [CategoryTheory.Limits.HasCokernels C] → {X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.MonoFactorisation f
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Submodule.isAssociatedPrime_def : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {I : Ideal R}, N.IsAssociatedPrime I ↔ I.IsPrime ∧ ∃ x, I = (N.colon {x}).radical
-- Mathlib.Geometry.Euclidean.Similarity
/-- For two similar triangles, the corresponding angles are equal.  -/
Similar.angle_eq : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [inst : NormedAddCommGroup V₁]
  [inst_1 : NormedAddCommGroup V₂] [inst_2 : InnerProductSpace ℝ V₁] [inst_3 : InnerProductSpace ℝ V₂]
  [inst_4 : MetricSpace P₁] [inst_5 : MetricSpace P₂] [inst_6 : NormedAddTorsor V₁ P₁] [inst_7 : NormedAddTorsor V₂ P₂]
  {a b c : P₁} {a' b' c' : P₂},
  Similar ![a, b, c] ![a', b', c'] → EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c'
-- Mathlib.Data.DFinsupp.Order
DFinsupp.coe_le_coe : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → LE (α i)] {f g : Π₀ (i : ι), α i},
  ⇑f ≤ ⇑g ↔ f ≤ g
-- Init.Data.Nat.Lemmas
Nat.add_one_mul_add_one : ∀ (a b : ℕ), (a + 1) * (b + 1) = a * b + a + b + 1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSemanticTokensRangeParams : Lean.ToJson Lean.Lsp.SemanticTokensRangeParams
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp'.eq_7 : ∀ (x : Turing.PartrecToTM2.Cont') (f : Turing.ToPartrec.Code),
  Turing.PartrecToTM2.codeSupp' f.fix x =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal f.fix x) ∪
      (Turing.PartrecToTM2.codeSupp' f (Turing.PartrecToTM2.Cont'.fix f x) ∪
        (Turing.PartrecToTM2.trStmts₁
            (Turing.PartrecToTM2.Λ'.clear Turing.PartrecToTM2.natEnd Turing.PartrecToTM2.K'.main
              (Turing.PartrecToTM2.trNormal f (Turing.PartrecToTM2.Cont'.fix f x))) ∪
          {Turing.PartrecToTM2.Λ'.ret x}))
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {s : UpperSet α} (g : β ≃o γ) (f : α ≃o β), (UpperSet.map g) ((UpperSet.map f) s) = (UpperSet.map (f.trans g)) s
-- Mathlib.Order.Interval.Finset.Defs
Finset.subtype_Ici_eq : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrderTop α]
  (a : Subtype p), Finset.Ici a = Finset.subtype p (Finset.Ici ↑a)
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Construct a right lift along `g : c ⟶ a` from a right lift along `𝟙 c ≫ g`.  -/
CategoryTheory.Bicategory.RightLift.ofIdComp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          CategoryTheory.Bicategory.RightLift f
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g) →
            CategoryTheory.Bicategory.RightLift f g
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instRing : {𝕜 : Type u_2} →
  {α : Type u_5} →
    [inst : Preorder α] → [LocallyFiniteOrder α] → [DecidableEq α] → [inst_3 : Ring 𝕜] → Ring (IncidenceAlgebra 𝕜 α)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.ext_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ₁ μ₂ : MeasureTheory.Measure α},
  μ₁ = μ₂ ↔ ∀ (s : Set α), MeasurableSet s → μ₁ s = μ₂ s
-- Mathlib.Order.Filter.Pointwise
Filter.neg_mem_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {f : Filter α} {s : Set α}, s ∈ f → -s ∈ -f
-- Mathlib.Probability.Kernel.Proper
ProbabilityTheory.Kernel.IsProper.setLIntegral_eq_comp : ∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X} {A B : Set X},
  π.IsProper →
    𝓑 ≤ 𝓧 →
      ∀ {μ : MeasureTheory.Measure X},
        MeasurableSet A → MeasurableSet B → ∫⁻ (a : X) in B, (π a) A ∂μ = (μ.bind ⇑π) (A ∩ B)
-- Mathlib.Probability.Distributions.Exponential
ProbabilityTheory.exponentialPDF.eq_1 : ∀ (r x : ℝ), ProbabilityTheory.exponentialPDF r x = ENNReal.ofReal (ProbabilityTheory.exponentialPDFReal r x)
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getEntryD : {α : Type u} → {β : α → Type v} → [BEq α] → α → (a : α) × β a → List ((a : α) × β a) → (a : α) × β a
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzOnWith.weaken : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {s : Set α}
  {f : α → β}, LipschitzOnWith K f s → ∀ {K' : NNReal}, K ≤ K' → LipschitzOnWith K' f s
-- Mathlib.Data.Vector.Basic
List.Vector.eraseIdx_val : ∀ {α : Type u_1} {n : ℕ} {i : Fin n} {v : List.Vector α n}, ↑(List.Vector.eraseIdx i v) = (↑v).eraseIdx ↑i
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_rev : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖a - b‖ = ‖b - a‖
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.instIsIsoFromLeftDerivedZero' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] {X : C}
  (P : CategoryTheory.ProjectiveResolution X), CategoryTheory.IsIso (P.fromLeftDerivedZero' F)
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Group α] {a b : α} [MulLeftMono α] [MulRightMono α],
  a⁻ᵐ < b ↔ b⁻¹ < a ∧ 1 < b
-- Mathlib.Order.Filter.Basic
Filter.eventually_true : ∀ {α : Type u} (f : Filter α), ∀ᶠ (x : α) in f, True
-- Mathlib.MeasureTheory.Integral.MeanInequalities
ENNReal.lintegral_rpow_add_le_add_eLpNorm_mul_lintegral_rpow_add : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q : ℝ},
  p.HolderConjugate q →
    ∀ {f g : α → ENNReal},
      AEMeasurable f μ →
        AEMeasurable g μ →
          ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
            ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
              (∫⁻ (a : α), (f a + g a) ^ p ∂μ) ^ (1 / q)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sub
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sub.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastSub.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (motive : aig.BinaryRefVec w → Sort u_1) (lhs rhs : aig.RefVec w)
  (h_1 : (lhs rhs : aig.RefVec w) → motive { lhs := lhs, rhs := rhs }),
  (match { lhs := lhs, rhs := rhs } with
    | { lhs := lhs, rhs := rhs } => h_1 lhs rhs) =
    h_1 lhs rhs
-- Mathlib.Topology.Order.OrderClosed
Filter.Tendsto.max_right : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f : β → α}
  {l : Filter β} {a : α}, Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun i => max a (f i)) l (nhds a)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_eq_none_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.min? = none ↔ t.isEmpty = true
-- Init.Data.List.Sublist
List.IsSuffix.filter : ∀ {α : Type u_1} (p : α → Bool) ⦃l₁ l₂ : List α⦄, l₁ <:+ l₂ → List.filter p l₁ <:+ List.filter p l₂
-- Mathlib.Algebra.Group.Subgroup.Even
/-- In a commutative additive semigroup `S`, `AddSubsemigroup.even S`
is the subsemigroup of even elements in `S`.  -/
AddSubsemigroup.even : (S : Type u_1) → [inst : AddCommSemigroup S] → AddSubsemigroup S
-- Mathlib.Computability.Primrec.List
Primrec.list_tail : ∀ {α : Type u_1} [inst : Primcodable α], Primrec List.tail
-- Mathlib.Analysis.Meromorphic.NormalForm
MeromorphicAt.toMeromorphicNFAt_eventuallyEq_nhds_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E},
  MeromorphicAt f x →
    MeromorphicAt g x → (toMeromorphicNFAt f x =ᶠ[nhds x] toMeromorphicNFAt g x ↔ f =ᶠ[nhdsWithin x {x}ᶜ] g)