mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- If `μ` satisfies `QuotientMeasureEqMeasurePreimage` relative to a both left- and right-
invariant measure `ν` on `G`, then it is a `G` invariant measure on `G ⧸ Γ`.  -/
MeasureTheory.QuotientMeasureEqMeasurePreimage.smulInvariantMeasure_quotient : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] (ν : MeasureTheory.Measure G) {Γ : Subgroup G}
  {μ : MeasureTheory.Measure (G ⧸ Γ)} [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ] [inst_3 : TopologicalSpace G]
  [IsTopologicalGroup G] [BorelSpace G] [PolishSpace G] [T2Space (G ⧸ Γ)] [SecondCountableTopology (G ⧸ Γ)]
  [ν.IsMulLeftInvariant] [hasFun : MeasureTheory.HasFundamentalDomain (↥Γ.op) G ν],
  MeasureTheory.SMulInvariantMeasure G (G ⧸ Γ) μ
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.image_sphere : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (x : α) (r : ℝ),
  ⇑h '' Metric.sphere x r = Metric.sphere (h x) r
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_rightHomologyIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.RightHomologyData) {Z : C}
  (h_1 : S.rightHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.homologyIso.hom (CategoryTheory.CategoryStruct.comp h.rightHomologyIso.inv h_1) =
    CategoryTheory.CategoryStruct.comp S.rightHomologyIso.inv h_1
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- The canonical group morphism from the special linear group
to the general linear group.  -/
SpecialLinearGroup.toGeneralLinearGroup : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → SpecialLinearGroup R V →* LinearMap.GeneralLinearGroup R V
-- Mathlib.Geometry.Convex.Cone.DualFinite
/-- The intersection of two dually finitely generated cones is again dually finitely generated.  -/
PointedCone.DualFG.inf : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} {C D : PointedCone R N},
  PointedCone.DualFG p C → PointedCone.DualFG p D → PointedCone.DualFG p (C ⊓ D)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_nat_eq_ascFactorial : ∀ (n k : ℕ), Polynomial.eval n (ascPochhammer ℕ k) = n.ascFactorial k
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.inst : Std.Time.Database Std.Time.Database.TZdb
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- Turn an element of a type `F` satisfying
`[FunLike F A B] [GradedFunLike F 𝒜 ℬ] [RingHomClass F A B]` into an actual `GradedRingHom`.

This should not be used directly. In the future, Mathlib will prefer structural projections over
these general constructions from hom classes.  -/
GradedRingHom.ofClass : {ι : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {σ : Type u_6} →
        {τ : Type u_7} →
          [inst : Semiring A] →
            [inst_1 : Semiring B] →
              [inst_2 : SetLike σ A] →
                [inst_3 : SetLike τ B] →
                  {𝒜 : ι → σ} →
                    {ℬ : ι → τ} →
                      {F : Type u_10} →
                        [inst_4 : FunLike F A B] → [GradedFunLike F 𝒜 ℬ] → [RingHomClass F A B] → F → 𝒜 →+*ᵍ ℬ
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.binomial_zero : ∀ {p : ↑unitInterval}, ProbabilityTheory.binomial 0 p = MeasureTheory.Measure.dirac 0
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForILeansParams.mk.sizeOf_spec : ∀ (uri? : Option Lean.Lsp.DocumentUri) (version? : Option ℕ),
  sizeOf { uri? := uri?, version? := version? } = 1 + sizeOf uri? + sizeOf version?
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.rightHom_inl : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (S : GroupExtension N E G) (n : N), S.rightHom (S.inl n) = 1
-- Mathlib.Topology.Homotopy.Product
/-- The product of a family of path homotopy classes.  -/
Path.Homotopic.pi : {ι : Type u_1} →
  {X : ι → Type u_2} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {as bs : (i : ι) → X i} → ((i : ι) → Path.Homotopic.Quotient (as i) (bs i)) → Path.Homotopic.Quotient as bs
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_ne_zero : ∀ {α : Type u_1} {G : SimpleGraph α} [Nontrivial α], G.ediam ≠ 0
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedGT_iff_pairwise`. -/
List.Pairwise.sortedGT : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], List.Pairwise (fun x1 x2 => x1 > x2) l → l.SortedGT
-- Mathlib.Algebra.Group.Pi.Lemmas
AddHom.coe_add : ∀ {M : Type u_5} {N : Type u_6} {x : Add M} {x_1 : AddCommSemigroup N} (f g : M →ₙ+ N),
  ⇑f + ⇑g = fun x_2 => f x_2 + g x_2
-- Mathlib.RingTheory.Ideal.Colon
Submodule.mem_colon_iff_le : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N N' : Submodule R M} {r : R}, r ∈ N.colon ↑N' ↔ r • N' ≤ N
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.instAssociativeHAdd : ∀ (α : Type u) [inst : Lean.Grind.Semiring α], Std.Associative fun x1 x2 => x1 + x2
-- Init.Internal.Order.While
_private.Init.Internal.Order.While.0.repeatM.body.match_1.eq_2 : ∀ {α β : Type u_1} (motive : α ⊕ β → Sort u_2) (b : β) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (b : β) → motive (Sum.inr b)),
  (match Sum.inr b with
    | Sum.inl a => h_1 a
    | Sum.inr b => h_2 b) =
    h_2 b
-- Lean.Data.Json.Basic
Lean.JsonNumber.normalize : Lean.JsonNumber → ℤ × ℕ × ℤ
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.evalComp_nil_nil : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g h : a ⟶ b} (α : f ≅ g) (β : g ≅ h),
  (α ≪≫ β).hom = (α ≪≫ β).hom
-- Mathlib.Algebra.Exact.Basic
Function.MulExact.monoidHom_ker_eq : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Group M] [inst_1 : Group N] [inst_2 : Group P] {f : M →* N}
  {g : N →* P}, Function.MulExact ⇑f ⇑g → g.ker = f.range
-- Mathlib.CategoryTheory.ConcreteCategory.Bundled
CategoryTheory.Bundled.coeSort : {c : Type u → Type v} → CoeSort (CategoryTheory.Bundled c) (Type u)
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.whiskerLeft₂_map_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u_1} {B : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_1} A]
  [inst_3 : CategoryTheory.Category.{v_2, u_2} B] (P : CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D)
  (F : CategoryTheory.Functor A C) (G : CategoryTheory.Functor B D) {X Y : A} (f : X ⟶ Y) (X_1 : Bᵒᵖ),
  ((P.whiskerLeft₂ F G).map f).app X_1 = (P.map (F.map f)).app (Opposite.op (G.obj (Opposite.unop X_1)))
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_prod : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → ENNReal}, ∑' (p : α × β), f p.1 p.2 = ∑' (a : α) (b : β), f a b
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
/-- The diagonal object of `X ×[Z] Y ⟶ X` is isomorphic to `Δ_{Y/Z} ×[Z] X`.  -/
CategoryTheory.Limits.diagonalObjPullbackFstIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {X Y Z : C} →
        (f : X ⟶ Z) →
          (g : Y ⟶ Z) →
            CategoryTheory.Limits.pullback.diagonalObj (CategoryTheory.Limits.pullback.fst f g) ≅
              CategoryTheory.Limits.pullback
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.eraseMax.match_1.splitter : {α : Type u_1} →
  (motive : Ordnode α → Sort u_2) →
    (x : Ordnode α) →
      (Unit → motive Ordnode.nil) →
        ((size : ℕ) → (l : Ordnode α) → (x : α) → motive (Ordnode.node size l x Ordnode.nil)) →
          ((size : ℕ) →
              (l : Ordnode α) →
                (x : α) →
                  (sz : ℕ) →
                    (l' : Ordnode α) →
                      (y : α) → (r' : Ordnode α) → motive (Ordnode.node size l x (Ordnode.node sz l' y r'))) →
            motive x
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.evalₗ_apply : ∀ (K : Type u_1) (σ : Type u_2) [inst : CommSemiring K] (p : MvPolynomial σ K) (e : σ → K),
  (MvPolynomial.evalₗ K σ) p e = (MvPolynomial.eval e) p
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- A family of `PowerSeries` is summable if their order tends to infinity.  -/
PowerSeries.WithPiTopology.summable_of_tendsto_order_atTop_nhds_top : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : Semiring R] {ι : Type u_2} {f : ι → PowerSeries R}
  [inst_2 : LinearOrder ι] [LocallyFiniteOrderBot ι],
  Filter.Tendsto (fun i => (f i).order) Filter.atTop (nhds ⊤) → Summable f
-- Mathlib.Order.BoundedOrder.Basic
/-- An order is an `OrderTop` if it has a greatest element.
We state this using a data mixin, holding the value of `⊤` and the greatest element constraint.  -/
OrderTop : (α : Type u) → [LE α] → Type u
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_4} [inst_3 : NormedRing R] [inst_4 : Module R E] [IsBoundedSMul R E]
  {U : Set 𝕜} [inst_6 : NormedAlgebra 𝕜 R] [IsScalarTower 𝕜 R E] {s : 𝕜 → R},
  MeromorphicOn s U → ∀ {f : 𝕜 → E}, MeromorphicOn f U → MeromorphicOn (s • f) U
-- Mathlib.Order.InitialSeg
PrincipalSeg.toRelEmbedding_inj : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Irrefl s] [Std.Trichotomous s]
  {f g : PrincipalSeg r s}, f.toRelEmbedding = g.toRelEmbedding ↔ f = g
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.coe_inf : ∀ {α : Type u_1} [inst : SemilatticeInf α] (a b : α), ↑(a ⊓ b) = ↑a ⊓ ↑b
-- Mathlib.Data.FinEnum
FinEnum.card_UInt8 : FinEnum.card UInt8 = 2 ^ 8
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.trans_apply : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α ↪ β) (g : β ↪ γ) (a : α), (f.trans g) a = g (f a)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `mul_inv_lt_iff₀'` for a version with multiplication on the other side.  -/
mul_inv_lt_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  0 < c → (b * c⁻¹ < a ↔ b < a * c)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
/-- The inverse functor establishing the equivalence `StructuredArrow.commaMapEquivalence`.  -/
CategoryTheory.StructuredArrow.commaMapEquivalenceInverse : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor C T} →
              {R : CategoryTheory.Functor D T} →
                {C' : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] →
                    {D' : Type u₅} →
                      [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] →
                        {T' : Type u₆} →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] →
                            {L' : CategoryTheory.Functor C' T'} →
                              {R' : CategoryTheory.Functor D' T'} →
                                {F₁ : CategoryTheory.Functor C C'} →
                                  {F₂ : CategoryTheory.Functor D D'} →
                                    {F : CategoryTheory.Functor T T'} →
                                      (α : F₁.comp L' ⟶ L.comp F) →
                                        (β : R.comp F ⟶ F₂.comp R') →
                                          [inst_6 : CategoryTheory.IsIso β] →
                                            (X : CategoryTheory.Comma L' R') →
                                              CategoryTheory.Functor
                                                (CategoryTheory.Comma
                                                  (CategoryTheory.StructuredArrow.map₂
                                                    (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α)
                                                  (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β)))
                                                (CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β))
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_subset_Ioc : ∀ {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₂ ≤ a₁ → b₁ ≤ b₂ → Finset.Ioc a₁ b₁ ⊆ Finset.Ioc a₂ b₂
-- Mathlib.CategoryTheory.Action.Limits
Action.instPreservesLimitsOfShapeForgetOfHasLimitsOfShape : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} J] [CategoryTheory.Limits.HasLimitsOfShape J V],
  CategoryTheory.Limits.PreservesLimitsOfShape J (Action.forget V G)
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_mul_right_eball : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ENNReal),
  (fun x => x * a) ⁻¹' Metric.eball b r = Metric.eball (b / a) r
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.domLCongr_symm : ∀ {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α₁ : Type u_9}
  {α₂ : Type u_10} (f : α₁ ≃ α₂), (Finsupp.domLCongr f).symm = Finsupp.domLCongr f.symm
-- Mathlib.Order.Filter.AtTopBot.Interval
Finset.tendsto_Icc_neg_atTop_atTop : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : LocallyFiniteOrder α], Filter.Tendsto (fun a => Finset.Icc (-a) a) Filter.atTop Filter.atTop
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_associator_hom : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [inst_3 : X₁.HasTensor X₂]
  [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [inst_5 : X₂.HasTensor X₃]
  [inst_6 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)]
  [inst_7 : X₁.HasGoodTensor₁₂Tensor X₂ X₃] [inst_8 : X₁.HasGoodTensorTensor₂₃ X₂ X₃] (i₁ i₂ i₃ j : I)
  (h : i₁ + i₂ + i₃ = j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h)
      ((CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).hom j) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (X₁ i₁) (X₂ i₂) (X₃ i₃)).hom
      (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
-- Mathlib.Probability.Density
MeasureTheory.pdf.integrable_pdf_smul_iff : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {F : Type u_3} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [MeasureTheory.IsFiniteMeasure ℙ] {X : Ω → E} [MeasureTheory.HasPDF X ℙ μ] {f : E → F},
  MeasureTheory.AEStronglyMeasurable f μ →
    (MeasureTheory.Integrable (fun x => (MeasureTheory.pdf X ℙ μ x).toReal • f x) μ ↔
      MeasureTheory.Integrable (fun x => f (X x)) ℙ)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLT_map_eq_truncLTι : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ), t.eTruncLT.map (CategoryTheory.homOfLE ⋯) = t.truncLTι n
-- Init.Data.String.Basic
String.toByteArray_extract : ∀ {s : String} {b e : s.Pos}, (String.extract b e).toByteArray = s.toByteArray.extract b.offset.byteIdx e.offset.byteIdx
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.instBEqMon.beq.match_1.splitter : (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) →
  (x x_1 : Lean.Grind.CommRing.Mon) →
    (Unit → motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit) →
      ((a : Lean.Grind.CommRing.Power) →
          (a_1 : Lean.Grind.CommRing.Mon) →
            (b : Lean.Grind.CommRing.Power) →
              (b_1 : Lean.Grind.CommRing.Mon) →
                motive (Lean.Grind.CommRing.Mon.mult a a_1) (Lean.Grind.CommRing.Mon.mult b b_1)) →
        ((x x_2 : Lean.Grind.CommRing.Mon) →
            (x = Lean.Grind.CommRing.Mon.unit → x_2 = Lean.Grind.CommRing.Mon.unit → False) →
              (∀ (a : Lean.Grind.CommRing.Power) (a_1 : Lean.Grind.CommRing.Mon) (b : Lean.Grind.CommRing.Power)
                  (b_1 : Lean.Grind.CommRing.Mon),
                  x = Lean.Grind.CommRing.Mon.mult a a_1 → x_2 = Lean.Grind.CommRing.Mon.mult b b_1 → False) →
                motive x x_2) →
          motive x x_1
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.TZif.mk.injEq : ∀ (v1 : Std.Time.TimeZone.TZif.TZifV1) (v2 : Option Std.Time.TimeZone.TZif.TZifV2)
  (v1_1 : Std.Time.TimeZone.TZif.TZifV1) (v2_1 : Option Std.Time.TimeZone.TZif.TZifV2),
  ({ v1 := v1, v2 := v2 } = { v1 := v1_1, v2 := v2_1 }) = (v1 = v1_1 ∧ v2 = v2_1)
-- Mathlib.Topology.EMetricSpace.Lipschitz
LocallyLipschitz.pow_end : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : Function.End α},
  LocallyLipschitz f → ∀ (n : ℕ), LocallyLipschitz (f ^ n)
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasNoetherianRange.comp_left : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [inst : Semiring K] [inst_1 : AddCommMonoid V]
  [inst_2 : Module K V] [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] [inst_5 : AddCommMonoid V₃]
  [inst_6 : Module K V₃] {u : V →ₗ[K] V₂}, u.HasNoetherianRange → ∀ (v : V₂ →ₗ[K] V₃), (v ∘ₗ u).HasNoetherianRange
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.tprod_prod' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousMul α]
  [T3Space α] {f : β × γ → α},
  Multipliable f → (∀ (b : β), Multipliable fun c => f (b, c)) → ∏' (p : β × γ), f p = ∏' (b : β) (c : γ), f (b, c)
-- Lean.Meta.Tactic.Congr
/-- Asserts the given congruence theorem as fresh hypothesis, and then applies it.
Return the `fvarId` for the new hypothesis and the new subgoals.
 -/
_private.Lean.Meta.Tactic.Congr.0.Lean.applyCongrThm? : Lean.MVarId → Lean.Meta.CongrTheorem → Lean.MetaM (List Lean.MVarId)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.prob_compl_le_one_sub_of_le_prob : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsZeroOrProbabilityMeasure μ] {p : ENNReal}, p ≤ μ s → MeasurableSet s → μ sᶜ ≤ 1 - p
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.opParallelPairIso_inv_app_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y),
  (CategoryTheory.Limits.opParallelPairIso f g).inv.app (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.walkingParallelPairOpEquiv.inverse.comp
            (CategoryTheory.Limits.parallelPair f.op g.op)).obj
        (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one))
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivAt.mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c d : 𝕜 → 𝔸} {c' d' : 𝔸},
  HasDerivAt c c' x → HasDerivAt d d' x → HasDerivAt (c * d) (c' * d x + c x * d') x
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_hom_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L'))
  (X_1 : C),
  ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).inverse.obj X).hom.app X_1 =
    CategoryTheory.CategoryStruct.comp (X.hom.app X_1) (X.right.map (iso₁.inv.app X_1))
-- Batteries.Logic
eqRec_heq_iff_heq : ∀ {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} {x : motive a ⋯} {a' : α} {e : a = a'} {β : Sort u_2}
  {y : β}, e ▸ x ≍ y ↔ x ≍ y
-- Std.Internal.Parsec.ByteArray
_private.Std.Internal.Parsec.ByteArray.0.Std.Internal.Parsec.ByteArray.skipBytes.go.eq_def : ∀ (arr : ByteArray) (idx : ℕ) (it : ByteArray.Iterator),
  Std.Internal.Parsec.ByteArray.skipBytes.go✝ arr idx it =
    if h : idx < arr.size then
      if hnext : it.hasNext = true then
        have got := it.curr' hnext;
        have want := arr[idx];
        if got = want then Std.Internal.Parsec.ByteArray.skipBytes.go✝ arr (idx + 1) (it.next' hnext)
        else
          Std.Internal.Parsec.ParseResult.error it
            (Std.Internal.Parsec.Error.other
              (toString "expected byte " ++ toString want ++ toString ", got " ++ toString got))
      else Std.Internal.Parsec.ParseResult.error it Std.Internal.Parsec.Error.eof
    else Std.Internal.Parsec.ParseResult.success it ()
-- Mathlib.Analysis.Complex.OperatorNorm
Complex.conjCLE_norm : ‖↑Complex.conjCLE‖ = 1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.closure_paramSet : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  closure (NumberField.mixedEmbedding.fundamentalCone.paramSet K) =
    Set.univ.pi fun w => if w = NumberField.Units.dirichletUnitTheorem.w₀ then Set.Iic 0 else Set.Icc 0 1
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDerivWithin_comp_two : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {g f : 𝕜 → 𝕜} {s t : Set 𝕜} {x : 𝕜},
  ContDiffWithinAt 𝕜 2 g t (f x) →
    ContDiffWithinAt 𝕜 2 f s x →
      UniqueDiffOn 𝕜 t →
        UniqueDiffOn 𝕜 s →
          x ∈ s →
            Set.MapsTo f s t →
              iteratedDerivWithin 2 (g ∘ f) s x =
                iteratedDerivWithin 2 g t (f x) * derivWithin f s x ^ 2 +
                  derivWithin g t (f x) * iteratedDerivWithin 2 f s x
-- Mathlib.RingTheory.Trace.Basic
/-- [Stacks Tag 0BIL](https://stacks.math.columbia.edu/tag/0BIL) -/
traceForm_nondegenerate_tfae : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L],
  [Algebra.IsSeparable K L, Algebra.trace K L ≠ 0, (Algebra.traceForm K L).Nondegenerate].TFAE
-- Mathlib.Analysis.Normed.Group.Basic
norm_multiset_sum_le : ∀ {E : Type u_9} [inst : SeminormedAddCommGroup E] (m : Multiset E), ‖m.sum‖ ≤ (Multiset.map (fun x => ‖x‖) m).sum
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_neg : ∀ {α : Type u_3} [inst : DivisionRing α] (q : ℚ), ↑(-q) = -↑q
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` creates finite colimits, then `F : C ⥤ Dᵒᵖ` creates finite
limits.  -/
CategoryTheory.Limits.createsFiniteLimitsOfLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C Dᵒᵖ) →
          [CategoryTheory.Limits.CreatesFiniteColimits F.leftOp] → CategoryTheory.Limits.CreatesFiniteLimits F
-- Mathlib.Analysis.InnerProductSpace.Symmetric
Submodule.isSymmetricProjection_projection_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} (hUV : IsCompl U V), (U.projection V hUV).IsSymmetricProjection ↔ U ⟂ V